TEXT   11

or shapes txt

Guest on 23rd June 2022 02:47:06 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 or.scm")
  10.  
  11. (defprotocol or basic
  12.   (defrole init
  13.     (vars (my_init_id yr_resp_id s name) (na text) (k skey) (m text))
  14.     (trace
  15.       (send
  16.         (cat m my_init_id yr_resp_id
  17.           (enc na m my_init_id yr_resp_id (ltk my_init_id s))))
  18.       (recv (cat m (enc na k (ltk my_init_id s))))))
  19.   (defrole resp
  20.     (vars (yr_init_id my_resp_id s name) (nb text) (k skey) (m text)
  21.       (x y mesg))
  22.     (trace (recv (cat m yr_init_id my_resp_id x))
  23.       (send
  24.         (cat m yr_init_id my_resp_id x
  25.           (enc nb m yr_init_id my_resp_id (ltk my_resp_id s))))
  26.       (recv (cat m y (enc nb k (ltk my_resp_id s)))) (send y)))
  27.   (defrole serv
  28.     (vars (a b s name) (na nb text) (k skey) (m text))
  29.     (trace
  30.       (recv
  31.         (cat m a b (enc na m a b (ltk a s)) (enc nb m a b (ltk b s))))
  32.       (send (cat m (enc na k (ltk a s)) (enc nb k (ltk b s)))))
  33.     (uniq-orig k)))
  34.  
  35. (defskeleton or
  36.   (vars (x y mesg) (nb m text) (s a b name) (k skey))
  37.   (defstrand resp 4 (x x) (y y) (nb nb) (m m) (yr_init_id a)
  38.     (my_resp_id b) (s s) (k k))
  39.   (non-orig (ltk a s) (ltk b s))
  40.   (uniq-orig nb)
  41.   (traces
  42.     ((recv (cat m a b x)) (send (cat m a b x (enc nb m a b (ltk b s))))
  43.       (recv (cat m y (enc nb k (ltk b s)))) (send y)))
  44.   (label 0)
  45.   (unrealized (0 2))
  46.   (origs (nb (0 1)))
  47.   (comment "2 in cohort - 2 not yet seen"))
  48.  
  49. (defskeleton or
  50.   (vars (x y mesg) (nb m nb-0 text) (s a name) (k skey))
  51.   (defstrand resp 4 (x x) (y y) (nb nb) (m m) (yr_init_id a)
  52.     (my_resp_id a) (s s) (k k))
  53.   (defstrand serv 2 (na nb) (nb nb-0) (m m) (a a) (b a) (s s) (k k))
  54.   (defstrand init 1 (na nb-0) (m m) (my_init_id a) (yr_resp_id a) (s s))
  55.   (precedes ((0 1) (1 0)) ((1 1) (0 2)) ((2 0) (1 0)))
  56.   (non-orig (ltk a s))
  57.   (uniq-orig nb k)
  58.   (operation encryption-test (added-strand init 1)
  59.     (enc nb-0 m a a (ltk a s)) (1 0))
  60.   (traces
  61.     ((recv (cat m a a x)) (send (cat m a a x (enc nb m a a (ltk a s))))
  62.       (recv (cat m y (enc nb k (ltk a s)))) (send y))
  63.     ((recv
  64.        (cat m a a (enc nb m a a (ltk a s)) (enc nb-0 m a a (ltk a s))))
  65.       (send (cat m (enc nb k (ltk a s)) (enc nb-0 k (ltk a s)))))
  66.     ((send (cat m a a (enc nb-0 m a a (ltk a s))))))
  67.   (label 5)
  68.   (parent 0)
  69.   (unrealized)
  70.   (shape)
  71.   (maps ((0) ((nb nb) (s s) (a a) (b a) (k k) (m m) (x x) (y y))))
  72.   (origs (k (1 1)) (nb (0 1))))
  73.  
  74. (defskeleton or
  75.   (vars (x y mesg) (nb m text) (s a name) (k skey))
  76.   (defstrand resp 4 (x x) (y y) (nb nb) (m m) (yr_init_id a)
  77.     (my_resp_id a) (s s) (k k))
  78.   (defstrand serv 2 (na nb) (nb nb) (m m) (a a) (b a) (s s) (k k))
  79.   (precedes ((0 1) (1 0)) ((1 1) (0 2)))
  80.   (non-orig (ltk a s))
  81.   (uniq-orig nb k)
  82.   (operation encryption-test (displaced 2 0 resp 2)
  83.     (enc nb-0 m a a (ltk a s)) (1 0))
  84.   (traces
  85.     ((recv (cat m a a x)) (send (cat m a a x (enc nb m a a (ltk a s))))
  86.       (recv (cat m y (enc nb k (ltk a s)))) (send y))
  87.     ((recv
  88.        (cat m a a (enc nb m a a (ltk a s)) (enc nb m a a (ltk a s))))
  89.       (send (cat m (enc nb k (ltk a s)) (enc nb k (ltk a s))))))
  90.   (label 6)
  91.   (parent 0)
  92.   (unrealized)
  93.   (shape)
  94.   (maps ((0) ((nb nb) (s s) (a a) (b a) (k k) (m m) (x x) (y y))))
  95.   (origs (k (1 1)) (nb (0 1))))
  96.  
  97. (defskeleton or
  98.   (vars (x y x-0 mesg) (nb m nb-0 text) (s a name) (k skey))
  99.   (defstrand resp 4 (x x) (y y) (nb nb) (m m) (yr_init_id a)
  100.     (my_resp_id a) (s s) (k k))
  101.   (defstrand serv 2 (na nb) (nb nb-0) (m m) (a a) (b a) (s s) (k k))
  102.   (defstrand resp 2 (x x-0) (nb nb-0) (m m) (yr_init_id a)
  103.     (my_resp_id a) (s s))
  104.   (precedes ((0 1) (1 0)) ((1 1) (0 2)) ((2 1) (1 0)))
  105.   (non-orig (ltk a s))
  106.   (uniq-orig nb k)
  107.   (operation encryption-test (added-strand resp 2)
  108.     (enc nb-0 m a a (ltk a s)) (1 0))
  109.   (traces
  110.     ((recv (cat m a a x)) (send (cat m a a x (enc nb m a a (ltk a s))))
  111.       (recv (cat m y (enc nb k (ltk a s)))) (send y))
  112.     ((recv
  113.        (cat m a a (enc nb m a a (ltk a s)) (enc nb-0 m a a (ltk a s))))
  114.       (send (cat m (enc nb k (ltk a s)) (enc nb-0 k (ltk a s)))))
  115.     ((recv (cat m a a x-0))
  116.       (send (cat m a a x-0 (enc nb-0 m a a (ltk a s))))))
  117.   (label 7)
  118.   (parent 0)
  119.   (unrealized)
  120.   (shape)
  121.   (maps ((0) ((nb nb) (s s) (a a) (b a) (k k) (m m) (x x) (y y))))
  122.   (origs (k (1 1)) (nb (0 1))))
  123.  
  124. (defskeleton or
  125.   (vars (x y mesg) (nb m na text) (s a b name) (k skey))
  126.   (defstrand resp 4 (x x) (y y) (nb nb) (m m) (yr_init_id a)
  127.     (my_resp_id b) (s s) (k k))
  128.   (defstrand serv 2 (na na) (nb nb) (m m) (a a) (b b) (s s) (k k))
  129.   (defstrand init 1 (na na) (m m) (my_init_id a) (yr_resp_id b) (s s))
  130.   (precedes ((0 1) (1 0)) ((1 1) (0 2)) ((2 0) (1 0)))
  131.   (non-orig (ltk a s) (ltk b s))
  132.   (uniq-orig nb k)
  133.   (operation encryption-test (added-strand init 1)
  134.     (enc na m a b (ltk a s)) (1 0))
  135.   (traces
  136.     ((recv (cat m a b x)) (send (cat m a b x (enc nb m a b (ltk b s))))
  137.       (recv (cat m y (enc nb k (ltk b s)))) (send y))
  138.     ((recv
  139.        (cat m a b (enc na m a b (ltk a s)) (enc nb m a b (ltk b s))))
  140.       (send (cat m (enc na k (ltk a s)) (enc nb k (ltk b s)))))
  141.     ((send (cat m a b (enc na m a b (ltk a s))))))
  142.   (label 8)
  143.   (parent 0)
  144.   (unrealized)
  145.   (shape)
  146.   (maps ((0) ((nb nb) (s s) (a a) (b b) (k k) (m m) (x x) (y y))))
  147.   (origs (k (1 1)) (nb (0 1))))
  148.  
  149. (defskeleton or
  150.   (vars (x y x-0 mesg) (nb m na text) (s a name) (k skey))
  151.   (defstrand resp 4 (x x) (y y) (nb nb) (m m) (yr_init_id a)
  152.     (my_resp_id a) (s s) (k k))
  153.   (defstrand serv 2 (na na) (nb nb) (m m) (a a) (b a) (s s) (k k))
  154.   (defstrand resp 2 (x x-0) (nb na) (m m) (yr_init_id a) (my_resp_id a)
  155.     (s s))
  156.   (precedes ((0 1) (1 0)) ((1 1) (0 2)) ((2 1) (1 0)))
  157.   (non-orig (ltk a s))
  158.   (uniq-orig nb k)
  159.   (operation encryption-test (added-strand resp 2)
  160.     (enc na m a a (ltk a s)) (1 0))
  161.   (traces
  162.     ((recv (cat m a a x)) (send (cat m a a x (enc nb m a a (ltk a s))))
  163.       (recv (cat m y (enc nb k (ltk a s)))) (send y))
  164.     ((recv
  165.        (cat m a a (enc na m a a (ltk a s)) (enc nb m a a (ltk a s))))
  166.       (send (cat m (enc na k (ltk a s)) (enc nb k (ltk a s)))))
  167.     ((recv (cat m a a x-0))
  168.       (send (cat m a a x-0 (enc na m a a (ltk a s))))))
  169.   (label 9)
  170.   (parent 0)
  171.   (unrealized)
  172.   (shape)
  173.   (maps ((0) ((nb nb) (s s) (a a) (b a) (k k) (m m) (x x) (y y))))
  174.   (origs (k (1 1)) (nb (0 1))))
  175.  
  176. (comment "Nothing left to do")
  177.  
  178. (defprotocol or basic
  179.   (defrole init
  180.     (vars (my_init_id yr_resp_id s name) (na text) (k skey) (m text))
  181.     (trace
  182.       (send
  183.         (cat m my_init_id yr_resp_id
  184.           (enc na m my_init_id yr_resp_id (ltk my_init_id s))))
  185.       (recv (cat m (enc na k (ltk my_init_id s))))))
  186.   (defrole resp
  187.     (vars (yr_init_id my_resp_id s name) (nb text) (k skey) (m text)
  188.       (x y mesg))
  189.     (trace (recv (cat m yr_init_id my_resp_id x))
  190.       (send
  191.         (cat m yr_init_id my_resp_id x
  192.           (enc nb m yr_init_id my_resp_id (ltk my_resp_id s))))
  193.       (recv (cat m y (enc nb k (ltk my_resp_id s)))) (send y)))
  194.   (defrole serv
  195.     (vars (a b s name) (na nb text) (k skey) (m text))
  196.     (trace
  197.       (recv
  198.         (cat m a b (enc na m a b (ltk a s)) (enc nb m a b (ltk b s))))
  199.       (send (cat m (enc na k (ltk a s)) (enc nb k (ltk b s)))))
  200.     (uniq-orig k)))
  201.  
  202. (defskeleton or
  203.   (vars (na m text) (s a b name) (k skey))
  204.   (defstrand init 2 (na na) (m m) (my_init_id a) (yr_resp_id b) (s s)
  205.     (k k))
  206.   (non-orig (ltk a s) (ltk b s))
  207.   (uniq-orig na)
  208.   (traces
  209.     ((send (cat m a b (enc na m a b (ltk a s))))
  210.       (recv (cat m (enc na k (ltk a s))))))
  211.   (label 10)
  212.   (unrealized (0 1))
  213.   (origs (na (0 0)))
  214.   (comment "2 in cohort - 2 not yet seen"))
  215.  
  216. (defskeleton or
  217.   (vars (na m text) (s b name) (k skey))
  218.   (defstrand init 2 (na na) (m m) (my_init_id b) (yr_resp_id b) (s s)
  219.     (k k))
  220.   (defstrand serv 2 (na na) (nb na) (m m) (a b) (b b) (s s) (k k))
  221.   (precedes ((0 0) (1 0)) ((1 1) (0 1)))
  222.   (non-orig (ltk b s))
  223.   (uniq-orig na k)
  224.   (operation encryption-test (displaced 2 0 init 1)
  225.     (enc nb m b b (ltk b s)) (1 0))
  226.   (traces
  227.     ((send (cat m b b (enc na m b b (ltk b s))))
  228.       (recv (cat m (enc na k (ltk b s)))))
  229.     ((recv
  230.        (cat m b b (enc na m b b (ltk b s)) (enc na m b b (ltk b s))))
  231.       (send (cat m (enc na k (ltk b s)) (enc na k (ltk b s))))))
  232.   (label 15)
  233.   (parent 10)
  234.   (unrealized)
  235.   (shape)
  236.   (maps ((0) ((na na) (s s) (a b) (b b) (k k) (m m))))
  237.   (origs (k (1 1)) (na (0 0))))
  238.  
  239. (defskeleton or
  240.   (vars (na m nb text) (s b name) (k skey))
  241.   (defstrand init 2 (na na) (m m) (my_init_id b) (yr_resp_id b) (s s)
  242.     (k k))
  243.   (defstrand serv 2 (na na) (nb nb) (m m) (a b) (b b) (s s) (k k))
  244.   (defstrand init 1 (na nb) (m m) (my_init_id b) (yr_resp_id b) (s s))
  245.   (precedes ((0 0) (1 0)) ((1 1) (0 1)) ((2 0) (1 0)))
  246.   (non-orig (ltk b s))
  247.   (uniq-orig na k)
  248.   (operation encryption-test (added-strand init 1)
  249.     (enc nb m b b (ltk b s)) (1 0))
  250.   (traces
  251.     ((send (cat m b b (enc na m b b (ltk b s))))
  252.       (recv (cat m (enc na k (ltk b s)))))
  253.     ((recv
  254.        (cat m b b (enc na m b b (ltk b s)) (enc nb m b b (ltk b s))))
  255.       (send (cat m (enc na k (ltk b s)) (enc nb k (ltk b s)))))
  256.     ((send (cat m b b (enc nb m b b (ltk b s))))))
  257.   (label 16)
  258.   (parent 10)
  259.   (unrealized)
  260.   (shape)
  261.   (maps ((0) ((na na) (s s) (a b) (b b) (k k) (m m))))
  262.   (origs (k (1 1)) (na (0 0))))
  263.  
  264. (defskeleton or
  265.   (vars (x mesg) (na m nb text) (s a b name) (k skey))
  266.   (defstrand init 2 (na na) (m m) (my_init_id a) (yr_resp_id b) (s s)
  267.     (k k))
  268.   (defstrand serv 2 (na na) (nb nb) (m m) (a a) (b b) (s s) (k k))
  269.   (defstrand resp 2 (x x) (nb nb) (m m) (yr_init_id a) (my_resp_id b)
  270.     (s s))
  271.   (precedes ((0 0) (1 0)) ((1 1) (0 1)) ((2 1) (1 0)))
  272.   (non-orig (ltk a s) (ltk b s))
  273.   (uniq-orig na k)
  274.   (operation encryption-test (added-strand resp 2)
  275.     (enc nb m a b (ltk b s)) (1 0))
  276.   (traces
  277.     ((send (cat m a b (enc na m a b (ltk a s))))
  278.       (recv (cat m (enc na k (ltk a s)))))
  279.     ((recv
  280.        (cat m a b (enc na m a b (ltk a s)) (enc nb m a b (ltk b s))))
  281.       (send (cat m (enc na k (ltk a s)) (enc nb k (ltk b s)))))
  282.     ((recv (cat m a b x))
  283.       (send (cat m a b x (enc nb m a b (ltk b s))))))
  284.   (label 17)
  285.   (parent 10)
  286.   (unrealized)
  287.   (shape)
  288.   (maps ((0) ((na na) (s s) (a a) (b b) (k k) (m m))))
  289.   (origs (k (1 1)) (na (0 0))))
  290.  
  291. (defskeleton or
  292.   (vars (na m na-0 text) (s b name) (k skey))
  293.   (defstrand init 2 (na na) (m m) (my_init_id b) (yr_resp_id b) (s s)
  294.     (k k))
  295.   (defstrand serv 2 (na na-0) (nb na) (m m) (a b) (b b) (s s) (k k))
  296.   (defstrand init 1 (na na-0) (m m) (my_init_id b) (yr_resp_id b) (s s))
  297.   (precedes ((0 0) (1 0)) ((1 1) (0 1)) ((2 0) (1 0)))
  298.   (non-orig (ltk b s))
  299.   (uniq-orig na k)
  300.   (operation encryption-test (added-strand init 1)
  301.     (enc na-0 m b b (ltk b s)) (1 0))
  302.   (traces
  303.     ((send (cat m b b (enc na m b b (ltk b s))))
  304.       (recv (cat m (enc na k (ltk b s)))))
  305.     ((recv
  306.        (cat m b b (enc na-0 m b b (ltk b s)) (enc na m b b (ltk b s))))
  307.       (send (cat m (enc na-0 k (ltk b s)) (enc na k (ltk b s)))))
  308.     ((send (cat m b b (enc na-0 m b b (ltk b s))))))
  309.   (label 18)
  310.   (parent 10)
  311.   (unrealized)
  312.   (shape)
  313.   (maps ((0) ((na na) (s s) (a b) (b b) (k k) (m m))))
  314.   (origs (k (1 1)) (na (0 0))))
  315.  
  316. (defskeleton or
  317.   (vars (x mesg) (na m na-0 text) (s b name) (k skey))
  318.   (defstrand init 2 (na na) (m m) (my_init_id b) (yr_resp_id b) (s s)
  319.     (k k))
  320.   (defstrand serv 2 (na na-0) (nb na) (m m) (a b) (b b) (s s) (k k))
  321.   (defstrand resp 2 (x x) (nb na-0) (m m) (yr_init_id b) (my_resp_id b)
  322.     (s s))
  323.   (precedes ((0 0) (1 0)) ((1 1) (0 1)) ((2 1) (1 0)))
  324.   (non-orig (ltk b s))
  325.   (uniq-orig na k)
  326.   (operation encryption-test (added-strand resp 2)
  327.     (enc na-0 m b b (ltk b s)) (1 0))
  328.   (traces
  329.     ((send (cat m b b (enc na m b b (ltk b s))))
  330.       (recv (cat m (enc na k (ltk b s)))))
  331.     ((recv
  332.        (cat m b b (enc na-0 m b b (ltk b s)) (enc na m b b (ltk b s))))
  333.       (send (cat m (enc na-0 k (ltk b s)) (enc na k (ltk b s)))))
  334.     ((recv (cat m b b x))
  335.       (send (cat m b b x (enc na-0 m b b (ltk b s))))))
  336.   (label 19)
  337.   (parent 10)
  338.   (unrealized)
  339.   (shape)
  340.   (maps ((0) ((na na) (s s) (a b) (b b) (k k) (m m))))
  341.   (origs (k (1 1)) (na (0 0))))
  342.  
  343. (comment "Nothing left to do")
  344.  
  345. (defprotocol or basic
  346.   (defrole init
  347.     (vars (my_init_id yr_resp_id s name) (na text) (k skey) (m text))
  348.     (trace
  349.       (send
  350.         (cat m my_init_id yr_resp_id
  351.           (enc na m my_init_id yr_resp_id (ltk my_init_id s))))
  352.       (recv (cat m (enc na k (ltk my_init_id s))))))
  353.   (defrole resp
  354.     (vars (yr_init_id my_resp_id s name) (nb text) (k skey) (m text)
  355.       (x y mesg))
  356.     (trace (recv (cat m yr_init_id my_resp_id x))
  357.       (send
  358.         (cat m yr_init_id my_resp_id x
  359.           (enc nb m yr_init_id my_resp_id (ltk my_resp_id s))))
  360.       (recv (cat m y (enc nb k (ltk my_resp_id s)))) (send y)))
  361.   (defrole serv
  362.     (vars (a b s name) (na nb text) (k skey) (m text))
  363.     (trace
  364.       (recv
  365.         (cat m a b (enc na m a b (ltk a s)) (enc nb m a b (ltk b s))))
  366.       (send (cat m (enc na k (ltk a s)) (enc nb k (ltk b s)))))
  367.     (uniq-orig k)))
  368.  
  369. (defskeleton or
  370.   (vars (x y mesg) (nb m text) (s a b name) (k skey))
  371.   (defstrand resp 4 (x x) (y y) (nb nb) (m m) (yr_init_id a)
  372.     (my_resp_id b) (s s) (k k))
  373.   (deflistener k)
  374.   (non-orig (ltk a s) (ltk b s))
  375.   (uniq-orig nb)
  376.   (traces
  377.     ((recv (cat m a b x)) (send (cat m a b x (enc nb m a b (ltk b s))))
  378.       (recv (cat m y (enc nb k (ltk b s)))) (send y))
  379.     ((recv k) (send k)))
  380.   (label 20)
  381.   (unrealized (0 2))
  382.   (origs (nb (0 1)))
  383.   (comment "2 in cohort - 2 not yet seen"))
  384.  
  385. (comment "Nothing left to do")
  386.  
  387. (defprotocol or basic
  388.   (defrole init
  389.     (vars (my_init_id yr_resp_id s name) (na text) (k skey) (m text))
  390.     (trace
  391.       (send
  392.         (cat m my_init_id yr_resp_id
  393.           (enc na m my_init_id yr_resp_id (ltk my_init_id s))))
  394.       (recv (cat m (enc na k (ltk my_init_id s))))))
  395.   (defrole resp
  396.     (vars (yr_init_id my_resp_id s name) (nb text) (k skey) (m text)
  397.       (x y mesg))
  398.     (trace (recv (cat m yr_init_id my_resp_id x))
  399.       (send
  400.         (cat m yr_init_id my_resp_id x
  401.           (enc nb m yr_init_id my_resp_id (ltk my_resp_id s))))
  402.       (recv (cat m y (enc nb k (ltk my_resp_id s)))) (send y)))
  403.   (defrole serv
  404.     (vars (a b s name) (na nb text) (k skey) (m text))
  405.     (trace
  406.       (recv
  407.         (cat m a b (enc na m a b (ltk a s)) (enc nb m a b (ltk b s))))
  408.       (send (cat m (enc na k (ltk a s)) (enc nb k (ltk b s)))))
  409.     (uniq-orig k)))
  410.  
  411. (defskeleton or
  412.   (vars (na m text) (s a b name) (k skey))
  413.   (defstrand init 2 (na na) (m m) (my_init_id a) (yr_resp_id b) (s s)
  414.     (k k))
  415.   (deflistener k)
  416.   (non-orig (ltk a s) (ltk b s))
  417.   (uniq-orig na)
  418.   (traces
  419.     ((send (cat m a b (enc na m a b (ltk a s))))
  420.       (recv (cat m (enc na k (ltk a s))))) ((recv k) (send k)))
  421.   (label 30)
  422.   (unrealized (0 1))
  423.   (origs (na (0 0)))
  424.   (comment "2 in cohort - 2 not yet seen"))
  425.  
  426. (comment "Nothing left to do")

Raw Paste

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