TEXT   24

tagged an or shapes txt

Guest on 23rd June 2022 02:52:11 AM

  1. (comment "CPSA 2.2.11")
  2. (comment "Extracted shapes")
  3.  
  4. (herald "Otway-Rees Protocol"
  5.   (comment "Standard version using variables of sort mesg"))
  6.  
  7. (comment "CPSA 2.2.11")
  8.  
  9. (comment "All input read from tagged_an_or.scm")
  10.  
  11. (defprotocol an_or basic
  12.   (defrole init
  13.     (vars (my_init_id yr_resp_id s name) (na text) (k skey))
  14.     (trace (send (cat my_init_id yr_resp_id na))
  15.       (recv
  16.         (enc "to_init" na my_init_id yr_resp_id k (ltk my_init_id s)))))
  17.   (defrole resp
  18.     (vars (yr_init_id my_resp_id s name) (na nb text) (k skey) (x mesg))
  19.     (trace (recv (cat yr_init_id my_resp_id na))
  20.       (send (cat yr_init_id my_resp_id na nb))
  21.       (recv
  22.         (cat x
  23.           (enc "to_resp" nb yr_init_id my_resp_id k
  24.             (ltk my_resp_id s)))) (send x)))
  25.   (defrole serv
  26.     (vars (a b s name) (na nb text) (k skey))
  27.     (trace (recv (cat a b na nb))
  28.       (send
  29.         (cat (enc "to_init" na a b k (ltk a s))
  30.           (enc "to_resp" nb a b k (ltk b s)))))
  31.     (uniq-orig k)))
  32.  
  33. (defskeleton an_or
  34.   (vars (x mesg) (nb na text) (s a b name) (k skey))
  35.   (defstrand resp 4 (x x) (na na) (nb nb) (yr_init_id a) (my_resp_id b)
  36.     (s s) (k k))
  37.   (non-orig (ltk a s) (ltk b s))
  38.   (uniq-orig nb)
  39.   (traces
  40.     ((recv (cat a b na)) (send (cat a b na nb))
  41.       (recv (cat x (enc "to_resp" nb a b k (ltk b s)))) (send x)))
  42.   (label 0)
  43.   (unrealized (0 2))
  44.   (origs (nb (0 1)))
  45.   (comment "1 in cohort - 1 not yet seen"))
  46.  
  47. (defskeleton an_or
  48.   (vars (x mesg) (nb na na-0 text) (s a b name) (k skey))
  49.   (defstrand resp 4 (x x) (na na) (nb nb) (yr_init_id a) (my_resp_id b)
  50.     (s s) (k k))
  51.   (defstrand serv 2 (na na-0) (nb nb) (a a) (b b) (s s) (k k))
  52.   (precedes ((0 1) (1 0)) ((1 1) (0 2)))
  53.   (non-orig (ltk a s) (ltk b s))
  54.   (uniq-orig nb k)
  55.   (operation encryption-test (added-strand serv 2)
  56.     (enc "to_resp" nb a b k (ltk b s)) (0 2))
  57.   (traces
  58.     ((recv (cat a b na)) (send (cat a b na nb))
  59.       (recv (cat x (enc "to_resp" nb a b k (ltk b s)))) (send x))
  60.     ((recv (cat a b na-0 nb))
  61.       (send
  62.         (cat (enc "to_init" na-0 a b k (ltk a s))
  63.           (enc "to_resp" nb a b k (ltk b s))))))
  64.   (label 1)
  65.   (parent 0)
  66.   (unrealized)
  67.   (shape)
  68.   (maps ((0) ((nb nb) (s s) (a a) (b b) (na na) (k k) (x x))))
  69.   (origs (k (1 1)) (nb (0 1))))
  70.  
  71. (comment "Nothing left to do")
  72.  
  73. (defprotocol an_or basic
  74.   (defrole init
  75.     (vars (my_init_id yr_resp_id s name) (na text) (k skey))
  76.     (trace (send (cat my_init_id yr_resp_id na))
  77.       (recv
  78.         (enc "to_init" na my_init_id yr_resp_id k (ltk my_init_id s)))))
  79.   (defrole resp
  80.     (vars (yr_init_id my_resp_id s name) (na nb text) (k skey) (x mesg))
  81.     (trace (recv (cat yr_init_id my_resp_id na))
  82.       (send (cat yr_init_id my_resp_id na nb))
  83.       (recv
  84.         (cat x
  85.           (enc "to_resp" nb yr_init_id my_resp_id k
  86.             (ltk my_resp_id s)))) (send x)))
  87.   (defrole serv
  88.     (vars (a b s name) (na nb text) (k skey))
  89.     (trace (recv (cat a b na nb))
  90.       (send
  91.         (cat (enc "to_init" na a b k (ltk a s))
  92.           (enc "to_resp" nb a b k (ltk b s)))))
  93.     (uniq-orig k)))
  94.  
  95. (defskeleton an_or
  96.   (vars (na text) (s a b name) (k skey))
  97.   (defstrand init 2 (na na) (my_init_id a) (yr_resp_id b) (s s) (k k))
  98.   (non-orig (ltk a s) (ltk b s))
  99.   (uniq-orig na)
  100.   (traces
  101.     ((send (cat a b na)) (recv (enc "to_init" na a b k (ltk a s)))))
  102.   (label 2)
  103.   (unrealized (0 1))
  104.   (origs (na (0 0)))
  105.   (comment "1 in cohort - 1 not yet seen"))
  106.  
  107. (defskeleton an_or
  108.   (vars (na nb text) (s a b name) (k skey))
  109.   (defstrand init 2 (na na) (my_init_id a) (yr_resp_id b) (s s) (k k))
  110.   (defstrand serv 2 (na na) (nb nb) (a a) (b b) (s s) (k k))
  111.   (precedes ((0 0) (1 0)) ((1 1) (0 1)))
  112.   (non-orig (ltk a s) (ltk b s))
  113.   (uniq-orig na k)
  114.   (operation encryption-test (added-strand serv 2)
  115.     (enc "to_init" na a b k (ltk a s)) (0 1))
  116.   (traces
  117.     ((send (cat a b na)) (recv (enc "to_init" na a b k (ltk a s))))
  118.     ((recv (cat a b na nb))
  119.       (send
  120.         (cat (enc "to_init" na a b k (ltk a s))
  121.           (enc "to_resp" nb a b k (ltk b s))))))
  122.   (label 3)
  123.   (parent 2)
  124.   (unrealized)
  125.   (shape)
  126.   (maps ((0) ((na na) (s s) (a a) (b b) (k k))))
  127.   (origs (k (1 1)) (na (0 0))))
  128.  
  129. (comment "Nothing left to do")
  130.  
  131. (defprotocol an_or basic
  132.   (defrole init
  133.     (vars (my_init_id yr_resp_id s name) (na text) (k skey))
  134.     (trace (send (cat my_init_id yr_resp_id na))
  135.       (recv
  136.         (enc "to_init" na my_init_id yr_resp_id k (ltk my_init_id s)))))
  137.   (defrole resp
  138.     (vars (yr_init_id my_resp_id s name) (na nb text) (k skey) (x mesg))
  139.     (trace (recv (cat yr_init_id my_resp_id na))
  140.       (send (cat yr_init_id my_resp_id na nb))
  141.       (recv
  142.         (cat x
  143.           (enc "to_resp" nb yr_init_id my_resp_id k
  144.             (ltk my_resp_id s)))) (send x)))
  145.   (defrole serv
  146.     (vars (a b s name) (na nb text) (k skey))
  147.     (trace (recv (cat a b na nb))
  148.       (send
  149.         (cat (enc "to_init" na a b k (ltk a s))
  150.           (enc "to_resp" nb a b k (ltk b s)))))
  151.     (uniq-orig k)))
  152.  
  153. (defskeleton an_or
  154.   (vars (x mesg) (nb na text) (s a b name) (k skey))
  155.   (defstrand resp 4 (x x) (na na) (nb nb) (yr_init_id a) (my_resp_id b)
  156.     (s s) (k k))
  157.   (deflistener k)
  158.   (non-orig (ltk a s) (ltk b s))
  159.   (uniq-orig nb)
  160.   (traces
  161.     ((recv (cat a b na)) (send (cat a b na nb))
  162.       (recv (cat x (enc "to_resp" nb a b k (ltk b s)))) (send x))
  163.     ((recv k) (send k)))
  164.   (label 4)
  165.   (unrealized (0 2))
  166.   (origs (nb (0 1)))
  167.   (comment "1 in cohort - 1 not yet seen"))
  168.  
  169. (comment "Nothing left to do")
  170.  
  171. (defprotocol an_or basic
  172.   (defrole init
  173.     (vars (my_init_id yr_resp_id s name) (na text) (k skey))
  174.     (trace (send (cat my_init_id yr_resp_id na))
  175.       (recv
  176.         (enc "to_init" na my_init_id yr_resp_id k (ltk my_init_id s)))))
  177.   (defrole resp
  178.     (vars (yr_init_id my_resp_id s name) (na nb text) (k skey) (x mesg))
  179.     (trace (recv (cat yr_init_id my_resp_id na))
  180.       (send (cat yr_init_id my_resp_id na nb))
  181.       (recv
  182.         (cat x
  183.           (enc "to_resp" nb yr_init_id my_resp_id k
  184.             (ltk my_resp_id s)))) (send x)))
  185.   (defrole serv
  186.     (vars (a b s name) (na nb text) (k skey))
  187.     (trace (recv (cat a b na nb))
  188.       (send
  189.         (cat (enc "to_init" na a b k (ltk a s))
  190.           (enc "to_resp" nb a b k (ltk b s)))))
  191.     (uniq-orig k)))
  192.  
  193. (defskeleton an_or
  194.   (vars (na text) (s a b name) (k skey))
  195.   (defstrand init 2 (na na) (my_init_id a) (yr_resp_id b) (s s) (k k))
  196.   (deflistener k)
  197.   (non-orig (ltk a s) (ltk b s))
  198.   (uniq-orig na)
  199.   (traces
  200.     ((send (cat a b na)) (recv (enc "to_init" na a b k (ltk a s))))
  201.     ((recv k) (send k)))
  202.   (label 6)
  203.   (unrealized (0 1))
  204.   (origs (na (0 0)))
  205.   (comment "1 in cohort - 1 not yet seen"))
  206.  
  207. (comment "Nothing left to do")

Raw Paste


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