TEXT   13

ps sym

Guest on 23rd June 2022 02:49:43 AM

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

Raw Paste


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