cpsa-4.4.7: tst/chan-yahalom.tst
(herald "Yahalom Protocol Without Forwarding" (bound 15))
(comment "CPSA 4.4.7")
(comment "All input read from tst/chan-yahalom.scm")
(comment "Strand count bounded at 15")
(defprotocol yahalom basic
(defrole init
(vars (a b name) (n-a n-b text) (k skey) (ch3 chan))
(trace (send (cat a n-a)) (recv ch3 (cat a b k n-a n-b))
(send (enc n-b k))))
(defrole resp
(vars (b a name) (n-a n-b text) (k skey) (ch1 ch2 chan))
(trace (recv (cat a n-a)) (send ch1 (cat a b n-a n-b))
(recv ch2 (cat a b k)) (recv (enc n-b k))))
(defrole serv
(vars (a b name) (n-a n-b text) (k skey) (ch1 ch2 ch3 chan))
(trace (recv ch1 (cat a b n-a n-b)) (send ch3 (cat a b k n-a n-b))
(send ch2 (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)))))
(defskeleton yahalom
(vars (k skey) (n-b n-a text) (a b name) (ch1 ch2 chan))
(defstrand resp 4 (k k) (n-a n-a) (n-b n-b) (b b) (a a) (ch1 ch1)
(ch2 ch2))
(uniq-orig n-b)
(auth ch2)
(traces
((recv (cat a n-a)) (send ch1 (cat a b n-a n-b))
(recv ch2 (cat a b k)) (recv (enc n-b k))))
(label 0)
(unrealized (0 2))
(maps
((0) ((a a) (b b) (n-b n-b) (ch1 ch1) (ch2 ch2) (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 name)
(ch1 ch2 ch1-0 ch3 chan))
(defstrand resp 4 (k k) (n-a n-a) (n-b n-b) (b b) (a a) (ch1 ch1)
(ch2 ch2))
(defstrand serv 3 (k k) (n-a n-a-0) (n-b n-b-0) (a a) (b b)
(ch1 ch1-0) (ch2 ch2) (ch3 ch3))
(precedes ((1 2) (0 2)))
(uniq-orig k n-b)
(auth ch2)
(operation channel-test (added-strand serv 3) (ch-msg ch2 (cat a b k))
(0 2))
(strand-map 0)
(traces
((recv (cat a n-a)) (send ch1 (cat a b n-a n-b))
(recv ch2 (cat a b k)) (recv (enc n-b k)))
((recv ch1-0 (cat a b n-a-0 n-b-0))
(send ch3 (cat a b k n-a-0 n-b-0)) (send ch2 (cat a b k))))
(label 1)
(parent 0)
(realized)
(shape)
(maps
((0) ((a a) (b b) (n-b n-b) (ch1 ch1) (ch2 ch2) (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 name) (n-a n-b text) (k skey) (ch3 chan))
(trace (send (cat a n-a)) (recv ch3 (cat a b k n-a n-b))
(send (enc n-b k))))
(defrole resp
(vars (b a name) (n-a n-b text) (k skey) (ch1 ch2 chan))
(trace (recv (cat a n-a)) (send ch1 (cat a b n-a n-b))
(recv ch2 (cat a b k)) (recv (enc n-b k))))
(defrole serv
(vars (a b name) (n-a n-b text) (k skey) (ch1 ch2 ch3 chan))
(trace (recv ch1 (cat a b n-a n-b)) (send ch3 (cat a b k n-a n-b))
(send ch2 (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)))))
(defskeleton yahalom
(vars (k skey) (n-b n-a n-a-0 n-b-0 text) (a b name)
(ch1 ch2 ch1-0 ch3 chan))
(defstrand resp 4 (k k) (n-a n-a) (n-b n-b) (b b) (a a) (ch1 ch1)
(ch2 ch2))
(defstrand serv 3 (k k) (n-a n-a-0) (n-b n-b-0) (a a) (b b)
(ch1 ch1-0) (ch2 ch2) (ch3 ch3))
(precedes ((1 2) (0 2)))
(uniq-orig k n-b)
(conf ch2 ch3)
(auth ch2)
(traces
((recv (cat a n-a)) (send ch1 (cat a b n-a n-b))
(recv ch2 (cat a b k)) (recv (enc n-b k)))
((recv ch1-0 (cat a b n-a-0 n-b-0))
(send ch3 (cat a b k n-a-0 n-b-0)) (send ch2 (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)
(ch1 ch1) (ch2 ch2) (ch1-0 ch1-0) (ch3 ch3))))
(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 a-0 b-0 name)
(ch1 ch2 ch1-0 ch3 ch3-0 chan))
(defstrand resp 4 (k k) (n-a n-a) (n-b n-b) (b b) (a a) (ch1 ch1)
(ch2 ch2))
(defstrand serv 3 (k k) (n-a n-a-0) (n-b n-b-0) (a a) (b b)
(ch1 ch1-0) (ch2 ch2) (ch3 ch3))
(defstrand init 3 (k k) (n-a n-a-1) (n-b n-b) (a a-0) (b b-0)
(ch3 ch3-0))
(precedes ((0 1) (2 1)) ((1 1) (2 1)) ((1 2) (0 2)) ((2 2) (0 3)))
(uniq-orig k n-b)
(conf ch2 ch3)
(auth ch2)
(operation encryption-test (added-strand init 3) (enc n-b k) (0 3))
(strand-map 0 1)
(traces
((recv (cat a n-a)) (send ch1 (cat a b n-a n-b))
(recv ch2 (cat a b k)) (recv (enc n-b k)))
((recv ch1-0 (cat a b n-a-0 n-b-0))
(send ch3 (cat a b k n-a-0 n-b-0)) (send ch2 (cat a b k)))
((send (cat a-0 n-a-1)) (recv ch3-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)
(ch1 ch1) (ch2 ch2) (ch1-0 ch1-0) (ch3 ch3))))
(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 name)
(ch1 ch2 ch1-0 ch3 chan))
(defstrand resp 4 (k k) (n-a n-a) (n-b n-b) (b b) (a a) (ch1 ch1)
(ch2 ch2))
(defstrand serv 3 (k k) (n-a n-a-0) (n-b n-b-0) (a a) (b b)
(ch1 ch1-0) (ch2 ch2) (ch3 ch3))
(deflistener k)
(precedes ((1 1) (2 0)) ((1 2) (0 2)) ((2 1) (0 3)))
(uniq-orig k n-b)
(conf ch2 ch3)
(auth ch2)
(operation encryption-test (added-listener k) (enc n-b k) (0 3))
(strand-map 0 1)
(traces
((recv (cat a n-a)) (send ch1 (cat a b n-a n-b))
(recv ch2 (cat a b k)) (recv (enc n-b k)))
((recv ch1-0 (cat a b n-a-0 n-b-0))
(send ch3 (cat a b k n-a-0 n-b-0)) (send ch2 (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)
(ch1 ch1) (ch2 ch2) (ch1-0 ch1-0) (ch3 ch3))))
(comment "1 in cohort - 1 not yet seen"))
(defskeleton yahalom
(vars (k skey) (n-a n-a-0 n-b text) (a b name)
(ch1 ch2 ch1-0 ch3 chan))
(defstrand resp 4 (k k) (n-a n-a) (n-b n-b) (b b) (a a) (ch1 ch1)
(ch2 ch2))
(defstrand serv 3 (k k) (n-a n-a-0) (n-b n-b) (a a) (b b) (ch1 ch1-0)
(ch2 ch2) (ch3 ch3))
(defstrand init 3 (k k) (n-a n-a-0) (n-b n-b) (a a) (b b) (ch3 ch3))
(precedes ((0 1) (1 0)) ((1 1) (2 1)) ((1 2) (0 2)) ((2 2) (0 3)))
(uniq-orig k n-b)
(conf ch2 ch3)
(auth ch2)
(operation nonce-test
(contracted (n-b-0 n-b) (a-0 a) (b-0 b) (n-a-1 n-a-0) (ch3-0 ch3)) k
(2 1) (ch-msg ch3 (cat a b k n-a-0 n-b)))
(strand-map 0 1 2)
(traces
((recv (cat a n-a)) (send ch1 (cat a b n-a n-b))
(recv ch2 (cat a b k)) (recv (enc n-b k)))
((recv ch1-0 (cat a b n-a-0 n-b)) (send ch3 (cat a b k n-a-0 n-b))
(send ch2 (cat a b k)))
((send (cat a n-a-0)) (recv ch3 (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)
(ch1 ch1) (ch2 ch2) (ch1-0 ch1-0) (ch3 ch3))))
(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 a-0 b-0 name)
(ch1 ch2 ch1-0 ch3 ch3-0 chan))
(defstrand resp 4 (k k) (n-a n-a) (n-b n-b) (b b) (a a) (ch1 ch1)
(ch2 ch2))
(defstrand serv 3 (k k) (n-a n-a-0) (n-b n-b-0) (a a) (b b)
(ch1 ch1-0) (ch2 ch2) (ch3 ch3))
(defstrand init 3 (k k) (n-a n-a-1) (n-b n-b) (a a-0) (b b-0)
(ch3 ch3-0))
(precedes ((0 1) (2 1)) ((1 2) (0 2)) ((1 2) (2 1)) ((2 2) (0 3)))
(uniq-orig k n-b)
(conf ch2 ch3)
(auth ch2)
(operation nonce-test (displaced 3 1 serv 3) k (2 1)
(ch-msg ch3 (cat a b k n-a-0 n-b-0)))
(strand-map 0 1 2)
(traces
((recv (cat a n-a)) (send ch1 (cat a b n-a n-b))
(recv ch2 (cat a b k)) (recv (enc n-b k)))
((recv ch1-0 (cat a b n-a-0 n-b-0))
(send ch3 (cat a b k n-a-0 n-b-0)) (send ch2 (cat a b k)))
((send (cat a-0 n-a-1)) (recv ch3-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)
(ch1 ch1) (ch2 ch2) (ch1-0 ch1-0) (ch3 ch3))))
(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 name)
(ch1 ch2 ch1-0 ch3 chan))
(defstrand resp 4 (k k) (n-a n-a) (n-b n-b) (b b) (a a) (ch1 ch1)
(ch2 ch2))
(defstrand serv 3 (k k) (n-a n-a-0) (n-b n-b-0) (a a) (b b)
(ch1 ch1-0) (ch2 ch2) (ch3 ch3))
(deflistener k)
(precedes ((1 2) (0 2)) ((1 2) (2 0)) ((2 1) (0 3)))
(uniq-orig k n-b)
(conf ch2 ch3)
(auth ch2)
(operation nonce-test (displaced 3 1 serv 3) k (2 0)
(ch-msg ch3 (cat a b k n-a-0 n-b-0)))
(strand-map 0 1 2)
(traces
((recv (cat a n-a)) (send ch1 (cat a b n-a n-b))
(recv ch2 (cat a b k)) (recv (enc n-b k)))
((recv ch1-0 (cat a b n-a-0 n-b-0))
(send ch3 (cat a b k n-a-0 n-b-0)) (send ch2 (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)
(ch1 ch1) (ch2 ch2) (ch1-0 ch1-0) (ch3 ch3))))
(comment "empty cohort"))
(defskeleton yahalom
(vars (k skey) (n-a n-a-0 n-b text) (a b name)
(ch1 ch2 ch1-0 ch3 chan))
(defstrand resp 4 (k k) (n-a n-a) (n-b n-b) (b b) (a a) (ch1 ch1)
(ch2 ch2))
(defstrand serv 3 (k k) (n-a n-a-0) (n-b n-b) (a a) (b b) (ch1 ch1-0)
(ch2 ch2) (ch3 ch3))
(defstrand init 3 (k k) (n-a n-a-0) (n-b n-b) (a a) (b b) (ch3 ch3))
(precedes ((0 1) (1 0)) ((1 2) (0 2)) ((1 2) (2 1)) ((2 2) (0 3)))
(uniq-orig k n-b)
(conf ch2 ch3)
(auth ch2)
(operation nonce-test
(contracted (n-b-0 n-b) (a-0 a) (b-0 b) (n-a-1 n-a-0) (ch3-0 ch3)) k
(2 1) (ch-msg ch2 (cat a b k)) (ch-msg ch3 (cat a b k n-a-0 n-b)))
(strand-map 0 1 2)
(traces
((recv (cat a n-a)) (send ch1 (cat a b n-a n-b))
(recv ch2 (cat a b k)) (recv (enc n-b k)))
((recv ch1-0 (cat a b n-a-0 n-b)) (send ch3 (cat a b k n-a-0 n-b))
(send ch2 (cat a b k)))
((send (cat a n-a-0)) (recv ch3 (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)
(ch1 ch1) (ch2 ch2) (ch1-0 ch1-0) (ch3 ch3))))
(comment "1 in cohort - 0 not yet seen"))
(comment "Nothing left to do")
(defprotocol yahalom basic
(defrole init
(vars (a b name) (n-a n-b text) (k skey) (ch3 chan))
(trace (send (cat a n-a)) (recv ch3 (cat a b k n-a n-b))
(send (enc n-b k))))
(defrole resp
(vars (b a name) (n-a n-b text) (k skey) (ch1 ch2 chan))
(trace (recv (cat a n-a)) (send ch1 (cat a b n-a n-b))
(recv ch2 (cat a b k)) (recv (enc n-b k))))
(defrole serv
(vars (a b name) (n-a n-b text) (k skey) (ch1 ch2 ch3 chan))
(trace (recv ch1 (cat a b n-a n-b)) (send ch3 (cat a b k n-a n-b))
(send ch2 (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)))))
(defskeleton yahalom
(vars (k skey) (n-b n-a n-a-0 n-b-0 text) (a b name)
(ch1 ch2 ch1-0 ch3 chan))
(defstrand resp 4 (k k) (n-a n-a) (n-b n-b) (b b) (a a) (ch1 ch1)
(ch2 ch2))
(defstrand serv 3 (k k) (n-a n-a-0) (n-b n-b-0) (a a) (b b)
(ch1 ch1-0) (ch2 ch2) (ch3 ch3))
(uniq-orig k n-b)
(conf ch2 ch3)
(auth ch2 ch1-0)
(traces
((recv (cat a n-a)) (send ch1 (cat a b n-a n-b))
(recv ch2 (cat a b k)) (recv (enc n-b k)))
((recv ch1-0 (cat a b n-a-0 n-b-0))
(send ch3 (cat a b k n-a-0 n-b-0)) (send ch2 (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)
(ch1 ch1) (ch2 ch2) (ch1-0 ch1-0) (ch3 ch3))))
(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 name)
(ch1 ch2 ch1-0 ch3 chan))
(defstrand resp 4 (k k) (n-a n-a) (n-b n-b) (b b) (a a) (ch1 ch1)
(ch2 ch2))
(defstrand serv 3 (k k) (n-a n-a-0) (n-b n-b-0) (a a) (b b)
(ch1 ch1-0) (ch2 ch2) (ch3 ch3))
(precedes ((1 1) (0 2)))
(uniq-orig k n-b)
(conf ch2 ch3)
(auth ch2 ch1-0)
(traces
((recv (cat a n-a)) (send ch1 (cat a b n-a n-b))
(recv ch2 (cat a b k)) (recv (enc n-b k)))
((recv ch1-0 (cat a b n-a-0 n-b-0))
(send ch3 (cat a b k n-a-0 n-b-0)) (send ch2 (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)
(ch1 ch1) (ch2 ch2) (ch1-0 ch1-0) (ch3 ch3))))
(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 name) (ch1 ch2 ch3 chan))
(defstrand resp 4 (k k) (n-a n-a) (n-b n-b) (b b) (a a) (ch1 ch1)
(ch2 ch2))
(defstrand serv 3 (k k) (n-a n-a) (n-b n-b) (a a) (b b) (ch1 ch1)
(ch2 ch2) (ch3 ch3))
(precedes ((0 1) (1 0)) ((1 1) (0 2)))
(uniq-orig k n-b)
(conf ch2 ch3)
(auth ch1 ch2)
(operation channel-test (displaced 2 0 resp 2)
(ch-msg ch1-0 (cat a b n-a-0 n-b-0)) (1 0))
(strand-map 0 1)
(traces
((recv (cat a n-a)) (send ch1 (cat a b n-a n-b))
(recv ch2 (cat a b k)) (recv (enc n-b k)))
((recv ch1 (cat a b n-a n-b)) (send ch3 (cat a b k n-a n-b))
(send ch2 (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)
(ch1 ch1) (ch2 ch2) (ch1-0 ch1) (ch3 ch3))))
(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 name)
(ch1 ch2 ch1-0 ch3 chan))
(defstrand resp 4 (k k) (n-a n-a) (n-b n-b) (b b) (a a) (ch1 ch1)
(ch2 ch2))
(defstrand serv 3 (k k) (n-a n-a-0) (n-b n-b-0) (a a) (b b)
(ch1 ch1-0) (ch2 ch2) (ch3 ch3))
(defstrand resp 2 (n-a n-a-0) (n-b n-b-0) (b b) (a a) (ch1 ch1-0))
(precedes ((1 1) (0 2)) ((2 1) (1 0)))
(uniq-orig k n-b)
(conf ch2 ch3)
(auth ch2 ch1-0)
(operation channel-test (added-strand resp 2)
(ch-msg ch1-0 (cat a b n-a-0 n-b-0)) (1 0))
(strand-map 0 1)
(traces
((recv (cat a n-a)) (send ch1 (cat a b n-a n-b))
(recv ch2 (cat a b k)) (recv (enc n-b k)))
((recv ch1-0 (cat a b n-a-0 n-b-0))
(send ch3 (cat a b k n-a-0 n-b-0)) (send ch2 (cat a b k)))
((recv (cat a n-a-0)) (send ch1-0 (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)
(ch1 ch1) (ch2 ch2) (ch1-0 ch1-0) (ch3 ch3))))
(comment "1 in cohort - 1 not yet seen"))
(defskeleton yahalom
(vars (k skey) (n-b n-a text) (a b name) (ch1 ch2 ch3 chan))
(defstrand resp 4 (k k) (n-a n-a) (n-b n-b) (b b) (a a) (ch1 ch1)
(ch2 ch2))
(defstrand serv 3 (k k) (n-a n-a) (n-b n-b) (a a) (b b) (ch1 ch1)
(ch2 ch2) (ch3 ch3))
(precedes ((0 1) (1 0)) ((1 2) (0 2)))
(uniq-orig k n-b)
(conf ch2 ch3)
(auth ch1 ch2)
(operation channel-test (displaced 2 1 serv 3)
(ch-msg ch2 (cat a b k)) (0 2))
(strand-map 0 1)
(traces
((recv (cat a n-a)) (send ch1 (cat a b n-a n-b))
(recv ch2 (cat a b k)) (recv (enc n-b k)))
((recv ch1 (cat a b n-a n-b)) (send ch3 (cat a b k n-a n-b))
(send ch2 (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)
(ch1 ch1) (ch2 ch2) (ch1-0 ch1) (ch3 ch3))))
(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 name)
(ch1 ch2 ch1-0 ch3 chan))
(defstrand resp 4 (k k) (n-a n-a) (n-b n-b) (b b) (a a) (ch1 ch1)
(ch2 ch2))
(defstrand serv 3 (k k) (n-a n-a-0) (n-b n-b-0) (a a) (b b)
(ch1 ch1-0) (ch2 ch2) (ch3 ch3))
(defstrand resp 2 (n-a n-a-0) (n-b n-b-0) (b b) (a a) (ch1 ch1-0))
(precedes ((1 2) (0 2)) ((2 1) (1 0)))
(uniq-orig k n-b)
(conf ch2 ch3)
(auth ch2 ch1-0)
(operation channel-test (displaced 3 1 serv 3)
(ch-msg ch2 (cat a b k)) (0 2))
(strand-map 0 1 2)
(traces
((recv (cat a n-a)) (send ch1 (cat a b n-a n-b))
(recv ch2 (cat a b k)) (recv (enc n-b k)))
((recv ch1-0 (cat a b n-a-0 n-b-0))
(send ch3 (cat a b k n-a-0 n-b-0)) (send ch2 (cat a b k)))
((recv (cat a n-a-0)) (send ch1-0 (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)
(ch1 ch1) (ch2 ch2) (ch1-0 ch1-0) (ch3 ch3))))
(comment "2 in cohort - 2 not yet seen"))
(defskeleton yahalom
(vars (k skey) (n-b n-a n-a-0 text) (a b a-0 b-0 name)
(ch1 ch2 ch3 ch3-0 chan))
(defstrand resp 4 (k k) (n-a n-a) (n-b n-b) (b b) (a a) (ch1 ch1)
(ch2 ch2))
(defstrand serv 3 (k k) (n-a n-a) (n-b n-b) (a a) (b b) (ch1 ch1)
(ch2 ch2) (ch3 ch3))
(defstrand init 3 (k k) (n-a n-a-0) (n-b n-b) (a a-0) (b b-0)
(ch3 ch3-0))
(precedes ((0 1) (1 0)) ((1 1) (2 1)) ((1 2) (0 2)) ((2 2) (0 3)))
(uniq-orig k n-b)
(conf ch2 ch3)
(auth ch1 ch2)
(operation encryption-test (added-strand init 3) (enc n-b k) (0 3))
(strand-map 0 1)
(traces
((recv (cat a n-a)) (send ch1 (cat a b n-a n-b))
(recv ch2 (cat a b k)) (recv (enc n-b k)))
((recv ch1 (cat a b n-a n-b)) (send ch3 (cat a b k n-a n-b))
(send ch2 (cat a b k)))
((send (cat a-0 n-a-0)) (recv ch3-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)
(ch1 ch1) (ch2 ch2) (ch1-0 ch1) (ch3 ch3))))
(comment "2 in cohort - 2 not yet seen"))
(defskeleton yahalom
(vars (k skey) (n-b n-a text) (a b name) (ch1 ch2 ch3 chan))
(defstrand resp 4 (k k) (n-a n-a) (n-b n-b) (b b) (a a) (ch1 ch1)
(ch2 ch2))
(defstrand serv 3 (k k) (n-a n-a) (n-b n-b) (a a) (b b) (ch1 ch1)
(ch2 ch2) (ch3 ch3))
(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 ch2 ch3)
(auth ch1 ch2)
(operation encryption-test (added-listener k) (enc n-b k) (0 3))
(strand-map 0 1)
(traces
((recv (cat a n-a)) (send ch1 (cat a b n-a n-b))
(recv ch2 (cat a b k)) (recv (enc n-b k)))
((recv ch1 (cat a b n-a n-b)) (send ch3 (cat a b k n-a n-b))
(send ch2 (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)
(ch1 ch1) (ch2 ch2) (ch1-0 ch1) (ch3 ch3))))
(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 a-0 b-0 name)
(ch1 ch2 ch1-0 ch3 ch3-0 chan))
(defstrand resp 4 (k k) (n-a n-a) (n-b n-b) (b b) (a a) (ch1 ch1)
(ch2 ch2))
(defstrand serv 3 (k k) (n-a n-a-0) (n-b n-b-0) (a a) (b b)
(ch1 ch1-0) (ch2 ch2) (ch3 ch3))
(defstrand resp 2 (n-a n-a-0) (n-b n-b-0) (b b) (a a) (ch1 ch1-0))
(defstrand init 3 (k k) (n-a n-a-1) (n-b n-b) (a a-0) (b b-0)
(ch3 ch3-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 ch2 ch3)
(auth ch2 ch1-0)
(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 ch1 (cat a b n-a n-b))
(recv ch2 (cat a b k)) (recv (enc n-b k)))
((recv ch1-0 (cat a b n-a-0 n-b-0))
(send ch3 (cat a b k n-a-0 n-b-0)) (send ch2 (cat a b k)))
((recv (cat a n-a-0)) (send ch1-0 (cat a b n-a-0 n-b-0)))
((send (cat a-0 n-a-1)) (recv ch3-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)
(ch1 ch1) (ch2 ch2) (ch1-0 ch1-0) (ch3 ch3))))
(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 name)
(ch1 ch2 ch1-0 ch3 chan))
(defstrand resp 4 (k k) (n-a n-a) (n-b n-b) (b b) (a a) (ch1 ch1)
(ch2 ch2))
(defstrand serv 3 (k k) (n-a n-a-0) (n-b n-b-0) (a a) (b b)
(ch1 ch1-0) (ch2 ch2) (ch3 ch3))
(defstrand resp 2 (n-a n-a-0) (n-b n-b-0) (b b) (a a) (ch1 ch1-0))
(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 ch2 ch3)
(auth ch2 ch1-0)
(operation encryption-test (added-listener k) (enc n-b k) (0 3))
(strand-map 0 1 2)
(traces
((recv (cat a n-a)) (send ch1 (cat a b n-a n-b))
(recv ch2 (cat a b k)) (recv (enc n-b k)))
((recv ch1-0 (cat a b n-a-0 n-b-0))
(send ch3 (cat a b k n-a-0 n-b-0)) (send ch2 (cat a b k)))
((recv (cat a n-a-0)) (send ch1-0 (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)
(ch1 ch1) (ch2 ch2) (ch1-0 ch1-0) (ch3 ch3))))
(comment "1 in cohort - 1 not yet seen"))
(defskeleton yahalom
(vars (k skey) (n-b n-a text) (a b name) (ch1 ch2 ch3 chan))
(defstrand resp 4 (k k) (n-a n-a) (n-b n-b) (b b) (a a) (ch1 ch1)
(ch2 ch2))
(defstrand serv 3 (k k) (n-a n-a) (n-b n-b) (a a) (b b) (ch1 ch1)
(ch2 ch2) (ch3 ch3))
(defstrand init 3 (k k) (n-a n-a) (n-b n-b) (a a) (b b) (ch3 ch3))
(precedes ((0 1) (1 0)) ((1 1) (2 1)) ((1 2) (0 2)) ((2 2) (0 3)))
(uniq-orig k n-b)
(conf ch2 ch3)
(auth ch1 ch2)
(operation nonce-test
(contracted (a-0 a) (b-0 b) (n-a-0 n-a) (ch3-0 ch3)) k (2 1)
(ch-msg ch3 (cat a b k n-a n-b)))
(strand-map 0 1 2)
(traces
((recv (cat a n-a)) (send ch1 (cat a b n-a n-b))
(recv ch2 (cat a b k)) (recv (enc n-b k)))
((recv ch1 (cat a b n-a n-b)) (send ch3 (cat a b k n-a n-b))
(send ch2 (cat a b k)))
((send (cat a n-a)) (recv ch3 (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)
(ch1 ch1) (ch2 ch2) (ch1-0 ch1) (ch3 ch3))))
(origs (k (1 1)) (n-b (0 1))))
(defskeleton yahalom
(vars (k skey) (n-b n-a n-a-0 text) (a b a-0 b-0 name)
(ch1 ch2 ch3 ch3-0 chan))
(defstrand resp 4 (k k) (n-a n-a) (n-b n-b) (b b) (a a) (ch1 ch1)
(ch2 ch2))
(defstrand serv 3 (k k) (n-a n-a) (n-b n-b) (a a) (b b) (ch1 ch1)
(ch2 ch2) (ch3 ch3))
(defstrand init 3 (k k) (n-a n-a-0) (n-b n-b) (a a-0) (b b-0)
(ch3 ch3-0))
(precedes ((0 1) (1 0)) ((1 2) (0 2)) ((1 2) (2 1)) ((2 2) (0 3)))
(uniq-orig k n-b)
(conf ch2 ch3)
(auth ch1 ch2)
(operation nonce-test (displaced 3 1 serv 3) k (2 1)
(ch-msg ch3 (cat a b k n-a n-b)))
(strand-map 0 1 2)
(traces
((recv (cat a n-a)) (send ch1 (cat a b n-a n-b))
(recv ch2 (cat a b k)) (recv (enc n-b k)))
((recv ch1 (cat a b n-a n-b)) (send ch3 (cat a b k n-a n-b))
(send ch2 (cat a b k)))
((send (cat a-0 n-a-0)) (recv ch3-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)
(ch1 ch1) (ch2 ch2) (ch1-0 ch1) (ch3 ch3))))
(comment "1 in cohort - 1 not yet seen"))
(defskeleton yahalom
(vars (k skey) (n-b n-a text) (a b name) (ch1 ch2 ch3 chan))
(defstrand resp 4 (k k) (n-a n-a) (n-b n-b) (b b) (a a) (ch1 ch1)
(ch2 ch2))
(defstrand serv 3 (k k) (n-a n-a) (n-b n-b) (a a) (b b) (ch1 ch1)
(ch2 ch2) (ch3 ch3))
(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 ch2 ch3)
(auth ch1 ch2)
(operation nonce-test (displaced 3 1 serv 3) k (2 0)
(ch-msg ch3 (cat a b k n-a n-b)))
(strand-map 0 1 2)
(traces
((recv (cat a n-a)) (send ch1 (cat a b n-a n-b))
(recv ch2 (cat a b k)) (recv (enc n-b k)))
((recv ch1 (cat a b n-a n-b)) (send ch3 (cat a b k n-a n-b))
(send ch2 (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)
(ch1 ch1) (ch2 ch2) (ch1-0 ch1) (ch3 ch3))))
(comment "empty cohort"))
(defskeleton yahalom
(vars (k skey) (n-b n-a n-a-0 n-b-0 n-a-1 text) (a b a-0 b-0 name)
(ch1 ch2 ch1-0 ch3 ch3-0 chan))
(defstrand resp 4 (k k) (n-a n-a) (n-b n-b) (b b) (a a) (ch1 ch1)
(ch2 ch2))
(defstrand serv 3 (k k) (n-a n-a-0) (n-b n-b-0) (a a) (b b)
(ch1 ch1-0) (ch2 ch2) (ch3 ch3))
(defstrand resp 2 (n-a n-a-0) (n-b n-b-0) (b b) (a a) (ch1 ch1-0))
(defstrand init 3 (k k) (n-a n-a-1) (n-b n-b) (a a-0) (b b-0)
(ch3 ch3-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 ch2 ch3)
(auth ch2 ch1-0)
(operation nonce-test (displaced 4 1 serv 3) k (3 1)
(ch-msg ch3 (cat a b k n-a-0 n-b-0)))
(strand-map 0 1 2 3)
(traces
((recv (cat a n-a)) (send ch1 (cat a b n-a n-b))
(recv ch2 (cat a b k)) (recv (enc n-b k)))
((recv ch1-0 (cat a b n-a-0 n-b-0))
(send ch3 (cat a b k n-a-0 n-b-0)) (send ch2 (cat a b k)))
((recv (cat a n-a-0)) (send ch1-0 (cat a b n-a-0 n-b-0)))
((send (cat a-0 n-a-1)) (recv ch3-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)
(ch1 ch1) (ch2 ch2) (ch1-0 ch1-0) (ch3 ch3))))
(comment "empty cohort"))
(defskeleton yahalom
(vars (k skey) (n-b n-a n-a-0 n-b-0 text) (a b name)
(ch1 ch2 ch1-0 ch3 chan))
(defstrand resp 4 (k k) (n-a n-a) (n-b n-b) (b b) (a a) (ch1 ch1)
(ch2 ch2))
(defstrand serv 3 (k k) (n-a n-a-0) (n-b n-b-0) (a a) (b b)
(ch1 ch1-0) (ch2 ch2) (ch3 ch3))
(defstrand resp 2 (n-a n-a-0) (n-b n-b-0) (b b) (a a) (ch1 ch1-0))
(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 ch2 ch3)
(auth ch2 ch1-0)
(operation nonce-test (displaced 4 1 serv 3) k (3 0)
(ch-msg ch3 (cat a b k n-a-0 n-b-0)))
(strand-map 0 1 2 3)
(traces
((recv (cat a n-a)) (send ch1 (cat a b n-a n-b))
(recv ch2 (cat a b k)) (recv (enc n-b k)))
((recv ch1-0 (cat a b n-a-0 n-b-0))
(send ch3 (cat a b k n-a-0 n-b-0)) (send ch2 (cat a b k)))
((recv (cat a n-a-0)) (send ch1-0 (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)
(ch1 ch1) (ch2 ch2) (ch1-0 ch1-0) (ch3 ch3))))
(comment "empty cohort"))
(defskeleton yahalom
(vars (k skey) (n-b n-a text) (a b name) (ch1 ch2 ch3 chan))
(defstrand resp 4 (k k) (n-a n-a) (n-b n-b) (b b) (a a) (ch1 ch1)
(ch2 ch2))
(defstrand serv 3 (k k) (n-a n-a) (n-b n-b) (a a) (b b) (ch1 ch1)
(ch2 ch2) (ch3 ch3))
(defstrand init 3 (k k) (n-a n-a) (n-b n-b) (a a) (b b) (ch3 ch3))
(precedes ((0 1) (1 0)) ((1 2) (0 2)) ((1 2) (2 1)) ((2 2) (0 3)))
(uniq-orig k n-b)
(conf ch2 ch3)
(auth ch1 ch2)
(operation nonce-test
(contracted (a-0 a) (b-0 b) (n-a-0 n-a) (ch3-0 ch3)) k (2 1)
(ch-msg ch2 (cat a b k)) (ch-msg ch3 (cat a b k n-a n-b)))
(strand-map 0 1 2)
(traces
((recv (cat a n-a)) (send ch1 (cat a b n-a n-b))
(recv ch2 (cat a b k)) (recv (enc n-b k)))
((recv ch1 (cat a b n-a n-b)) (send ch3 (cat a b k n-a n-b))
(send ch2 (cat a b k)))
((send (cat a n-a)) (recv ch3 (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)
(ch1 ch1) (ch2 ch2) (ch1-0 ch1) (ch3 ch3))))
(comment "1 in cohort - 0 not yet seen"))
(comment "Nothing left to do")
(defprotocol yahalom basic
(defrole init
(vars (a b name) (n-a n-b text) (k skey) (ch3 chan))
(trace (send (cat a n-a)) (recv ch3 (cat a b k n-a n-b))
(send (enc n-b k))))
(defrole resp
(vars (b a name) (n-a n-b text) (k skey) (ch1 ch2 chan))
(trace (recv (cat a n-a)) (send ch1 (cat a b n-a n-b))
(recv ch2 (cat a b k)) (recv (enc n-b k))))
(defrole serv
(vars (a b name) (n-a n-b text) (k skey) (ch1 ch2 ch3 chan))
(trace (recv ch1 (cat a b n-a n-b)) (send ch3 (cat a b k n-a n-b))
(send ch2 (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)))))
(defskeleton yahalom
(vars (k skey) (n-b n-a n-a-0 n-b-0 text) (a b name)
(ch1 ch2 ch1-0 ch3 chan))
(defstrand resp 4 (k k) (n-a n-a) (n-b n-b) (b b) (a a) (ch1 ch1)
(ch2 ch2))
(defstrand serv 3 (k k) (n-a n-a-0) (n-b n-b-0) (a a) (b b)
(ch1 ch1-0) (ch2 ch2) (ch3 ch3))
(deflistener k)
(uniq-orig k n-b)
(conf ch2 ch3)
(auth ch2 ch1-0)
(traces
((recv (cat a n-a)) (send ch1 (cat a b n-a n-b))
(recv ch2 (cat a b k)) (recv (enc n-b k)))
((recv ch1-0 (cat a b n-a-0 n-b-0))
(send ch3 (cat a b k n-a-0 n-b-0)) (send ch2 (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)
(ch1 ch1) (ch2 ch2) (ch1-0 ch1-0) (ch3 ch3))))
(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 name)
(ch1 ch2 ch1-0 ch3 chan))
(defstrand resp 4 (k k) (n-a n-a) (n-b n-b) (b b) (a a) (ch1 ch1)
(ch2 ch2))
(defstrand serv 3 (k k) (n-a n-a-0) (n-b n-b-0) (a a) (b b)
(ch1 ch1-0) (ch2 ch2) (ch3 ch3))
(deflistener k)
(precedes ((1 1) (0 2)) ((1 1) (2 0)))
(uniq-orig k n-b)
(conf ch2 ch3)
(auth ch2 ch1-0)
(traces
((recv (cat a n-a)) (send ch1 (cat a b n-a n-b))
(recv ch2 (cat a b k)) (recv (enc n-b k)))
((recv ch1-0 (cat a b n-a-0 n-b-0))
(send ch3 (cat a b k n-a-0 n-b-0)) (send ch2 (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)
(ch1 ch1) (ch2 ch2) (ch1-0 ch1-0) (ch3 ch3))))
(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 name)
(ch1 ch2 ch1-0 ch3 chan))
(defstrand resp 4 (k k) (n-a n-a) (n-b n-b) (b b) (a a) (ch1 ch1)
(ch2 ch2))
(defstrand serv 3 (k k) (n-a n-a-0) (n-b n-b-0) (a a) (b b)
(ch1 ch1-0) (ch2 ch2) (ch3 ch3))
(deflistener k)
(precedes ((1 1) (0 2)) ((1 2) (2 0)))
(uniq-orig k n-b)
(conf ch2 ch3)
(auth ch2 ch1-0)
(operation nonce-test (displaced 3 1 serv 3) k (2 0)
(ch-msg ch3 (cat a b k n-a-0 n-b-0)))
(strand-map 0 1 2)
(traces
((recv (cat a n-a)) (send ch1 (cat a b n-a n-b))
(recv ch2 (cat a b k)) (recv (enc n-b k)))
((recv ch1-0 (cat a b n-a-0 n-b-0))
(send ch3 (cat a b k n-a-0 n-b-0)) (send ch2 (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)
(ch1 ch1) (ch2 ch2) (ch1-0 ch1-0) (ch3 ch3))))
(origs (k (1 1)) (n-b (0 1)))
(comment "empty cohort"))
(comment "Nothing left to do")
(defprotocol yahalom basic
(defrole init
(vars (a b name) (n-a n-b text) (k skey) (ch3 chan))
(trace (send (cat a n-a)) (recv ch3 (cat a b k n-a n-b))
(send (enc n-b k))))
(defrole resp
(vars (b a name) (n-a n-b text) (k skey) (ch1 ch2 chan))
(trace (recv (cat a n-a)) (send ch1 (cat a b n-a n-b))
(recv ch2 (cat a b k)) (recv (enc n-b k))))
(defrole serv
(vars (a b name) (n-a n-b text) (k skey) (ch1 ch2 ch3 chan))
(trace (recv ch1 (cat a b n-a n-b)) (send ch3 (cat a b k n-a n-b))
(send ch2 (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)))))
(defskeleton yahalom
(vars (k skey) (n-a n-b text) (a b name) (ch3 chan))
(defstrand init 3 (k k) (n-a n-a) (n-b n-b) (a a) (b b) (ch3 ch3))
(uniq-orig n-a)
(auth ch3)
(traces
((send (cat a n-a)) (recv ch3 (cat a b k n-a n-b))
(send (enc n-b k))))
(label 28)
(unrealized (0 1))
(maps ((0) ((n-a n-a) (ch3 ch3) (a 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 b name) (ch3 ch1 chan))
(defstrand init 3 (k k) (n-a n-a) (n-b n-b) (a a) (b b) (ch3 ch3))
(defstrand serv 2 (k k) (n-a n-a) (n-b n-b) (a a) (b b) (ch1 ch1)
(ch3 ch3))
(precedes ((0 0) (1 0)) ((1 1) (0 1)))
(uniq-orig k n-a)
(auth ch3)
(operation channel-test (added-strand serv 2)
(ch-msg ch3 (cat a b k n-a n-b)) (0 1))
(strand-map 0)
(traces
((send (cat a n-a)) (recv ch3 (cat a b k n-a n-b))
(send (enc n-b k)))
((recv ch1 (cat a b n-a n-b)) (send ch3 (cat a b k n-a n-b))))
(label 29)
(parent 28)
(realized)
(shape)
(maps ((0) ((n-a n-a) (ch3 ch3) (a 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 name) (n-a n-b text) (k skey) (ch3 chan))
(trace (send (cat a n-a)) (recv ch3 (cat a b k n-a n-b))
(send (enc n-b k))))
(defrole resp
(vars (b a name) (n-a n-b text) (k skey) (ch1 ch2 chan))
(trace (recv (cat a n-a)) (send ch1 (cat a b n-a n-b))
(recv ch2 (cat a b k)) (recv (enc n-b k))))
(defrole serv
(vars (a b name) (n-a n-b text) (k skey) (ch1 ch2 ch3 chan))
(trace (recv ch1 (cat a b n-a n-b)) (send ch3 (cat a b k n-a n-b))
(send ch2 (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)))))
(defskeleton yahalom
(vars (k skey) (n-a n-b text) (a b name) (ch3 ch3-0 ch1 chan))
(defstrand init 3 (k k) (n-a n-a) (n-b n-b) (a a) (b b) (ch3 ch3))
(defstrand serv 2 (k k) (n-a n-a) (n-b n-b) (a a) (b b) (ch1 ch1)
(ch3 ch3-0))
(precedes ((0 0) (1 0)) ((1 1) (0 1)))
(uniq-orig k n-a)
(conf ch3-0)
(auth ch3 ch1)
(traces
((send (cat a n-a)) (recv ch3 (cat a b k n-a n-b))
(send (enc n-b k)))
((recv ch1 (cat a b n-a n-b)) (send ch3-0 (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) (b b) (ch3 ch3) (ch3-0 ch3-0)
(ch1 ch1))))
(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 b name) (ch3 ch3-0 ch1 chan))
(defstrand init 3 (k k) (n-a n-a) (n-b n-b) (a a) (b b) (ch3 ch3))
(defstrand serv 2 (k k) (n-a n-a) (n-b n-b) (a a) (b b) (ch1 ch1)
(ch3 ch3-0))
(defstrand resp 2 (n-a n-a) (n-b n-b) (b b) (a a) (ch1 ch1))
(precedes ((0 0) (2 0)) ((1 1) (0 1)) ((2 1) (1 0)))
(uniq-orig k n-a)
(conf ch3-0)
(auth ch3 ch1)
(operation channel-test (added-strand resp 2)
(ch-msg ch1 (cat a b n-a n-b)) (1 0))
(strand-map 0 1)
(traces
((send (cat a n-a)) (recv ch3 (cat a b k n-a n-b))
(send (enc n-b k)))
((recv ch1 (cat a b n-a n-b)) (send ch3-0 (cat a b k n-a n-b)))
((recv (cat a n-a)) (send ch1 (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) (b b) (ch3 ch3) (ch3-0 ch3-0)
(ch1 ch1))))
(comment "1 in cohort - 1 not yet seen"))
(defskeleton yahalom
(vars (k skey) (n-a n-b text) (a b name) (ch3 ch1 chan))
(defstrand init 3 (k k) (n-a n-a) (n-b n-b) (a a) (b b) (ch3 ch3))
(defstrand serv 2 (k k) (n-a n-a) (n-b n-b) (a a) (b b) (ch1 ch1)
(ch3 ch3))
(defstrand resp 2 (n-a n-a) (n-b n-b) (b b) (a a) (ch1 ch1))
(precedes ((0 0) (2 0)) ((1 1) (0 1)) ((2 1) (1 0)))
(uniq-orig k n-a)
(conf ch3)
(auth ch3 ch1)
(operation channel-test (displaced 3 1 serv 2)
(ch-msg ch3-0 (cat a b k n-a n-b)) (0 1))
(strand-map 0 1 2)
(traces
((send (cat a n-a)) (recv ch3 (cat a b k n-a n-b))
(send (enc n-b k)))
((recv ch1 (cat a b n-a n-b)) (send ch3 (cat a b k n-a n-b)))
((recv (cat a n-a)) (send ch1 (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) (b b) (ch3 ch3) (ch3-0 ch3)
(ch1 ch1))))
(origs (k (1 1)) (n-a (0 0))))
(comment "Nothing left to do")
(defprotocol yahalom basic
(defrole init
(vars (a b name) (n-a n-b text) (k skey) (ch3 chan))
(trace (send (cat a n-a)) (recv ch3 (cat a b k n-a n-b))
(send (enc n-b k))))
(defrole resp
(vars (b a name) (n-a n-b text) (k skey) (ch1 ch2 chan))
(trace (recv (cat a n-a)) (send ch1 (cat a b n-a n-b))
(recv ch2 (cat a b k)) (recv (enc n-b k))))
(defrole serv
(vars (a b name) (n-a n-b text) (k skey) (ch1 ch2 ch3 chan))
(trace (recv ch1 (cat a b n-a n-b)) (send ch3 (cat a b k n-a n-b))
(send ch2 (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)))))
(defskeleton yahalom
(vars (k skey) (n-a n-b text) (a b name) (ch1 ch2 ch3 chan))
(defstrand serv 3 (k k) (n-a n-a) (n-b n-b) (a a) (b b) (ch1 ch1)
(ch2 ch2) (ch3 ch3))
(uniq-orig k)
(conf ch2 ch3)
(auth ch1)
(traces
((recv ch1 (cat a b n-a n-b)) (send ch3 (cat a b k n-a n-b))
(send ch2 (cat a b k))))
(label 33)
(unrealized (0 0))
(maps
((0)
((ch1 ch1) (ch2 ch2) (ch3 ch3) (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) (a b name) (ch1 ch2 ch3 chan))
(defstrand serv 3 (k k) (n-a n-a) (n-b n-b) (a a) (b b) (ch1 ch1)
(ch2 ch2) (ch3 ch3))
(defstrand resp 2 (n-a n-a) (n-b n-b) (b b) (a a) (ch1 ch1))
(precedes ((1 1) (0 0)))
(uniq-orig k)
(conf ch2 ch3)
(auth ch1)
(operation channel-test (added-strand resp 2)
(ch-msg ch1 (cat a b n-a n-b)) (0 0))
(strand-map 0)
(traces
((recv ch1 (cat a b n-a n-b)) (send ch3 (cat a b k n-a n-b))
(send ch2 (cat a b k)))
((recv (cat a n-a)) (send ch1 (cat a b n-a n-b))))
(label 34)
(parent 33)
(realized)
(shape)
(maps
((0)
((ch1 ch1) (ch2 ch2) (ch3 ch3) (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 name) (n-a n-b text) (k skey) (ch3 chan))
(trace (send (cat a n-a)) (recv ch3 (cat a b k n-a n-b))
(send (enc n-b k))))
(defrole resp
(vars (b a name) (n-a n-b text) (k skey) (ch1 ch2 chan))
(trace (recv (cat a n-a)) (send ch1 (cat a b n-a n-b))
(recv ch2 (cat a b k)) (recv (enc n-b k))))
(defrole serv
(vars (a b name) (n-a n-b text) (k skey) (ch1 ch2 ch3 chan))
(trace (recv ch1 (cat a b n-a n-b)) (send ch3 (cat a b k n-a n-b))
(send ch2 (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)))))
(defskeleton yahalom
(vars (k skey) (n-a n-b text) (a b name) (ch1 ch2 ch3 chan))
(defstrand serv 3 (k k) (n-a n-a) (n-b n-b) (a a) (b b) (ch1 ch1)
(ch2 ch2) (ch3 ch3))
(deflistener k)
(uniq-orig k)
(conf ch2 ch3)
(auth ch1)
(traces
((recv ch1 (cat a b n-a n-b)) (send ch3 (cat a b k n-a n-b))
(send ch2 (cat a b k))) ((recv k) (send k)))
(label 35)
(unrealized (0 0) (1 0))
(preskeleton)
(maps
((0 1)
((k k) (ch1 ch1) (ch2 ch2) (ch3 ch3) (a a) (b b) (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) (a b name) (ch1 ch2 ch3 chan))
(defstrand serv 3 (k k) (n-a n-a) (n-b n-b) (a a) (b b) (ch1 ch1)
(ch2 ch2) (ch3 ch3))
(deflistener k)
(precedes ((0 1) (1 0)))
(uniq-orig k)
(conf ch2 ch3)
(auth ch1)
(traces
((recv ch1 (cat a b n-a n-b)) (send ch3 (cat a b k n-a n-b))
(send ch2 (cat a b k))) ((recv k) (send k)))
(label 36)
(parent 35)
(unrealized (0 0) (1 0))
(maps
((0 1)
((k k) (ch1 ch1) (ch2 ch2) (ch3 ch3) (a a) (b b) (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) (a b name) (ch1 ch2 ch3 chan))
(defstrand serv 3 (k k) (n-a n-a) (n-b n-b) (a a) (b b) (ch1 ch1)
(ch2 ch2) (ch3 ch3))
(deflistener k)
(precedes ((0 2) (1 0)))
(uniq-orig k)
(conf ch2 ch3)
(auth ch1)
(operation nonce-test (displaced 2 0 serv 3) k (1 0)
(ch-msg ch3 (cat a b k n-a n-b)))
(strand-map 0 1)
(traces
((recv ch1 (cat a b n-a n-b)) (send ch3 (cat a b k n-a n-b))
(send ch2 (cat a b k))) ((recv k) (send k)))
(label 37)
(parent 36)
(unrealized (0 0) (1 0))
(dead)
(maps
((0 1)
((k k) (ch1 ch1) (ch2 ch2) (ch3 ch3) (a a) (b b) (n-a n-a)
(n-b n-b))))
(origs (k (0 1)))
(comment "empty cohort"))
(comment "Nothing left to do")