cpsa-4.4.9: tst/chan-mesg.tst

(herald "Yahalom Protocol Without Forwarding" (bound 15)
  (comment "Testing channels as arbitrary messages."))

(comment "CPSA 4.4.9")
(comment "All input read from tst/chan-mesg.scm")
(comment "Strand count bounded at 15")

(defprotocol yahalom basic
  (defrole init
    (vars (a b c name) (n-a n-b text) (k skey))
    (trace (send (cat a n-a)) (recv (cat c a) (cat a b k n-a n-b))
      (send (enc n-b k))))
  (defrole resp
    (vars (b a c name) (n-a n-b text) (k skey))
    (trace (recv (cat a n-a)) (send (cat b c) (cat a b n-a n-b))
      (recv (cat c b) (cat a b k)) (recv (enc n-b k))))
  (defrole serv
    (vars (c a b name) (n-a n-b text) (k skey))
    (trace (recv (cat b c) (cat a b n-a n-b))
      (send (cat c a) (cat a b k n-a n-b)) (send (cat c b) (cat a b k)))
    (uniq-orig k))
  (defgenrule neqRl_indx
    (forall ((x indx)) (implies (fact neq x x) (false))))
  (defgenrule neqRl_strd
    (forall ((x strd)) (implies (fact neq x x) (false))))
  (defgenrule neqRl_mesg
    (forall ((x mesg)) (implies (fact neq x x) (false))))
  (comment
    "Use (cat x y) as channel from x to y. Matching channel should force matching names."))

(defskeleton yahalom
  (vars (k skey) (n-b n-a text) (a b c name))
  (defstrand resp 4 (k k) (n-a n-a) (n-b n-b) (b b) (a a) (c c))
  (uniq-orig n-b)
  (auth (cat c b))
  (traces
    ((recv (cat a n-a)) (send (cat b c) (cat a b n-a n-b))
      (recv (cat c b) (cat a b k)) (recv (enc n-b k))))
  (label 0)
  (unrealized (0 2))
  (maps ((0) ((a a) (b b) (c c) (n-b n-b) (n-a n-a) (k k))))
  (origs (n-b (0 1)))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton yahalom
  (vars (k skey) (n-b n-a n-a-0 n-b-0 text) (a b c name))
  (defstrand resp 4 (k k) (n-a n-a) (n-b n-b) (b b) (a a) (c c))
  (defstrand serv 3 (k k) (n-a n-a-0) (n-b n-b-0) (c c) (a a) (b b))
  (precedes ((1 2) (0 2)))
  (uniq-orig k n-b)
  (auth (cat c b))
  (operation channel-test (added-strand serv 3)
    (ch-msg (cat c b) (cat a b k)) (0 2))
  (strand-map 0)
  (traces
    ((recv (cat a n-a)) (send (cat b c) (cat a b n-a n-b))
      (recv (cat c b) (cat a b k)) (recv (enc n-b k)))
    ((recv (cat b c) (cat a b n-a-0 n-b-0))
      (send (cat c a) (cat a b k n-a-0 n-b-0))
      (send (cat c b) (cat a b k))))
  (label 1)
  (parent 0)
  (realized)
  (shape)
  (maps ((0) ((a a) (b b) (c c) (n-b n-b) (n-a n-a) (k k))))
  (origs (k (1 1)) (n-b (0 1))))

(comment "Nothing left to do")

(defprotocol yahalom basic
  (defrole init
    (vars (a b c name) (n-a n-b text) (k skey))
    (trace (send (cat a n-a)) (recv (cat c a) (cat a b k n-a n-b))
      (send (enc n-b k))))
  (defrole resp
    (vars (b a c name) (n-a n-b text) (k skey))
    (trace (recv (cat a n-a)) (send (cat b c) (cat a b n-a n-b))
      (recv (cat c b) (cat a b k)) (recv (enc n-b k))))
  (defrole serv
    (vars (c a b name) (n-a n-b text) (k skey))
    (trace (recv (cat b c) (cat a b n-a n-b))
      (send (cat c a) (cat a b k n-a n-b)) (send (cat c b) (cat a b k)))
    (uniq-orig k))
  (defgenrule neqRl_indx
    (forall ((x indx)) (implies (fact neq x x) (false))))
  (defgenrule neqRl_strd
    (forall ((x strd)) (implies (fact neq x x) (false))))
  (defgenrule neqRl_mesg
    (forall ((x mesg)) (implies (fact neq x x) (false))))
  (comment
    "Use (cat x y) as channel from x to y. Matching channel should force matching names."))

(defskeleton yahalom
  (vars (k skey) (n-b n-a n-a-0 n-b-0 text) (a b c name))
  (defstrand resp 4 (k k) (n-a n-a) (n-b n-b) (b b) (a a) (c c))
  (defstrand serv 3 (k k) (n-a n-a-0) (n-b n-b-0) (c c) (a a) (b b))
  (precedes ((1 2) (0 2)))
  (uniq-orig k n-b)
  (conf (cat c a) (cat c b))
  (auth (cat c b))
  (traces
    ((recv (cat a n-a)) (send (cat b c) (cat a b n-a n-b))
      (recv (cat c b) (cat a b k)) (recv (enc n-b k)))
    ((recv (cat b c) (cat a b n-a-0 n-b-0))
      (send (cat c a) (cat a b k n-a-0 n-b-0))
      (send (cat c b) (cat a b k))))
  (label 2)
  (unrealized (0 3))
  (maps
    ((0 1)
      ((k k) (n-b n-b) (n-a n-a) (n-a-0 n-a-0) (n-b-0 n-b-0) (a a) (b b)
        (c c))))
  (origs (k (1 1)) (n-b (0 1)))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton yahalom
  (vars (k skey) (n-b n-a n-a-0 n-b-0 n-a-1 text)
    (a b c a-0 b-0 c-0 name))
  (defstrand resp 4 (k k) (n-a n-a) (n-b n-b) (b b) (a a) (c c))
  (defstrand serv 3 (k k) (n-a n-a-0) (n-b n-b-0) (c c) (a a) (b b))
  (defstrand init 3 (k k) (n-a n-a-1) (n-b n-b) (a a-0) (b b-0) (c c-0))
  (precedes ((0 1) (2 1)) ((1 1) (2 1)) ((1 2) (0 2)) ((2 2) (0 3)))
  (uniq-orig k n-b)
  (conf (cat c a) (cat c b))
  (auth (cat c b))
  (operation encryption-test (added-strand init 3) (enc n-b k) (0 3))
  (strand-map 0 1)
  (traces
    ((recv (cat a n-a)) (send (cat b c) (cat a b n-a n-b))
      (recv (cat c b) (cat a b k)) (recv (enc n-b k)))
    ((recv (cat b c) (cat a b n-a-0 n-b-0))
      (send (cat c a) (cat a b k n-a-0 n-b-0))
      (send (cat c b) (cat a b k)))
    ((send (cat a-0 n-a-1))
      (recv (cat c-0 a-0) (cat a-0 b-0 k n-a-1 n-b))
      (send (enc n-b k))))
  (label 3)
  (parent 2)
  (unrealized (2 1))
  (maps
    ((0 1)
      ((k k) (n-b n-b) (n-a n-a) (n-a-0 n-a-0) (n-b-0 n-b-0) (a a) (b b)
        (c c))))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton yahalom
  (vars (k skey) (n-b n-a n-a-0 n-b-0 text) (a b c name))
  (defstrand resp 4 (k k) (n-a n-a) (n-b n-b) (b b) (a a) (c c))
  (defstrand serv 3 (k k) (n-a n-a-0) (n-b n-b-0) (c c) (a a) (b b))
  (deflistener k)
  (precedes ((1 1) (2 0)) ((1 2) (0 2)) ((2 1) (0 3)))
  (uniq-orig k n-b)
  (conf (cat c a) (cat c b))
  (auth (cat c b))
  (operation encryption-test (added-listener k) (enc n-b k) (0 3))
  (strand-map 0 1)
  (traces
    ((recv (cat a n-a)) (send (cat b c) (cat a b n-a n-b))
      (recv (cat c b) (cat a b k)) (recv (enc n-b k)))
    ((recv (cat b c) (cat a b n-a-0 n-b-0))
      (send (cat c a) (cat a b k n-a-0 n-b-0))
      (send (cat c b) (cat a b k))) ((recv k) (send k)))
  (label 4)
  (parent 2)
  (unrealized (2 0))
  (maps
    ((0 1)
      ((k k) (n-b n-b) (n-a n-a) (n-a-0 n-a-0) (n-b-0 n-b-0) (a a) (b b)
        (c c))))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton yahalom
  (vars (k skey) (n-a n-a-0 n-b text) (a b c name))
  (defstrand resp 4 (k k) (n-a n-a) (n-b n-b) (b b) (a a) (c c))
  (defstrand serv 3 (k k) (n-a n-a-0) (n-b n-b) (c c) (a a) (b b))
  (defstrand init 3 (k k) (n-a n-a-0) (n-b n-b) (a a) (b b) (c c))
  (precedes ((0 1) (1 0)) ((1 1) (2 1)) ((1 2) (0 2)) ((2 2) (0 3)))
  (uniq-orig k n-b)
  (conf (cat c a) (cat c b))
  (auth (cat c b))
  (operation nonce-test
    (contracted (n-b-0 n-b) (a-0 a) (b-0 b) (c-0 c) (n-a-1 n-a-0)) k
    (2 1) (ch-msg (cat c a) (cat a b k n-a-0 n-b)))
  (strand-map 0 1 2)
  (traces
    ((recv (cat a n-a)) (send (cat b c) (cat a b n-a n-b))
      (recv (cat c b) (cat a b k)) (recv (enc n-b k)))
    ((recv (cat b c) (cat a b n-a-0 n-b))
      (send (cat c a) (cat a b k n-a-0 n-b))
      (send (cat c b) (cat a b k)))
    ((send (cat a n-a-0)) (recv (cat c a) (cat a b k n-a-0 n-b))
      (send (enc n-b k))))
  (label 5)
  (parent 3)
  (realized)
  (shape)
  (maps
    ((0 1)
      ((k k) (n-b n-b) (n-a n-a) (n-a-0 n-a-0) (n-b-0 n-b) (a a) (b b)
        (c c))))
  (origs (k (1 1)) (n-b (0 1))))

(defskeleton yahalom
  (vars (k skey) (n-b n-a n-a-0 n-b-0 n-a-1 text)
    (a b c a-0 b-0 c-0 name))
  (defstrand resp 4 (k k) (n-a n-a) (n-b n-b) (b b) (a a) (c c))
  (defstrand serv 3 (k k) (n-a n-a-0) (n-b n-b-0) (c c) (a a) (b b))
  (defstrand init 3 (k k) (n-a n-a-1) (n-b n-b) (a a-0) (b b-0) (c c-0))
  (precedes ((0 1) (2 1)) ((1 2) (0 2)) ((1 2) (2 1)) ((2 2) (0 3)))
  (uniq-orig k n-b)
  (conf (cat c a) (cat c b))
  (auth (cat c b))
  (operation nonce-test (displaced 3 1 serv 3) k (2 1)
    (ch-msg (cat c a) (cat a b k n-a-0 n-b-0)))
  (strand-map 0 1 2)
  (traces
    ((recv (cat a n-a)) (send (cat b c) (cat a b n-a n-b))
      (recv (cat c b) (cat a b k)) (recv (enc n-b k)))
    ((recv (cat b c) (cat a b n-a-0 n-b-0))
      (send (cat c a) (cat a b k n-a-0 n-b-0))
      (send (cat c b) (cat a b k)))
    ((send (cat a-0 n-a-1))
      (recv (cat c-0 a-0) (cat a-0 b-0 k n-a-1 n-b))
      (send (enc n-b k))))
  (label 6)
  (parent 3)
  (unrealized (2 1))
  (maps
    ((0 1)
      ((k k) (n-b n-b) (n-a n-a) (n-a-0 n-a-0) (n-b-0 n-b-0) (a a) (b b)
        (c c))))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton yahalom
  (vars (k skey) (n-b n-a n-a-0 n-b-0 text) (a b c name))
  (defstrand resp 4 (k k) (n-a n-a) (n-b n-b) (b b) (a a) (c c))
  (defstrand serv 3 (k k) (n-a n-a-0) (n-b n-b-0) (c c) (a a) (b b))
  (deflistener k)
  (precedes ((1 2) (0 2)) ((1 2) (2 0)) ((2 1) (0 3)))
  (uniq-orig k n-b)
  (conf (cat c a) (cat c b))
  (auth (cat c b))
  (operation nonce-test (displaced 3 1 serv 3) k (2 0)
    (ch-msg (cat c a) (cat a b k n-a-0 n-b-0)))
  (strand-map 0 1 2)
  (traces
    ((recv (cat a n-a)) (send (cat b c) (cat a b n-a n-b))
      (recv (cat c b) (cat a b k)) (recv (enc n-b k)))
    ((recv (cat b c) (cat a b n-a-0 n-b-0))
      (send (cat c a) (cat a b k n-a-0 n-b-0))
      (send (cat c b) (cat a b k))) ((recv k) (send k)))
  (label 7)
  (parent 4)
  (unrealized (2 0))
  (dead)
  (maps
    ((0 1)
      ((k k) (n-b n-b) (n-a n-a) (n-a-0 n-a-0) (n-b-0 n-b-0) (a a) (b b)
        (c c))))
  (comment "empty cohort"))

(defskeleton yahalom
  (vars (k skey) (n-a n-a-0 n-b text) (a b c name))
  (defstrand resp 4 (k k) (n-a n-a) (n-b n-b) (b b) (a a) (c c))
  (defstrand serv 3 (k k) (n-a n-a-0) (n-b n-b) (c c) (a a) (b b))
  (defstrand init 3 (k k) (n-a n-a-0) (n-b n-b) (a a) (b b) (c c))
  (precedes ((0 1) (1 0)) ((1 2) (0 2)) ((1 2) (2 1)) ((2 2) (0 3)))
  (uniq-orig k n-b)
  (conf (cat c a) (cat c b))
  (auth (cat c b))
  (operation nonce-test
    (contracted (n-b-0 n-b) (a-0 a) (b-0 b) (c-0 c) (n-a-1 n-a-0)) k
    (2 1) (ch-msg (cat c a) (cat a b k n-a-0 n-b))
    (ch-msg (cat c b) (cat a b k)))
  (strand-map 0 1 2)
  (traces
    ((recv (cat a n-a)) (send (cat b c) (cat a b n-a n-b))
      (recv (cat c b) (cat a b k)) (recv (enc n-b k)))
    ((recv (cat b c) (cat a b n-a-0 n-b))
      (send (cat c a) (cat a b k n-a-0 n-b))
      (send (cat c b) (cat a b k)))
    ((send (cat a n-a-0)) (recv (cat c a) (cat a b k n-a-0 n-b))
      (send (enc n-b k))))
  (label 8)
  (parent 6)
  (seen 5)
  (seen-ops
    (5 (operation generalization weakened ((1 2) (2 1)))
      (strand-map 0 1 2)))
  (realized)
  (maps
    ((0 1)
      ((k k) (n-b n-b) (n-a n-a) (n-a-0 n-a-0) (n-b-0 n-b) (a a) (b b)
        (c c))))
  (comment "1 in cohort - 0 not yet seen"))

(comment "Nothing left to do")

(defprotocol yahalom basic
  (defrole init
    (vars (a b c name) (n-a n-b text) (k skey))
    (trace (send (cat a n-a)) (recv (cat c a) (cat a b k n-a n-b))
      (send (enc n-b k))))
  (defrole resp
    (vars (b a c name) (n-a n-b text) (k skey))
    (trace (recv (cat a n-a)) (send (cat b c) (cat a b n-a n-b))
      (recv (cat c b) (cat a b k)) (recv (enc n-b k))))
  (defrole serv
    (vars (c a b name) (n-a n-b text) (k skey))
    (trace (recv (cat b c) (cat a b n-a n-b))
      (send (cat c a) (cat a b k n-a n-b)) (send (cat c b) (cat a b k)))
    (uniq-orig k))
  (defgenrule neqRl_indx
    (forall ((x indx)) (implies (fact neq x x) (false))))
  (defgenrule neqRl_strd
    (forall ((x strd)) (implies (fact neq x x) (false))))
  (defgenrule neqRl_mesg
    (forall ((x mesg)) (implies (fact neq x x) (false))))
  (comment
    "Use (cat x y) as channel from x to y. Matching channel should force matching names."))

(defskeleton yahalom
  (vars (k skey) (n-b n-a n-a-0 n-b-0 text) (a b c name))
  (defstrand resp 4 (k k) (n-a n-a) (n-b n-b) (b b) (a a) (c c))
  (defstrand serv 3 (k k) (n-a n-a-0) (n-b n-b-0) (c c) (a a) (b b))
  (uniq-orig k n-b)
  (conf (cat c a) (cat c b))
  (auth (cat b c) (cat c b))
  (traces
    ((recv (cat a n-a)) (send (cat b c) (cat a b n-a n-b))
      (recv (cat c b) (cat a b k)) (recv (enc n-b k)))
    ((recv (cat b c) (cat a b n-a-0 n-b-0))
      (send (cat c a) (cat a b k n-a-0 n-b-0))
      (send (cat c b) (cat a b k))))
  (label 9)
  (unrealized (0 2) (0 3) (1 0))
  (preskeleton)
  (maps
    ((0 1)
      ((k k) (n-b n-b) (n-a n-a) (n-a-0 n-a-0) (n-b-0 n-b-0) (a a) (b b)
        (c c))))
  (origs (k (1 1)) (n-b (0 1)))
  (comment "Not a skeleton"))

(defskeleton yahalom
  (vars (k skey) (n-b n-a n-a-0 n-b-0 text) (a b c name))
  (defstrand resp 4 (k k) (n-a n-a) (n-b n-b) (b b) (a a) (c c))
  (defstrand serv 3 (k k) (n-a n-a-0) (n-b n-b-0) (c c) (a a) (b b))
  (precedes ((1 1) (0 2)))
  (uniq-orig k n-b)
  (conf (cat c a) (cat c b))
  (auth (cat b c) (cat c b))
  (traces
    ((recv (cat a n-a)) (send (cat b c) (cat a b n-a n-b))
      (recv (cat c b) (cat a b k)) (recv (enc n-b k)))
    ((recv (cat b c) (cat a b n-a-0 n-b-0))
      (send (cat c a) (cat a b k n-a-0 n-b-0))
      (send (cat c b) (cat a b k))))
  (label 10)
  (parent 9)
  (unrealized (0 2) (0 3) (1 0))
  (maps
    ((0 1)
      ((k k) (n-b n-b) (n-a n-a) (n-a-0 n-a-0) (n-b-0 n-b-0) (a a) (b b)
        (c c))))
  (origs (k (1 1)) (n-b (0 1)))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton yahalom
  (vars (k skey) (n-b n-a text) (a b c name))
  (defstrand resp 4 (k k) (n-a n-a) (n-b n-b) (b b) (a a) (c c))
  (defstrand serv 3 (k k) (n-a n-a) (n-b n-b) (c c) (a a) (b b))
  (precedes ((0 1) (1 0)) ((1 1) (0 2)))
  (uniq-orig k n-b)
  (conf (cat c a) (cat c b))
  (auth (cat b c) (cat c b))
  (operation channel-test (displaced 2 0 resp 2)
    (ch-msg (cat b c) (cat a b n-a-0 n-b-0)) (1 0))
  (strand-map 0 1)
  (traces
    ((recv (cat a n-a)) (send (cat b c) (cat a b n-a n-b))
      (recv (cat c b) (cat a b k)) (recv (enc n-b k)))
    ((recv (cat b c) (cat a b n-a n-b))
      (send (cat c a) (cat a b k n-a n-b))
      (send (cat c b) (cat a b k))))
  (label 11)
  (parent 10)
  (unrealized (0 2) (0 3))
  (maps
    ((0 1)
      ((k k) (n-b n-b) (n-a n-a) (n-a-0 n-a) (n-b-0 n-b) (a a) (b b)
        (c c))))
  (origs (k (1 1)) (n-b (0 1)))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton yahalom
  (vars (k skey) (n-b n-a n-a-0 n-b-0 text) (a b c name))
  (defstrand resp 4 (k k) (n-a n-a) (n-b n-b) (b b) (a a) (c c))
  (defstrand serv 3 (k k) (n-a n-a-0) (n-b n-b-0) (c c) (a a) (b b))
  (defstrand resp 2 (n-a n-a-0) (n-b n-b-0) (b b) (a a) (c c))
  (precedes ((1 1) (0 2)) ((2 1) (1 0)))
  (uniq-orig k n-b)
  (conf (cat c a) (cat c b))
  (auth (cat b c) (cat c b))
  (operation channel-test (added-strand resp 2)
    (ch-msg (cat b c) (cat a b n-a-0 n-b-0)) (1 0))
  (strand-map 0 1)
  (traces
    ((recv (cat a n-a)) (send (cat b c) (cat a b n-a n-b))
      (recv (cat c b) (cat a b k)) (recv (enc n-b k)))
    ((recv (cat b c) (cat a b n-a-0 n-b-0))
      (send (cat c a) (cat a b k n-a-0 n-b-0))
      (send (cat c b) (cat a b k)))
    ((recv (cat a n-a-0)) (send (cat b c) (cat a b n-a-0 n-b-0))))
  (label 12)
  (parent 10)
  (unrealized (0 2) (0 3))
  (maps
    ((0 1)
      ((k k) (n-b n-b) (n-a n-a) (n-a-0 n-a-0) (n-b-0 n-b-0) (a a) (b b)
        (c c))))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton yahalom
  (vars (k skey) (n-b n-a text) (a b c name))
  (defstrand resp 4 (k k) (n-a n-a) (n-b n-b) (b b) (a a) (c c))
  (defstrand serv 3 (k k) (n-a n-a) (n-b n-b) (c c) (a a) (b b))
  (precedes ((0 1) (1 0)) ((1 2) (0 2)))
  (uniq-orig k n-b)
  (conf (cat c a) (cat c b))
  (auth (cat b c) (cat c b))
  (operation channel-test (displaced 2 1 serv 3)
    (ch-msg (cat c b) (cat a b k)) (0 2))
  (strand-map 0 1)
  (traces
    ((recv (cat a n-a)) (send (cat b c) (cat a b n-a n-b))
      (recv (cat c b) (cat a b k)) (recv (enc n-b k)))
    ((recv (cat b c) (cat a b n-a n-b))
      (send (cat c a) (cat a b k n-a n-b))
      (send (cat c b) (cat a b k))))
  (label 13)
  (parent 11)
  (unrealized (0 3))
  (maps
    ((0 1)
      ((k k) (n-b n-b) (n-a n-a) (n-a-0 n-a) (n-b-0 n-b) (a a) (b b)
        (c c))))
  (origs (k (1 1)) (n-b (0 1)))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton yahalom
  (vars (k skey) (n-b n-a n-a-0 n-b-0 text) (a b c name))
  (defstrand resp 4 (k k) (n-a n-a) (n-b n-b) (b b) (a a) (c c))
  (defstrand serv 3 (k k) (n-a n-a-0) (n-b n-b-0) (c c) (a a) (b b))
  (defstrand resp 2 (n-a n-a-0) (n-b n-b-0) (b b) (a a) (c c))
  (precedes ((1 2) (0 2)) ((2 1) (1 0)))
  (uniq-orig k n-b)
  (conf (cat c a) (cat c b))
  (auth (cat b c) (cat c b))
  (operation channel-test (displaced 3 1 serv 3)
    (ch-msg (cat c b) (cat a b k)) (0 2))
  (strand-map 0 1 2)
  (traces
    ((recv (cat a n-a)) (send (cat b c) (cat a b n-a n-b))
      (recv (cat c b) (cat a b k)) (recv (enc n-b k)))
    ((recv (cat b c) (cat a b n-a-0 n-b-0))
      (send (cat c a) (cat a b k n-a-0 n-b-0))
      (send (cat c b) (cat a b k)))
    ((recv (cat a n-a-0)) (send (cat b c) (cat a b n-a-0 n-b-0))))
  (label 14)
  (parent 12)
  (unrealized (0 3))
  (maps
    ((0 1)
      ((k k) (n-b n-b) (n-a n-a) (n-a-0 n-a-0) (n-b-0 n-b-0) (a a) (b b)
        (c c))))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton yahalom
  (vars (k skey) (n-b n-a n-a-0 text) (a b c a-0 b-0 c-0 name))
  (defstrand resp 4 (k k) (n-a n-a) (n-b n-b) (b b) (a a) (c c))
  (defstrand serv 3 (k k) (n-a n-a) (n-b n-b) (c c) (a a) (b b))
  (defstrand init 3 (k k) (n-a n-a-0) (n-b n-b) (a a-0) (b b-0) (c c-0))
  (precedes ((0 1) (1 0)) ((1 1) (2 1)) ((1 2) (0 2)) ((2 2) (0 3)))
  (uniq-orig k n-b)
  (conf (cat c a) (cat c b))
  (auth (cat b c) (cat c b))
  (operation encryption-test (added-strand init 3) (enc n-b k) (0 3))
  (strand-map 0 1)
  (traces
    ((recv (cat a n-a)) (send (cat b c) (cat a b n-a n-b))
      (recv (cat c b) (cat a b k)) (recv (enc n-b k)))
    ((recv (cat b c) (cat a b n-a n-b))
      (send (cat c a) (cat a b k n-a n-b)) (send (cat c b) (cat a b k)))
    ((send (cat a-0 n-a-0))
      (recv (cat c-0 a-0) (cat a-0 b-0 k n-a-0 n-b))
      (send (enc n-b k))))
  (label 15)
  (parent 13)
  (unrealized (2 1))
  (maps
    ((0 1)
      ((k k) (n-b n-b) (n-a n-a) (n-a-0 n-a) (n-b-0 n-b) (a a) (b b)
        (c c))))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton yahalom
  (vars (k skey) (n-b n-a text) (a b c name))
  (defstrand resp 4 (k k) (n-a n-a) (n-b n-b) (b b) (a a) (c c))
  (defstrand serv 3 (k k) (n-a n-a) (n-b n-b) (c c) (a a) (b b))
  (deflistener k)
  (precedes ((0 1) (1 0)) ((1 1) (2 0)) ((1 2) (0 2)) ((2 1) (0 3)))
  (uniq-orig k n-b)
  (conf (cat c a) (cat c b))
  (auth (cat b c) (cat c b))
  (operation encryption-test (added-listener k) (enc n-b k) (0 3))
  (strand-map 0 1)
  (traces
    ((recv (cat a n-a)) (send (cat b c) (cat a b n-a n-b))
      (recv (cat c b) (cat a b k)) (recv (enc n-b k)))
    ((recv (cat b c) (cat a b n-a n-b))
      (send (cat c a) (cat a b k n-a n-b)) (send (cat c b) (cat a b k)))
    ((recv k) (send k)))
  (label 16)
  (parent 13)
  (unrealized (2 0))
  (maps
    ((0 1)
      ((k k) (n-b n-b) (n-a n-a) (n-a-0 n-a) (n-b-0 n-b) (a a) (b b)
        (c c))))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton yahalom
  (vars (k skey) (n-b n-a n-a-0 n-b-0 n-a-1 text)
    (a b c a-0 b-0 c-0 name))
  (defstrand resp 4 (k k) (n-a n-a) (n-b n-b) (b b) (a a) (c c))
  (defstrand serv 3 (k k) (n-a n-a-0) (n-b n-b-0) (c c) (a a) (b b))
  (defstrand resp 2 (n-a n-a-0) (n-b n-b-0) (b b) (a a) (c c))
  (defstrand init 3 (k k) (n-a n-a-1) (n-b n-b) (a a-0) (b b-0) (c c-0))
  (precedes ((0 1) (3 1)) ((1 1) (3 1)) ((1 2) (0 2)) ((2 1) (1 0))
    ((3 2) (0 3)))
  (uniq-orig k n-b)
  (conf (cat c a) (cat c b))
  (auth (cat b c) (cat c b))
  (operation encryption-test (added-strand init 3) (enc n-b k) (0 3))
  (strand-map 0 1 2)
  (traces
    ((recv (cat a n-a)) (send (cat b c) (cat a b n-a n-b))
      (recv (cat c b) (cat a b k)) (recv (enc n-b k)))
    ((recv (cat b c) (cat a b n-a-0 n-b-0))
      (send (cat c a) (cat a b k n-a-0 n-b-0))
      (send (cat c b) (cat a b k)))
    ((recv (cat a n-a-0)) (send (cat b c) (cat a b n-a-0 n-b-0)))
    ((send (cat a-0 n-a-1))
      (recv (cat c-0 a-0) (cat a-0 b-0 k n-a-1 n-b))
      (send (enc n-b k))))
  (label 17)
  (parent 14)
  (unrealized (3 1))
  (maps
    ((0 1)
      ((k k) (n-b n-b) (n-a n-a) (n-a-0 n-a-0) (n-b-0 n-b-0) (a a) (b b)
        (c c))))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton yahalom
  (vars (k skey) (n-b n-a n-a-0 n-b-0 text) (a b c name))
  (defstrand resp 4 (k k) (n-a n-a) (n-b n-b) (b b) (a a) (c c))
  (defstrand serv 3 (k k) (n-a n-a-0) (n-b n-b-0) (c c) (a a) (b b))
  (defstrand resp 2 (n-a n-a-0) (n-b n-b-0) (b b) (a a) (c c))
  (deflistener k)
  (precedes ((1 1) (3 0)) ((1 2) (0 2)) ((2 1) (1 0)) ((3 1) (0 3)))
  (uniq-orig k n-b)
  (conf (cat c a) (cat c b))
  (auth (cat b c) (cat c b))
  (operation encryption-test (added-listener k) (enc n-b k) (0 3))
  (strand-map 0 1 2)
  (traces
    ((recv (cat a n-a)) (send (cat b c) (cat a b n-a n-b))
      (recv (cat c b) (cat a b k)) (recv (enc n-b k)))
    ((recv (cat b c) (cat a b n-a-0 n-b-0))
      (send (cat c a) (cat a b k n-a-0 n-b-0))
      (send (cat c b) (cat a b k)))
    ((recv (cat a n-a-0)) (send (cat b c) (cat a b n-a-0 n-b-0)))
    ((recv k) (send k)))
  (label 18)
  (parent 14)
  (unrealized (3 0))
  (maps
    ((0 1)
      ((k k) (n-b n-b) (n-a n-a) (n-a-0 n-a-0) (n-b-0 n-b-0) (a a) (b b)
        (c c))))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton yahalom
  (vars (k skey) (n-b n-a text) (a b c name))
  (defstrand resp 4 (k k) (n-a n-a) (n-b n-b) (b b) (a a) (c c))
  (defstrand serv 3 (k k) (n-a n-a) (n-b n-b) (c c) (a a) (b b))
  (defstrand init 3 (k k) (n-a n-a) (n-b n-b) (a a) (b b) (c c))
  (precedes ((0 1) (1 0)) ((1 1) (2 1)) ((1 2) (0 2)) ((2 2) (0 3)))
  (uniq-orig k n-b)
  (conf (cat c a) (cat c b))
  (auth (cat b c) (cat c b))
  (operation nonce-test (contracted (a-0 a) (b-0 b) (c-0 c) (n-a-0 n-a))
    k (2 1) (ch-msg (cat c a) (cat a b k n-a n-b)))
  (strand-map 0 1 2)
  (traces
    ((recv (cat a n-a)) (send (cat b c) (cat a b n-a n-b))
      (recv (cat c b) (cat a b k)) (recv (enc n-b k)))
    ((recv (cat b c) (cat a b n-a n-b))
      (send (cat c a) (cat a b k n-a n-b)) (send (cat c b) (cat a b k)))
    ((send (cat a n-a)) (recv (cat c a) (cat a b k n-a n-b))
      (send (enc n-b k))))
  (label 19)
  (parent 15)
  (realized)
  (shape)
  (maps
    ((0 1)
      ((k k) (n-b n-b) (n-a n-a) (n-a-0 n-a) (n-b-0 n-b) (a a) (b b)
        (c c))))
  (origs (k (1 1)) (n-b (0 1))))

(defskeleton yahalom
  (vars (k skey) (n-b n-a n-a-0 text) (a b c a-0 b-0 c-0 name))
  (defstrand resp 4 (k k) (n-a n-a) (n-b n-b) (b b) (a a) (c c))
  (defstrand serv 3 (k k) (n-a n-a) (n-b n-b) (c c) (a a) (b b))
  (defstrand init 3 (k k) (n-a n-a-0) (n-b n-b) (a a-0) (b b-0) (c c-0))
  (precedes ((0 1) (1 0)) ((1 2) (0 2)) ((1 2) (2 1)) ((2 2) (0 3)))
  (uniq-orig k n-b)
  (conf (cat c a) (cat c b))
  (auth (cat b c) (cat c b))
  (operation nonce-test (displaced 3 1 serv 3) k (2 1)
    (ch-msg (cat c a) (cat a b k n-a n-b)))
  (strand-map 0 1 2)
  (traces
    ((recv (cat a n-a)) (send (cat b c) (cat a b n-a n-b))
      (recv (cat c b) (cat a b k)) (recv (enc n-b k)))
    ((recv (cat b c) (cat a b n-a n-b))
      (send (cat c a) (cat a b k n-a n-b)) (send (cat c b) (cat a b k)))
    ((send (cat a-0 n-a-0))
      (recv (cat c-0 a-0) (cat a-0 b-0 k n-a-0 n-b))
      (send (enc n-b k))))
  (label 20)
  (parent 15)
  (unrealized (2 1))
  (maps
    ((0 1)
      ((k k) (n-b n-b) (n-a n-a) (n-a-0 n-a) (n-b-0 n-b) (a a) (b b)
        (c c))))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton yahalom
  (vars (k skey) (n-b n-a text) (a b c name))
  (defstrand resp 4 (k k) (n-a n-a) (n-b n-b) (b b) (a a) (c c))
  (defstrand serv 3 (k k) (n-a n-a) (n-b n-b) (c c) (a a) (b b))
  (deflistener k)
  (precedes ((0 1) (1 0)) ((1 2) (0 2)) ((1 2) (2 0)) ((2 1) (0 3)))
  (uniq-orig k n-b)
  (conf (cat c a) (cat c b))
  (auth (cat b c) (cat c b))
  (operation nonce-test (displaced 3 1 serv 3) k (2 0)
    (ch-msg (cat c a) (cat a b k n-a n-b)))
  (strand-map 0 1 2)
  (traces
    ((recv (cat a n-a)) (send (cat b c) (cat a b n-a n-b))
      (recv (cat c b) (cat a b k)) (recv (enc n-b k)))
    ((recv (cat b c) (cat a b n-a n-b))
      (send (cat c a) (cat a b k n-a n-b)) (send (cat c b) (cat a b k)))
    ((recv k) (send k)))
  (label 21)
  (parent 16)
  (unrealized (2 0))
  (dead)
  (maps
    ((0 1)
      ((k k) (n-b n-b) (n-a n-a) (n-a-0 n-a) (n-b-0 n-b) (a a) (b b)
        (c c))))
  (comment "empty cohort"))

(defskeleton yahalom
  (vars (k skey) (n-b n-a n-a-0 n-b-0 n-a-1 text)
    (a b c a-0 b-0 c-0 name))
  (defstrand resp 4 (k k) (n-a n-a) (n-b n-b) (b b) (a a) (c c))
  (defstrand serv 3 (k k) (n-a n-a-0) (n-b n-b-0) (c c) (a a) (b b))
  (defstrand resp 2 (n-a n-a-0) (n-b n-b-0) (b b) (a a) (c c))
  (defstrand init 3 (k k) (n-a n-a-1) (n-b n-b) (a a-0) (b b-0) (c c-0))
  (precedes ((0 1) (3 1)) ((1 2) (0 2)) ((1 2) (3 1)) ((2 1) (1 0))
    ((3 2) (0 3)))
  (uniq-orig k n-b)
  (conf (cat c a) (cat c b))
  (auth (cat b c) (cat c b))
  (operation nonce-test (displaced 4 1 serv 3) k (3 1)
    (ch-msg (cat c a) (cat a b k n-a-0 n-b-0)))
  (strand-map 0 1 2 3)
  (traces
    ((recv (cat a n-a)) (send (cat b c) (cat a b n-a n-b))
      (recv (cat c b) (cat a b k)) (recv (enc n-b k)))
    ((recv (cat b c) (cat a b n-a-0 n-b-0))
      (send (cat c a) (cat a b k n-a-0 n-b-0))
      (send (cat c b) (cat a b k)))
    ((recv (cat a n-a-0)) (send (cat b c) (cat a b n-a-0 n-b-0)))
    ((send (cat a-0 n-a-1))
      (recv (cat c-0 a-0) (cat a-0 b-0 k n-a-1 n-b))
      (send (enc n-b k))))
  (label 22)
  (parent 17)
  (unrealized (3 1))
  (dead)
  (maps
    ((0 1)
      ((k k) (n-b n-b) (n-a n-a) (n-a-0 n-a-0) (n-b-0 n-b-0) (a a) (b b)
        (c c))))
  (comment "empty cohort"))

(defskeleton yahalom
  (vars (k skey) (n-b n-a n-a-0 n-b-0 text) (a b c name))
  (defstrand resp 4 (k k) (n-a n-a) (n-b n-b) (b b) (a a) (c c))
  (defstrand serv 3 (k k) (n-a n-a-0) (n-b n-b-0) (c c) (a a) (b b))
  (defstrand resp 2 (n-a n-a-0) (n-b n-b-0) (b b) (a a) (c c))
  (deflistener k)
  (precedes ((1 2) (0 2)) ((1 2) (3 0)) ((2 1) (1 0)) ((3 1) (0 3)))
  (uniq-orig k n-b)
  (conf (cat c a) (cat c b))
  (auth (cat b c) (cat c b))
  (operation nonce-test (displaced 4 1 serv 3) k (3 0)
    (ch-msg (cat c a) (cat a b k n-a-0 n-b-0)))
  (strand-map 0 1 2 3)
  (traces
    ((recv (cat a n-a)) (send (cat b c) (cat a b n-a n-b))
      (recv (cat c b) (cat a b k)) (recv (enc n-b k)))
    ((recv (cat b c) (cat a b n-a-0 n-b-0))
      (send (cat c a) (cat a b k n-a-0 n-b-0))
      (send (cat c b) (cat a b k)))
    ((recv (cat a n-a-0)) (send (cat b c) (cat a b n-a-0 n-b-0)))
    ((recv k) (send k)))
  (label 23)
  (parent 18)
  (unrealized (3 0))
  (dead)
  (maps
    ((0 1)
      ((k k) (n-b n-b) (n-a n-a) (n-a-0 n-a-0) (n-b-0 n-b-0) (a a) (b b)
        (c c))))
  (comment "empty cohort"))

(defskeleton yahalom
  (vars (k skey) (n-b n-a text) (a b c name))
  (defstrand resp 4 (k k) (n-a n-a) (n-b n-b) (b b) (a a) (c c))
  (defstrand serv 3 (k k) (n-a n-a) (n-b n-b) (c c) (a a) (b b))
  (defstrand init 3 (k k) (n-a n-a) (n-b n-b) (a a) (b b) (c c))
  (precedes ((0 1) (1 0)) ((1 2) (0 2)) ((1 2) (2 1)) ((2 2) (0 3)))
  (uniq-orig k n-b)
  (conf (cat c a) (cat c b))
  (auth (cat b c) (cat c b))
  (operation nonce-test (contracted (a-0 a) (b-0 b) (c-0 c) (n-a-0 n-a))
    k (2 1) (ch-msg (cat c a) (cat a b k n-a n-b))
    (ch-msg (cat c b) (cat a b k)))
  (strand-map 0 1 2)
  (traces
    ((recv (cat a n-a)) (send (cat b c) (cat a b n-a n-b))
      (recv (cat c b) (cat a b k)) (recv (enc n-b k)))
    ((recv (cat b c) (cat a b n-a n-b))
      (send (cat c a) (cat a b k n-a n-b)) (send (cat c b) (cat a b k)))
    ((send (cat a n-a)) (recv (cat c a) (cat a b k n-a n-b))
      (send (enc n-b k))))
  (label 24)
  (parent 20)
  (seen 19)
  (seen-ops
    (19 (operation generalization weakened ((1 2) (2 1)))
      (strand-map 0 1 2)))
  (realized)
  (maps
    ((0 1)
      ((k k) (n-b n-b) (n-a n-a) (n-a-0 n-a) (n-b-0 n-b) (a a) (b b)
        (c c))))
  (comment "1 in cohort - 0 not yet seen"))

(comment "Nothing left to do")

(defprotocol yahalom basic
  (defrole init
    (vars (a b c name) (n-a n-b text) (k skey))
    (trace (send (cat a n-a)) (recv (cat c a) (cat a b k n-a n-b))
      (send (enc n-b k))))
  (defrole resp
    (vars (b a c name) (n-a n-b text) (k skey))
    (trace (recv (cat a n-a)) (send (cat b c) (cat a b n-a n-b))
      (recv (cat c b) (cat a b k)) (recv (enc n-b k))))
  (defrole serv
    (vars (c a b name) (n-a n-b text) (k skey))
    (trace (recv (cat b c) (cat a b n-a n-b))
      (send (cat c a) (cat a b k n-a n-b)) (send (cat c b) (cat a b k)))
    (uniq-orig k))
  (defgenrule neqRl_indx
    (forall ((x indx)) (implies (fact neq x x) (false))))
  (defgenrule neqRl_strd
    (forall ((x strd)) (implies (fact neq x x) (false))))
  (defgenrule neqRl_mesg
    (forall ((x mesg)) (implies (fact neq x x) (false))))
  (comment
    "Use (cat x y) as channel from x to y. Matching channel should force matching names."))

(defskeleton yahalom
  (vars (k skey) (n-b n-a n-a-0 n-b-0 text) (a b c name))
  (defstrand resp 4 (k k) (n-a n-a) (n-b n-b) (b b) (a a) (c c))
  (defstrand serv 3 (k k) (n-a n-a-0) (n-b n-b-0) (c c) (a a) (b b))
  (deflistener k)
  (uniq-orig k n-b)
  (conf (cat c a) (cat c b))
  (auth (cat b c) (cat c b))
  (traces
    ((recv (cat a n-a)) (send (cat b c) (cat a b n-a n-b))
      (recv (cat c b) (cat a b k)) (recv (enc n-b k)))
    ((recv (cat b c) (cat a b n-a-0 n-b-0))
      (send (cat c a) (cat a b k n-a-0 n-b-0))
      (send (cat c b) (cat a b k))) ((recv k) (send k)))
  (label 25)
  (unrealized (0 2) (0 3) (1 0) (2 0))
  (preskeleton)
  (maps
    ((0 1 2)
      ((k k) (n-b n-b) (n-a n-a) (n-a-0 n-a-0) (n-b-0 n-b-0) (a a) (b b)
        (c c))))
  (origs (k (1 1)) (n-b (0 1)))
  (comment "Not a skeleton"))

(defskeleton yahalom
  (vars (k skey) (n-b n-a n-a-0 n-b-0 text) (a b c name))
  (defstrand resp 4 (k k) (n-a n-a) (n-b n-b) (b b) (a a) (c c))
  (defstrand serv 3 (k k) (n-a n-a-0) (n-b n-b-0) (c c) (a a) (b b))
  (deflistener k)
  (precedes ((1 1) (0 2)) ((1 1) (2 0)))
  (uniq-orig k n-b)
  (conf (cat c a) (cat c b))
  (auth (cat b c) (cat c b))
  (traces
    ((recv (cat a n-a)) (send (cat b c) (cat a b n-a n-b))
      (recv (cat c b) (cat a b k)) (recv (enc n-b k)))
    ((recv (cat b c) (cat a b n-a-0 n-b-0))
      (send (cat c a) (cat a b k n-a-0 n-b-0))
      (send (cat c b) (cat a b k))) ((recv k) (send k)))
  (label 26)
  (parent 25)
  (unrealized (0 2) (0 3) (1 0) (2 0))
  (maps
    ((0 1 2)
      ((k k) (n-b n-b) (n-a n-a) (n-a-0 n-a-0) (n-b-0 n-b-0) (a a) (b b)
        (c c))))
  (origs (k (1 1)) (n-b (0 1)))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton yahalom
  (vars (k skey) (n-b n-a n-a-0 n-b-0 text) (a b c name))
  (defstrand resp 4 (k k) (n-a n-a) (n-b n-b) (b b) (a a) (c c))
  (defstrand serv 3 (k k) (n-a n-a-0) (n-b n-b-0) (c c) (a a) (b b))
  (deflistener k)
  (precedes ((1 1) (0 2)) ((1 2) (2 0)))
  (uniq-orig k n-b)
  (conf (cat c a) (cat c b))
  (auth (cat b c) (cat c b))
  (operation nonce-test (displaced 3 1 serv 3) k (2 0)
    (ch-msg (cat c a) (cat a b k n-a-0 n-b-0)))
  (strand-map 0 1 2)
  (traces
    ((recv (cat a n-a)) (send (cat b c) (cat a b n-a n-b))
      (recv (cat c b) (cat a b k)) (recv (enc n-b k)))
    ((recv (cat b c) (cat a b n-a-0 n-b-0))
      (send (cat c a) (cat a b k n-a-0 n-b-0))
      (send (cat c b) (cat a b k))) ((recv k) (send k)))
  (label 27)
  (parent 26)
  (unrealized (0 2) (0 3) (1 0) (2 0))
  (dead)
  (maps
    ((0 1 2)
      ((k k) (n-b n-b) (n-a n-a) (n-a-0 n-a-0) (n-b-0 n-b-0) (a a) (b b)
        (c c))))
  (origs (k (1 1)) (n-b (0 1)))
  (comment "empty cohort"))

(comment "Nothing left to do")

(defprotocol yahalom basic
  (defrole init
    (vars (a b c name) (n-a n-b text) (k skey))
    (trace (send (cat a n-a)) (recv (cat c a) (cat a b k n-a n-b))
      (send (enc n-b k))))
  (defrole resp
    (vars (b a c name) (n-a n-b text) (k skey))
    (trace (recv (cat a n-a)) (send (cat b c) (cat a b n-a n-b))
      (recv (cat c b) (cat a b k)) (recv (enc n-b k))))
  (defrole serv
    (vars (c a b name) (n-a n-b text) (k skey))
    (trace (recv (cat b c) (cat a b n-a n-b))
      (send (cat c a) (cat a b k n-a n-b)) (send (cat c b) (cat a b k)))
    (uniq-orig k))
  (defgenrule neqRl_indx
    (forall ((x indx)) (implies (fact neq x x) (false))))
  (defgenrule neqRl_strd
    (forall ((x strd)) (implies (fact neq x x) (false))))
  (defgenrule neqRl_mesg
    (forall ((x mesg)) (implies (fact neq x x) (false))))
  (comment
    "Use (cat x y) as channel from x to y. Matching channel should force matching names."))

(defskeleton yahalom
  (vars (k skey) (n-a n-b text) (a c b name))
  (defstrand init 3 (k k) (n-a n-a) (n-b n-b) (a a) (b b) (c c))
  (uniq-orig n-a)
  (auth (cat c a))
  (traces
    ((send (cat a n-a)) (recv (cat c a) (cat a b k n-a n-b))
      (send (enc n-b k))))
  (label 28)
  (unrealized (0 1))
  (maps ((0) ((a a) (c c) (n-a n-a) (b b) (n-b n-b) (k k))))
  (origs (n-a (0 0)))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton yahalom
  (vars (k skey) (n-a n-b text) (a c b name))
  (defstrand init 3 (k k) (n-a n-a) (n-b n-b) (a a) (b b) (c c))
  (defstrand serv 2 (k k) (n-a n-a) (n-b n-b) (c c) (a a) (b b))
  (precedes ((0 0) (1 0)) ((1 1) (0 1)))
  (uniq-orig k n-a)
  (auth (cat c a))
  (operation channel-test (added-strand serv 2)
    (ch-msg (cat c a) (cat a b k n-a n-b)) (0 1))
  (strand-map 0)
  (traces
    ((send (cat a n-a)) (recv (cat c a) (cat a b k n-a n-b))
      (send (enc n-b k)))
    ((recv (cat b c) (cat a b n-a n-b))
      (send (cat c a) (cat a b k n-a n-b))))
  (label 29)
  (parent 28)
  (realized)
  (shape)
  (maps ((0) ((a a) (c c) (n-a n-a) (b b) (n-b n-b) (k k))))
  (origs (k (1 1)) (n-a (0 0))))

(comment "Nothing left to do")

(defprotocol yahalom basic
  (defrole init
    (vars (a b c name) (n-a n-b text) (k skey))
    (trace (send (cat a n-a)) (recv (cat c a) (cat a b k n-a n-b))
      (send (enc n-b k))))
  (defrole resp
    (vars (b a c name) (n-a n-b text) (k skey))
    (trace (recv (cat a n-a)) (send (cat b c) (cat a b n-a n-b))
      (recv (cat c b) (cat a b k)) (recv (enc n-b k))))
  (defrole serv
    (vars (c a b name) (n-a n-b text) (k skey))
    (trace (recv (cat b c) (cat a b n-a n-b))
      (send (cat c a) (cat a b k n-a n-b)) (send (cat c b) (cat a b k)))
    (uniq-orig k))
  (defgenrule neqRl_indx
    (forall ((x indx)) (implies (fact neq x x) (false))))
  (defgenrule neqRl_strd
    (forall ((x strd)) (implies (fact neq x x) (false))))
  (defgenrule neqRl_mesg
    (forall ((x mesg)) (implies (fact neq x x) (false))))
  (comment
    "Use (cat x y) as channel from x to y. Matching channel should force matching names."))

(defskeleton yahalom
  (vars (k skey) (n-a n-b text) (a c b c-0 name))
  (defstrand init 3 (k k) (n-a n-a) (n-b n-b) (a a) (b b) (c c))
  (defstrand serv 2 (k k) (n-a n-a) (n-b n-b) (c c-0) (a a) (b b))
  (precedes ((0 0) (1 0)) ((1 1) (0 1)))
  (uniq-orig k n-a)
  (conf (cat c-0 a))
  (auth (cat c a) (cat b c-0))
  (traces
    ((send (cat a n-a)) (recv (cat c a) (cat a b k n-a n-b))
      (send (enc n-b k)))
    ((recv (cat b c-0) (cat a b n-a n-b))
      (send (cat c-0 a) (cat a b k n-a n-b))))
  (label 30)
  (unrealized (0 1) (1 0))
  (maps ((0 1) ((k k) (n-a n-a) (n-b n-b) (a a) (c c) (b b) (c-0 c-0))))
  (origs (k (1 1)) (n-a (0 0)))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton yahalom
  (vars (k skey) (n-a n-b text) (a c b c-0 name))
  (defstrand init 3 (k k) (n-a n-a) (n-b n-b) (a a) (b b) (c c))
  (defstrand serv 2 (k k) (n-a n-a) (n-b n-b) (c c-0) (a a) (b b))
  (defstrand resp 2 (n-a n-a) (n-b n-b) (b b) (a a) (c c-0))
  (precedes ((0 0) (2 0)) ((1 1) (0 1)) ((2 1) (1 0)))
  (uniq-orig k n-a)
  (conf (cat c-0 a))
  (auth (cat c a) (cat b c-0))
  (operation channel-test (added-strand resp 2)
    (ch-msg (cat b c-0) (cat a b n-a n-b)) (1 0))
  (strand-map 0 1)
  (traces
    ((send (cat a n-a)) (recv (cat c a) (cat a b k n-a n-b))
      (send (enc n-b k)))
    ((recv (cat b c-0) (cat a b n-a n-b))
      (send (cat c-0 a) (cat a b k n-a n-b)))
    ((recv (cat a n-a)) (send (cat b c-0) (cat a b n-a n-b))))
  (label 31)
  (parent 30)
  (unrealized (0 1))
  (maps ((0 1) ((k k) (n-a n-a) (n-b n-b) (a a) (c c) (b b) (c-0 c-0))))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton yahalom
  (vars (k skey) (n-a n-b text) (a b c name))
  (defstrand init 3 (k k) (n-a n-a) (n-b n-b) (a a) (b b) (c c))
  (defstrand serv 2 (k k) (n-a n-a) (n-b n-b) (c c) (a a) (b b))
  (defstrand resp 2 (n-a n-a) (n-b n-b) (b b) (a a) (c c))
  (precedes ((0 0) (2 0)) ((1 1) (0 1)) ((2 1) (1 0)))
  (uniq-orig k n-a)
  (conf (cat c a))
  (auth (cat b c) (cat c a))
  (operation channel-test (displaced 3 1 serv 2)
    (ch-msg (cat c-0 a) (cat a b k n-a n-b)) (0 1))
  (strand-map 0 1 2)
  (traces
    ((send (cat a n-a)) (recv (cat c a) (cat a b k n-a n-b))
      (send (enc n-b k)))
    ((recv (cat b c) (cat a b n-a n-b))
      (send (cat c a) (cat a b k n-a n-b)))
    ((recv (cat a n-a)) (send (cat b c) (cat a b n-a n-b))))
  (label 32)
  (parent 31)
  (realized)
  (shape)
  (maps ((0 1) ((k k) (n-a n-a) (n-b n-b) (a a) (c c) (b b) (c-0 c))))
  (origs (k (1 1)) (n-a (0 0))))

(comment "Nothing left to do")

(defprotocol yahalom basic
  (defrole init
    (vars (a b c name) (n-a n-b text) (k skey))
    (trace (send (cat a n-a)) (recv (cat c a) (cat a b k n-a n-b))
      (send (enc n-b k))))
  (defrole resp
    (vars (b a c name) (n-a n-b text) (k skey))
    (trace (recv (cat a n-a)) (send (cat b c) (cat a b n-a n-b))
      (recv (cat c b) (cat a b k)) (recv (enc n-b k))))
  (defrole serv
    (vars (c a b name) (n-a n-b text) (k skey))
    (trace (recv (cat b c) (cat a b n-a n-b))
      (send (cat c a) (cat a b k n-a n-b)) (send (cat c b) (cat a b k)))
    (uniq-orig k))
  (defgenrule neqRl_indx
    (forall ((x indx)) (implies (fact neq x x) (false))))
  (defgenrule neqRl_strd
    (forall ((x strd)) (implies (fact neq x x) (false))))
  (defgenrule neqRl_mesg
    (forall ((x mesg)) (implies (fact neq x x) (false))))
  (comment
    "Use (cat x y) as channel from x to y. Matching channel should force matching names."))

(defskeleton yahalom
  (vars (k skey) (n-a n-b text) (c a b name))
  (defstrand serv 3 (k k) (n-a n-a) (n-b n-b) (c c) (a a) (b b))
  (uniq-orig k)
  (conf (cat c a) (cat c b))
  (auth (cat b c))
  (traces
    ((recv (cat b c) (cat a b n-a n-b))
      (send (cat c a) (cat a b k n-a n-b))
      (send (cat c b) (cat a b k))))
  (label 33)
  (unrealized (0 0))
  (maps ((0) ((c c) (a a) (b b) (n-a n-a) (n-b n-b) (k k))))
  (origs (k (0 1)))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton yahalom
  (vars (k skey) (n-a n-b text) (c a b name))
  (defstrand serv 3 (k k) (n-a n-a) (n-b n-b) (c c) (a a) (b b))
  (defstrand resp 2 (n-a n-a) (n-b n-b) (b b) (a a) (c c))
  (precedes ((1 1) (0 0)))
  (uniq-orig k)
  (conf (cat c a) (cat c b))
  (auth (cat b c))
  (operation channel-test (added-strand resp 2)
    (ch-msg (cat b c) (cat a b n-a n-b)) (0 0))
  (strand-map 0)
  (traces
    ((recv (cat b c) (cat a b n-a n-b))
      (send (cat c a) (cat a b k n-a n-b)) (send (cat c b) (cat a b k)))
    ((recv (cat a n-a)) (send (cat b c) (cat a b n-a n-b))))
  (label 34)
  (parent 33)
  (realized)
  (shape)
  (maps ((0) ((c c) (a a) (b b) (n-a n-a) (n-b n-b) (k k))))
  (origs (k (0 1))))

(comment "Nothing left to do")

(defprotocol yahalom basic
  (defrole init
    (vars (a b c name) (n-a n-b text) (k skey))
    (trace (send (cat a n-a)) (recv (cat c a) (cat a b k n-a n-b))
      (send (enc n-b k))))
  (defrole resp
    (vars (b a c name) (n-a n-b text) (k skey))
    (trace (recv (cat a n-a)) (send (cat b c) (cat a b n-a n-b))
      (recv (cat c b) (cat a b k)) (recv (enc n-b k))))
  (defrole serv
    (vars (c a b name) (n-a n-b text) (k skey))
    (trace (recv (cat b c) (cat a b n-a n-b))
      (send (cat c a) (cat a b k n-a n-b)) (send (cat c b) (cat a b k)))
    (uniq-orig k))
  (defgenrule neqRl_indx
    (forall ((x indx)) (implies (fact neq x x) (false))))
  (defgenrule neqRl_strd
    (forall ((x strd)) (implies (fact neq x x) (false))))
  (defgenrule neqRl_mesg
    (forall ((x mesg)) (implies (fact neq x x) (false))))
  (comment
    "Use (cat x y) as channel from x to y. Matching channel should force matching names."))

(defskeleton yahalom
  (vars (k skey) (n-a n-b text) (c a b name))
  (defstrand serv 3 (k k) (n-a n-a) (n-b n-b) (c c) (a a) (b b))
  (deflistener k)
  (uniq-orig k)
  (conf (cat c a) (cat c b))
  (auth (cat b c))
  (traces
    ((recv (cat b c) (cat a b n-a n-b))
      (send (cat c a) (cat a b k n-a n-b)) (send (cat c b) (cat a b k)))
    ((recv k) (send k)))
  (label 35)
  (unrealized (0 0) (1 0))
  (preskeleton)
  (maps ((0 1) ((c c) (a a) (b b) (k k) (n-a n-a) (n-b n-b))))
  (origs (k (0 1)))
  (comment "Not a skeleton"))

(defskeleton yahalom
  (vars (k skey) (n-a n-b text) (c a b name))
  (defstrand serv 3 (k k) (n-a n-a) (n-b n-b) (c c) (a a) (b b))
  (deflistener k)
  (precedes ((0 1) (1 0)))
  (uniq-orig k)
  (conf (cat c a) (cat c b))
  (auth (cat b c))
  (traces
    ((recv (cat b c) (cat a b n-a n-b))
      (send (cat c a) (cat a b k n-a n-b)) (send (cat c b) (cat a b k)))
    ((recv k) (send k)))
  (label 36)
  (parent 35)
  (unrealized (0 0) (1 0))
  (maps ((0 1) ((c c) (a a) (b b) (k k) (n-a n-a) (n-b n-b))))
  (origs (k (0 1)))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton yahalom
  (vars (k skey) (n-a n-b text) (c a b name))
  (defstrand serv 3 (k k) (n-a n-a) (n-b n-b) (c c) (a a) (b b))
  (deflistener k)
  (precedes ((0 2) (1 0)))
  (uniq-orig k)
  (conf (cat c a) (cat c b))
  (auth (cat b c))
  (operation nonce-test (displaced 2 0 serv 3) k (1 0)
    (ch-msg (cat c a) (cat a b k n-a n-b)))
  (strand-map 0 1)
  (traces
    ((recv (cat b c) (cat a b n-a n-b))
      (send (cat c a) (cat a b k n-a n-b)) (send (cat c b) (cat a b k)))
    ((recv k) (send k)))
  (label 37)
  (parent 36)
  (unrealized (0 0) (1 0))
  (dead)
  (maps ((0 1) ((c c) (a a) (b b) (k k) (n-a n-a) (n-b n-b))))
  (origs (k (0 1)))
  (comment "empty cohort"))

(comment "Nothing left to do")