TEXT   60
ps sym shapes
Guest on 23rd June 2022 02:50:23 AM


  1. (comment "CPSA 2.2.11")
  2. (comment "Extracted shapes")
  3.  
  4. (herald "Perrig-Song Example protocol, symmetrized."
  5.   (comment "auth failure known to them."
  6.     "Symmetrized to symulate (ltk a b) = (ltk b a)"))
  7.  
  8. (comment "CPSA 2.2.11")
  9.  
  10. (comment "All input read from ps_sym.scm")
  11.  
  12. (defprotocol ps basic
  13.   (defrole init_l
  14.     (vars (my_init_id yr_resp_id name) (n1 n2 text))
  15.     (trace (send (cat my_init_id n1))
  16.       (recv (enc n1 n2 (ltk my_init_id yr_resp_id))) (send n2)))
  17.   (defrole init_r
  18.     (vars (my_init_id yr_resp_id name) (n1 n2 text))
  19.     (trace (send (cat my_init_id n1))
  20.       (recv (enc n1 n2 (ltk yr_resp_id my_init_id))) (send n2)))
  21.   (defrole resp_l
  22.     (vars (my_resp_id yr_init_id name) (n2 n1 text))
  23.     (trace (recv (cat yr_init_id n1))
  24.       (send (enc n1 n2 (ltk yr_init_id my_resp_id))) (recv n2)))
  25.   (defrole resp_r
  26.     (vars (my_resp_id yr_init_id name) (n2 n1 text))
  27.     (trace (recv (cat yr_init_id n1))
  28.       (send (enc n1 n2 (ltk my_resp_id yr_init_id))) (recv n2))))
  29.  
  30. (defskeleton ps
  31.   (vars (n1 n2 text) (a b name))
  32.   (defstrand init_l 3 (n1 n1) (n2 n2) (my_init_id a) (yr_resp_id b))
  33.   (non-orig (ltk a b) (ltk b a))
  34.   (uniq-orig n1)
  35.   (comment "Initiator point-of-view")
  36.   (traces ((send (cat a n1)) (recv (enc n1 n2 (ltk a b))) (send n2)))
  37.   (label 0)
  38.   (unrealized (0 1))
  39.   (origs (n1 (0 0)))
  40.   (comment "2 in cohort - 2 not yet seen"))
  41.  
  42. (defskeleton ps
  43.   (vars (n1 n2 text) (a b name))
  44.   (defstrand init_l 3 (n1 n1) (n2 n2) (my_init_id a) (yr_resp_id b))
  45.   (defstrand resp_l 2 (n2 n2) (n1 n1) (my_resp_id b) (yr_init_id a))
  46.   (precedes ((0 0) (1 0)) ((1 1) (0 1)))
  47.   (non-orig (ltk a b) (ltk b a))
  48.   (uniq-orig n1)
  49.   (operation encryption-test (added-strand resp_l 2)
  50.     (enc n1 n2 (ltk a b)) (0 1))
  51.   (traces ((send (cat a n1)) (recv (enc n1 n2 (ltk a b))) (send n2))
  52.     ((recv (cat a n1)) (send (enc n1 n2 (ltk a b)))))
  53.   (label 1)
  54.   (parent 0)
  55.   (unrealized)
  56.   (shape)
  57.   (maps ((0) ((a a) (b b) (n1 n1) (n2 n2))))
  58.   (origs (n1 (0 0))))
  59.  
  60. (defskeleton ps
  61.   (vars (n1 n2 text) (a b name))
  62.   (defstrand init_l 3 (n1 n1) (n2 n2) (my_init_id a) (yr_resp_id b))
  63.   (defstrand resp_r 2 (n2 n2) (n1 n1) (my_resp_id a) (yr_init_id b))
  64.   (precedes ((0 0) (1 0)) ((1 1) (0 1)))
  65.   (non-orig (ltk a b) (ltk b a))
  66.   (uniq-orig n1)
  67.   (operation encryption-test (added-strand resp_r 2)
  68.     (enc n1 n2 (ltk a b)) (0 1))
  69.   (traces ((send (cat a n1)) (recv (enc n1 n2 (ltk a b))) (send n2))
  70.     ((recv (cat b n1)) (send (enc n1 n2 (ltk a b)))))
  71.   (label 2)
  72.   (parent 0)
  73.   (unrealized)
  74.   (shape)
  75.   (maps ((0) ((a a) (b b) (n1 n1) (n2 n2))))
  76.   (origs (n1 (0 0))))
  77.  
  78. (comment "Nothing left to do")
  79.  
  80. (defprotocol ps basic
  81.   (defrole init_l
  82.     (vars (my_init_id yr_resp_id name) (n1 n2 text))
  83.     (trace (send (cat my_init_id n1))
  84.       (recv (enc n1 n2 (ltk my_init_id yr_resp_id))) (send n2)))
  85.   (defrole init_r
  86.     (vars (my_init_id yr_resp_id name) (n1 n2 text))
  87.     (trace (send (cat my_init_id n1))
  88.       (recv (enc n1 n2 (ltk yr_resp_id my_init_id))) (send n2)))
  89.   (defrole resp_l
  90.     (vars (my_resp_id yr_init_id name) (n2 n1 text))
  91.     (trace (recv (cat yr_init_id n1))
  92.       (send (enc n1 n2 (ltk yr_init_id my_resp_id))) (recv n2)))
  93.   (defrole resp_r
  94.     (vars (my_resp_id yr_init_id name) (n2 n1 text))
  95.     (trace (recv (cat yr_init_id n1))
  96.       (send (enc n1 n2 (ltk my_resp_id yr_init_id))) (recv n2))))
  97.  
  98. (defskeleton ps
  99.   (vars (n1 n2 text) (a b name))
  100.   (defstrand init_r 3 (n1 n1) (n2 n2) (my_init_id a) (yr_resp_id b))
  101.   (non-orig (ltk a b) (ltk b a))
  102.   (uniq-orig n1)
  103.   (comment "Initiator point-of-view, symmetric")
  104.   (traces ((send (cat a n1)) (recv (enc n1 n2 (ltk b a))) (send n2)))
  105.   (label 3)
  106.   (unrealized (0 1))
  107.   (origs (n1 (0 0)))
  108.   (comment "2 in cohort - 2 not yet seen"))
  109.  
  110. (defskeleton ps
  111.   (vars (n1 n2 text) (a b name))
  112.   (defstrand init_r 3 (n1 n1) (n2 n2) (my_init_id a) (yr_resp_id b))
  113.   (defstrand resp_l 2 (n2 n2) (n1 n1) (my_resp_id a) (yr_init_id b))
  114.   (precedes ((0 0) (1 0)) ((1 1) (0 1)))
  115.   (non-orig (ltk a b) (ltk b a))
  116.   (uniq-orig n1)
  117.   (operation encryption-test (added-strand resp_l 2)
  118.     (enc n1 n2 (ltk b a)) (0 1))
  119.   (traces ((send (cat a n1)) (recv (enc n1 n2 (ltk b a))) (send n2))
  120.     ((recv (cat b n1)) (send (enc n1 n2 (ltk b a)))))
  121.   (label 4)
  122.   (parent 3)
  123.   (unrealized)
  124.   (shape)
  125.   (maps ((0) ((a a) (b b) (n1 n1) (n2 n2))))
  126.   (origs (n1 (0 0))))
  127.  
  128. (defskeleton ps
  129.   (vars (n1 n2 text) (a b name))
  130.   (defstrand init_r 3 (n1 n1) (n2 n2) (my_init_id a) (yr_resp_id b))
  131.   (defstrand resp_r 2 (n2 n2) (n1 n1) (my_resp_id b) (yr_init_id a))
  132.   (precedes ((0 0) (1 0)) ((1 1) (0 1)))
  133.   (non-orig (ltk a b) (ltk b a))
  134.   (uniq-orig n1)
  135.   (operation encryption-test (added-strand resp_r 2)
  136.     (enc n1 n2 (ltk b a)) (0 1))
  137.   (traces ((send (cat a n1)) (recv (enc n1 n2 (ltk b a))) (send n2))
  138.     ((recv (cat a n1)) (send (enc n1 n2 (ltk b a)))))
  139.   (label 5)
  140.   (parent 3)
  141.   (unrealized)
  142.   (shape)
  143.   (maps ((0) ((a a) (b b) (n1 n1) (n2 n2))))
  144.   (origs (n1 (0 0))))
  145.  
  146. (comment "Nothing left to do")
Raw Paste

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