TEXT   15

ns shapes txt

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

  1. (comment "CPSA 2.2.11")
  2. (comment "Extracted shapes")
  3.  
  4. (herald "Needham-Schroeder Public-Key Protocol"
  5.   (comment "This protocol contains a man-in-the-middle"
  6.     "attack discovered by Galvin Lowe."))
  7.  
  8. (comment "CPSA 2.2.11")
  9.  
  10. (comment "All input read from ns.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 (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 (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 (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 n2 (pubk a)) (enc n1 a (pubk b)))
  48.   (traces
  49.     ((send (enc n1 a (pubk b))) (recv (enc n1 n2 (pubk a)))
  50.       (send (enc n2 (pubk b))))
  51.     ((recv (enc n1 a (pubk b))) (send (enc n1 n2 (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 (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 (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 (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 yr_resp_id 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)
  92.     (yr_resp_id yr_resp_id))
  93.   (precedes ((0 1) (1 1)) ((1 2) (0 2)))
  94.   (non-orig (privk a))
  95.   (uniq-orig n2)
  96.   (operation nonce-test (added-strand init 3) n2 (0 2)
  97.     (enc n1 n2 (pubk a)))
  98.   (traces
  99.     ((recv (enc n1 a (pubk b))) (send (enc n1 n2 (pubk a)))
  100.       (recv (enc n2 (pubk b))))
  101.     ((send (enc n1 a (pubk yr_resp_id))) (recv (enc n1 n2 (pubk a)))
  102.       (send (enc n2 (pubk yr_resp_id)))))
  103.   (label 4)
  104.   (parent 3)
  105.   (unrealized)
  106.   (shape)
  107.   (maps ((0) ((a a) (b b) (n2 n2) (n1 n1))))
  108.   (origs (n2 (0 1))))
  109.  
  110. (comment "Nothing left to do")
  111.  
  112. (defprotocol ns basic
  113.   (defrole init
  114.     (vars (my_init_id yr_resp_id name) (n1 n2 text))
  115.     (trace (send (enc n1 my_init_id (pubk yr_resp_id)))
  116.       (recv (enc n1 n2 (pubk my_init_id)))
  117.       (send (enc n2 (pubk yr_resp_id)))))
  118.   (defrole resp
  119.     (vars (my_resp_id yr_init_id name) (n2 n1 text))
  120.     (trace (recv (enc n1 yr_init_id (pubk my_resp_id)))
  121.       (send (enc n1 n2 (pubk yr_init_id)))
  122.       (recv (enc n2 (pubk my_resp_id)))))
  123.   (comment "Needham-Schroeder"))
  124.  
  125. (defskeleton ns
  126.   (vars (n1 n2 text) (a b name))
  127.   (defstrand resp 3 (n2 n2) (n1 n1) (my_resp_id b) (yr_init_id a))
  128.   (deflistener n2)
  129.   (non-orig (privk a) (privk b))
  130.   (uniq-orig n1 n2)
  131.   (comment "Responder point-of-view, secrecy?")
  132.   (traces
  133.     ((recv (enc n1 a (pubk b))) (send (enc n1 n2 (pubk a)))
  134.       (recv (enc n2 (pubk b)))) ((recv n2) (send n2)))
  135.   (label 5)
  136.   (unrealized (0 2) (1 0))
  137.   (preskeleton)
  138.   (comment "Not a skeleton"))
  139.  
  140. (defskeleton ns
  141.   (vars (n1 n2 text) (a b yr_resp_id name))
  142.   (defstrand resp 3 (n2 n2) (n1 n1) (my_resp_id b) (yr_init_id a))
  143.   (deflistener n2)
  144.   (defstrand init 3 (n1 n1) (n2 n2) (my_init_id a)
  145.     (yr_resp_id yr_resp_id))
  146.   (precedes ((0 1) (2 1)) ((2 0) (0 0)) ((2 2) (0 2)) ((2 2) (1 0)))
  147.   (non-orig (privk a) (privk b))
  148.   (uniq-orig n1 n2)
  149.   (operation nonce-test (displaced 3 2 init 3) n2 (0 2)
  150.     (enc n1 n2 (pubk a)))
  151.   (traces
  152.     ((recv (enc n1 a (pubk b))) (send (enc n1 n2 (pubk a)))
  153.       (recv (enc n2 (pubk b)))) ((recv n2) (send n2))
  154.     ((send (enc n1 a (pubk yr_resp_id))) (recv (enc n1 n2 (pubk a)))
  155.       (send (enc n2 (pubk yr_resp_id)))))
  156.   (label 8)
  157.   (parent 5)
  158.   (unrealized)
  159.   (shape)
  160.   (maps ((0 1) ((a a) (b b) (n1 n1) (n2 n2))))
  161.   (origs (n1 (2 0)) (n2 (0 1))))
  162.  
  163. (comment "Nothing left to do")
  164.  
  165. (defprotocol ns basic
  166.   (defrole init
  167.     (vars (my_init_id yr_resp_id name) (n1 n2 text))
  168.     (trace (send (enc n1 my_init_id (pubk yr_resp_id)))
  169.       (recv (enc n1 n2 (pubk my_init_id)))
  170.       (send (enc n2 (pubk yr_resp_id)))))
  171.   (defrole resp
  172.     (vars (my_resp_id yr_init_id name) (n2 n1 text))
  173.     (trace (recv (enc n1 yr_init_id (pubk my_resp_id)))
  174.       (send (enc n1 n2 (pubk yr_init_id)))
  175.       (recv (enc n2 (pubk my_resp_id)))))
  176.   (comment "Needham-Schroeder"))
  177.  
  178. (defskeleton ns
  179.   (vars (n1 n2 text) (a b a1 b1 name))
  180.   (defstrand resp 3 (n2 n2) (n1 n1) (my_resp_id b) (yr_init_id a))
  181.   (defstrand init 3 (n1 n1) (n2 n2) (my_init_id a1) (yr_resp_id b1))
  182.   (non-orig (privk a) (privk b))
  183.   (uniq-orig n1 n2)
  184.   (comment "Implicit auth, both nonces u.o.")
  185.   (traces
  186.     ((recv (enc n1 a (pubk b))) (send (enc n1 n2 (pubk a)))
  187.       (recv (enc n2 (pubk b))))
  188.     ((send (enc n1 a1 (pubk b1))) (recv (enc n1 n2 (pubk a1)))
  189.       (send (enc n2 (pubk b1)))))
  190.   (label 9)
  191.   (unrealized (0 0) (0 2) (1 1))
  192.   (preskeleton)
  193.   (comment "Not a skeleton"))
  194.  
  195. (defskeleton ns
  196.   (vars (n1 n2 text) (a b b1 name))
  197.   (defstrand resp 3 (n2 n2) (n1 n1) (my_resp_id b) (yr_init_id a))
  198.   (defstrand init 3 (n1 n1) (n2 n2) (my_init_id a) (yr_resp_id b1))
  199.   (precedes ((0 1) (1 1)) ((1 0) (0 0)) ((1 2) (0 2)))
  200.   (non-orig (privk a) (privk b))
  201.   (uniq-orig n1 n2)
  202.   (operation nonce-test (displaced 2 1 init 3) n2 (0 2)
  203.     (enc n1 n2 (pubk a)))
  204.   (traces
  205.     ((recv (enc n1 a (pubk b))) (send (enc n1 n2 (pubk a)))
  206.       (recv (enc n2 (pubk b))))
  207.     ((send (enc n1 a (pubk b1))) (recv (enc n1 n2 (pubk a)))
  208.       (send (enc n2 (pubk b1)))))
  209.   (label 12)
  210.   (parent 9)
  211.   (unrealized)
  212.   (shape)
  213.   (maps ((0 1) ((a a) (b b) (a1 a) (b1 b1) (n1 n1) (n2 n2))))
  214.   (origs (n1 (1 0)) (n2 (0 1))))
  215.  
  216. (comment "Nothing left to do")

Raw Paste


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