TEXT   16

ps shapes txt

Guest on 23rd June 2022 02:48:50 AM

  1. (comment "CPSA 2.2.11")
  2. (comment "Extracted shapes")
  3.  
  4. (herald "Perrig-Song Example protocol"
  5.   (comment "auth failure known to them."))
  6.  
  7. (comment "CPSA 2.2.11")
  8.  
  9. (comment "All input read from ps.scm")
  10.  
  11. (defprotocol ps basic
  12.   (defrole init
  13.     (vars (my_init_id yr_resp_id name) (n1 n2 text))
  14.     (trace (send (cat my_init_id n1))
  15.       (recv (enc n1 n2 (ltk my_init_id yr_resp_id))) (send n2)))
  16.   (defrole resp
  17.     (vars (my_resp_id yr_init_id name) (n2 n1 text))
  18.     (trace (recv (cat yr_init_id n1))
  19.       (send (enc n1 n2 (ltk yr_init_id my_resp_id))) (recv n2))))
  20.  
  21. (defskeleton ps
  22.   (vars (n1 n2 text) (a b name))
  23.   (defstrand init 3 (n1 n1) (n2 n2) (my_init_id a) (yr_resp_id b))
  24.   (non-orig (ltk a b))
  25.   (uniq-orig n1)
  26.   (comment "Initiator point-of-view")
  27.   (traces ((send (cat a n1)) (recv (enc n1 n2 (ltk a b))) (send n2)))
  28.   (label 0)
  29.   (unrealized (0 1))
  30.   (origs (n1 (0 0)))
  31.   (comment "1 in cohort - 1 not yet seen"))
  32.  
  33. (defskeleton ps
  34.   (vars (n1 n2 text) (a b name))
  35.   (defstrand init 3 (n1 n1) (n2 n2) (my_init_id a) (yr_resp_id b))
  36.   (defstrand resp 2 (n2 n2) (n1 n1) (my_resp_id b) (yr_init_id a))
  37.   (precedes ((0 0) (1 0)) ((1 1) (0 1)))
  38.   (non-orig (ltk a b))
  39.   (uniq-orig n1)
  40.   (operation encryption-test (added-strand resp 2) (enc n1 n2 (ltk a b))
  41.     (0 1))
  42.   (traces ((send (cat a n1)) (recv (enc n1 n2 (ltk a b))) (send n2))
  43.     ((recv (cat a n1)) (send (enc n1 n2 (ltk a b)))))
  44.   (label 1)
  45.   (parent 0)
  46.   (unrealized)
  47.   (shape)
  48.   (maps ((0) ((a a) (b b) (n1 n1) (n2 n2))))
  49.   (origs (n1 (0 0))))
  50.  
  51. (comment "Nothing left to do")

Raw Paste


Login or Register to edit or fork this paste. It's free.