TEXT   12

nsl shapes txt

Guest on 23rd June 2022 02:45:16 AM

  1. (comment "CPSA 2.2.11")
  2. (comment "Extracted shapes")
  3.  
  4. (herald "Needham-Schroeder Lowe Public-Key Protocol"
  5.   (comment "This protocol eliminates the man-in-the-middle"
  6.     "attack discovered by Gavin Lowe."))
  7.  
  8. (comment "CPSA 2.2.11")
  9.  
  10. (comment "All input read from nsl.scm")
  11.  
  12. (defprotocol ns basic
  13.   (defrole init
  14.     (vars (my_init_id yr_resp_id name) (n1 n2 text))
  15.     (trace (send (enc n1 my_init_id (pubk yr_resp_id)))
  16.       (recv (enc n1 n2 yr_resp_id (pubk my_init_id)))
  17.       (send (enc n2 (pubk yr_resp_id)))))
  18.   (defrole resp
  19.     (vars (my_resp_id yr_init_id name) (n2 n1 text))
  20.     (trace (recv (enc n1 yr_init_id (pubk my_resp_id)))
  21.       (send (enc n1 n2 my_resp_id (pubk yr_init_id)))
  22.       (recv (enc n2 (pubk my_resp_id)))))
  23.   (comment "Needham-Schroeder"))
  24.  
  25. (defskeleton ns
  26.   (vars (n1 n2 text) (a b name))
  27.   (defstrand init 3 (n1 n1) (n2 n2) (my_init_id a) (yr_resp_id b))
  28.   (non-orig (privk a) (privk b))
  29.   (uniq-orig n1)
  30.   (comment "Initiator point-of-view")
  31.   (traces
  32.     ((send (enc n1 a (pubk b))) (recv (enc n1 n2 b (pubk a)))
  33.       (send (enc n2 (pubk b)))))
  34.   (label 0)
  35.   (unrealized (0 1))
  36.   (origs (n1 (0 0)))
  37.   (comment "1 in cohort - 1 not yet seen"))
  38.  
  39. (defskeleton ns
  40.   (vars (n1 n2 text) (a b name))
  41.   (defstrand init 3 (n1 n1) (n2 n2) (my_init_id a) (yr_resp_id b))
  42.   (defstrand resp 2 (n2 n2) (n1 n1) (my_resp_id b) (yr_init_id a))
  43.   (precedes ((0 0) (1 0)) ((1 1) (0 1)))
  44.   (non-orig (privk a) (privk b))
  45.   (uniq-orig n1)
  46.   (operation nonce-test (contracted (n2-0 n2)) n1 (0 1)
  47.     (enc n1 a (pubk b)) (enc n1 n2 b (pubk a)))
  48.   (traces
  49.     ((send (enc n1 a (pubk b))) (recv (enc n1 n2 b (pubk a)))
  50.       (send (enc n2 (pubk b))))
  51.     ((recv (enc n1 a (pubk b))) (send (enc n1 n2 b (pubk a)))))
  52.   (label 2)
  53.   (parent 0)
  54.   (unrealized)
  55.   (shape)
  56.   (maps ((0) ((a a) (b b) (n1 n1) (n2 n2))))
  57.   (origs (n1 (0 0))))
  58.  
  59. (comment "Nothing left to do")
  60.  
  61. (defprotocol ns basic
  62.   (defrole init
  63.     (vars (my_init_id yr_resp_id name) (n1 n2 text))
  64.     (trace (send (enc n1 my_init_id (pubk yr_resp_id)))
  65.       (recv (enc n1 n2 yr_resp_id (pubk my_init_id)))
  66.       (send (enc n2 (pubk yr_resp_id)))))
  67.   (defrole resp
  68.     (vars (my_resp_id yr_init_id name) (n2 n1 text))
  69.     (trace (recv (enc n1 yr_init_id (pubk my_resp_id)))
  70.       (send (enc n1 n2 my_resp_id (pubk yr_init_id)))
  71.       (recv (enc n2 (pubk my_resp_id)))))
  72.   (comment "Needham-Schroeder"))
  73.  
  74. (defskeleton ns
  75.   (vars (n2 n1 text) (a b name))
  76.   (defstrand resp 3 (n2 n2) (n1 n1) (my_resp_id b) (yr_init_id a))
  77.   (non-orig (privk a))
  78.   (uniq-orig n2)
  79.   (comment "Responder point-of-view")
  80.   (traces
  81.     ((recv (enc n1 a (pubk b))) (send (enc n1 n2 b (pubk a)))
  82.       (recv (enc n2 (pubk b)))))
  83.   (label 3)
  84.   (unrealized (0 2))
  85.   (origs (n2 (0 1)))
  86.   (comment "1 in cohort - 1 not yet seen"))
  87.  
  88. (defskeleton ns
  89.   (vars (n2 n1 text) (a b name))
  90.   (defstrand resp 3 (n2 n2) (n1 n1) (my_resp_id b) (yr_init_id a))
  91.   (defstrand init 3 (n1 n1) (n2 n2) (my_init_id a) (yr_resp_id b))
  92.   (precedes ((0 1) (1 1)) ((1 2) (0 2)))
  93.   (non-orig (privk a))
  94.   (uniq-orig n2)
  95.   (operation nonce-test (added-strand init 3) n2 (0 2)
  96.     (enc n1 n2 b (pubk a)))
  97.   (traces
  98.     ((recv (enc n1 a (pubk b))) (send (enc n1 n2 b (pubk a)))
  99.       (recv (enc n2 (pubk b))))
  100.     ((send (enc n1 a (pubk b))) (recv (enc n1 n2 b (pubk a)))
  101.       (send (enc n2 (pubk b)))))
  102.   (label 4)
  103.   (parent 3)
  104.   (unrealized)
  105.   (shape)
  106.   (maps ((0) ((a a) (b b) (n2 n2) (n1 n1))))
  107.   (origs (n2 (0 1))))
  108.  
  109. (comment "Nothing left to do")
  110.  
  111. (defprotocol ns basic
  112.   (defrole init
  113.     (vars (my_init_id yr_resp_id name) (n1 n2 text))
  114.     (trace (send (enc n1 my_init_id (pubk yr_resp_id)))
  115.       (recv (enc n1 n2 yr_resp_id (pubk my_init_id)))
  116.       (send (enc n2 (pubk yr_resp_id)))))
  117.   (defrole resp
  118.     (vars (my_resp_id yr_init_id name) (n2 n1 text))
  119.     (trace (recv (enc n1 yr_init_id (pubk my_resp_id)))
  120.       (send (enc n1 n2 my_resp_id (pubk yr_init_id)))
  121.       (recv (enc n2 (pubk my_resp_id)))))
  122.   (comment "Needham-Schroeder"))
  123.  
  124. (defskeleton ns
  125.   (vars (n1 n2 text) (a b name))
  126.   (defstrand resp 3 (n2 n2) (n1 n1) (my_resp_id b) (yr_init_id a))
  127.   (deflistener n2)
  128.   (non-orig (privk a) (privk b))
  129.   (uniq-orig n1 n2)
  130.   (comment "Responder point-of-view, secrecy?")
  131.   (traces
  132.     ((recv (enc n1 a (pubk b))) (send (enc n1 n2 b (pubk a)))
  133.       (recv (enc n2 (pubk b)))) ((recv n2) (send n2)))
  134.   (label 5)
  135.   (unrealized (0 2) (1 0))
  136.   (preskeleton)
  137.   (comment "Not a skeleton"))
  138.  
  139. (comment "Nothing left to do")
  140.  
  141. (defprotocol ns basic
  142.   (defrole init
  143.     (vars (my_init_id yr_resp_id name) (n1 n2 text))
  144.     (trace (send (enc n1 my_init_id (pubk yr_resp_id)))
  145.       (recv (enc n1 n2 yr_resp_id (pubk my_init_id)))
  146.       (send (enc n2 (pubk yr_resp_id)))))
  147.   (defrole resp
  148.     (vars (my_resp_id yr_init_id name) (n2 n1 text))
  149.     (trace (recv (enc n1 yr_init_id (pubk my_resp_id)))
  150.       (send (enc n1 n2 my_resp_id (pubk yr_init_id)))
  151.       (recv (enc n2 (pubk my_resp_id)))))
  152.   (comment "Needham-Schroeder"))
  153.  
  154. (defskeleton ns
  155.   (vars (n1 n2 text) (a b a1 b1 name))
  156.   (defstrand resp 3 (n2 n2) (n1 n1) (my_resp_id b) (yr_init_id a))
  157.   (defstrand init 3 (n1 n1) (n2 n2) (my_init_id a1) (yr_resp_id b1))
  158.   (non-orig (privk a) (privk b))
  159.   (uniq-orig n1 n2)
  160.   (comment "Implicit auth, both nonces u.o.")
  161.   (traces
  162.     ((recv (enc n1 a (pubk b))) (send (enc n1 n2 b (pubk a)))
  163.       (recv (enc n2 (pubk b))))
  164.     ((send (enc n1 a1 (pubk b1))) (recv (enc n1 n2 b1 (pubk a1)))
  165.       (send (enc n2 (pubk b1)))))
  166.   (label 8)
  167.   (unrealized (0 0) (0 2) (1 1))
  168.   (preskeleton)
  169.   (comment "Not a skeleton"))
  170.  
  171. (defskeleton ns
  172.   (vars (n1 n2 text) (a b name))
  173.   (defstrand resp 3 (n2 n2) (n1 n1) (my_resp_id b) (yr_init_id a))
  174.   (defstrand init 3 (n1 n1) (n2 n2) (my_init_id a) (yr_resp_id b))
  175.   (precedes ((0 1) (1 1)) ((1 0) (0 0)) ((1 2) (0 2)))
  176.   (non-orig (privk a) (privk b))
  177.   (uniq-orig n1 n2)
  178.   (operation nonce-test (displaced 2 1 init 3) n2 (0 2)
  179.     (enc n1 n2 b (pubk a)))
  180.   (traces
  181.     ((recv (enc n1 a (pubk b))) (send (enc n1 n2 b (pubk a)))
  182.       (recv (enc n2 (pubk b))))
  183.     ((send (enc n1 a (pubk b))) (recv (enc n1 n2 b (pubk a)))
  184.       (send (enc n2 (pubk b)))))
  185.   (label 11)
  186.   (parent 8)
  187.   (unrealized)
  188.   (shape)
  189.   (maps ((0 1) ((a a) (b b) (a1 a) (b1 b) (n1 n1) (n2 n2))))
  190.   (origs (n1 (1 0)) (n2 (0 1))))
  191.  
  192. (comment "Nothing left to do")

Raw Paste


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