TEXT   17

ns txt

Guest on 23rd June 2022 02:42:55 AM

  1. (herald "Needham-Schroeder Public-Key Protocol"
  2.   (comment "This protocol contains a man-in-the-middle"
  3.     "attack discovered by Galvin Lowe."))
  4.  
  5. (comment "CPSA 2.2.11")
  6. (comment "All input read from ns.scm")
  7.  
  8. (defprotocol ns basic
  9.   (defrole init
  10.     (vars (my_init_id yr_resp_id name) (n1 n2 text))
  11.     (trace (send (enc n1 my_init_id (pubk yr_resp_id)))
  12.       (recv (enc n1 n2 (pubk my_init_id)))
  13.       (send (enc n2 (pubk yr_resp_id)))))
  14.   (defrole resp
  15.     (vars (my_resp_id yr_init_id name) (n2 n1 text))
  16.     (trace (recv (enc n1 yr_init_id (pubk my_resp_id)))
  17.       (send (enc n1 n2 (pubk yr_init_id)))
  18.       (recv (enc n2 (pubk my_resp_id)))))
  19.   (comment "Needham-Schroeder"))
  20.  
  21. (defskeleton ns
  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 (privk a) (privk b))
  25.   (uniq-orig n1)
  26.   (comment "Initiator point-of-view")
  27.   (traces
  28.     ((send (enc n1 a (pubk b))) (recv (enc n1 n2 (pubk a)))
  29.       (send (enc n2 (pubk b)))))
  30.   (label 0)
  31.   (unrealized (0 1))
  32.   (origs (n1 (0 0)))
  33.   (comment "1 in cohort - 1 not yet seen"))
  34.  
  35. (defskeleton ns
  36.   (vars (n1 n2 n2-0 text) (a b name))
  37.   (defstrand init 3 (n1 n1) (n2 n2) (my_init_id a) (yr_resp_id b))
  38.   (defstrand resp 2 (n2 n2-0) (n1 n1) (my_resp_id b) (yr_init_id a))
  39.   (precedes ((0 0) (1 0)) ((1 1) (0 1)))
  40.   (non-orig (privk a) (privk b))
  41.   (uniq-orig n1)
  42.   (operation nonce-test (added-strand resp 2) n1 (0 1)
  43.     (enc n1 a (pubk b)))
  44.   (traces
  45.     ((send (enc n1 a (pubk b))) (recv (enc n1 n2 (pubk a)))
  46.       (send (enc n2 (pubk b))))
  47.     ((recv (enc n1 a (pubk b))) (send (enc n1 n2-0 (pubk a)))))
  48.   (label 1)
  49.   (parent 0)
  50.   (unrealized (0 1))
  51.   (comment "1 in cohort - 1 not yet seen"))
  52.  
  53. (defskeleton ns
  54.   (vars (n1 n2 text) (a b name))
  55.   (defstrand init 3 (n1 n1) (n2 n2) (my_init_id a) (yr_resp_id b))
  56.   (defstrand resp 2 (n2 n2) (n1 n1) (my_resp_id b) (yr_init_id a))
  57.   (precedes ((0 0) (1 0)) ((1 1) (0 1)))
  58.   (non-orig (privk a) (privk b))
  59.   (uniq-orig n1)
  60.   (operation nonce-test (contracted (n2-0 n2)) n1 (0 1)
  61.     (enc n1 n2 (pubk a)) (enc n1 a (pubk b)))
  62.   (traces
  63.     ((send (enc n1 a (pubk b))) (recv (enc n1 n2 (pubk a)))
  64.       (send (enc n2 (pubk b))))
  65.     ((recv (enc n1 a (pubk b))) (send (enc n1 n2 (pubk a)))))
  66.   (label 2)
  67.   (parent 1)
  68.   (unrealized)
  69.   (shape)
  70.   (maps ((0) ((a a) (b b) (n1 n1) (n2 n2))))
  71.   (origs (n1 (0 0))))
  72.  
  73. (comment "Nothing left to do")
  74.  
  75. (defprotocol ns basic
  76.   (defrole init
  77.     (vars (my_init_id yr_resp_id name) (n1 n2 text))
  78.     (trace (send (enc n1 my_init_id (pubk yr_resp_id)))
  79.       (recv (enc n1 n2 (pubk my_init_id)))
  80.       (send (enc n2 (pubk yr_resp_id)))))
  81.   (defrole resp
  82.     (vars (my_resp_id yr_init_id name) (n2 n1 text))
  83.     (trace (recv (enc n1 yr_init_id (pubk my_resp_id)))
  84.       (send (enc n1 n2 (pubk yr_init_id)))
  85.       (recv (enc n2 (pubk my_resp_id)))))
  86.   (comment "Needham-Schroeder"))
  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.   (non-orig (privk a))
  92.   (uniq-orig n2)
  93.   (comment "Responder point-of-view")
  94.   (traces
  95.     ((recv (enc n1 a (pubk b))) (send (enc n1 n2 (pubk a)))
  96.       (recv (enc n2 (pubk b)))))
  97.   (label 3)
  98.   (unrealized (0 2))
  99.   (origs (n2 (0 1)))
  100.   (comment "1 in cohort - 1 not yet seen"))
  101.  
  102. (defskeleton ns
  103.   (vars (n2 n1 text) (a b yr_resp_id name))
  104.   (defstrand resp 3 (n2 n2) (n1 n1) (my_resp_id b) (yr_init_id a))
  105.   (defstrand init 3 (n1 n1) (n2 n2) (my_init_id a)
  106.     (yr_resp_id yr_resp_id))
  107.   (precedes ((0 1) (1 1)) ((1 2) (0 2)))
  108.   (non-orig (privk a))
  109.   (uniq-orig n2)
  110.   (operation nonce-test (added-strand init 3) n2 (0 2)
  111.     (enc n1 n2 (pubk a)))
  112.   (traces
  113.     ((recv (enc n1 a (pubk b))) (send (enc n1 n2 (pubk a)))
  114.       (recv (enc n2 (pubk b))))
  115.     ((send (enc n1 a (pubk yr_resp_id))) (recv (enc n1 n2 (pubk a)))
  116.       (send (enc n2 (pubk yr_resp_id)))))
  117.   (label 4)
  118.   (parent 3)
  119.   (unrealized)
  120.   (shape)
  121.   (maps ((0) ((a a) (b b) (n2 n2) (n1 n1))))
  122.   (origs (n2 (0 1))))
  123.  
  124. (comment "Nothing left to do")
  125.  
  126. (defprotocol ns basic
  127.   (defrole init
  128.     (vars (my_init_id yr_resp_id name) (n1 n2 text))
  129.     (trace (send (enc n1 my_init_id (pubk yr_resp_id)))
  130.       (recv (enc n1 n2 (pubk my_init_id)))
  131.       (send (enc n2 (pubk yr_resp_id)))))
  132.   (defrole resp
  133.     (vars (my_resp_id yr_init_id name) (n2 n1 text))
  134.     (trace (recv (enc n1 yr_init_id (pubk my_resp_id)))
  135.       (send (enc n1 n2 (pubk yr_init_id)))
  136.       (recv (enc n2 (pubk my_resp_id)))))
  137.   (comment "Needham-Schroeder"))
  138.  
  139. (defskeleton ns
  140.   (vars (n1 n2 text) (a b name))
  141.   (defstrand resp 3 (n2 n2) (n1 n1) (my_resp_id b) (yr_init_id a))
  142.   (deflistener n2)
  143.   (non-orig (privk a) (privk b))
  144.   (uniq-orig n1 n2)
  145.   (comment "Responder point-of-view, secrecy?")
  146.   (traces
  147.     ((recv (enc n1 a (pubk b))) (send (enc n1 n2 (pubk a)))
  148.       (recv (enc n2 (pubk b)))) ((recv n2) (send n2)))
  149.   (label 5)
  150.   (unrealized (0 2) (1 0))
  151.   (preskeleton)
  152.   (comment "Not a skeleton"))
  153.  
  154. (defskeleton ns
  155.   (vars (n1 n2 text) (a b name))
  156.   (defstrand resp 3 (n2 n2) (n1 n1) (my_resp_id b) (yr_init_id a))
  157.   (deflistener n2)
  158.   (precedes ((0 1) (1 0)))
  159.   (non-orig (privk a) (privk b))
  160.   (uniq-orig n1 n2)
  161.   (traces
  162.     ((recv (enc n1 a (pubk b))) (send (enc n1 n2 (pubk a)))
  163.       (recv (enc n2 (pubk b)))) ((recv n2) (send n2)))
  164.   (label 6)
  165.   (parent 5)
  166.   (unrealized (0 2) (1 0))
  167.   (origs (n2 (0 1)))
  168.   (comment "1 in cohort - 1 not yet seen"))
  169.  
  170. (defskeleton ns
  171.   (vars (n1 n2 text) (a b yr_resp_id name))
  172.   (defstrand resp 3 (n2 n2) (n1 n1) (my_resp_id b) (yr_init_id a))
  173.   (deflistener n2)
  174.   (defstrand init 3 (n1 n1) (n2 n2) (my_init_id a)
  175.     (yr_resp_id yr_resp_id))
  176.   (precedes ((0 1) (2 1)) ((2 0) (0 0)) ((2 2) (1 0)))
  177.   (non-orig (privk a) (privk b))
  178.   (uniq-orig n1 n2)
  179.   (operation nonce-test (added-strand init 3) n2 (1 0)
  180.     (enc n1 n2 (pubk a)))
  181.   (traces
  182.     ((recv (enc n1 a (pubk b))) (send (enc n1 n2 (pubk a)))
  183.       (recv (enc n2 (pubk b)))) ((recv n2) (send n2))
  184.     ((send (enc n1 a (pubk yr_resp_id))) (recv (enc n1 n2 (pubk a)))
  185.       (send (enc n2 (pubk yr_resp_id)))))
  186.   (label 7)
  187.   (parent 6)
  188.   (unrealized (0 2))
  189.   (comment "1 in cohort - 1 not yet seen"))
  190.  
  191. (defskeleton ns
  192.   (vars (n1 n2 text) (a b yr_resp_id name))
  193.   (defstrand resp 3 (n2 n2) (n1 n1) (my_resp_id b) (yr_init_id a))
  194.   (deflistener n2)
  195.   (defstrand init 3 (n1 n1) (n2 n2) (my_init_id a)
  196.     (yr_resp_id yr_resp_id))
  197.   (precedes ((0 1) (2 1)) ((2 0) (0 0)) ((2 2) (0 2)) ((2 2) (1 0)))
  198.   (non-orig (privk a) (privk b))
  199.   (uniq-orig n1 n2)
  200.   (operation nonce-test (displaced 3 2 init 3) n2 (0 2)
  201.     (enc n1 n2 (pubk a)))
  202.   (traces
  203.     ((recv (enc n1 a (pubk b))) (send (enc n1 n2 (pubk a)))
  204.       (recv (enc n2 (pubk b)))) ((recv n2) (send n2))
  205.     ((send (enc n1 a (pubk yr_resp_id))) (recv (enc n1 n2 (pubk a)))
  206.       (send (enc n2 (pubk yr_resp_id)))))
  207.   (label 8)
  208.   (parent 7)
  209.   (unrealized)
  210.   (shape)
  211.   (maps ((0 1) ((a a) (b b) (n1 n1) (n2 n2))))
  212.   (origs (n1 (2 0)) (n2 (0 1))))
  213.  
  214. (comment "Nothing left to do")
  215.  
  216. (defprotocol ns basic
  217.   (defrole init
  218.     (vars (my_init_id yr_resp_id name) (n1 n2 text))
  219.     (trace (send (enc n1 my_init_id (pubk yr_resp_id)))
  220.       (recv (enc n1 n2 (pubk my_init_id)))
  221.       (send (enc n2 (pubk yr_resp_id)))))
  222.   (defrole resp
  223.     (vars (my_resp_id yr_init_id name) (n2 n1 text))
  224.     (trace (recv (enc n1 yr_init_id (pubk my_resp_id)))
  225.       (send (enc n1 n2 (pubk yr_init_id)))
  226.       (recv (enc n2 (pubk my_resp_id)))))
  227.   (comment "Needham-Schroeder"))
  228.  
  229. (defskeleton ns
  230.   (vars (n1 n2 text) (a b a1 b1 name))
  231.   (defstrand resp 3 (n2 n2) (n1 n1) (my_resp_id b) (yr_init_id a))
  232.   (defstrand init 3 (n1 n1) (n2 n2) (my_init_id a1) (yr_resp_id b1))
  233.   (non-orig (privk a) (privk b))
  234.   (uniq-orig n1 n2)
  235.   (comment "Implicit auth, both nonces u.o.")
  236.   (traces
  237.     ((recv (enc n1 a (pubk b))) (send (enc n1 n2 (pubk a)))
  238.       (recv (enc n2 (pubk b))))
  239.     ((send (enc n1 a1 (pubk b1))) (recv (enc n1 n2 (pubk a1)))
  240.       (send (enc n2 (pubk b1)))))
  241.   (label 9)
  242.   (unrealized (0 0) (0 2) (1 1))
  243.   (preskeleton)
  244.   (comment "Not a skeleton"))
  245.  
  246. (defskeleton ns
  247.   (vars (n1 n2 text) (a b a1 b1 name))
  248.   (defstrand resp 3 (n2 n2) (n1 n1) (my_resp_id b) (yr_init_id a))
  249.   (defstrand init 3 (n1 n1) (n2 n2) (my_init_id a1) (yr_resp_id b1))
  250.   (precedes ((0 1) (1 1)) ((1 0) (0 0)))
  251.   (non-orig (privk a) (privk b))
  252.   (uniq-orig n1 n2)
  253.   (traces
  254.     ((recv (enc n1 a (pubk b))) (send (enc n1 n2 (pubk a)))
  255.       (recv (enc n2 (pubk b))))
  256.     ((send (enc n1 a1 (pubk b1))) (recv (enc n1 n2 (pubk a1)))
  257.       (send (enc n2 (pubk b1)))))
  258.   (label 10)
  259.   (parent 9)
  260.   (unrealized (0 2) (1 1))
  261.   (origs (n1 (1 0)) (n2 (0 1)))
  262.   (comment "1 in cohort - 1 not yet seen"))
  263.  
  264. (defskeleton ns
  265.   (vars (n1 n2 text) (a b b1 name))
  266.   (defstrand resp 3 (n2 n2) (n1 n1) (my_resp_id b) (yr_init_id a))
  267.   (defstrand init 3 (n1 n1) (n2 n2) (my_init_id a) (yr_resp_id b1))
  268.   (precedes ((0 1) (1 1)) ((1 0) (0 0)))
  269.   (non-orig (privk a) (privk b))
  270.   (uniq-orig n1 n2)
  271.   (operation nonce-test (contracted (a1 a)) n2 (1 1)
  272.     (enc n1 n2 (pubk a)))
  273.   (traces
  274.     ((recv (enc n1 a (pubk b))) (send (enc n1 n2 (pubk a)))
  275.       (recv (enc n2 (pubk b))))
  276.     ((send (enc n1 a (pubk b1))) (recv (enc n1 n2 (pubk a)))
  277.       (send (enc n2 (pubk b1)))))
  278.   (label 11)
  279.   (parent 10)
  280.   (unrealized (0 2))
  281.   (origs (n1 (1 0)) (n2 (0 1)))
  282.   (comment "1 in cohort - 1 not yet seen"))
  283.  
  284. (defskeleton ns
  285.   (vars (n1 n2 text) (a b b1 name))
  286.   (defstrand resp 3 (n2 n2) (n1 n1) (my_resp_id b) (yr_init_id a))
  287.   (defstrand init 3 (n1 n1) (n2 n2) (my_init_id a) (yr_resp_id b1))
  288.   (precedes ((0 1) (1 1)) ((1 0) (0 0)) ((1 2) (0 2)))
  289.   (non-orig (privk a) (privk b))
  290.   (uniq-orig n1 n2)
  291.   (operation nonce-test (displaced 2 1 init 3) n2 (0 2)
  292.     (enc n1 n2 (pubk a)))
  293.   (traces
  294.     ((recv (enc n1 a (pubk b))) (send (enc n1 n2 (pubk a)))
  295.       (recv (enc n2 (pubk b))))
  296.     ((send (enc n1 a (pubk b1))) (recv (enc n1 n2 (pubk a)))
  297.       (send (enc n2 (pubk b1)))))
  298.   (label 12)
  299.   (parent 11)
  300.   (unrealized)
  301.   (shape)
  302.   (maps ((0 1) ((a a) (b b) (a1 a) (b1 b1) (n1 n1) (n2 n2))))
  303.   (origs (n1 (1 0)) (n2 (0 1))))
  304.  
  305. (comment "Nothing left to do")

Raw Paste


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