TEXT   29

woo lam

Guest on 23rd June 2022 02:54:40 AM

  1. (herald "Woo-Lam Protocol")
  2.  
  3. (comment "CPSA 2.2.11")
  4. (comment "All input read from woo_lam.scm")
  5.  
  6. (defprotocol woo_lam basic
  7.   (defrole init
  8.     (vars (my_init_id s name) (nb text))
  9.     (trace (send my_init_id) (recv nb)
  10.       (send (enc nb (ltk my_init_id s)))))
  11.   (defrole resp
  12.     (vars (my_resp_id yr_init_id s name) (nb text) (x mesg))
  13.     (trace (recv yr_init_id) (send nb) (recv x)
  14.       (send (enc yr_init_id x (ltk my_resp_id s)))
  15.       (recv (enc nb (ltk my_resp_id s)))))
  16.   (defrole server
  17.     (vars (a b s name) (nb text))
  18.     (trace (recv (enc a (enc nb (ltk a s)) (ltk b s)))
  19.       (send (enc nb (ltk b s))))))
  20.  
  21. (defskeleton woo_lam
  22.   (vars (x mesg) (nb text) (s a b name))
  23.   (defstrand resp 5 (x x) (nb nb) (my_resp_id b) (yr_init_id a) (s s))
  24.   (non-orig (ltk a s) (ltk b s))
  25.   (uniq-orig nb)
  26.   (traces
  27.     ((recv a) (send nb) (recv x) (send (enc a x (ltk b s)))
  28.       (recv (enc nb (ltk b s)))))
  29.   (label 0)
  30.   (unrealized (0 4))
  31.   (origs (nb (0 1)))
  32.   (comment "2 in cohort - 2 not yet seen"))
  33.  
  34. (defskeleton woo_lam
  35.   (vars (x mesg) (nb text) (s a b name))
  36.   (defstrand resp 5 (x x) (nb nb) (my_resp_id b) (yr_init_id a) (s s))
  37.   (defstrand init 3 (nb nb) (my_init_id b) (s s))
  38.   (precedes ((0 1) (1 1)) ((1 2) (0 4)))
  39.   (non-orig (ltk a s) (ltk b s))
  40.   (uniq-orig nb)
  41.   (operation encryption-test (added-strand init 3) (enc nb (ltk b s))
  42.     (0 4))
  43.   (traces
  44.     ((recv a) (send nb) (recv x) (send (enc a x (ltk b s)))
  45.       (recv (enc nb (ltk b s))))
  46.     ((send b) (recv nb) (send (enc nb (ltk b s)))))
  47.   (label 1)
  48.   (parent 0)
  49.   (unrealized)
  50.   (shape)
  51.   (maps ((0) ((nb nb) (s s) (a a) (b b) (x x))))
  52.   (origs (nb (0 1))))
  53.  
  54. (defskeleton woo_lam
  55.   (vars (x mesg) (nb text) (s a b a-0 name))
  56.   (defstrand resp 5 (x x) (nb nb) (my_resp_id b) (yr_init_id a) (s s))
  57.   (defstrand server 2 (nb nb) (a a-0) (b b) (s s))
  58.   (precedes ((0 1) (1 0)) ((1 1) (0 4)))
  59.   (non-orig (ltk a s) (ltk b s))
  60.   (uniq-orig nb)
  61.   (operation encryption-test (added-strand server 2) (enc nb (ltk b s))
  62.     (0 4))
  63.   (traces
  64.     ((recv a) (send nb) (recv x) (send (enc a x (ltk b s)))
  65.       (recv (enc nb (ltk b s))))
  66.     ((recv (enc a-0 (enc nb (ltk a-0 s)) (ltk b s)))
  67.       (send (enc nb (ltk b s)))))
  68.   (label 2)
  69.   (parent 0)
  70.   (unrealized (1 0))
  71.   (comment "2 in cohort - 2 not yet seen"))
  72.  
  73. (defskeleton woo_lam
  74.   (vars (nb text) (s a b name))
  75.   (defstrand resp 5 (x (enc nb (ltk a s))) (nb nb) (my_resp_id b)
  76.     (yr_init_id a) (s s))
  77.   (defstrand server 2 (nb nb) (a a) (b b) (s s))
  78.   (precedes ((0 3) (1 0)) ((1 1) (0 4)))
  79.   (non-orig (ltk a s) (ltk b s))
  80.   (uniq-orig nb)
  81.   (operation encryption-test (displaced 2 0 resp 4)
  82.     (enc a-0 (enc nb (ltk a-0 s)) (ltk b s)) (1 0))
  83.   (traces
  84.     ((recv a) (send nb) (recv (enc nb (ltk a s)))
  85.       (send (enc a (enc nb (ltk a s)) (ltk b s)))
  86.       (recv (enc nb (ltk b s))))
  87.     ((recv (enc a (enc nb (ltk a s)) (ltk b s)))
  88.       (send (enc nb (ltk b s)))))
  89.   (label 3)
  90.   (parent 2)
  91.   (unrealized (0 2))
  92.   (comment "2 in cohort - 2 not yet seen"))
  93.  
  94. (defskeleton woo_lam
  95.   (vars (x mesg) (nb nb-0 text) (s a b a-0 name))
  96.   (defstrand resp 5 (x x) (nb nb) (my_resp_id b) (yr_init_id a) (s s))
  97.   (defstrand server 2 (nb nb) (a a-0) (b b) (s s))
  98.   (defstrand resp 4 (x (enc nb (ltk a-0 s))) (nb nb-0) (my_resp_id b)
  99.     (yr_init_id a-0) (s s))
  100.   (precedes ((0 1) (2 2)) ((1 1) (0 4)) ((2 3) (1 0)))
  101.   (non-orig (ltk a s) (ltk b s))
  102.   (uniq-orig nb)
  103.   (operation encryption-test (added-strand resp 4)
  104.     (enc a-0 (enc nb (ltk a-0 s)) (ltk b s)) (1 0))
  105.   (traces
  106.     ((recv a) (send nb) (recv x) (send (enc a x (ltk b s)))
  107.       (recv (enc nb (ltk b s))))
  108.     ((recv (enc a-0 (enc nb (ltk a-0 s)) (ltk b s)))
  109.       (send (enc nb (ltk b s))))
  110.     ((recv a-0) (send nb-0) (recv (enc nb (ltk a-0 s)))
  111.       (send (enc a-0 (enc nb (ltk a-0 s)) (ltk b s)))))
  112.   (label 4)
  113.   (parent 2)
  114.   (unrealized)
  115.   (shape)
  116.   (maps ((0) ((nb nb) (s s) (a a) (b b) (x x))))
  117.   (origs (nb (0 1))))
  118.  
  119. (defskeleton woo_lam
  120.   (vars (nb text) (s a b name))
  121.   (defstrand resp 5 (x (enc nb (ltk a s))) (nb nb) (my_resp_id b)
  122.     (yr_init_id a) (s s))
  123.   (defstrand server 2 (nb nb) (a a) (b b) (s s))
  124.   (defstrand init 3 (nb nb) (my_init_id a) (s s))
  125.   (precedes ((0 1) (2 1)) ((0 3) (1 0)) ((1 1) (0 4)) ((2 2) (0 2)))
  126.   (non-orig (ltk a s) (ltk b s))
  127.   (uniq-orig nb)
  128.   (operation encryption-test (added-strand init 3) (enc nb (ltk a s))
  129.     (0 2))
  130.   (traces
  131.     ((recv a) (send nb) (recv (enc nb (ltk a s)))
  132.       (send (enc a (enc nb (ltk a s)) (ltk b s)))
  133.       (recv (enc nb (ltk b s))))
  134.     ((recv (enc a (enc nb (ltk a s)) (ltk b s)))
  135.       (send (enc nb (ltk b s))))
  136.     ((send a) (recv nb) (send (enc nb (ltk a s)))))
  137.   (label 5)
  138.   (parent 3)
  139.   (unrealized)
  140.   (shape)
  141.   (maps ((0) ((nb nb) (s s) (a a) (b b) (x (enc nb (ltk a s))))))
  142.   (origs (nb (0 1))))
  143.  
  144. (defskeleton woo_lam
  145.   (vars (nb text) (s a b a-0 name))
  146.   (defstrand resp 5 (x (enc nb (ltk a s))) (nb nb) (my_resp_id b)
  147.     (yr_init_id a) (s s))
  148.   (defstrand server 2 (nb nb) (a a) (b b) (s s))
  149.   (defstrand server 2 (nb nb) (a a-0) (b a) (s s))
  150.   (precedes ((0 1) (2 0)) ((0 3) (1 0)) ((1 1) (0 4)) ((2 1) (0 2)))
  151.   (non-orig (ltk a s) (ltk b s))
  152.   (uniq-orig nb)
  153.   (operation encryption-test (added-strand server 2) (enc nb (ltk a s))
  154.     (0 2))
  155.   (traces
  156.     ((recv a) (send nb) (recv (enc nb (ltk a s)))
  157.       (send (enc a (enc nb (ltk a s)) (ltk b s)))
  158.       (recv (enc nb (ltk b s))))
  159.     ((recv (enc a (enc nb (ltk a s)) (ltk b s)))
  160.       (send (enc nb (ltk b s))))
  161.     ((recv (enc a-0 (enc nb (ltk a-0 s)) (ltk a s)))
  162.       (send (enc nb (ltk a s)))))
  163.   (label 6)
  164.   (parent 3)
  165.   (unrealized (2 0))
  166.   (comment "1 in cohort - 1 not yet seen"))
  167.  
  168. (defskeleton woo_lam
  169.   (vars (nb nb-0 text) (s a b a-0 name))
  170.   (defstrand resp 5 (x (enc nb (ltk a s))) (nb nb) (my_resp_id b)
  171.     (yr_init_id a) (s s))
  172.   (defstrand server 2 (nb nb) (a a) (b b) (s s))
  173.   (defstrand server 2 (nb nb) (a a-0) (b a) (s s))
  174.   (defstrand resp 4 (x (enc nb (ltk a-0 s))) (nb nb-0) (my_resp_id a)
  175.     (yr_init_id a-0) (s s))
  176.   (precedes ((0 1) (3 2)) ((0 3) (1 0)) ((1 1) (0 4)) ((2 1) (0 2))
  177.     ((3 3) (2 0)))
  178.   (non-orig (ltk a s) (ltk b s))
  179.   (uniq-orig nb)
  180.   (operation encryption-test (added-strand resp 4)
  181.     (enc a-0 (enc nb (ltk a-0 s)) (ltk a s)) (2 0))
  182.   (traces
  183.     ((recv a) (send nb) (recv (enc nb (ltk a s)))
  184.       (send (enc a (enc nb (ltk a s)) (ltk b s)))
  185.       (recv (enc nb (ltk b s))))
  186.     ((recv (enc a (enc nb (ltk a s)) (ltk b s)))
  187.       (send (enc nb (ltk b s))))
  188.     ((recv (enc a-0 (enc nb (ltk a-0 s)) (ltk a s)))
  189.       (send (enc nb (ltk a s))))
  190.     ((recv a-0) (send nb-0) (recv (enc nb (ltk a-0 s)))
  191.       (send (enc a-0 (enc nb (ltk a-0 s)) (ltk a s)))))
  192.   (label 7)
  193.   (parent 6)
  194.   (unrealized)
  195.   (shape)
  196.   (maps ((0) ((nb nb) (s s) (a a) (b b) (x (enc nb (ltk a s))))))
  197.   (origs (nb (0 1))))
  198.  
  199. (comment "Nothing left to do")
  200.  
  201. (defprotocol an_woo_lam basic
  202.   (defrole init
  203.     (vars (my_init_id s name) (nb text))
  204.     (trace (send my_init_id) (recv nb)
  205.       (send (enc nb (ltk my_init_id s)))))
  206.   (defrole resp
  207.     (vars (my_resp_id yr_init_id s name) (nb text) (x mesg))
  208.     (trace (recv yr_init_id) (send nb) (recv x)
  209.       (send (enc yr_init_id x (ltk my_resp_id s)))
  210.       (recv (enc yr_init_id nb (ltk my_resp_id s)))))
  211.   (defrole server
  212.     (vars (a b s name) (nb text))
  213.     (trace (recv (enc a (enc nb (ltk a s)) (ltk b s)))
  214.       (send (enc a nb (ltk b s))))))
  215.  
  216. (defskeleton an_woo_lam
  217.   (vars (x mesg) (nb text) (s a b name))
  218.   (defstrand resp 5 (x x) (nb nb) (my_resp_id b) (yr_init_id a) (s s))
  219.   (non-orig (ltk a s) (ltk b s))
  220.   (uniq-orig nb)
  221.   (traces
  222.     ((recv a) (send nb) (recv x) (send (enc a x (ltk b s)))
  223.       (recv (enc a nb (ltk b s)))))
  224.   (label 8)
  225.   (unrealized (0 4))
  226.   (origs (nb (0 1)))
  227.   (comment "3 in cohort - 3 not yet seen"))
  228.  
  229. (defskeleton an_woo_lam
  230.   (vars (nb text) (s a b name))
  231.   (defstrand resp 5 (x nb) (nb nb) (my_resp_id b) (yr_init_id a) (s s))
  232.   (non-orig (ltk a s) (ltk b s))
  233.   (uniq-orig nb)
  234.   (operation encryption-test (displaced 1 0 resp 4) (enc a nb (ltk b s))
  235.     (0 4))
  236.   (traces
  237.     ((recv a) (send nb) (recv nb) (send (enc a nb (ltk b s)))
  238.       (recv (enc a nb (ltk b s)))))
  239.   (label 9)
  240.   (parent 8)
  241.   (unrealized)
  242.   (shape)
  243.   (maps ((0) ((nb nb) (s s) (a a) (b b) (x nb))))
  244.   (origs (nb (0 1))))
  245.  
  246. (defskeleton an_woo_lam
  247.   (vars (x mesg) (nb nb-0 text) (s a b name))
  248.   (defstrand resp 5 (x x) (nb nb) (my_resp_id b) (yr_init_id a) (s s))
  249.   (defstrand resp 4 (x nb) (nb nb-0) (my_resp_id b) (yr_init_id a)
  250.     (s s))
  251.   (precedes ((0 1) (1 2)) ((1 3) (0 4)))
  252.   (non-orig (ltk a s) (ltk b s))
  253.   (uniq-orig nb)
  254.   (operation encryption-test (added-strand resp 4) (enc a nb (ltk b s))
  255.     (0 4))
  256.   (traces
  257.     ((recv a) (send nb) (recv x) (send (enc a x (ltk b s)))
  258.       (recv (enc a nb (ltk b s))))
  259.     ((recv a) (send nb-0) (recv nb) (send (enc a nb (ltk b s)))))
  260.   (label 10)
  261.   (parent 8)
  262.   (unrealized)
  263.   (shape)
  264.   (maps ((0) ((nb nb) (s s) (a a) (b b) (x x))))
  265.   (origs (nb (0 1))))
  266.  
  267. (defskeleton an_woo_lam
  268.   (vars (x mesg) (nb text) (s a b name))
  269.   (defstrand resp 5 (x x) (nb nb) (my_resp_id b) (yr_init_id a) (s s))
  270.   (defstrand server 2 (nb nb) (a a) (b b) (s s))
  271.   (precedes ((0 1) (1 0)) ((1 1) (0 4)))
  272.   (non-orig (ltk a s) (ltk b s))
  273.   (uniq-orig nb)
  274.   (operation encryption-test (added-strand server 2)
  275.     (enc a nb (ltk b s)) (0 4))
  276.   (traces
  277.     ((recv a) (send nb) (recv x) (send (enc a x (ltk b s)))
  278.       (recv (enc a nb (ltk b s))))
  279.     ((recv (enc a (enc nb (ltk a s)) (ltk b s)))
  280.       (send (enc a nb (ltk b s)))))
  281.   (label 11)
  282.   (parent 8)
  283.   (unrealized (1 0))
  284.   (comment "2 in cohort - 2 not yet seen"))
  285.  
  286. (defskeleton an_woo_lam
  287.   (vars (nb text) (s a b name))
  288.   (defstrand resp 5 (x (enc nb (ltk a s))) (nb nb) (my_resp_id b)
  289.     (yr_init_id a) (s s))
  290.   (defstrand server 2 (nb nb) (a a) (b b) (s s))
  291.   (precedes ((0 3) (1 0)) ((1 1) (0 4)))
  292.   (non-orig (ltk a s) (ltk b s))
  293.   (uniq-orig nb)
  294.   (operation encryption-test (displaced 2 0 resp 4)
  295.     (enc a (enc nb (ltk a s)) (ltk b s)) (1 0))
  296.   (traces
  297.     ((recv a) (send nb) (recv (enc nb (ltk a s)))
  298.       (send (enc a (enc nb (ltk a s)) (ltk b s)))
  299.       (recv (enc a nb (ltk b s))))
  300.     ((recv (enc a (enc nb (ltk a s)) (ltk b s)))
  301.       (send (enc a nb (ltk b s)))))
  302.   (label 12)
  303.   (parent 11)
  304.   (unrealized (0 2))
  305.   (comment "1 in cohort - 1 not yet seen"))
  306.  
  307. (defskeleton an_woo_lam
  308.   (vars (x mesg) (nb nb-0 text) (s a b name))
  309.   (defstrand resp 5 (x x) (nb nb) (my_resp_id b) (yr_init_id a) (s s))
  310.   (defstrand server 2 (nb nb) (a a) (b b) (s s))
  311.   (defstrand resp 4 (x (enc nb (ltk a s))) (nb nb-0) (my_resp_id b)
  312.     (yr_init_id a) (s s))
  313.   (precedes ((0 1) (2 2)) ((1 1) (0 4)) ((2 3) (1 0)))
  314.   (non-orig (ltk a s) (ltk b s))
  315.   (uniq-orig nb)
  316.   (operation encryption-test (added-strand resp 4)
  317.     (enc a (enc nb (ltk a s)) (ltk b s)) (1 0))
  318.   (traces
  319.     ((recv a) (send nb) (recv x) (send (enc a x (ltk b s)))
  320.       (recv (enc a nb (ltk b s))))
  321.     ((recv (enc a (enc nb (ltk a s)) (ltk b s)))
  322.       (send (enc a nb (ltk b s))))
  323.     ((recv a) (send nb-0) (recv (enc nb (ltk a s)))
  324.       (send (enc a (enc nb (ltk a s)) (ltk b s)))))
  325.   (label 13)
  326.   (parent 11)
  327.   (unrealized (2 2))
  328.   (comment "1 in cohort - 1 not yet seen"))
  329.  
  330. (defskeleton an_woo_lam
  331.   (vars (nb text) (s a b name))
  332.   (defstrand resp 5 (x (enc nb (ltk a s))) (nb nb) (my_resp_id b)
  333.     (yr_init_id a) (s s))
  334.   (defstrand server 2 (nb nb) (a a) (b b) (s s))
  335.   (defstrand init 3 (nb nb) (my_init_id a) (s s))
  336.   (precedes ((0 1) (2 1)) ((0 3) (1 0)) ((1 1) (0 4)) ((2 2) (0 2)))
  337.   (non-orig (ltk a s) (ltk b s))
  338.   (uniq-orig nb)
  339.   (operation encryption-test (added-strand init 3) (enc nb (ltk a s))
  340.     (0 2))
  341.   (traces
  342.     ((recv a) (send nb) (recv (enc nb (ltk a s)))
  343.       (send (enc a (enc nb (ltk a s)) (ltk b s)))
  344.       (recv (enc a nb (ltk b s))))
  345.     ((recv (enc a (enc nb (ltk a s)) (ltk b s)))
  346.       (send (enc a nb (ltk b s))))
  347.     ((send a) (recv nb) (send (enc nb (ltk a s)))))
  348.   (label 14)
  349.   (parent 12)
  350.   (unrealized)
  351.   (shape)
  352.   (maps ((0) ((nb nb) (s s) (a a) (b b) (x (enc nb (ltk a s))))))
  353.   (origs (nb (0 1))))
  354.  
  355. (defskeleton an_woo_lam
  356.   (vars (x mesg) (nb nb-0 text) (s a b name))
  357.   (defstrand resp 5 (x x) (nb nb) (my_resp_id b) (yr_init_id a) (s s))
  358.   (defstrand server 2 (nb nb) (a a) (b b) (s s))
  359.   (defstrand resp 4 (x (enc nb (ltk a s))) (nb nb-0) (my_resp_id b)
  360.     (yr_init_id a) (s s))
  361.   (defstrand init 3 (nb nb) (my_init_id a) (s s))
  362.   (precedes ((0 1) (3 1)) ((1 1) (0 4)) ((2 3) (1 0)) ((3 2) (2 2)))
  363.   (non-orig (ltk a s) (ltk b s))
  364.   (uniq-orig nb)
  365.   (operation encryption-test (added-strand init 3) (enc nb (ltk a s))
  366.     (2 2))
  367.   (traces
  368.     ((recv a) (send nb) (recv x) (send (enc a x (ltk b s)))
  369.       (recv (enc a nb (ltk b s))))
  370.     ((recv (enc a (enc nb (ltk a s)) (ltk b s)))
  371.       (send (enc a nb (ltk b s))))
  372.     ((recv a) (send nb-0) (recv (enc nb (ltk a s)))
  373.       (send (enc a (enc nb (ltk a s)) (ltk b s))))
  374.     ((send a) (recv nb) (send (enc nb (ltk a s)))))
  375.   (label 15)
  376.   (parent 13)
  377.   (unrealized)
  378.   (shape)
  379.   (maps ((0) ((nb nb) (s s) (a a) (b b) (x x))))
  380.   (origs (nb (0 1))))
  381.  
  382. (comment "Nothing left to do")
  383.  
  384. (defprotocol tagged_an_woo_lam basic
  385.   (defrole init
  386.     (vars (my_init_id s name) (nb text))
  387.     (trace (send my_init_id) (recv nb)
  388.       (send (enc nb (ltk my_init_id s)))))
  389.   (defrole resp
  390.     (vars (my_resp_id yr_init_id s name) (nb text) (x mesg))
  391.     (trace (recv yr_init_id) (send nb) (recv x)
  392.       (send (enc yr_init_id x (ltk my_resp_id s)))
  393.       (recv (enc "result" yr_init_id nb (ltk my_resp_id s)))))
  394.   (defrole server
  395.     (vars (a b s name) (nb text))
  396.     (trace (recv (enc a (enc nb (ltk a s)) (ltk b s)))
  397.       (send (enc "result" a nb (ltk b s))))))
  398.  
  399. (defskeleton tagged_an_woo_lam
  400.   (vars (x mesg) (nb text) (s a b name))
  401.   (defstrand resp 5 (x x) (nb nb) (my_resp_id b) (yr_init_id a) (s s))
  402.   (non-orig (ltk a s) (ltk b s))
  403.   (uniq-orig nb)
  404.   (traces
  405.     ((recv a) (send nb) (recv x) (send (enc a x (ltk b s)))
  406.       (recv (enc "result" a nb (ltk b s)))))
  407.   (label 16)
  408.   (unrealized (0 4))
  409.   (origs (nb (0 1)))
  410.   (comment "1 in cohort - 1 not yet seen"))
  411.  
  412. (defskeleton tagged_an_woo_lam
  413.   (vars (x mesg) (nb text) (s a b name))
  414.   (defstrand resp 5 (x x) (nb nb) (my_resp_id b) (yr_init_id a) (s s))
  415.   (defstrand server 2 (nb nb) (a a) (b b) (s s))
  416.   (precedes ((0 1) (1 0)) ((1 1) (0 4)))
  417.   (non-orig (ltk a s) (ltk b s))
  418.   (uniq-orig nb)
  419.   (operation encryption-test (added-strand server 2)
  420.     (enc "result" a nb (ltk b s)) (0 4))
  421.   (traces
  422.     ((recv a) (send nb) (recv x) (send (enc a x (ltk b s)))
  423.       (recv (enc "result" a nb (ltk b s))))
  424.     ((recv (enc a (enc nb (ltk a s)) (ltk b s)))
  425.       (send (enc "result" a nb (ltk b s)))))
  426.   (label 17)
  427.   (parent 16)
  428.   (unrealized (1 0))
  429.   (comment "2 in cohort - 2 not yet seen"))
  430.  
  431. (defskeleton tagged_an_woo_lam
  432.   (vars (nb text) (s a b name))
  433.   (defstrand resp 5 (x (enc nb (ltk a s))) (nb nb) (my_resp_id b)
  434.     (yr_init_id a) (s s))
  435.   (defstrand server 2 (nb nb) (a a) (b b) (s s))
  436.   (precedes ((0 3) (1 0)) ((1 1) (0 4)))
  437.   (non-orig (ltk a s) (ltk b s))
  438.   (uniq-orig nb)
  439.   (operation encryption-test (displaced 2 0 resp 4)
  440.     (enc a (enc nb (ltk a s)) (ltk b s)) (1 0))
  441.   (traces
  442.     ((recv a) (send nb) (recv (enc nb (ltk a s)))
  443.       (send (enc a (enc nb (ltk a s)) (ltk b s)))
  444.       (recv (enc "result" a nb (ltk b s))))
  445.     ((recv (enc a (enc nb (ltk a s)) (ltk b s)))
  446.       (send (enc "result" a nb (ltk b s)))))
  447.   (label 18)
  448.   (parent 17)
  449.   (unrealized (0 2))
  450.   (comment "1 in cohort - 1 not yet seen"))
  451.  
  452. (defskeleton tagged_an_woo_lam
  453.   (vars (x mesg) (nb nb-0 text) (s a b name))
  454.   (defstrand resp 5 (x x) (nb nb) (my_resp_id b) (yr_init_id a) (s s))
  455.   (defstrand server 2 (nb nb) (a a) (b b) (s s))
  456.   (defstrand resp 4 (x (enc nb (ltk a s))) (nb nb-0) (my_resp_id b)
  457.     (yr_init_id a) (s s))
  458.   (precedes ((0 1) (2 2)) ((1 1) (0 4)) ((2 3) (1 0)))
  459.   (non-orig (ltk a s) (ltk b s))
  460.   (uniq-orig nb)
  461.   (operation encryption-test (added-strand resp 4)
  462.     (enc a (enc nb (ltk a s)) (ltk b s)) (1 0))
  463.   (traces
  464.     ((recv a) (send nb) (recv x) (send (enc a x (ltk b s)))
  465.       (recv (enc "result" a nb (ltk b s))))
  466.     ((recv (enc a (enc nb (ltk a s)) (ltk b s)))
  467.       (send (enc "result" a nb (ltk b s))))
  468.     ((recv a) (send nb-0) (recv (enc nb (ltk a s)))
  469.       (send (enc a (enc nb (ltk a s)) (ltk b s)))))
  470.   (label 19)
  471.   (parent 17)
  472.   (unrealized (2 2))
  473.   (comment "1 in cohort - 1 not yet seen"))
  474.  
  475. (defskeleton tagged_an_woo_lam
  476.   (vars (nb text) (s a b name))
  477.   (defstrand resp 5 (x (enc nb (ltk a s))) (nb nb) (my_resp_id b)
  478.     (yr_init_id a) (s s))
  479.   (defstrand server 2 (nb nb) (a a) (b b) (s s))
  480.   (defstrand init 3 (nb nb) (my_init_id a) (s s))
  481.   (precedes ((0 1) (2 1)) ((0 3) (1 0)) ((1 1) (0 4)) ((2 2) (0 2)))
  482.   (non-orig (ltk a s) (ltk b s))
  483.   (uniq-orig nb)
  484.   (operation encryption-test (added-strand init 3) (enc nb (ltk a s))
  485.     (0 2))
  486.   (traces
  487.     ((recv a) (send nb) (recv (enc nb (ltk a s)))
  488.       (send (enc a (enc nb (ltk a s)) (ltk b s)))
  489.       (recv (enc "result" a nb (ltk b s))))
  490.     ((recv (enc a (enc nb (ltk a s)) (ltk b s)))
  491.       (send (enc "result" a nb (ltk b s))))
  492.     ((send a) (recv nb) (send (enc nb (ltk a s)))))
  493.   (label 20)
  494.   (parent 18)
  495.   (unrealized)
  496.   (shape)
  497.   (maps ((0) ((nb nb) (s s) (a a) (b b) (x (enc nb (ltk a s))))))
  498.   (origs (nb (0 1))))
  499.  
  500. (defskeleton tagged_an_woo_lam
  501.   (vars (x mesg) (nb nb-0 text) (s a b name))
  502.   (defstrand resp 5 (x x) (nb nb) (my_resp_id b) (yr_init_id a) (s s))
  503.   (defstrand server 2 (nb nb) (a a) (b b) (s s))
  504.   (defstrand resp 4 (x (enc nb (ltk a s))) (nb nb-0) (my_resp_id b)
  505.     (yr_init_id a) (s s))
  506.   (defstrand init 3 (nb nb) (my_init_id a) (s s))
  507.   (precedes ((0 1) (3 1)) ((1 1) (0 4)) ((2 3) (1 0)) ((3 2) (2 2)))
  508.   (non-orig (ltk a s) (ltk b s))
  509.   (uniq-orig nb)
  510.   (operation encryption-test (added-strand init 3) (enc nb (ltk a s))
  511.     (2 2))
  512.   (traces
  513.     ((recv a) (send nb) (recv x) (send (enc a x (ltk b s)))
  514.       (recv (enc "result" a nb (ltk b s))))
  515.     ((recv (enc a (enc nb (ltk a s)) (ltk b s)))
  516.       (send (enc "result" a nb (ltk b s))))
  517.     ((recv a) (send nb-0) (recv (enc nb (ltk a s)))
  518.       (send (enc a (enc nb (ltk a s)) (ltk b s))))
  519.     ((send a) (recv nb) (send (enc nb (ltk a s)))))
  520.   (label 21)
  521.   (parent 19)
  522.   (unrealized)
  523.   (shape)
  524.   (maps ((0) ((nb nb) (s s) (a a) (b b) (x x))))
  525.   (origs (nb (0 1))))
  526.  
  527. (comment "Nothing left to do")

Raw Paste


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