(herald dhca (algebra basic) (bound 12)) (comment "CPSA 4.4.3") (comment "All input read from tst/dh-ca_hack.scm") (defprotocol dhca basic (defrole init (vars (gx h akey) (dhkey skey) (a b ca name) (n text)) (trace (recv (enc gx a (privk ca))) (send (cat gx (enc gx a (privk ca)))) (recv (cat h (enc h b (privk ca)) (enc n (enc "dh" gx h dhkey)))) (send (enc "check" n (enc "dh" gx h dhkey)))) (non-orig dhkey (privk ca))) (defrole resp (vars (gy h akey) (dhkey skey) (a b ca name) (n text)) (trace (recv (enc gy b (privk ca))) (recv (cat h (enc h a (privk ca)))) (send (cat gy (enc gy b (privk ca)) (enc n (enc "dh" h gy dhkey)))) (recv (enc "check" n (enc "dh" h gy dhkey)))) (non-orig dhkey (privk ca))) (defrole ca (vars (subject ca name) (gz akey)) (trace (send (enc gz subject (privk ca)))) (non-orig (invk gz))) (defrole CDHcalc1 (vars (gx gy akey) (dhkey skey)) (trace (recv (cat gx (invk gy))) (send (enc "dh" gx gy dhkey)))) (defrole CDHcalc2 (vars (gx gy akey) (dhkey skey)) (trace (recv (cat gy (invk gx))) (send (enc "dh" gx gy dhkey)))) (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 dhca (vars (dhkey skey) (n text) (gx h akey) (a b ca name)) (defstrand init 4 (dhkey dhkey) (n n) (gx gx) (h h) (a a) (b b) (ca ca)) (non-orig dhkey (privk ca)) (comment "Full initiator point-of-view. No need to make extra assumptions.") (traces ((recv (enc gx a (privk ca))) (send (cat gx (enc gx a (privk ca)))) (recv (cat h (enc h b (privk ca)) (enc n (enc "dh" gx h dhkey)))) (send (enc "check" n (enc "dh" gx h dhkey))))) (label 0) (unrealized (0 0) (0 2)) (origs) (comment "1 in cohort - 1 not yet seen")) (defskeleton dhca (vars (dhkey skey) (n text) (gx h akey) (a b ca name)) (defstrand init 4 (dhkey dhkey) (n n) (gx gx) (h h) (a a) (b b) (ca ca)) (defstrand ca 1 (gz gx) (subject a) (ca ca)) (precedes ((1 0) (0 0))) (non-orig dhkey (invk gx) (privk ca)) (operation encryption-test (added-strand ca 1) (enc gx a (privk ca)) (0 0)) (traces ((recv (enc gx a (privk ca))) (send (cat gx (enc gx a (privk ca)))) (recv (cat h (enc h b (privk ca)) (enc n (enc "dh" gx h dhkey)))) (send (enc "check" n (enc "dh" gx h dhkey)))) ((send (enc gx a (privk ca))))) (label 1) (parent 0) (unrealized (0 2)) (comment "2 in cohort - 2 not yet seen")) (defskeleton dhca (vars (dhkey skey) (n text) (gx akey) (a ca name)) (defstrand init 4 (dhkey dhkey) (n n) (gx gx) (h gx) (a a) (b a) (ca ca)) (defstrand ca 1 (gz gx) (subject a) (ca ca)) (precedes ((1 0) (0 0))) (non-orig dhkey (invk gx) (privk ca)) (operation encryption-test (displaced 2 1 ca 1) (enc h b (privk ca)) (0 2)) (traces ((recv (enc gx a (privk ca))) (send (cat gx (enc gx a (privk ca)))) (recv (cat gx (enc gx a (privk ca)) (enc n (enc "dh" gx gx dhkey)))) (send (enc "check" n (enc "dh" gx gx dhkey)))) ((send (enc gx a (privk ca))))) (label 2) (parent 1) (unrealized (0 2)) (comment "2 in cohort - 2 not yet seen")) (defskeleton dhca (vars (dhkey skey) (n text) (gx h akey) (a b ca name)) (defstrand init 4 (dhkey dhkey) (n n) (gx gx) (h h) (a a) (b b) (ca ca)) (defstrand ca 1 (gz gx) (subject a) (ca ca)) (defstrand ca 1 (gz h) (subject b) (ca ca)) (precedes ((1 0) (0 0)) ((2 0) (0 2))) (non-orig dhkey (invk gx) (invk h) (privk ca)) (operation encryption-test (added-strand ca 1) (enc h b (privk ca)) (0 2)) (traces ((recv (enc gx a (privk ca))) (send (cat gx (enc gx a (privk ca)))) (recv (cat h (enc h b (privk ca)) (enc n (enc "dh" gx h dhkey)))) (send (enc "check" n (enc "dh" gx h dhkey)))) ((send (enc gx a (privk ca)))) ((send (enc h b (privk ca))))) (label 3) (parent 1) (unrealized (0 2)) (comment "2 in cohort - 2 not yet seen")) (defskeleton dhca (vars (dhkey skey) (n text) (gx akey) (a ca a-0 b ca-0 name)) (defstrand init 4 (dhkey dhkey) (n n) (gx gx) (h gx) (a a) (b a) (ca ca)) (defstrand ca 1 (gz gx) (subject a) (ca ca)) (defstrand resp 3 (dhkey dhkey) (n n) (gy gx) (h gx) (a a-0) (b b) (ca ca-0)) (precedes ((1 0) (0 0)) ((2 2) (0 2))) (non-orig dhkey (invk gx) (privk ca) (privk ca-0)) (operation encryption-test (added-strand resp 3) (enc n (enc "dh" gx gx dhkey)) (0 2)) (traces ((recv (enc gx a (privk ca))) (send (cat gx (enc gx a (privk ca)))) (recv (cat gx (enc gx a (privk ca)) (enc n (enc "dh" gx gx dhkey)))) (send (enc "check" n (enc "dh" gx gx dhkey)))) ((send (enc gx a (privk ca)))) ((recv (enc gx b (privk ca-0))) (recv (cat gx (enc gx a-0 (privk ca-0)))) (send (cat gx (enc gx b (privk ca-0)) (enc n (enc "dh" gx gx dhkey)))))) (label 4) (parent 2) (unrealized (2 0) (2 1)) (comment "2 in cohort - 2 not yet seen")) (defskeleton dhca (vars (dhkey skey) (n text) (gx akey) (a ca name)) (defstrand init 4 (dhkey dhkey) (n n) (gx gx) (h gx) (a a) (b a) (ca ca)) (defstrand ca 1 (gz gx) (subject a) (ca ca)) (deflistener (enc "dh" gx gx dhkey)) (precedes ((1 0) (0 0)) ((2 1) (0 2))) (non-orig dhkey (invk gx) (privk ca)) (operation encryption-test (added-listener (enc "dh" gx gx dhkey)) (enc n (enc "dh" gx gx dhkey)) (0 2)) (traces ((recv (enc gx a (privk ca))) (send (cat gx (enc gx a (privk ca)))) (recv (cat gx (enc gx a (privk ca)) (enc n (enc "dh" gx gx dhkey)))) (send (enc "check" n (enc "dh" gx gx dhkey)))) ((send (enc gx a (privk ca)))) ((recv (enc "dh" gx gx dhkey)) (send (enc "dh" gx gx dhkey)))) (label 5) (parent 2) (unrealized (2 0)) (dead) (comment "empty cohort")) (defskeleton dhca (vars (dhkey skey) (n text) (gx h akey) (a b ca a-0 b-0 ca-0 name)) (defstrand init 4 (dhkey dhkey) (n n) (gx gx) (h h) (a a) (b b) (ca ca)) (defstrand ca 1 (gz gx) (subject a) (ca ca)) (defstrand ca 1 (gz h) (subject b) (ca ca)) (defstrand resp 3 (dhkey dhkey) (n n) (gy h) (h gx) (a a-0) (b b-0) (ca ca-0)) (precedes ((1 0) (0 0)) ((2 0) (0 2)) ((3 2) (0 2))) (non-orig dhkey (invk gx) (invk h) (privk ca) (privk ca-0)) (operation encryption-test (added-strand resp 3) (enc n (enc "dh" gx h dhkey)) (0 2)) (traces ((recv (enc gx a (privk ca))) (send (cat gx (enc gx a (privk ca)))) (recv (cat h (enc h b (privk ca)) (enc n (enc "dh" gx h dhkey)))) (send (enc "check" n (enc "dh" gx h dhkey)))) ((send (enc gx a (privk ca)))) ((send (enc h b (privk ca)))) ((recv (enc h b-0 (privk ca-0))) (recv (cat gx (enc gx a-0 (privk ca-0)))) (send (cat h (enc h b-0 (privk ca-0)) (enc n (enc "dh" gx h dhkey)))))) (label 6) (parent 3) (unrealized (3 0) (3 1)) (comment "3 in cohort - 3 not yet seen")) (defskeleton dhca (vars (dhkey skey) (n text) (gx h akey) (a b ca name)) (defstrand init 4 (dhkey dhkey) (n n) (gx gx) (h h) (a a) (b b) (ca ca)) (defstrand ca 1 (gz gx) (subject a) (ca ca)) (defstrand ca 1 (gz h) (subject b) (ca ca)) (deflistener (enc "dh" gx h dhkey)) (precedes ((1 0) (0 0)) ((2 0) (0 2)) ((3 1) (0 2))) (non-orig dhkey (invk gx) (invk h) (privk ca)) (operation encryption-test (added-listener (enc "dh" gx h dhkey)) (enc n (enc "dh" gx h dhkey)) (0 2)) (traces ((recv (enc gx a (privk ca))) (send (cat gx (enc gx a (privk ca)))) (recv (cat h (enc h b (privk ca)) (enc n (enc "dh" gx h dhkey)))) (send (enc "check" n (enc "dh" gx h dhkey)))) ((send (enc gx a (privk ca)))) ((send (enc h b (privk ca)))) ((recv (enc "dh" gx h dhkey)) (send (enc "dh" gx h dhkey)))) (label 7) (parent 3) (unrealized (3 0)) (dead) (comment "empty cohort")) (defskeleton dhca (vars (dhkey skey) (n text) (gx akey) (a ca a-0 name)) (defstrand init 4 (dhkey dhkey) (n n) (gx gx) (h gx) (a a) (b a) (ca ca)) (defstrand ca 1 (gz gx) (subject a) (ca ca)) (defstrand resp 3 (dhkey dhkey) (n n) (gy gx) (h gx) (a a-0) (b a) (ca ca)) (precedes ((1 0) (0 0)) ((1 0) (2 0)) ((2 2) (0 2))) (non-orig dhkey (invk gx) (privk ca)) (operation encryption-test (displaced 3 1 ca 1) (enc gx b (privk ca-0)) (2 0)) (traces ((recv (enc gx a (privk ca))) (send (cat gx (enc gx a (privk ca)))) (recv (cat gx (enc gx a (privk ca)) (enc n (enc "dh" gx gx dhkey)))) (send (enc "check" n (enc "dh" gx gx dhkey)))) ((send (enc gx a (privk ca)))) ((recv (enc gx a (privk ca))) (recv (cat gx (enc gx a-0 (privk ca)))) (send (cat gx (enc gx a (privk ca)) (enc n (enc "dh" gx gx dhkey)))))) (label 8) (parent 4) (unrealized (2 1)) (comment "2 in cohort - 2 not yet seen")) (defskeleton dhca (vars (dhkey skey) (n text) (gx akey) (a ca a-0 b ca-0 name)) (defstrand init 4 (dhkey dhkey) (n n) (gx gx) (h gx) (a a) (b a) (ca ca)) (defstrand ca 1 (gz gx) (subject a) (ca ca)) (defstrand resp 3 (dhkey dhkey) (n n) (gy gx) (h gx) (a a-0) (b b) (ca ca-0)) (defstrand ca 1 (gz gx) (subject b) (ca ca-0)) (precedes ((1 0) (0 0)) ((2 2) (0 2)) ((3 0) (2 0))) (non-orig dhkey (invk gx) (privk ca) (privk ca-0)) (operation encryption-test (added-strand ca 1) (enc gx b (privk ca-0)) (2 0)) (traces ((recv (enc gx a (privk ca))) (send (cat gx (enc gx a (privk ca)))) (recv (cat gx (enc gx a (privk ca)) (enc n (enc "dh" gx gx dhkey)))) (send (enc "check" n (enc "dh" gx gx dhkey)))) ((send (enc gx a (privk ca)))) ((recv (enc gx b (privk ca-0))) (recv (cat gx (enc gx a-0 (privk ca-0)))) (send (cat gx (enc gx b (privk ca-0)) (enc n (enc "dh" gx gx dhkey))))) ((send (enc gx b (privk ca-0))))) (label 9) (parent 4) (unrealized (2 1)) (comment "3 in cohort - 3 not yet seen")) (defskeleton dhca (vars (dhkey skey) (n text) (gx akey) (a b ca a-0 name)) (defstrand init 4 (dhkey dhkey) (n n) (gx gx) (h gx) (a a) (b b) (ca ca)) (defstrand ca 1 (gz gx) (subject a) (ca ca)) (defstrand ca 1 (gz gx) (subject b) (ca ca)) (defstrand resp 3 (dhkey dhkey) (n n) (gy gx) (h gx) (a a-0) (b a) (ca ca)) (precedes ((1 0) (0 0)) ((1 0) (3 0)) ((2 0) (0 2)) ((3 2) (0 2))) (non-orig dhkey (invk gx) (privk ca)) (operation encryption-test (displaced 4 1 ca 1) (enc h b-0 (privk ca-0)) (3 0)) (traces ((recv (enc gx a (privk ca))) (send (cat gx (enc gx a (privk ca)))) (recv (cat gx (enc gx b (privk ca)) (enc n (enc "dh" gx gx dhkey)))) (send (enc "check" n (enc "dh" gx gx dhkey)))) ((send (enc gx a (privk ca)))) ((send (enc gx b (privk ca)))) ((recv (enc gx a (privk ca))) (recv (cat gx (enc gx a-0 (privk ca)))) (send (cat gx (enc gx a (privk ca)) (enc n (enc "dh" gx gx dhkey)))))) (label 10) (parent 6) (unrealized (3 1)) (comment "3 in cohort - 3 not yet seen")) (defskeleton dhca (vars (dhkey skey) (n text) (gx h akey) (a b ca a-0 name)) (defstrand init 4 (dhkey dhkey) (n n) (gx gx) (h h) (a a) (b b) (ca ca)) (defstrand ca 1 (gz gx) (subject a) (ca ca)) (defstrand ca 1 (gz h) (subject b) (ca ca)) (defstrand resp 3 (dhkey dhkey) (n n) (gy h) (h gx) (a a-0) (b b) (ca ca)) (precedes ((1 0) (0 0)) ((2 0) (3 0)) ((3 2) (0 2))) (non-orig dhkey (invk gx) (invk h) (privk ca)) (operation encryption-test (displaced 4 2 ca 1) (enc h b-0 (privk ca-0)) (3 0)) (traces ((recv (enc gx a (privk ca))) (send (cat gx (enc gx a (privk ca)))) (recv (cat h (enc h b (privk ca)) (enc n (enc "dh" gx h dhkey)))) (send (enc "check" n (enc "dh" gx h dhkey)))) ((send (enc gx a (privk ca)))) ((send (enc h b (privk ca)))) ((recv (enc h b (privk ca))) (recv (cat gx (enc gx a-0 (privk ca)))) (send (cat h (enc h b (privk ca)) (enc n (enc "dh" gx h dhkey)))))) (label 11) (parent 6) (unrealized (3 1)) (comment "3 in cohort - 3 not yet seen")) (defskeleton dhca (vars (dhkey skey) (n text) (gx h akey) (a b ca a-0 b-0 ca-0 name)) (defstrand init 4 (dhkey dhkey) (n n) (gx gx) (h h) (a a) (b b) (ca ca)) (defstrand ca 1 (gz gx) (subject a) (ca ca)) (defstrand ca 1 (gz h) (subject b) (ca ca)) (defstrand resp 3 (dhkey dhkey) (n n) (gy h) (h gx) (a a-0) (b b-0) (ca ca-0)) (defstrand ca 1 (gz h) (subject b-0) (ca ca-0)) (precedes ((1 0) (0 0)) ((2 0) (0 2)) ((3 2) (0 2)) ((4 0) (3 0))) (non-orig dhkey (invk gx) (invk h) (privk ca) (privk ca-0)) (operation encryption-test (added-strand ca 1) (enc h b-0 (privk ca-0)) (3 0)) (traces ((recv (enc gx a (privk ca))) (send (cat gx (enc gx a (privk ca)))) (recv (cat h (enc h b (privk ca)) (enc n (enc "dh" gx h dhkey)))) (send (enc "check" n (enc "dh" gx h dhkey)))) ((send (enc gx a (privk ca)))) ((send (enc h b (privk ca)))) ((recv (enc h b-0 (privk ca-0))) (recv (cat gx (enc gx a-0 (privk ca-0)))) (send (cat h (enc h b-0 (privk ca-0)) (enc n (enc "dh" gx h dhkey))))) ((send (enc h b-0 (privk ca-0))))) (label 12) (parent 6) (unrealized (3 1)) (comment "4 in cohort - 4 not yet seen")) (defskeleton dhca (vars (dhkey skey) (n text) (gx akey) (a ca name)) (defstrand init 4 (dhkey dhkey) (n n) (gx gx) (h gx) (a a) (b a) (ca ca)) (defstrand ca 1 (gz gx) (subject a) (ca ca)) (defstrand resp 3 (dhkey dhkey) (n n) (gy gx) (h gx) (a a) (b a) (ca ca)) (precedes ((1 0) (0 0)) ((1 0) (2 0)) ((2 2) (0 2))) (non-orig dhkey (invk gx) (privk ca)) (operation encryption-test (displaced 3 1 ca 1) (enc gx a-0 (privk ca)) (2 1)) (traces ((recv (enc gx a (privk ca))) (send (cat gx (enc gx a (privk ca)))) (recv (cat gx (enc gx a (privk ca)) (enc n (enc "dh" gx gx dhkey)))) (send (enc "check" n (enc "dh" gx gx dhkey)))) ((send (enc gx a (privk ca)))) ((recv (enc gx a (privk ca))) (recv (cat gx (enc gx a (privk ca)))) (send (cat gx (enc gx a (privk ca)) (enc n (enc "dh" gx gx dhkey)))))) (label 13) (parent 8) (realized) (shape) (maps ((0) ((gx gx) (h gx) (dhkey dhkey) (a a) (b a) (ca ca) (n n)))) (origs)) (defskeleton dhca (vars (dhkey skey) (n text) (gx akey) (a ca a-0 name)) (defstrand init 4 (dhkey dhkey) (n n) (gx gx) (h gx) (a a) (b a) (ca ca)) (defstrand ca 1 (gz gx) (subject a) (ca ca)) (defstrand resp 3 (dhkey dhkey) (n n) (gy gx) (h gx) (a a-0) (b a) (ca ca)) (defstrand ca 1 (gz gx) (subject a-0) (ca ca)) (precedes ((1 0) (0 0)) ((1 0) (2 0)) ((2 2) (0 2)) ((3 0) (2 1))) (non-orig dhkey (invk gx) (privk ca)) (operation encryption-test (added-strand ca 1) (enc gx a-0 (privk ca)) (2 1)) (traces ((recv (enc gx a (privk ca))) (send (cat gx (enc gx a (privk ca)))) (recv (cat gx (enc gx a (privk ca)) (enc n (enc "dh" gx gx dhkey)))) (send (enc "check" n (enc "dh" gx gx dhkey)))) ((send (enc gx a (privk ca)))) ((recv (enc gx a (privk ca))) (recv (cat gx (enc gx a-0 (privk ca)))) (send (cat gx (enc gx a (privk ca)) (enc n (enc "dh" gx gx dhkey))))) ((send (enc gx a-0 (privk ca))))) (label 14) (parent 8) (realized) (shape) (maps ((0) ((gx gx) (h gx) (dhkey dhkey) (a a) (b a) (ca ca) (n n)))) (origs)) (defskeleton dhca (vars (dhkey skey) (n text) (gx akey) (a ca b name)) (defstrand init 4 (dhkey dhkey) (n n) (gx gx) (h gx) (a a) (b a) (ca ca)) (defstrand ca 1 (gz gx) (subject a) (ca ca)) (defstrand resp 3 (dhkey dhkey) (n n) (gy gx) (h gx) (a a) (b b) (ca ca)) (defstrand ca 1 (gz gx) (subject b) (ca ca)) (precedes ((1 0) (0 0)) ((1 0) (2 1)) ((2 2) (0 2)) ((3 0) (2 0))) (non-orig dhkey (invk gx) (privk ca)) (operation encryption-test (displaced 4 1 ca 1) (enc gx a-0 (privk ca-0)) (2 1)) (traces ((recv (enc gx a (privk ca))) (send (cat gx (enc gx a (privk ca)))) (recv (cat gx (enc gx a (privk ca)) (enc n (enc "dh" gx gx dhkey)))) (send (enc "check" n (enc "dh" gx gx dhkey)))) ((send (enc gx a (privk ca)))) ((recv (enc gx b (privk ca))) (recv (cat gx (enc gx a (privk ca)))) (send (cat gx (enc gx b (privk ca)) (enc n (enc "dh" gx gx dhkey))))) ((send (enc gx b (privk ca))))) (label 15) (parent 9) (realized) (shape) (maps ((0) ((gx gx) (h gx) (dhkey dhkey) (a a) (b a) (ca ca) (n n)))) (origs)) (defskeleton dhca (vars (dhkey skey) (n text) (gx akey) (a ca b ca-0 name)) (defstrand init 4 (dhkey dhkey) (n n) (gx gx) (h gx) (a a) (b a) (ca ca)) (defstrand ca 1 (gz gx) (subject a) (ca ca)) (defstrand resp 3 (dhkey dhkey) (n n) (gy gx) (h gx) (a b) (b b) (ca ca-0)) (defstrand ca 1 (gz gx) (subject b) (ca ca-0)) (precedes ((1 0) (0 0)) ((2 2) (0 2)) ((3 0) (2 0))) (non-orig dhkey (invk gx) (privk ca) (privk ca-0)) (operation encryption-test (displaced 4 3 ca 1) (enc gx a-0 (privk ca-0)) (2 1)) (traces ((recv (enc gx a (privk ca))) (send (cat gx (enc gx a (privk ca)))) (recv (cat gx (enc gx a (privk ca)) (enc n (enc "dh" gx gx dhkey)))) (send (enc "check" n (enc "dh" gx gx dhkey)))) ((send (enc gx a (privk ca)))) ((recv (enc gx b (privk ca-0))) (recv (cat gx (enc gx b (privk ca-0)))) (send (cat gx (enc gx b (privk ca-0)) (enc n (enc "dh" gx gx dhkey))))) ((send (enc gx b (privk ca-0))))) (label 16) (parent 9) (realized) (shape) (maps ((0) ((gx gx) (h gx) (dhkey dhkey) (a a) (b a) (ca ca) (n n)))) (origs)) (defskeleton dhca (vars (dhkey skey) (n text) (gx akey) (a ca a-0 b ca-0 name)) (defstrand init 4 (dhkey dhkey) (n n) (gx gx) (h gx) (a a) (b a) (ca ca)) (defstrand ca 1 (gz gx) (subject a) (ca ca)) (defstrand resp 3 (dhkey dhkey) (n n) (gy gx) (h gx) (a a-0) (b b) (ca ca-0)) (defstrand ca 1 (gz gx) (subject b) (ca ca-0)) (defstrand ca 1 (gz gx) (subject a-0) (ca ca-0)) (precedes ((1 0) (0 0)) ((2 2) (0 2)) ((3 0) (2 0)) ((4 0) (2 1))) (non-orig dhkey (invk gx) (privk ca) (privk ca-0)) (operation encryption-test (added-strand ca 1) (enc gx a-0 (privk ca-0)) (2 1)) (traces ((recv (enc gx a (privk ca))) (send (cat gx (enc gx a (privk ca)))) (recv (cat gx (enc gx a (privk ca)) (enc n (enc "dh" gx gx dhkey)))) (send (enc "check" n (enc "dh" gx gx dhkey)))) ((send (enc gx a (privk ca)))) ((recv (enc gx b (privk ca-0))) (recv (cat gx (enc gx a-0 (privk ca-0)))) (send (cat gx (enc gx b (privk ca-0)) (enc n (enc "dh" gx gx dhkey))))) ((send (enc gx b (privk ca-0)))) ((send (enc gx a-0 (privk ca-0))))) (label 17) (parent 9) (realized) (shape) (maps ((0) ((gx gx) (h gx) (dhkey dhkey) (a a) (b a) (ca ca) (n n)))) (origs)) (defskeleton dhca (vars (dhkey skey) (n text) (gx akey) (a b ca name)) (defstrand init 4 (dhkey dhkey) (n n) (gx gx) (h gx) (a a) (b b) (ca ca)) (defstrand ca 1 (gz gx) (subject a) (ca ca)) (defstrand ca 1 (gz gx) (subject b) (ca ca)) (defstrand resp 3 (dhkey dhkey) (n n) (gy gx) (h gx) (a a) (b a) (ca ca)) (precedes ((1 0) (0 0)) ((1 0) (3 0)) ((2 0) (0 2)) ((3 2) (0 2))) (non-orig dhkey (invk gx) (privk ca)) (operation encryption-test (displaced 4 1 ca 1) (enc gx a-0 (privk ca)) (3 1)) (traces ((recv (enc gx a (privk ca))) (send (cat gx (enc gx a (privk ca)))) (recv (cat gx (enc gx b (privk ca)) (enc n (enc "dh" gx gx dhkey)))) (send (enc "check" n (enc "dh" gx gx dhkey)))) ((send (enc gx a (privk ca)))) ((send (enc gx b (privk ca)))) ((recv (enc gx a (privk ca))) (recv (cat gx (enc gx a (privk ca)))) (send (cat gx (enc gx a (privk ca)) (enc n (enc "dh" gx gx dhkey)))))) (label 18) (parent 10) (realized) (shape) (maps ((0) ((gx gx) (h gx) (dhkey dhkey) (a a) (b b) (ca ca) (n n)))) (origs)) (defskeleton dhca (vars (dhkey skey) (n text) (gx akey) (a b ca name)) (defstrand init 4 (dhkey dhkey) (n n) (gx gx) (h gx) (a a) (b b) (ca ca)) (defstrand ca 1 (gz gx) (subject a) (ca ca)) (defstrand ca 1 (gz gx) (subject b) (ca ca)) (defstrand resp 3 (dhkey dhkey) (n n) (gy gx) (h gx) (a b) (b a) (ca ca)) (precedes ((1 0) (0 0)) ((1 0) (3 0)) ((2 0) (3 1)) ((3 2) (0 2))) (non-orig dhkey (invk gx) (privk ca)) (operation encryption-test (displaced 4 2 ca 1) (enc gx a-0 (privk ca)) (3 1)) (traces ((recv (enc gx a (privk ca))) (send (cat gx (enc gx a (privk ca)))) (recv (cat gx (enc gx b (privk ca)) (enc n (enc "dh" gx gx dhkey)))) (send (enc "check" n (enc "dh" gx gx dhkey)))) ((send (enc gx a (privk ca)))) ((send (enc gx b (privk ca)))) ((recv (enc gx a (privk ca))) (recv (cat gx (enc gx b (privk ca)))) (send (cat gx (enc gx a (privk ca)) (enc n (enc "dh" gx gx dhkey)))))) (label 19) (parent 10) (realized) (shape) (maps ((0) ((gx gx) (h gx) (dhkey dhkey) (a a) (b b) (ca ca) (n n)))) (origs)) (defskeleton dhca (vars (dhkey skey) (n text) (gx akey) (a b ca a-0 name)) (defstrand init 4 (dhkey dhkey) (n n) (gx gx) (h gx) (a a) (b b) (ca ca)) (defstrand ca 1 (gz gx) (subject a) (ca ca)) (defstrand ca 1 (gz gx) (subject b) (ca ca)) (defstrand resp 3 (dhkey dhkey) (n n) (gy gx) (h gx) (a a-0) (b a) (ca ca)) (defstrand ca 1 (gz gx) (subject a-0) (ca ca)) (precedes ((1 0) (0 0)) ((1 0) (3 0)) ((2 0) (0 2)) ((3 2) (0 2)) ((4 0) (3 1))) (non-orig dhkey (invk gx) (privk ca)) (operation encryption-test (added-strand ca 1) (enc gx a-0 (privk ca)) (3 1)) (traces ((recv (enc gx a (privk ca))) (send (cat gx (enc gx a (privk ca)))) (recv (cat gx (enc gx b (privk ca)) (enc n (enc "dh" gx gx dhkey)))) (send (enc "check" n (enc "dh" gx gx dhkey)))) ((send (enc gx a (privk ca)))) ((send (enc gx b (privk ca)))) ((recv (enc gx a (privk ca))) (recv (cat gx (enc gx a-0 (privk ca)))) (send (cat gx (enc gx a (privk ca)) (enc n (enc "dh" gx gx dhkey))))) ((send (enc gx a-0 (privk ca))))) (label 20) (parent 10) (realized) (shape) (maps ((0) ((gx gx) (h gx) (dhkey dhkey) (a a) (b b) (ca ca) (n n)))) (origs)) (defskeleton dhca (vars (dhkey skey) (n text) (gx h akey) (a b ca name)) (defstrand init 4 (dhkey dhkey) (n n) (gx gx) (h h) (a a) (b b) (ca ca)) (defstrand ca 1 (gz gx) (subject a) (ca ca)) (defstrand ca 1 (gz h) (subject b) (ca ca)) (defstrand resp 3 (dhkey dhkey) (n n) (gy h) (h gx) (a a) (b b) (ca ca)) (precedes ((1 0) (0 0)) ((1 0) (3 1)) ((2 0) (3 0)) ((3 2) (0 2))) (non-orig dhkey (invk gx) (invk h) (privk ca)) (operation encryption-test (displaced 4 1 ca 1) (enc gx a-0 (privk ca)) (3 1)) (traces ((recv (enc gx a (privk ca))) (send (cat gx (enc gx a (privk ca)))) (recv (cat h (enc h b (privk ca)) (enc n (enc "dh" gx h dhkey)))) (send (enc "check" n (enc "dh" gx h dhkey)))) ((send (enc gx a (privk ca)))) ((send (enc h b (privk ca)))) ((recv (enc h b (privk ca))) (recv (cat gx (enc gx a (privk ca)))) (send (cat h (enc h b (privk ca)) (enc n (enc "dh" gx h dhkey)))))) (label 21) (parent 11) (realized) (shape) (maps ((0) ((gx gx) (h h) (dhkey dhkey) (a a) (b b) (ca ca) (n n)))) (origs)) (defskeleton dhca (vars (dhkey skey) (n text) (h akey) (a b ca name)) (defstrand init 4 (dhkey dhkey) (n n) (gx h) (h h) (a a) (b b) (ca ca)) (defstrand ca 1 (gz h) (subject a) (ca ca)) (defstrand ca 1 (gz h) (subject b) (ca ca)) (defstrand resp 3 (dhkey dhkey) (n n) (gy h) (h h) (a b) (b b) (ca ca)) (precedes ((1 0) (0 0)) ((2 0) (3 0)) ((3 2) (0 2))) (non-orig dhkey (invk h) (privk ca)) (operation encryption-test (displaced 4 2 ca 1) (enc gx a-0 (privk ca)) (3 1)) (traces ((recv (enc h a (privk ca))) (send (cat h (enc h a (privk ca)))) (recv (cat h (enc h b (privk ca)) (enc n (enc "dh" h h dhkey)))) (send (enc "check" n (enc "dh" h h dhkey)))) ((send (enc h a (privk ca)))) ((send (enc h b (privk ca)))) ((recv (enc h b (privk ca))) (recv (cat h (enc h b (privk ca)))) (send (cat h (enc h b (privk ca)) (enc n (enc "dh" h h dhkey)))))) (label 22) (parent 11) (realized) (shape) (maps ((0) ((gx h) (h h) (dhkey dhkey) (a a) (b b) (ca ca) (n n)))) (origs)) (defskeleton dhca (vars (dhkey skey) (n text) (gx h akey) (a b ca a-0 name)) (defstrand init 4 (dhkey dhkey) (n n) (gx gx) (h h) (a a) (b b) (ca ca)) (defstrand ca 1 (gz gx) (subject a) (ca ca)) (defstrand ca 1 (gz h) (subject b) (ca ca)) (defstrand resp 3 (dhkey dhkey) (n n) (gy h) (h gx) (a a-0) (b b) (ca ca)) (defstrand ca 1 (gz gx) (subject a-0) (ca ca)) (precedes ((1 0) (0 0)) ((2 0) (3 0)) ((3 2) (0 2)) ((4 0) (3 1))) (non-orig dhkey (invk gx) (invk h) (privk ca)) (operation encryption-test (added-strand ca 1) (enc gx a-0 (privk ca)) (3 1)) (traces ((recv (enc gx a (privk ca))) (send (cat gx (enc gx a (privk ca)))) (recv (cat h (enc h b (privk ca)) (enc n (enc "dh" gx h dhkey)))) (send (enc "check" n (enc "dh" gx h dhkey)))) ((send (enc gx a (privk ca)))) ((send (enc h b (privk ca)))) ((recv (enc h b (privk ca))) (recv (cat gx (enc gx a-0 (privk ca)))) (send (cat h (enc h b (privk ca)) (enc n (enc "dh" gx h dhkey))))) ((send (enc gx a-0 (privk ca))))) (label 23) (parent 11) (realized) (shape) (maps ((0) ((gx gx) (h h) (dhkey dhkey) (a a) (b b) (ca ca) (n n)))) (origs)) (defskeleton dhca (vars (dhkey skey) (n text) (h akey) (a b ca b-0 name)) (defstrand init 4 (dhkey dhkey) (n n) (gx h) (h h) (a a) (b b) (ca ca)) (defstrand ca 1 (gz h) (subject a) (ca ca)) (defstrand ca 1 (gz h) (subject b) (ca ca)) (defstrand resp 3 (dhkey dhkey) (n n) (gy h) (h h) (a b) (b b-0) (ca ca)) (defstrand ca 1 (gz h) (subject b-0) (ca ca)) (precedes ((1 0) (0 0)) ((2 0) (3 1)) ((3 2) (0 2)) ((4 0) (3 0))) (non-orig dhkey (invk h) (privk ca)) (operation encryption-test (displaced 5 2 ca 1) (enc gx a-0 (privk ca-0)) (3 1)) (traces ((recv (enc h a (privk ca))) (send (cat h (enc h a (privk ca)))) (recv (cat h (enc h b (privk ca)) (enc n (enc "dh" h h dhkey)))) (send (enc "check" n (enc "dh" h h dhkey)))) ((send (enc h a (privk ca)))) ((send (enc h b (privk ca)))) ((recv (enc h b-0 (privk ca))) (recv (cat h (enc h b (privk ca)))) (send (cat h (enc h b-0 (privk ca)) (enc n (enc "dh" h h dhkey))))) ((send (enc h b-0 (privk ca))))) (label 24) (parent 12) (realized) (shape) (maps ((0) ((gx h) (h h) (dhkey dhkey) (a a) (b b) (ca ca) (n n)))) (origs)) (defskeleton dhca (vars (dhkey skey) (n text) (gx h akey) (a b ca b-0 name)) (defstrand init 4 (dhkey dhkey) (n n) (gx gx) (h h) (a a) (b b) (ca ca)) (defstrand ca 1 (gz gx) (subject a) (ca ca)) (defstrand ca 1 (gz h) (subject b) (ca ca)) (defstrand resp 3 (dhkey dhkey) (n n) (gy h) (h gx) (a a) (b b-0) (ca ca)) (defstrand ca 1 (gz h) (subject b-0) (ca ca)) (precedes ((1 0) (0 0)) ((1 0) (3 1)) ((2 0) (0 2)) ((3 2) (0 2)) ((4 0) (3 0))) (non-orig dhkey (invk gx) (invk h) (privk ca)) (operation encryption-test (displaced 5 1 ca 1) (enc gx a-0 (privk ca-0)) (3 1)) (traces ((recv (enc gx a (privk ca))) (send (cat gx (enc gx a (privk ca)))) (recv (cat h (enc h b (privk ca)) (enc n (enc "dh" gx h dhkey)))) (send (enc "check" n (enc "dh" gx h dhkey)))) ((send (enc gx a (privk ca)))) ((send (enc h b (privk ca)))) ((recv (enc h b-0 (privk ca))) (recv (cat gx (enc gx a (privk ca)))) (send (cat h (enc h b-0 (privk ca)) (enc n (enc "dh" gx h dhkey))))) ((send (enc h b-0 (privk ca))))) (label 25) (parent 12) (realized) (shape) (maps ((0) ((gx gx) (h h) (dhkey dhkey) (a a) (b b) (ca ca) (n n)))) (origs)) (defskeleton dhca (vars (dhkey skey) (n text) (h akey) (a b ca b-0 ca-0 name)) (defstrand init 4 (dhkey dhkey) (n n) (gx h) (h h) (a a) (b b) (ca ca)) (defstrand ca 1 (gz h) (subject a) (ca ca)) (defstrand ca 1 (gz h) (subject b) (ca ca)) (defstrand resp 3 (dhkey dhkey) (n n) (gy h) (h h) (a b-0) (b b-0) (ca ca-0)) (defstrand ca 1 (gz h) (subject b-0) (ca ca-0)) (precedes ((1 0) (0 0)) ((2 0) (0 2)) ((3 2) (0 2)) ((4 0) (3 0))) (non-orig dhkey (invk h) (privk ca) (privk ca-0)) (operation encryption-test (displaced 5 4 ca 1) (enc gx a-0 (privk ca-0)) (3 1)) (traces ((recv (enc h a (privk ca))) (send (cat h (enc h a (privk ca)))) (recv (cat h (enc h b (privk ca)) (enc n (enc "dh" h h dhkey)))) (send (enc "check" n (enc "dh" h h dhkey)))) ((send (enc h a (privk ca)))) ((send (enc h b (privk ca)))) ((recv (enc h b-0 (privk ca-0))) (recv (cat h (enc h b-0 (privk ca-0)))) (send (cat h (enc h b-0 (privk ca-0)) (enc n (enc "dh" h h dhkey))))) ((send (enc h b-0 (privk ca-0))))) (label 26) (parent 12) (realized) (shape) (maps ((0) ((gx h) (h h) (dhkey dhkey) (a a) (b b) (ca ca) (n n)))) (origs)) (defskeleton dhca (vars (dhkey skey) (n text) (gx h akey) (a b ca a-0 b-0 ca-0 name)) (defstrand init 4 (dhkey dhkey) (n n) (gx gx) (h h) (a a) (b b) (ca ca)) (defstrand ca 1 (gz gx) (subject a) (ca ca)) (defstrand ca 1 (gz h) (subject b) (ca ca)) (defstrand resp 3 (dhkey dhkey) (n n) (gy h) (h gx) (a a-0) (b b-0) (ca ca-0)) (defstrand ca 1 (gz h) (subject b-0) (ca ca-0)) (defstrand ca 1 (gz gx) (subject a-0) (ca ca-0)) (precedes ((1 0) (0 0)) ((2 0) (0 2)) ((3 2) (0 2)) ((4 0) (3 0)) ((5 0) (3 1))) (non-orig dhkey (invk gx) (invk h) (privk ca) (privk ca-0)) (operation encryption-test (added-strand ca 1) (enc gx a-0 (privk ca-0)) (3 1)) (traces ((recv (enc gx a (privk ca))) (send (cat gx (enc gx a (privk ca)))) (recv (cat h (enc h b (privk ca)) (enc n (enc "dh" gx h dhkey)))) (send (enc "check" n (enc "dh" gx h dhkey)))) ((send (enc gx a (privk ca)))) ((send (enc h b (privk ca)))) ((recv (enc h b-0 (privk ca-0))) (recv (cat gx (enc gx a-0 (privk ca-0)))) (send (cat h (enc h b-0 (privk ca-0)) (enc n (enc "dh" gx h dhkey))))) ((send (enc h b-0 (privk ca-0)))) ((send (enc gx a-0 (privk ca-0))))) (label 27) (parent 12) (realized) (shape) (maps ((0) ((gx gx) (h h) (dhkey dhkey) (a a) (b b) (ca ca) (n n)))) (origs)) (comment "Nothing left to do") (defprotocol dhca basic (defrole init (vars (gx h akey) (dhkey skey) (a b ca name) (n text)) (trace (recv (enc gx a (privk ca))) (send (cat gx (enc gx a (privk ca)))) (recv (cat h (enc h b (privk ca)) (enc n (enc "dh" gx h dhkey)))) (send (enc "check" n (enc "dh" gx h dhkey)))) (non-orig dhkey (privk ca))) (defrole resp (vars (gy h akey) (dhkey skey) (a b ca name) (n text)) (trace (recv (enc gy b (privk ca))) (recv (cat h (enc h a (privk ca)))) (send (cat gy (enc gy b (privk ca)) (enc n (enc "dh" h gy dhkey)))) (recv (enc "check" n (enc "dh" h gy dhkey)))) (non-orig dhkey (privk ca))) (defrole ca (vars (subject ca name) (gz akey)) (trace (send (enc gz subject (privk ca)))) (non-orig (invk gz))) (defrole CDHcalc1 (vars (gx gy akey) (dhkey skey)) (trace (recv (cat gx (invk gy))) (send (enc "dh" gx gy dhkey)))) (defrole CDHcalc2 (vars (gx gy akey) (dhkey skey)) (trace (recv (cat gy (invk gx))) (send (enc "dh" gx gy dhkey)))) (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 dhca (vars (dhkey skey) (n text) (gy h akey) (a b ca name)) (defstrand resp 4 (dhkey dhkey) (n n) (gy gy) (h h) (a a) (b b) (ca ca)) (non-orig dhkey (privk ca)) (uniq-orig n) (comment "Full responder point of view with freshly chosen n") (traces ((recv (enc gy b (privk ca))) (recv (cat h (enc h a (privk ca)))) (send (cat gy (enc gy b (privk ca)) (enc n (enc "dh" h gy dhkey)))) (recv (enc "check" n (enc "dh" h gy dhkey))))) (label 28) (unrealized (0 0) (0 1) (0 3)) (origs (n (0 2))) (comment "1 in cohort - 1 not yet seen")) (defskeleton dhca (vars (dhkey skey) (n text) (gy h akey) (a b ca name)) (defstrand resp 4 (dhkey dhkey) (n n) (gy gy) (h h) (a a) (b b) (ca ca)) (defstrand ca 1 (gz gy) (subject b) (ca ca)) (precedes ((1 0) (0 0))) (non-orig dhkey (invk gy) (privk ca)) (uniq-orig n) (operation encryption-test (added-strand ca 1) (enc gy b (privk ca)) (0 0)) (traces ((recv (enc gy b (privk ca))) (recv (cat h (enc h a (privk ca)))) (send (cat gy (enc gy b (privk ca)) (enc n (enc "dh" h gy dhkey)))) (recv (enc "check" n (enc "dh" h gy dhkey)))) ((send (enc gy b (privk ca))))) (label 29) (parent 28) (unrealized (0 1) (0 3)) (comment "2 in cohort - 2 not yet seen")) (defskeleton dhca (vars (dhkey skey) (n text) (gy akey) (b ca name)) (defstrand resp 4 (dhkey dhkey) (n n) (gy gy) (h gy) (a b) (b b) (ca ca)) (defstrand ca 1 (gz gy) (subject b) (ca ca)) (precedes ((1 0) (0 0))) (non-orig dhkey (invk gy) (privk ca)) (uniq-orig n) (operation encryption-test (displaced 2 1 ca 1) (enc h a (privk ca)) (0 1)) (traces ((recv (enc gy b (privk ca))) (recv (cat gy (enc gy b (privk ca)))) (send (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gy gy dhkey)))) (recv (enc "check" n (enc "dh" gy gy dhkey)))) ((send (enc gy b (privk ca))))) (label 30) (parent 29) (unrealized (0 3)) (comment "2 in cohort - 2 not yet seen")) (defskeleton dhca (vars (dhkey skey) (n text) (gy h akey) (a b ca name)) (defstrand resp 4 (dhkey dhkey) (n n) (gy gy) (h h) (a a) (b b) (ca ca)) (defstrand ca 1 (gz gy) (subject b) (ca ca)) (defstrand ca 1 (gz h) (subject a) (ca ca)) (precedes ((1 0) (0 0)) ((2 0) (0 1))) (non-orig dhkey (invk gy) (invk h) (privk ca)) (uniq-orig n) (operation encryption-test (added-strand ca 1) (enc h a (privk ca)) (0 1)) (traces ((recv (enc gy b (privk ca))) (recv (cat h (enc h a (privk ca)))) (send (cat gy (enc gy b (privk ca)) (enc n (enc "dh" h gy dhkey)))) (recv (enc "check" n (enc "dh" h gy dhkey)))) ((send (enc gy b (privk ca)))) ((send (enc h a (privk ca))))) (label 31) (parent 29) (unrealized (0 3)) (comment "2 in cohort - 2 not yet seen")) (defskeleton dhca (vars (dhkey skey) (n text) (gy akey) (b ca a b-0 ca-0 name)) (defstrand resp 4 (dhkey dhkey) (n n) (gy gy) (h gy) (a b) (b b) (ca ca)) (defstrand ca 1 (gz gy) (subject b) (ca ca)) (defstrand init 4 (dhkey dhkey) (n n) (gx gy) (h gy) (a a) (b b-0) (ca ca-0)) (precedes ((0 2) (2 2)) ((1 0) (0 0)) ((2 3) (0 3))) (non-orig dhkey (invk gy) (privk ca) (privk ca-0)) (uniq-orig n) (operation encryption-test (added-strand init 4) (enc "check" n (enc "dh" gy gy dhkey)) (0 3)) (traces ((recv (enc gy b (privk ca))) (recv (cat gy (enc gy b (privk ca)))) (send (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gy gy dhkey)))) (recv (enc "check" n (enc "dh" gy gy dhkey)))) ((send (enc gy b (privk ca)))) ((recv (enc gy a (privk ca-0))) (send (cat gy (enc gy a (privk ca-0)))) (recv (cat gy (enc gy b-0 (privk ca-0)) (enc n (enc "dh" gy gy dhkey)))) (send (enc "check" n (enc "dh" gy gy dhkey))))) (label 32) (parent 30) (unrealized (2 0) (2 2)) (comment "2 in cohort - 2 not yet seen")) (defskeleton dhca (vars (dhkey skey) (n text) (gy akey) (b ca name)) (defstrand resp 4 (dhkey dhkey) (n n) (gy gy) (h gy) (a b) (b b) (ca ca)) (defstrand ca 1 (gz gy) (subject b) (ca ca)) (deflistener (enc "dh" gy gy dhkey)) (precedes ((1 0) (0 0)) ((2 1) (0 3))) (non-orig dhkey (invk gy) (privk ca)) (uniq-orig n) (operation encryption-test (added-listener (enc "dh" gy gy dhkey)) (enc "check" n (enc "dh" gy gy dhkey)) (0 3)) (traces ((recv (enc gy b (privk ca))) (recv (cat gy (enc gy b (privk ca)))) (send (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gy gy dhkey)))) (recv (enc "check" n (enc "dh" gy gy dhkey)))) ((send (enc gy b (privk ca)))) ((recv (enc "dh" gy gy dhkey)) (send (enc "dh" gy gy dhkey)))) (label 33) (parent 30) (unrealized (2 0)) (dead) (comment "empty cohort")) (defskeleton dhca (vars (dhkey skey) (n text) (gy h akey) (a b ca a-0 b-0 ca-0 name)) (defstrand resp 4 (dhkey dhkey) (n n) (gy gy) (h h) (a a) (b b) (ca ca)) (defstrand ca 1 (gz gy) (subject b) (ca ca)) (defstrand ca 1 (gz h) (subject a) (ca ca)) (defstrand init 4 (dhkey dhkey) (n n) (gx h) (h gy) (a a-0) (b b-0) (ca ca-0)) (precedes ((0 2) (3 2)) ((1 0) (0 0)) ((2 0) (0 1)) ((3 3) (0 3))) (non-orig dhkey (invk gy) (invk h) (privk ca) (privk ca-0)) (uniq-orig n) (operation encryption-test (added-strand init 4) (enc "check" n (enc "dh" h gy dhkey)) (0 3)) (traces ((recv (enc gy b (privk ca))) (recv (cat h (enc h a (privk ca)))) (send (cat gy (enc gy b (privk ca)) (enc n (enc "dh" h gy dhkey)))) (recv (enc "check" n (enc "dh" h gy dhkey)))) ((send (enc gy b (privk ca)))) ((send (enc h a (privk ca)))) ((recv (enc h a-0 (privk ca-0))) (send (cat h (enc h a-0 (privk ca-0)))) (recv (cat gy (enc gy b-0 (privk ca-0)) (enc n (enc "dh" h gy dhkey)))) (send (enc "check" n (enc "dh" h gy dhkey))))) (label 34) (parent 31) (unrealized (3 0) (3 2)) (comment "3 in cohort - 3 not yet seen")) (defskeleton dhca (vars (dhkey skey) (n text) (gy h akey) (a b ca name)) (defstrand resp 4 (dhkey dhkey) (n n) (gy gy) (h h) (a a) (b b) (ca ca)) (defstrand ca 1 (gz gy) (subject b) (ca ca)) (defstrand ca 1 (gz h) (subject a) (ca ca)) (deflistener (enc "dh" h gy dhkey)) (precedes ((1 0) (0 0)) ((2 0) (0 1)) ((3 1) (0 3))) (non-orig dhkey (invk gy) (invk h) (privk ca)) (uniq-orig n) (operation encryption-test (added-listener (enc "dh" h gy dhkey)) (enc "check" n (enc "dh" h gy dhkey)) (0 3)) (traces ((recv (enc gy b (privk ca))) (recv (cat h (enc h a (privk ca)))) (send (cat gy (enc gy b (privk ca)) (enc n (enc "dh" h gy dhkey)))) (recv (enc "check" n (enc "dh" h gy dhkey)))) ((send (enc gy b (privk ca)))) ((send (enc h a (privk ca)))) ((recv (enc "dh" h gy dhkey)) (send (enc "dh" h gy dhkey)))) (label 35) (parent 31) (unrealized (3 0)) (dead) (comment "empty cohort")) (defskeleton dhca (vars (dhkey skey) (n text) (gy akey) (b ca b-0 name)) (defstrand resp 4 (dhkey dhkey) (n n) (gy gy) (h gy) (a b) (b b) (ca ca)) (defstrand ca 1 (gz gy) (subject b) (ca ca)) (defstrand init 4 (dhkey dhkey) (n n) (gx gy) (h gy) (a b) (b b-0) (ca ca)) (precedes ((0 2) (2 2)) ((1 0) (0 0)) ((1 0) (2 0)) ((2 3) (0 3))) (non-orig dhkey (invk gy) (privk ca)) (uniq-orig n) (operation encryption-test (displaced 3 1 ca 1) (enc gy a (privk ca-0)) (2 0)) (traces ((recv (enc gy b (privk ca))) (recv (cat gy (enc gy b (privk ca)))) (send (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gy gy dhkey)))) (recv (enc "check" n (enc "dh" gy gy dhkey)))) ((send (enc gy b (privk ca)))) ((recv (enc gy b (privk ca))) (send (cat gy (enc gy b (privk ca)))) (recv (cat gy (enc gy b-0 (privk ca)) (enc n (enc "dh" gy gy dhkey)))) (send (enc "check" n (enc "dh" gy gy dhkey))))) (label 36) (parent 32) (unrealized (2 2)) (comment "2 in cohort - 2 not yet seen")) (defskeleton dhca (vars (dhkey skey) (n text) (gy akey) (b ca a b-0 ca-0 name)) (defstrand resp 4 (dhkey dhkey) (n n) (gy gy) (h gy) (a b) (b b) (ca ca)) (defstrand ca 1 (gz gy) (subject b) (ca ca)) (defstrand init 4 (dhkey dhkey) (n n) (gx gy) (h gy) (a a) (b b-0) (ca ca-0)) (defstrand ca 1 (gz gy) (subject a) (ca ca-0)) (precedes ((0 2) (2 2)) ((1 0) (0 0)) ((2 3) (0 3)) ((3 0) (2 0))) (non-orig dhkey (invk gy) (privk ca) (privk ca-0)) (uniq-orig n) (operation encryption-test (added-strand ca 1) (enc gy a (privk ca-0)) (2 0)) (traces ((recv (enc gy b (privk ca))) (recv (cat gy (enc gy b (privk ca)))) (send (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gy gy dhkey)))) (recv (enc "check" n (enc "dh" gy gy dhkey)))) ((send (enc gy b (privk ca)))) ((recv (enc gy a (privk ca-0))) (send (cat gy (enc gy a (privk ca-0)))) (recv (cat gy (enc gy b-0 (privk ca-0)) (enc n (enc "dh" gy gy dhkey)))) (send (enc "check" n (enc "dh" gy gy dhkey)))) ((send (enc gy a (privk ca-0))))) (label 37) (parent 32) (unrealized (2 2)) (comment "3 in cohort - 3 not yet seen")) (defskeleton dhca (vars (dhkey skey) (n text) (gy akey) (a b ca b-0 name)) (defstrand resp 4 (dhkey dhkey) (n n) (gy gy) (h gy) (a a) (b b) (ca ca)) (defstrand ca 1 (gz gy) (subject b) (ca ca)) (defstrand ca 1 (gz gy) (subject a) (ca ca)) (defstrand init 4 (dhkey dhkey) (n n) (gx gy) (h gy) (a b) (b b-0) (ca ca)) (precedes ((0 2) (3 2)) ((1 0) (0 0)) ((1 0) (3 0)) ((2 0) (0 1)) ((3 3) (0 3))) (non-orig dhkey (invk gy) (privk ca)) (uniq-orig n) (operation encryption-test (displaced 4 1 ca 1) (enc h a-0 (privk ca-0)) (3 0)) (traces ((recv (enc gy b (privk ca))) (recv (cat gy (enc gy a (privk ca)))) (send (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gy gy dhkey)))) (recv (enc "check" n (enc "dh" gy gy dhkey)))) ((send (enc gy b (privk ca)))) ((send (enc gy a (privk ca)))) ((recv (enc gy b (privk ca))) (send (cat gy (enc gy b (privk ca)))) (recv (cat gy (enc gy b-0 (privk ca)) (enc n (enc "dh" gy gy dhkey)))) (send (enc "check" n (enc "dh" gy gy dhkey))))) (label 38) (parent 34) (unrealized (3 2)) (comment "3 in cohort - 3 not yet seen")) (defskeleton dhca (vars (dhkey skey) (n text) (gy h akey) (a b ca b-0 name)) (defstrand resp 4 (dhkey dhkey) (n n) (gy gy) (h h) (a a) (b b) (ca ca)) (defstrand ca 1 (gz gy) (subject b) (ca ca)) (defstrand ca 1 (gz h) (subject a) (ca ca)) (defstrand init 4 (dhkey dhkey) (n n) (gx h) (h gy) (a a) (b b-0) (ca ca)) (precedes ((0 2) (3 2)) ((1 0) (0 0)) ((2 0) (0 1)) ((2 0) (3 0)) ((3 3) (0 3))) (non-orig dhkey (invk gy) (invk h) (privk ca)) (uniq-orig n) (operation encryption-test (displaced 4 2 ca 1) (enc h a-0 (privk ca-0)) (3 0)) (traces ((recv (enc gy b (privk ca))) (recv (cat h (enc h a (privk ca)))) (send (cat gy (enc gy b (privk ca)) (enc n (enc "dh" h gy dhkey)))) (recv (enc "check" n (enc "dh" h gy dhkey)))) ((send (enc gy b (privk ca)))) ((send (enc h a (privk ca)))) ((recv (enc h a (privk ca))) (send (cat h (enc h a (privk ca)))) (recv (cat gy (enc gy b-0 (privk ca)) (enc n (enc "dh" h gy dhkey)))) (send (enc "check" n (enc "dh" h gy dhkey))))) (label 39) (parent 34) (unrealized (3 2)) (comment "3 in cohort - 3 not yet seen")) (defskeleton dhca (vars (dhkey skey) (n text) (gy h akey) (a b ca a-0 b-0 ca-0 name)) (defstrand resp 4 (dhkey dhkey) (n n) (gy gy) (h h) (a a) (b b) (ca ca)) (defstrand ca 1 (gz gy) (subject b) (ca ca)) (defstrand ca 1 (gz h) (subject a) (ca ca)) (defstrand init 4 (dhkey dhkey) (n n) (gx h) (h gy) (a a-0) (b b-0) (ca ca-0)) (defstrand ca 1 (gz h) (subject a-0) (ca ca-0)) (precedes ((0 2) (3 2)) ((1 0) (0 0)) ((2 0) (0 1)) ((3 3) (0 3)) ((4 0) (3 0))) (non-orig dhkey (invk gy) (invk h) (privk ca) (privk ca-0)) (uniq-orig n) (operation encryption-test (added-strand ca 1) (enc h a-0 (privk ca-0)) (3 0)) (traces ((recv (enc gy b (privk ca))) (recv (cat h (enc h a (privk ca)))) (send (cat gy (enc gy b (privk ca)) (enc n (enc "dh" h gy dhkey)))) (recv (enc "check" n (enc "dh" h gy dhkey)))) ((send (enc gy b (privk ca)))) ((send (enc h a (privk ca)))) ((recv (enc h a-0 (privk ca-0))) (send (cat h (enc h a-0 (privk ca-0)))) (recv (cat gy (enc gy b-0 (privk ca-0)) (enc n (enc "dh" h gy dhkey)))) (send (enc "check" n (enc "dh" h gy dhkey)))) ((send (enc h a-0 (privk ca-0))))) (label 40) (parent 34) (unrealized (3 2)) (comment "4 in cohort - 4 not yet seen")) (defskeleton dhca (vars (dhkey skey) (n text) (gy akey) (b ca name)) (defstrand resp 4 (dhkey dhkey) (n n) (gy gy) (h gy) (a b) (b b) (ca ca)) (defstrand ca 1 (gz gy) (subject b) (ca ca)) (defstrand init 4 (dhkey dhkey) (n n) (gx gy) (h gy) (a b) (b b) (ca ca)) (precedes ((0 2) (2 2)) ((1 0) (0 0)) ((1 0) (2 0)) ((2 3) (0 3))) (non-orig dhkey (invk gy) (privk ca)) (uniq-orig n) (operation encryption-test (displaced 3 1 ca 1) (enc gy b-0 (privk ca)) (2 2)) (traces ((recv (enc gy b (privk ca))) (recv (cat gy (enc gy b (privk ca)))) (send (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gy gy dhkey)))) (recv (enc "check" n (enc "dh" gy gy dhkey)))) ((send (enc gy b (privk ca)))) ((recv (enc gy b (privk ca))) (send (cat gy (enc gy b (privk ca)))) (recv (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gy gy dhkey)))) (send (enc "check" n (enc "dh" gy gy dhkey))))) (label 41) (parent 36) (realized) (shape) (maps ((0) ((n n) (gy gy) (h gy) (dhkey dhkey) (a b) (b b) (ca ca)))) (origs (n (0 2)))) (defskeleton dhca (vars (dhkey skey) (n text) (gy akey) (b ca b-0 name)) (defstrand resp 4 (dhkey dhkey) (n n) (gy gy) (h gy) (a b) (b b) (ca ca)) (defstrand ca 1 (gz gy) (subject b) (ca ca)) (defstrand init 4 (dhkey dhkey) (n n) (gx gy) (h gy) (a b) (b b-0) (ca ca)) (defstrand ca 1 (gz gy) (subject b-0) (ca ca)) (precedes ((0 2) (2 2)) ((1 0) (0 0)) ((1 0) (2 0)) ((2 3) (0 3)) ((3 0) (2 2))) (non-orig dhkey (invk gy) (privk ca)) (uniq-orig n) (operation encryption-test (added-strand ca 1) (enc gy b-0 (privk ca)) (2 2)) (traces ((recv (enc gy b (privk ca))) (recv (cat gy (enc gy b (privk ca)))) (send (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gy gy dhkey)))) (recv (enc "check" n (enc "dh" gy gy dhkey)))) ((send (enc gy b (privk ca)))) ((recv (enc gy b (privk ca))) (send (cat gy (enc gy b (privk ca)))) (recv (cat gy (enc gy b-0 (privk ca)) (enc n (enc "dh" gy gy dhkey)))) (send (enc "check" n (enc "dh" gy gy dhkey)))) ((send (enc gy b-0 (privk ca))))) (label 42) (parent 36) (realized) (shape) (maps ((0) ((n n) (gy gy) (h gy) (dhkey dhkey) (a b) (b b) (ca ca)))) (origs (n (0 2)))) (defskeleton dhca (vars (dhkey skey) (n text) (gy akey) (b ca a name)) (defstrand resp 4 (dhkey dhkey) (n n) (gy gy) (h gy) (a b) (b b) (ca ca)) (defstrand ca 1 (gz gy) (subject b) (ca ca)) (defstrand init 4 (dhkey dhkey) (n n) (gx gy) (h gy) (a a) (b b) (ca ca)) (defstrand ca 1 (gz gy) (subject a) (ca ca)) (precedes ((0 2) (2 2)) ((1 0) (0 0)) ((2 3) (0 3)) ((3 0) (2 0))) (non-orig dhkey (invk gy) (privk ca)) (uniq-orig n) (operation encryption-test (displaced 4 1 ca 1) (enc gy b-0 (privk ca-0)) (2 2)) (traces ((recv (enc gy b (privk ca))) (recv (cat gy (enc gy b (privk ca)))) (send (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gy gy dhkey)))) (recv (enc "check" n (enc "dh" gy gy dhkey)))) ((send (enc gy b (privk ca)))) ((recv (enc gy a (privk ca))) (send (cat gy (enc gy a (privk ca)))) (recv (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gy gy dhkey)))) (send (enc "check" n (enc "dh" gy gy dhkey)))) ((send (enc gy a (privk ca))))) (label 43) (parent 37) (realized) (shape) (maps ((0) ((n n) (gy gy) (h gy) (dhkey dhkey) (a b) (b b) (ca ca)))) (origs (n (0 2)))) (defskeleton dhca (vars (dhkey skey) (n text) (gy akey) (b ca a ca-0 name)) (defstrand resp 4 (dhkey dhkey) (n n) (gy gy) (h gy) (a b) (b b) (ca ca)) (defstrand ca 1 (gz gy) (subject b) (ca ca)) (defstrand init 4 (dhkey dhkey) (n n) (gx gy) (h gy) (a a) (b a) (ca ca-0)) (defstrand ca 1 (gz gy) (subject a) (ca ca-0)) (precedes ((0 2) (2 2)) ((1 0) (0 0)) ((2 3) (0 3)) ((3 0) (2 0))) (non-orig dhkey (invk gy) (privk ca) (privk ca-0)) (uniq-orig n) (operation encryption-test (displaced 4 3 ca 1) (enc gy b-0 (privk ca-0)) (2 2)) (traces ((recv (enc gy b (privk ca))) (recv (cat gy (enc gy b (privk ca)))) (send (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gy gy dhkey)))) (recv (enc "check" n (enc "dh" gy gy dhkey)))) ((send (enc gy b (privk ca)))) ((recv (enc gy a (privk ca-0))) (send (cat gy (enc gy a (privk ca-0)))) (recv (cat gy (enc gy a (privk ca-0)) (enc n (enc "dh" gy gy dhkey)))) (send (enc "check" n (enc "dh" gy gy dhkey)))) ((send (enc gy a (privk ca-0))))) (label 44) (parent 37) (realized) (shape) (maps ((0) ((n n) (gy gy) (h gy) (dhkey dhkey) (a b) (b b) (ca ca)))) (origs (n (0 2)))) (defskeleton dhca (vars (dhkey skey) (n text) (gy akey) (b ca a b-0 ca-0 name)) (defstrand resp 4 (dhkey dhkey) (n n) (gy gy) (h gy) (a b) (b b) (ca ca)) (defstrand ca 1 (gz gy) (subject b) (ca ca)) (defstrand init 4 (dhkey dhkey) (n n) (gx gy) (h gy) (a a) (b b-0) (ca ca-0)) (defstrand ca 1 (gz gy) (subject a) (ca ca-0)) (defstrand ca 1 (gz gy) (subject b-0) (ca ca-0)) (precedes ((0 2) (2 2)) ((1 0) (0 0)) ((2 3) (0 3)) ((3 0) (2 0)) ((4 0) (2 2))) (non-orig dhkey (invk gy) (privk ca) (privk ca-0)) (uniq-orig n) (operation encryption-test (added-strand ca 1) (enc gy b-0 (privk ca-0)) (2 2)) (traces ((recv (enc gy b (privk ca))) (recv (cat gy (enc gy b (privk ca)))) (send (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gy gy dhkey)))) (recv (enc "check" n (enc "dh" gy gy dhkey)))) ((send (enc gy b (privk ca)))) ((recv (enc gy a (privk ca-0))) (send (cat gy (enc gy a (privk ca-0)))) (recv (cat gy (enc gy b-0 (privk ca-0)) (enc n (enc "dh" gy gy dhkey)))) (send (enc "check" n (enc "dh" gy gy dhkey)))) ((send (enc gy a (privk ca-0)))) ((send (enc gy b-0 (privk ca-0))))) (label 45) (parent 37) (realized) (shape) (maps ((0) ((n n) (gy gy) (h gy) (dhkey dhkey) (a b) (b b) (ca ca)))) (origs (n (0 2)))) (defskeleton dhca (vars (dhkey skey) (n text) (gy akey) (a b ca name)) (defstrand resp 4 (dhkey dhkey) (n n) (gy gy) (h gy) (a a) (b b) (ca ca)) (defstrand ca 1 (gz gy) (subject b) (ca ca)) (defstrand ca 1 (gz gy) (subject a) (ca ca)) (defstrand init 4 (dhkey dhkey) (n n) (gx gy) (h gy) (a b) (b b) (ca ca)) (precedes ((0 2) (3 2)) ((1 0) (0 0)) ((1 0) (3 0)) ((2 0) (0 1)) ((3 3) (0 3))) (non-orig dhkey (invk gy) (privk ca)) (uniq-orig n) (operation encryption-test (displaced 4 1 ca 1) (enc gy b-0 (privk ca)) (3 2)) (traces ((recv (enc gy b (privk ca))) (recv (cat gy (enc gy a (privk ca)))) (send (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gy gy dhkey)))) (recv (enc "check" n (enc "dh" gy gy dhkey)))) ((send (enc gy b (privk ca)))) ((send (enc gy a (privk ca)))) ((recv (enc gy b (privk ca))) (send (cat gy (enc gy b (privk ca)))) (recv (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gy gy dhkey)))) (send (enc "check" n (enc "dh" gy gy dhkey))))) (label 46) (parent 38) (realized) (shape) (maps ((0) ((n n) (gy gy) (h gy) (dhkey dhkey) (a a) (b b) (ca ca)))) (origs (n (0 2)))) (defskeleton dhca (vars (dhkey skey) (n text) (gy akey) (a b ca name)) (defstrand resp 4 (dhkey dhkey) (n n) (gy gy) (h gy) (a a) (b b) (ca ca)) (defstrand ca 1 (gz gy) (subject b) (ca ca)) (defstrand ca 1 (gz gy) (subject a) (ca ca)) (defstrand init 4 (dhkey dhkey) (n n) (gx gy) (h gy) (a b) (b a) (ca ca)) (precedes ((0 2) (3 2)) ((1 0) (0 0)) ((1 0) (3 0)) ((2 0) (0 1)) ((3 3) (0 3))) (non-orig dhkey (invk gy) (privk ca)) (uniq-orig n) (operation encryption-test (displaced 4 2 ca 1) (enc gy b-0 (privk ca)) (3 2)) (traces ((recv (enc gy b (privk ca))) (recv (cat gy (enc gy a (privk ca)))) (send (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gy gy dhkey)))) (recv (enc "check" n (enc "dh" gy gy dhkey)))) ((send (enc gy b (privk ca)))) ((send (enc gy a (privk ca)))) ((recv (enc gy b (privk ca))) (send (cat gy (enc gy b (privk ca)))) (recv (cat gy (enc gy a (privk ca)) (enc n (enc "dh" gy gy dhkey)))) (send (enc "check" n (enc "dh" gy gy dhkey))))) (label 47) (parent 38) (realized) (shape) (maps ((0) ((n n) (gy gy) (h gy) (dhkey dhkey) (a a) (b b) (ca ca)))) (origs (n (0 2)))) (defskeleton dhca (vars (dhkey skey) (n text) (gy akey) (a b ca b-0 name)) (defstrand resp 4 (dhkey dhkey) (n n) (gy gy) (h gy) (a a) (b b) (ca ca)) (defstrand ca 1 (gz gy) (subject b) (ca ca)) (defstrand ca 1 (gz gy) (subject a) (ca ca)) (defstrand init 4 (dhkey dhkey) (n n) (gx gy) (h gy) (a b) (b b-0) (ca ca)) (defstrand ca 1 (gz gy) (subject b-0) (ca ca)) (precedes ((0 2) (3 2)) ((1 0) (0 0)) ((1 0) (3 0)) ((2 0) (0 1)) ((3 3) (0 3)) ((4 0) (3 2))) (non-orig dhkey (invk gy) (privk ca)) (uniq-orig n) (operation encryption-test (added-strand ca 1) (enc gy b-0 (privk ca)) (3 2)) (traces ((recv (enc gy b (privk ca))) (recv (cat gy (enc gy a (privk ca)))) (send (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gy gy dhkey)))) (recv (enc "check" n (enc "dh" gy gy dhkey)))) ((send (enc gy b (privk ca)))) ((send (enc gy a (privk ca)))) ((recv (enc gy b (privk ca))) (send (cat gy (enc gy b (privk ca)))) (recv (cat gy (enc gy b-0 (privk ca)) (enc n (enc "dh" gy gy dhkey)))) (send (enc "check" n (enc "dh" gy gy dhkey)))) ((send (enc gy b-0 (privk ca))))) (label 48) (parent 38) (realized) (shape) (maps ((0) ((n n) (gy gy) (h gy) (dhkey dhkey) (a a) (b b) (ca ca)))) (origs (n (0 2)))) (defskeleton dhca (vars (dhkey skey) (n text) (gy h akey) (a b ca name)) (defstrand resp 4 (dhkey dhkey) (n n) (gy gy) (h h) (a a) (b b) (ca ca)) (defstrand ca 1 (gz gy) (subject b) (ca ca)) (defstrand ca 1 (gz h) (subject a) (ca ca)) (defstrand init 4 (dhkey dhkey) (n n) (gx h) (h gy) (a a) (b b) (ca ca)) (precedes ((0 2) (3 2)) ((1 0) (0 0)) ((2 0) (0 1)) ((2 0) (3 0)) ((3 3) (0 3))) (non-orig dhkey (invk gy) (invk h) (privk ca)) (uniq-orig n) (operation encryption-test (displaced 4 1 ca 1) (enc gy b-0 (privk ca)) (3 2)) (traces ((recv (enc gy b (privk ca))) (recv (cat h (enc h a (privk ca)))) (send (cat gy (enc gy b (privk ca)) (enc n (enc "dh" h gy dhkey)))) (recv (enc "check" n (enc "dh" h gy dhkey)))) ((send (enc gy b (privk ca)))) ((send (enc h a (privk ca)))) ((recv (enc h a (privk ca))) (send (cat h (enc h a (privk ca)))) (recv (cat gy (enc gy b (privk ca)) (enc n (enc "dh" h gy dhkey)))) (send (enc "check" n (enc "dh" h gy dhkey))))) (label 49) (parent 39) (realized) (shape) (maps ((0) ((n n) (gy gy) (h h) (dhkey dhkey) (a a) (b b) (ca ca)))) (origs (n (0 2)))) (defskeleton dhca (vars (dhkey skey) (n text) (h akey) (a b ca name)) (defstrand resp 4 (dhkey dhkey) (n n) (gy h) (h h) (a a) (b b) (ca ca)) (defstrand ca 1 (gz h) (subject b) (ca ca)) (defstrand ca 1 (gz h) (subject a) (ca ca)) (defstrand init 4 (dhkey dhkey) (n n) (gx h) (h h) (a a) (b a) (ca ca)) (precedes ((0 2) (3 2)) ((1 0) (0 0)) ((2 0) (0 1)) ((2 0) (3 0)) ((3 3) (0 3))) (non-orig dhkey (invk h) (privk ca)) (uniq-orig n) (operation encryption-test (displaced 4 2 ca 1) (enc gy b-0 (privk ca)) (3 2)) (traces ((recv (enc h b (privk ca))) (recv (cat h (enc h a (privk ca)))) (send (cat h (enc h b (privk ca)) (enc n (enc "dh" h h dhkey)))) (recv (enc "check" n (enc "dh" h h dhkey)))) ((send (enc h b (privk ca)))) ((send (enc h a (privk ca)))) ((recv (enc h a (privk ca))) (send (cat h (enc h a (privk ca)))) (recv (cat h (enc h a (privk ca)) (enc n (enc "dh" h h dhkey)))) (send (enc "check" n (enc "dh" h h dhkey))))) (label 50) (parent 39) (realized) (shape) (maps ((0) ((n n) (gy h) (h h) (dhkey dhkey) (a a) (b b) (ca ca)))) (origs (n (0 2)))) (defskeleton dhca (vars (dhkey skey) (n text) (gy h akey) (a b ca b-0 name)) (defstrand resp 4 (dhkey dhkey) (n n) (gy gy) (h h) (a a) (b b) (ca ca)) (defstrand ca 1 (gz gy) (subject b) (ca ca)) (defstrand ca 1 (gz h) (subject a) (ca ca)) (defstrand init 4 (dhkey dhkey) (n n) (gx h) (h gy) (a a) (b b-0) (ca ca)) (defstrand ca 1 (gz gy) (subject b-0) (ca ca)) (precedes ((0 2) (3 2)) ((1 0) (0 0)) ((2 0) (0 1)) ((2 0) (3 0)) ((3 3) (0 3)) ((4 0) (3 2))) (non-orig dhkey (invk gy) (invk h) (privk ca)) (uniq-orig n) (operation encryption-test (added-strand ca 1) (enc gy b-0 (privk ca)) (3 2)) (traces ((recv (enc gy b (privk ca))) (recv (cat h (enc h a (privk ca)))) (send (cat gy (enc gy b (privk ca)) (enc n (enc "dh" h gy dhkey)))) (recv (enc "check" n (enc "dh" h gy dhkey)))) ((send (enc gy b (privk ca)))) ((send (enc h a (privk ca)))) ((recv (enc h a (privk ca))) (send (cat h (enc h a (privk ca)))) (recv (cat gy (enc gy b-0 (privk ca)) (enc n (enc "dh" h gy dhkey)))) (send (enc "check" n (enc "dh" h gy dhkey)))) ((send (enc gy b-0 (privk ca))))) (label 51) (parent 39) (realized) (shape) (maps ((0) ((n n) (gy gy) (h h) (dhkey dhkey) (a a) (b b) (ca ca)))) (origs (n (0 2)))) (defskeleton dhca (vars (dhkey skey) (n text) (h akey) (a b ca a-0 name)) (defstrand resp 4 (dhkey dhkey) (n n) (gy h) (h h) (a a) (b b) (ca ca)) (defstrand ca 1 (gz h) (subject b) (ca ca)) (defstrand ca 1 (gz h) (subject a) (ca ca)) (defstrand init 4 (dhkey dhkey) (n n) (gx h) (h h) (a a-0) (b a) (ca ca)) (defstrand ca 1 (gz h) (subject a-0) (ca ca)) (precedes ((0 2) (3 2)) ((1 0) (0 0)) ((2 0) (0 1)) ((3 3) (0 3)) ((4 0) (3 0))) (non-orig dhkey (invk h) (privk ca)) (uniq-orig n) (operation encryption-test (displaced 5 2 ca 1) (enc gy b-0 (privk ca-0)) (3 2)) (traces ((recv (enc h b (privk ca))) (recv (cat h (enc h a (privk ca)))) (send (cat h (enc h b (privk ca)) (enc n (enc "dh" h h dhkey)))) (recv (enc "check" n (enc "dh" h h dhkey)))) ((send (enc h b (privk ca)))) ((send (enc h a (privk ca)))) ((recv (enc h a-0 (privk ca))) (send (cat h (enc h a-0 (privk ca)))) (recv (cat h (enc h a (privk ca)) (enc n (enc "dh" h h dhkey)))) (send (enc "check" n (enc "dh" h h dhkey)))) ((send (enc h a-0 (privk ca))))) (label 52) (parent 40) (realized) (shape) (maps ((0) ((n n) (gy h) (h h) (dhkey dhkey) (a a) (b b) (ca ca)))) (origs (n (0 2)))) (defskeleton dhca (vars (dhkey skey) (n text) (gy h akey) (a b ca a-0 name)) (defstrand resp 4 (dhkey dhkey) (n n) (gy gy) (h h) (a a) (b b) (ca ca)) (defstrand ca 1 (gz gy) (subject b) (ca ca)) (defstrand ca 1 (gz h) (subject a) (ca ca)) (defstrand init 4 (dhkey dhkey) (n n) (gx h) (h gy) (a a-0) (b b) (ca ca)) (defstrand ca 1 (gz h) (subject a-0) (ca ca)) (precedes ((0 2) (3 2)) ((1 0) (0 0)) ((2 0) (0 1)) ((3 3) (0 3)) ((4 0) (3 0))) (non-orig dhkey (invk gy) (invk h) (privk ca)) (uniq-orig n) (operation encryption-test (displaced 5 1 ca 1) (enc gy b-0 (privk ca-0)) (3 2)) (traces ((recv (enc gy b (privk ca))) (recv (cat h (enc h a (privk ca)))) (send (cat gy (enc gy b (privk ca)) (enc n (enc "dh" h gy dhkey)))) (recv (enc "check" n (enc "dh" h gy dhkey)))) ((send (enc gy b (privk ca)))) ((send (enc h a (privk ca)))) ((recv (enc h a-0 (privk ca))) (send (cat h (enc h a-0 (privk ca)))) (recv (cat gy (enc gy b (privk ca)) (enc n (enc "dh" h gy dhkey)))) (send (enc "check" n (enc "dh" h gy dhkey)))) ((send (enc h a-0 (privk ca))))) (label 53) (parent 40) (realized) (shape) (maps ((0) ((n n) (gy gy) (h h) (dhkey dhkey) (a a) (b b) (ca ca)))) (origs (n (0 2)))) (defskeleton dhca (vars (dhkey skey) (n text) (h akey) (a b ca a-0 ca-0 name)) (defstrand resp 4 (dhkey dhkey) (n n) (gy h) (h h) (a a) (b b) (ca ca)) (defstrand ca 1 (gz h) (subject b) (ca ca)) (defstrand ca 1 (gz h) (subject a) (ca ca)) (defstrand init 4 (dhkey dhkey) (n n) (gx h) (h h) (a a-0) (b a-0) (ca ca-0)) (defstrand ca 1 (gz h) (subject a-0) (ca ca-0)) (precedes ((0 2) (3 2)) ((1 0) (0 0)) ((2 0) (0 1)) ((3 3) (0 3)) ((4 0) (3 0))) (non-orig dhkey (invk h) (privk ca) (privk ca-0)) (uniq-orig n) (operation encryption-test (displaced 5 4 ca 1) (enc gy b-0 (privk ca-0)) (3 2)) (traces ((recv (enc h b (privk ca))) (recv (cat h (enc h a (privk ca)))) (send (cat h (enc h b (privk ca)) (enc n (enc "dh" h h dhkey)))) (recv (enc "check" n (enc "dh" h h dhkey)))) ((send (enc h b (privk ca)))) ((send (enc h a (privk ca)))) ((recv (enc h a-0 (privk ca-0))) (send (cat h (enc h a-0 (privk ca-0)))) (recv (cat h (enc h a-0 (privk ca-0)) (enc n (enc "dh" h h dhkey)))) (send (enc "check" n (enc "dh" h h dhkey)))) ((send (enc h a-0 (privk ca-0))))) (label 54) (parent 40) (realized) (shape) (maps ((0) ((n n) (gy h) (h h) (dhkey dhkey) (a a) (b b) (ca ca)))) (origs (n (0 2)))) (defskeleton dhca (vars (dhkey skey) (n text) (gy h akey) (a b ca a-0 b-0 ca-0 name)) (defstrand resp 4 (dhkey dhkey) (n n) (gy gy) (h h) (a a) (b b) (ca ca)) (defstrand ca 1 (gz gy) (subject b) (ca ca)) (defstrand ca 1 (gz h) (subject a) (ca ca)) (defstrand init 4 (dhkey dhkey) (n n) (gx h) (h gy) (a a-0) (b b-0) (ca ca-0)) (defstrand ca 1 (gz h) (subject a-0) (ca ca-0)) (defstrand ca 1 (gz gy) (subject b-0) (ca ca-0)) (precedes ((0 2) (3 2)) ((1 0) (0 0)) ((2 0) (0 1)) ((3 3) (0 3)) ((4 0) (3 0)) ((5 0) (3 2))) (non-orig dhkey (invk gy) (invk h) (privk ca) (privk ca-0)) (uniq-orig n) (operation encryption-test (added-strand ca 1) (enc gy b-0 (privk ca-0)) (3 2)) (traces ((recv (enc gy b (privk ca))) (recv (cat h (enc h a (privk ca)))) (send (cat gy (enc gy b (privk ca)) (enc n (enc "dh" h gy dhkey)))) (recv (enc "check" n (enc "dh" h gy dhkey)))) ((send (enc gy b (privk ca)))) ((send (enc h a (privk ca)))) ((recv (enc h a-0 (privk ca-0))) (send (cat h (enc h a-0 (privk ca-0)))) (recv (cat gy (enc gy b-0 (privk ca-0)) (enc n (enc "dh" h gy dhkey)))) (send (enc "check" n (enc "dh" h gy dhkey)))) ((send (enc h a-0 (privk ca-0)))) ((send (enc gy b-0 (privk ca-0))))) (label 55) (parent 40) (realized) (shape) (maps ((0) ((n n) (gy gy) (h h) (dhkey dhkey) (a a) (b b) (ca ca)))) (origs (n (0 2)))) (comment "Nothing left to do") (defprotocol dhca basic (defrole init (vars (gx h akey) (dhkey skey) (a b ca name) (n text)) (trace (recv (enc gx a (privk ca))) (send (cat gx (enc gx a (privk ca)))) (recv (cat h (enc h b (privk ca)) (enc n (enc "dh" gx h dhkey)))) (send (enc "check" n (enc "dh" gx h dhkey)))) (non-orig dhkey (privk ca))) (defrole resp (vars (gy h akey) (dhkey skey) (a b ca name) (n text)) (trace (recv (enc gy b (privk ca))) (recv (cat h (enc h a (privk ca)))) (send (cat gy (enc gy b (privk ca)) (enc n (enc "dh" h gy dhkey)))) (recv (enc "check" n (enc "dh" h gy dhkey)))) (non-orig dhkey (privk ca))) (defrole ca (vars (subject ca name) (gz akey)) (trace (send (enc gz subject (privk ca)))) (non-orig (invk gz))) (defrole CDHcalc1 (vars (gx gy akey) (dhkey skey)) (trace (recv (cat gx (invk gy))) (send (enc "dh" gx gy dhkey)))) (defrole CDHcalc2 (vars (gx gy akey) (dhkey skey)) (trace (recv (cat gy (invk gx))) (send (enc "dh" gx gy dhkey)))) (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 dhca (vars (dhkey skey) (n text) (gy h akey) (a b ca name)) (defstrand resp 4 (dhkey dhkey) (n n) (gy gy) (h h) (a a) (b b) (ca ca)) (deflistener n) (non-orig dhkey (privk ca)) (uniq-orig n) (comment "Full responder point of view with freshly chosen n") (traces ((recv (enc gy b (privk ca))) (recv (cat h (enc h a (privk ca)))) (send (cat gy (enc gy b (privk ca)) (enc n (enc "dh" h gy dhkey)))) (recv (enc "check" n (enc "dh" h gy dhkey)))) ((recv n) (send n))) (label 56) (unrealized (0 0) (0 1) (0 3) (1 0)) (preskeleton) (origs (n (0 2))) (comment "Not a skeleton")) (defskeleton dhca (vars (dhkey skey) (n text) (gy h akey) (a b ca name)) (defstrand resp 4 (dhkey dhkey) (n n) (gy gy) (h h) (a a) (b b) (ca ca)) (deflistener n) (precedes ((0 2) (1 0))) (non-orig dhkey (privk ca)) (uniq-orig n) (traces ((recv (enc gy b (privk ca))) (recv (cat h (enc h a (privk ca)))) (send (cat gy (enc gy b (privk ca)) (enc n (enc "dh" h gy dhkey)))) (recv (enc "check" n (enc "dh" h gy dhkey)))) ((recv n) (send n))) (label 57) (parent 56) (unrealized (0 0) (0 1) (0 3) (1 0)) (origs (n (0 2))) (comment "2 in cohort - 2 not yet seen")) (defskeleton dhca (vars (dhkey skey) (n text) (gy h akey) (a b ca a-0 b-0 ca-0 name)) (defstrand resp 4 (dhkey dhkey) (n n) (gy gy) (h h) (a a) (b b) (ca ca)) (deflistener n) (defstrand init 4 (dhkey dhkey) (n n) (gx h) (h gy) (a a-0) (b b-0) (ca ca-0)) (precedes ((0 2) (2 2)) ((2 3) (1 0))) (non-orig dhkey (privk ca) (privk ca-0)) (uniq-orig n) (operation nonce-test (added-strand init 4) n (1 0) (enc n (enc "dh" h gy dhkey))) (traces ((recv (enc gy b (privk ca))) (recv (cat h (enc h a (privk ca)))) (send (cat gy (enc gy b (privk ca)) (enc n (enc "dh" h gy dhkey)))) (recv (enc "check" n (enc "dh" h gy dhkey)))) ((recv n) (send n)) ((recv (enc h a-0 (privk ca-0))) (send (cat h (enc h a-0 (privk ca-0)))) (recv (cat gy (enc gy b-0 (privk ca-0)) (enc n (enc "dh" h gy dhkey)))) (send (enc "check" n (enc "dh" h gy dhkey))))) (label 58) (parent 57) (unrealized (0 0) (0 1) (0 3) (1 0) (2 0) (2 2)) (comment "1 in cohort - 1 not yet seen")) (defskeleton dhca (vars (dhkey skey) (n text) (gy h akey) (a b ca name)) (defstrand resp 4 (dhkey dhkey) (n n) (gy gy) (h h) (a a) (b b) (ca ca)) (deflistener n) (deflistener (enc "dh" h gy dhkey)) (precedes ((0 2) (1 0)) ((2 1) (1 0))) (non-orig dhkey (privk ca)) (uniq-orig n) (operation nonce-test (added-listener (enc "dh" h gy dhkey)) n (1 0) (enc n (enc "dh" h gy dhkey))) (traces ((recv (enc gy b (privk ca))) (recv (cat h (enc h a (privk ca)))) (send (cat gy (enc gy b (privk ca)) (enc n (enc "dh" h gy dhkey)))) (recv (enc "check" n (enc "dh" h gy dhkey)))) ((recv n) (send n)) ((recv (enc "dh" h gy dhkey)) (send (enc "dh" h gy dhkey)))) (label 59) (parent 57) (unrealized (0 0) (0 1) (0 3) (2 0)) (comment "2 in cohort - 2 not yet seen")) (defskeleton dhca (vars (dhkey skey) (n text) (gy h akey) (a b ca a-0 b-0 ca-0 name)) (defstrand resp 4 (dhkey dhkey) (n n) (gy gy) (h h) (a a) (b b) (ca ca)) (deflistener n) (defstrand init 4 (dhkey dhkey) (n n) (gx h) (h gy) (a a-0) (b b-0) (ca ca-0)) (defstrand ca 1 (gz h) (subject a-0) (ca ca-0)) (precedes ((0 2) (2 2)) ((2 3) (1 0)) ((3 0) (2 0))) (non-orig dhkey (invk h) (privk ca) (privk ca-0)) (uniq-orig n) (operation encryption-test (added-strand ca 1) (enc h a-0 (privk ca-0)) (2 0)) (traces ((recv (enc gy b (privk ca))) (recv (cat h (enc h a (privk ca)))) (send (cat gy (enc gy b (privk ca)) (enc n (enc "dh" h gy dhkey)))) (recv (enc "check" n (enc "dh" h gy dhkey)))) ((recv n) (send n)) ((recv (enc h a-0 (privk ca-0))) (send (cat h (enc h a-0 (privk ca-0)))) (recv (cat gy (enc gy b-0 (privk ca-0)) (enc n (enc "dh" h gy dhkey)))) (send (enc "check" n (enc "dh" h gy dhkey)))) ((send (enc h a-0 (privk ca-0))))) (label 60) (parent 58) (unrealized (0 0) (0 1) (0 3) (1 0) (2 2)) (comment "2 in cohort - 2 not yet seen")) (defskeleton dhca (vars (dhkey skey) (n text) (gy h akey) (a b ca name)) (defstrand resp 4 (dhkey dhkey) (n n) (gy gy) (h h) (a a) (b b) (ca ca)) (deflistener n) (deflistener (enc "dh" h gy dhkey)) (defstrand CDHcalc1 2 (dhkey dhkey) (gx h) (gy gy)) (precedes ((0 2) (1 0)) ((2 1) (1 0)) ((3 1) (2 0))) (non-orig dhkey (privk ca)) (uniq-orig n) (operation encryption-test (added-strand CDHcalc1 2) (enc "dh" h gy dhkey) (2 0)) (traces ((recv (enc gy b (privk ca))) (recv (cat h (enc h a (privk ca)))) (send (cat gy (enc gy b (privk ca)) (enc n (enc "dh" h gy dhkey)))) (recv (enc "check" n (enc "dh" h gy dhkey)))) ((recv n) (send n)) ((recv (enc "dh" h gy dhkey)) (send (enc "dh" h gy dhkey))) ((recv (cat h (invk gy))) (send (enc "dh" h gy dhkey)))) (label 61) (parent 59) (unrealized (0 0) (0 1) (0 3)) (dead) (comment "empty cohort")) (defskeleton dhca (vars (dhkey skey) (n text) (gy h akey) (a b ca name)) (defstrand resp 4 (dhkey dhkey) (n n) (gy gy) (h h) (a a) (b b) (ca ca)) (deflistener n) (deflistener (enc "dh" h gy dhkey)) (defstrand CDHcalc2 2 (dhkey dhkey) (gx h) (gy gy)) (precedes ((0 2) (1 0)) ((2 1) (1 0)) ((3 1) (2 0))) (non-orig dhkey (privk ca)) (uniq-orig n) (operation encryption-test (added-strand CDHcalc2 2) (enc "dh" h gy dhkey) (2 0)) (traces ((recv (enc gy b (privk ca))) (recv (cat h (enc h a (privk ca)))) (send (cat gy (enc gy b (privk ca)) (enc n (enc "dh" h gy dhkey)))) (recv (enc "check" n (enc "dh" h gy dhkey)))) ((recv n) (send n)) ((recv (enc "dh" h gy dhkey)) (send (enc "dh" h gy dhkey))) ((recv (cat gy (invk h))) (send (enc "dh" h gy dhkey)))) (label 62) (parent 59) (unrealized (0 0) (0 1) (0 3)) (comment "1 in cohort - 1 not yet seen")) (defskeleton dhca (vars (dhkey skey) (n text) (h akey) (a b ca a-0 ca-0 name)) (defstrand resp 4 (dhkey dhkey) (n n) (gy h) (h h) (a a) (b b) (ca ca)) (deflistener n) (defstrand init 4 (dhkey dhkey) (n n) (gx h) (h h) (a a-0) (b a-0) (ca ca-0)) (defstrand ca 1 (gz h) (subject a-0) (ca ca-0)) (precedes ((0 2) (2 2)) ((2 3) (1 0)) ((3 0) (2 0))) (non-orig dhkey (invk h) (privk ca) (privk ca-0)) (uniq-orig n) (operation encryption-test (displaced 4 3 ca 1) (enc gy b-0 (privk ca-0)) (2 2)) (traces ((recv (enc h b (privk ca))) (recv (cat h (enc h a (privk ca)))) (send (cat h (enc h b (privk ca)) (enc n (enc "dh" h h dhkey)))) (recv (enc "check" n (enc "dh" h h dhkey)))) ((recv n) (send n)) ((recv (enc h a-0 (privk ca-0))) (send (cat h (enc h a-0 (privk ca-0)))) (recv (cat h (enc h a-0 (privk ca-0)) (enc n (enc "dh" h h dhkey)))) (send (enc "check" n (enc "dh" h h dhkey)))) ((send (enc h a-0 (privk ca-0))))) (label 63) (parent 60) (unrealized (0 0) (0 1) (0 3) (1 0)) (comment "1 in cohort - 1 not yet seen")) (defskeleton dhca (vars (dhkey skey) (n text) (gy h akey) (a b ca a-0 b-0 ca-0 name)) (defstrand resp 4 (dhkey dhkey) (n n) (gy gy) (h h) (a a) (b b) (ca ca)) (deflistener n) (defstrand init 4 (dhkey dhkey) (n n) (gx h) (h gy) (a a-0) (b b-0) (ca ca-0)) (defstrand ca 1 (gz h) (subject a-0) (ca ca-0)) (defstrand ca 1 (gz gy) (subject b-0) (ca ca-0)) (precedes ((0 2) (2 2)) ((2 3) (1 0)) ((3 0) (2 0)) ((4 0) (2 2))) (non-orig dhkey (invk gy) (invk h) (privk ca) (privk ca-0)) (uniq-orig n) (operation encryption-test (added-strand ca 1) (enc gy b-0 (privk ca-0)) (2 2)) (traces ((recv (enc gy b (privk ca))) (recv (cat h (enc h a (privk ca)))) (send (cat gy (enc gy b (privk ca)) (enc n (enc "dh" h gy dhkey)))) (recv (enc "check" n (enc "dh" h gy dhkey)))) ((recv n) (send n)) ((recv (enc h a-0 (privk ca-0))) (send (cat h (enc h a-0 (privk ca-0)))) (recv (cat gy (enc gy b-0 (privk ca-0)) (enc n (enc "dh" h gy dhkey)))) (send (enc "check" n (enc "dh" h gy dhkey)))) ((send (enc h a-0 (privk ca-0)))) ((send (enc gy b-0 (privk ca-0))))) (label 64) (parent 60) (unrealized (0 0) (0 1) (0 3) (1 0)) (comment "1 in cohort - 1 not yet seen")) (defskeleton dhca (vars (dhkey skey) (n text) (gy h akey) (a b ca name)) (defstrand resp 4 (dhkey dhkey) (n n) (gy gy) (h h) (a a) (b b) (ca ca)) (deflistener n) (deflistener (enc "dh" h gy dhkey)) (defstrand CDHcalc2 2 (dhkey dhkey) (gx h) (gy gy)) (defstrand ca 1 (gz gy) (subject b) (ca ca)) (precedes ((0 2) (1 0)) ((2 1) (1 0)) ((3 1) (2 0)) ((4 0) (0 0))) (non-orig dhkey (invk gy) (privk ca)) (uniq-orig n) (operation encryption-test (added-strand ca 1) (enc gy b (privk ca)) (0 0)) (traces ((recv (enc gy b (privk ca))) (recv (cat h (enc h a (privk ca)))) (send (cat gy (enc gy b (privk ca)) (enc n (enc "dh" h gy dhkey)))) (recv (enc "check" n (enc "dh" h gy dhkey)))) ((recv n) (send n)) ((recv (enc "dh" h gy dhkey)) (send (enc "dh" h gy dhkey))) ((recv (cat gy (invk h))) (send (enc "dh" h gy dhkey))) ((send (enc gy b (privk ca))))) (label 65) (parent 62) (unrealized (0 1) (0 3)) (dead) (comment "empty cohort")) (defskeleton dhca (vars (dhkey skey) (n text) (h akey) (a b ca a-0 ca-0 name)) (defstrand resp 4 (dhkey dhkey) (n n) (gy h) (h h) (a a) (b b) (ca ca)) (deflistener n) (defstrand init 4 (dhkey dhkey) (n n) (gx h) (h h) (a a-0) (b a-0) (ca ca-0)) (defstrand ca 1 (gz h) (subject a-0) (ca ca-0)) (deflistener (enc "dh" h h dhkey)) (precedes ((0 2) (2 2)) ((2 3) (1 0)) ((3 0) (2 0)) ((4 1) (1 0))) (non-orig dhkey (invk h) (privk ca) (privk ca-0)) (uniq-orig n) (operation nonce-test (added-listener (enc "dh" h h dhkey)) n (1 0) (enc n (enc "dh" h h dhkey)) (enc "check" n (enc "dh" h h dhkey))) (traces ((recv (enc h b (privk ca))) (recv (cat h (enc h a (privk ca)))) (send (cat h (enc h b (privk ca)) (enc n (enc "dh" h h dhkey)))) (recv (enc "check" n (enc "dh" h h dhkey)))) ((recv n) (send n)) ((recv (enc h a-0 (privk ca-0))) (send (cat h (enc h a-0 (privk ca-0)))) (recv (cat h (enc h a-0 (privk ca-0)) (enc n (enc "dh" h h dhkey)))) (send (enc "check" n (enc "dh" h h dhkey)))) ((send (enc h a-0 (privk ca-0)))) ((recv (enc "dh" h h dhkey)) (send (enc "dh" h h dhkey)))) (label 66) (parent 63) (unrealized (0 0) (0 1) (0 3) (4 0)) (dead) (comment "empty cohort")) (defskeleton dhca (vars (dhkey skey) (n text) (gy h akey) (a b ca a-0 b-0 ca-0 name)) (defstrand resp 4 (dhkey dhkey) (n n) (gy gy) (h h) (a a) (b b) (ca ca)) (deflistener n) (defstrand init 4 (dhkey dhkey) (n n) (gx h) (h gy) (a a-0) (b b-0) (ca ca-0)) (defstrand ca 1 (gz h) (subject a-0) (ca ca-0)) (defstrand ca 1 (gz gy) (subject b-0) (ca ca-0)) (deflistener (enc "dh" h gy dhkey)) (precedes ((0 2) (2 2)) ((2 3) (1 0)) ((3 0) (2 0)) ((4 0) (2 2)) ((5 1) (1 0))) (non-orig dhkey (invk gy) (invk h) (privk ca) (privk ca-0)) (uniq-orig n) (operation nonce-test (added-listener (enc "dh" h gy dhkey)) n (1 0) (enc n (enc "dh" h gy dhkey)) (enc "check" n (enc "dh" h gy dhkey))) (traces ((recv (enc gy b (privk ca))) (recv (cat h (enc h a (privk ca)))) (send (cat gy (enc gy b (privk ca)) (enc n (enc "dh" h gy dhkey)))) (recv (enc "check" n (enc "dh" h gy dhkey)))) ((recv n) (send n)) ((recv (enc h a-0 (privk ca-0))) (send (cat h (enc h a-0 (privk ca-0)))) (recv (cat gy (enc gy b-0 (privk ca-0)) (enc n (enc "dh" h gy dhkey)))) (send (enc "check" n (enc "dh" h gy dhkey)))) ((send (enc h a-0 (privk ca-0)))) ((send (enc gy b-0 (privk ca-0)))) ((recv (enc "dh" h gy dhkey)) (send (enc "dh" h gy dhkey)))) (label 67) (parent 64) (unrealized (0 0) (0 1) (0 3) (5 0)) (dead) (comment "empty cohort")) (comment "Nothing left to do") (defprotocol dhca basic (defrole init (vars (gx h akey) (dhkey skey) (a b ca name) (n text)) (trace (recv (enc gx a (privk ca))) (send (cat gx (enc gx a (privk ca)))) (recv (cat h (enc h b (privk ca)) (enc n (enc "dh" gx h dhkey)))) (send (enc "check" n (enc "dh" gx h dhkey)))) (non-orig dhkey (privk ca))) (defrole resp (vars (gy h akey) (dhkey skey) (a b ca name) (n text)) (trace (recv (enc gy b (privk ca))) (recv (cat h (enc h a (privk ca)))) (send (cat gy (enc gy b (privk ca)) (enc n (enc "dh" h gy dhkey)))) (recv (enc "check" n (enc "dh" h gy dhkey)))) (non-orig dhkey (privk ca))) (defrole ca (vars (subject ca name) (gz akey)) (trace (send (enc gz subject (privk ca)))) (non-orig (invk gz))) (defrole CDHcalc1 (vars (gx gy akey) (dhkey skey)) (trace (recv (cat gx (invk gy))) (send (enc "dh" gx gy dhkey)))) (defrole CDHcalc2 (vars (gx gy akey) (dhkey skey)) (trace (recv (cat gy (invk gx))) (send (enc "dh" gx gy dhkey)))) (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 dhca (vars (dhkey skey) (n text) (gx gy akey) (a b ca name)) (defstrand init 4 (dhkey dhkey) (n n) (gx gx) (h gy) (a a) (b b) (ca ca)) (defstrand resp 4 (dhkey dhkey) (n n) (gy gy) (h gx) (a a) (b b) (ca ca)) (non-orig dhkey (privk ca)) (uniq-orig n) (traces ((recv (enc gx a (privk ca))) (send (cat gx (enc gx a (privk ca)))) (recv (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gx gy dhkey)))) (send (enc "check" n (enc "dh" gx gy dhkey)))) ((recv (enc gy b (privk ca))) (recv (cat gx (enc gx a (privk ca)))) (send (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gx gy dhkey)))) (recv (enc "check" n (enc "dh" gx gy dhkey))))) (label 68) (unrealized (0 0) (0 2) (1 0) (1 1) (1 3)) (preskeleton) (origs (n (1 2))) (comment "Not a skeleton")) (defskeleton dhca (vars (dhkey skey) (n text) (gx gy akey) (a b ca name)) (defstrand init 4 (dhkey dhkey) (n n) (gx gx) (h gy) (a a) (b b) (ca ca)) (defstrand resp 4 (dhkey dhkey) (n n) (gy gy) (h gx) (a a) (b b) (ca ca)) (precedes ((1 2) (0 2))) (non-orig dhkey (privk ca)) (uniq-orig n) (traces ((recv (enc gx a (privk ca))) (send (cat gx (enc gx a (privk ca)))) (recv (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gx gy dhkey)))) (send (enc "check" n (enc "dh" gx gy dhkey)))) ((recv (enc gy b (privk ca))) (recv (cat gx (enc gx a (privk ca)))) (send (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gx gy dhkey)))) (recv (enc "check" n (enc "dh" gx gy dhkey))))) (label 69) (parent 68) (unrealized (0 0) (1 0) (1 1) (1 3)) (origs (n (1 2))) (comment "1 in cohort - 1 not yet seen")) (defskeleton dhca (vars (dhkey skey) (n text) (gx gy akey) (a b ca name)) (defstrand init 4 (dhkey dhkey) (n n) (gx gx) (h gy) (a a) (b b) (ca ca)) (defstrand resp 4 (dhkey dhkey) (n n) (gy gy) (h gx) (a a) (b b) (ca ca)) (defstrand ca 1 (gz gy) (subject b) (ca ca)) (precedes ((1 2) (0 2)) ((2 0) (1 0))) (non-orig dhkey (invk gy) (privk ca)) (uniq-orig n) (operation encryption-test (added-strand ca 1) (enc gy b (privk ca)) (1 0)) (traces ((recv (enc gx a (privk ca))) (send (cat gx (enc gx a (privk ca)))) (recv (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gx gy dhkey)))) (send (enc "check" n (enc "dh" gx gy dhkey)))) ((recv (enc gy b (privk ca))) (recv (cat gx (enc gx a (privk ca)))) (send (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gx gy dhkey)))) (recv (enc "check" n (enc "dh" gx gy dhkey)))) ((send (enc gy b (privk ca))))) (label 70) (parent 69) (unrealized (0 0) (1 1) (1 3)) (comment "2 in cohort - 2 not yet seen")) (defskeleton dhca (vars (dhkey skey) (n text) (gy akey) (b ca name)) (defstrand init 4 (dhkey dhkey) (n n) (gx gy) (h gy) (a b) (b b) (ca ca)) (defstrand resp 4 (dhkey dhkey) (n n) (gy gy) (h gy) (a b) (b b) (ca ca)) (defstrand ca 1 (gz gy) (subject b) (ca ca)) (precedes ((1 2) (0 2)) ((2 0) (1 0))) (non-orig dhkey (invk gy) (privk ca)) (uniq-orig n) (operation encryption-test (displaced 3 2 ca 1) (enc gx a (privk ca)) (1 1)) (traces ((recv (enc gy b (privk ca))) (send (cat gy (enc gy b (privk ca)))) (recv (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gy gy dhkey)))) (send (enc "check" n (enc "dh" gy gy dhkey)))) ((recv (enc gy b (privk ca))) (recv (cat gy (enc gy b (privk ca)))) (send (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gy gy dhkey)))) (recv (enc "check" n (enc "dh" gy gy dhkey)))) ((send (enc gy b (privk ca))))) (label 71) (parent 70) (unrealized (0 0) (1 3)) (comment "3 in cohort - 3 not yet seen")) (defskeleton dhca (vars (dhkey skey) (n text) (gx gy akey) (a b ca name)) (defstrand init 4 (dhkey dhkey) (n n) (gx gx) (h gy) (a a) (b b) (ca ca)) (defstrand resp 4 (dhkey dhkey) (n n) (gy gy) (h gx) (a a) (b b) (ca ca)) (defstrand ca 1 (gz gy) (subject b) (ca ca)) (defstrand ca 1 (gz gx) (subject a) (ca ca)) (precedes ((1 2) (0 2)) ((2 0) (1 0)) ((3 0) (1 1))) (non-orig dhkey (invk gx) (invk gy) (privk ca)) (uniq-orig n) (operation encryption-test (added-strand ca 1) (enc gx a (privk ca)) (1 1)) (traces ((recv (enc gx a (privk ca))) (send (cat gx (enc gx a (privk ca)))) (recv (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gx gy dhkey)))) (send (enc "check" n (enc "dh" gx gy dhkey)))) ((recv (enc gy b (privk ca))) (recv (cat gx (enc gx a (privk ca)))) (send (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gx gy dhkey)))) (recv (enc "check" n (enc "dh" gx gy dhkey)))) ((send (enc gy b (privk ca)))) ((send (enc gx a (privk ca))))) (label 72) (parent 70) (unrealized (0 0) (1 3)) (comment "3 in cohort - 3 not yet seen")) (defskeleton dhca (vars (dhkey skey) (n text) (gy akey) (b ca name)) (defstrand init 4 (dhkey dhkey) (n n) (gx gy) (h gy) (a b) (b b) (ca ca)) (defstrand resp 4 (dhkey dhkey) (n n) (gy gy) (h gy) (a b) (b b) (ca ca)) (defstrand ca 1 (gz gy) (subject b) (ca ca)) (precedes ((0 3) (1 3)) ((1 2) (0 2)) ((2 0) (1 0))) (non-orig dhkey (invk gy) (privk ca)) (uniq-orig n) (operation encryption-test (displaced 3 0 init 4) (enc "check" n (enc "dh" gy gy dhkey)) (1 3)) (traces ((recv (enc gy b (privk ca))) (send (cat gy (enc gy b (privk ca)))) (recv (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gy gy dhkey)))) (send (enc "check" n (enc "dh" gy gy dhkey)))) ((recv (enc gy b (privk ca))) (recv (cat gy (enc gy b (privk ca)))) (send (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gy gy dhkey)))) (recv (enc "check" n (enc "dh" gy gy dhkey)))) ((send (enc gy b (privk ca))))) (label 73) (parent 71) (unrealized (0 0)) (comment "2 in cohort - 2 not yet seen")) (defskeleton dhca (vars (dhkey skey) (n text) (gy akey) (b ca a b-0 ca-0 name)) (defstrand init 4 (dhkey dhkey) (n n) (gx gy) (h gy) (a b) (b b) (ca ca)) (defstrand resp 4 (dhkey dhkey) (n n) (gy gy) (h gy) (a b) (b b) (ca ca)) (defstrand ca 1 (gz gy) (subject b) (ca ca)) (defstrand init 4 (dhkey dhkey) (n n) (gx gy) (h gy) (a a) (b b-0) (ca ca-0)) (precedes ((1 2) (0 2)) ((1 2) (3 2)) ((2 0) (1 0)) ((3 3) (1 3))) (non-orig dhkey (invk gy) (privk ca) (privk ca-0)) (uniq-orig n) (operation encryption-test (added-strand init 4) (enc "check" n (enc "dh" gy gy dhkey)) (1 3)) (traces ((recv (enc gy b (privk ca))) (send (cat gy (enc gy b (privk ca)))) (recv (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gy gy dhkey)))) (send (enc "check" n (enc "dh" gy gy dhkey)))) ((recv (enc gy b (privk ca))) (recv (cat gy (enc gy b (privk ca)))) (send (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gy gy dhkey)))) (recv (enc "check" n (enc "dh" gy gy dhkey)))) ((send (enc gy b (privk ca)))) ((recv (enc gy a (privk ca-0))) (send (cat gy (enc gy a (privk ca-0)))) (recv (cat gy (enc gy b-0 (privk ca-0)) (enc n (enc "dh" gy gy dhkey)))) (send (enc "check" n (enc "dh" gy gy dhkey))))) (label 74) (parent 71) (unrealized (0 0) (3 0) (3 2)) (comment "2 in cohort - 2 not yet seen")) (defskeleton dhca (vars (dhkey skey) (n text) (gy akey) (b ca name)) (defstrand init 4 (dhkey dhkey) (n n) (gx gy) (h gy) (a b) (b b) (ca ca)) (defstrand resp 4 (dhkey dhkey) (n n) (gy gy) (h gy) (a b) (b b) (ca ca)) (defstrand ca 1 (gz gy) (subject b) (ca ca)) (deflistener (enc "dh" gy gy dhkey)) (precedes ((1 2) (0 2)) ((2 0) (1 0)) ((3 1) (1 3))) (non-orig dhkey (invk gy) (privk ca)) (uniq-orig n) (operation encryption-test (added-listener (enc "dh" gy gy dhkey)) (enc "check" n (enc "dh" gy gy dhkey)) (1 3)) (traces ((recv (enc gy b (privk ca))) (send (cat gy (enc gy b (privk ca)))) (recv (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gy gy dhkey)))) (send (enc "check" n (enc "dh" gy gy dhkey)))) ((recv (enc gy b (privk ca))) (recv (cat gy (enc gy b (privk ca)))) (send (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gy gy dhkey)))) (recv (enc "check" n (enc "dh" gy gy dhkey)))) ((send (enc gy b (privk ca)))) ((recv (enc "dh" gy gy dhkey)) (send (enc "dh" gy gy dhkey)))) (label 75) (parent 71) (unrealized (0 0) (3 0)) (dead) (comment "empty cohort")) (defskeleton dhca (vars (dhkey skey) (n text) (gx gy akey) (a b ca name)) (defstrand init 4 (dhkey dhkey) (n n) (gx gx) (h gy) (a a) (b b) (ca ca)) (defstrand resp 4 (dhkey dhkey) (n n) (gy gy) (h gx) (a a) (b b) (ca ca)) (defstrand ca 1 (gz gy) (subject b) (ca ca)) (defstrand ca 1 (gz gx) (subject a) (ca ca)) (precedes ((0 3) (1 3)) ((1 2) (0 2)) ((2 0) (1 0)) ((3 0) (1 1))) (non-orig dhkey (invk gx) (invk gy) (privk ca)) (uniq-orig n) (operation encryption-test (displaced 4 0 init 4) (enc "check" n (enc "dh" gx gy dhkey)) (1 3)) (traces ((recv (enc gx a (privk ca))) (send (cat gx (enc gx a (privk ca)))) (recv (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gx gy dhkey)))) (send (enc "check" n (enc "dh" gx gy dhkey)))) ((recv (enc gy b (privk ca))) (recv (cat gx (enc gx a (privk ca)))) (send (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gx gy dhkey)))) (recv (enc "check" n (enc "dh" gx gy dhkey)))) ((send (enc gy b (privk ca)))) ((send (enc gx a (privk ca))))) (label 76) (parent 72) (unrealized (0 0)) (comment "3 in cohort - 3 not yet seen")) (defskeleton dhca (vars (dhkey skey) (n text) (gx gy akey) (a b ca a-0 b-0 ca-0 name)) (defstrand init 4 (dhkey dhkey) (n n) (gx gx) (h gy) (a a) (b b) (ca ca)) (defstrand resp 4 (dhkey dhkey) (n n) (gy gy) (h gx) (a a) (b b) (ca ca)) (defstrand ca 1 (gz gy) (subject b) (ca ca)) (defstrand ca 1 (gz gx) (subject a) (ca ca)) (defstrand init 4 (dhkey dhkey) (n n) (gx gx) (h gy) (a a-0) (b b-0) (ca ca-0)) (precedes ((1 2) (0 2)) ((1 2) (4 2)) ((2 0) (1 0)) ((3 0) (1 1)) ((4 3) (1 3))) (non-orig dhkey (invk gx) (invk gy) (privk ca) (privk ca-0)) (uniq-orig n) (operation encryption-test (added-strand init 4) (enc "check" n (enc "dh" gx gy dhkey)) (1 3)) (traces ((recv (enc gx a (privk ca))) (send (cat gx (enc gx a (privk ca)))) (recv (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gx gy dhkey)))) (send (enc "check" n (enc "dh" gx gy dhkey)))) ((recv (enc gy b (privk ca))) (recv (cat gx (enc gx a (privk ca)))) (send (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gx gy dhkey)))) (recv (enc "check" n (enc "dh" gx gy dhkey)))) ((send (enc gy b (privk ca)))) ((send (enc gx a (privk ca)))) ((recv (enc gx a-0 (privk ca-0))) (send (cat gx (enc gx a-0 (privk ca-0)))) (recv (cat gy (enc gy b-0 (privk ca-0)) (enc n (enc "dh" gx gy dhkey)))) (send (enc "check" n (enc "dh" gx gy dhkey))))) (label 77) (parent 72) (unrealized (0 0) (4 0) (4 2)) (comment "3 in cohort - 3 not yet seen")) (defskeleton dhca (vars (dhkey skey) (n text) (gx gy akey) (a b ca name)) (defstrand init 4 (dhkey dhkey) (n n) (gx gx) (h gy) (a a) (b b) (ca ca)) (defstrand resp 4 (dhkey dhkey) (n n) (gy gy) (h gx) (a a) (b b) (ca ca)) (defstrand ca 1 (gz gy) (subject b) (ca ca)) (defstrand ca 1 (gz gx) (subject a) (ca ca)) (deflistener (enc "dh" gx gy dhkey)) (precedes ((1 2) (0 2)) ((2 0) (1 0)) ((3 0) (1 1)) ((4 1) (1 3))) (non-orig dhkey (invk gx) (invk gy) (privk ca)) (uniq-orig n) (operation encryption-test (added-listener (enc "dh" gx gy dhkey)) (enc "check" n (enc "dh" gx gy dhkey)) (1 3)) (traces ((recv (enc gx a (privk ca))) (send (cat gx (enc gx a (privk ca)))) (recv (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gx gy dhkey)))) (send (enc "check" n (enc "dh" gx gy dhkey)))) ((recv (enc gy b (privk ca))) (recv (cat gx (enc gx a (privk ca)))) (send (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gx gy dhkey)))) (recv (enc "check" n (enc "dh" gx gy dhkey)))) ((send (enc gy b (privk ca)))) ((send (enc gx a (privk ca)))) ((recv (enc "dh" gx gy dhkey)) (send (enc "dh" gx gy dhkey)))) (label 78) (parent 72) (unrealized (0 0) (4 0)) (dead) (comment "empty cohort")) (defskeleton dhca (vars (dhkey skey) (n text) (gy akey) (b ca name)) (defstrand init 4 (dhkey dhkey) (n n) (gx gy) (h gy) (a b) (b b) (ca ca)) (defstrand resp 4 (dhkey dhkey) (n n) (gy gy) (h gy) (a b) (b b) (ca ca)) (defstrand ca 1 (gz gy) (subject b) (ca ca)) (precedes ((0 3) (1 3)) ((1 2) (0 2)) ((2 0) (0 0)) ((2 0) (1 0))) (non-orig dhkey (invk gy) (privk ca)) (uniq-orig n) (operation encryption-test (displaced 3 2 ca 1) (enc gy b (privk ca)) (0 0)) (traces ((recv (enc gy b (privk ca))) (send (cat gy (enc gy b (privk ca)))) (recv (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gy gy dhkey)))) (send (enc "check" n (enc "dh" gy gy dhkey)))) ((recv (enc gy b (privk ca))) (recv (cat gy (enc gy b (privk ca)))) (send (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gy gy dhkey)))) (recv (enc "check" n (enc "dh" gy gy dhkey)))) ((send (enc gy b (privk ca))))) (label 79) (parent 73) (realized) (shape) (maps ((0 1) ((a b) (b b) (ca ca) (gx gy) (gy gy) (n n) (dhkey dhkey)))) (origs (n (1 2)))) (defskeleton dhca (vars (dhkey skey) (n text) (gy akey) (b ca name)) (defstrand init 4 (dhkey dhkey) (n n) (gx gy) (h gy) (a b) (b b) (ca ca)) (defstrand resp 4 (dhkey dhkey) (n n) (gy gy) (h gy) (a b) (b b) (ca ca)) (defstrand ca 1 (gz gy) (subject b) (ca ca)) (defstrand ca 1 (gz gy) (subject b) (ca ca)) (precedes ((0 3) (1 3)) ((1 2) (0 2)) ((2 0) (1 0)) ((3 0) (0 0))) (non-orig dhkey (invk gy) (privk ca)) (uniq-orig n) (operation encryption-test (added-strand ca 1) (enc gy b (privk ca)) (0 0)) (traces ((recv (enc gy b (privk ca))) (send (cat gy (enc gy b (privk ca)))) (recv (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gy gy dhkey)))) (send (enc "check" n (enc "dh" gy gy dhkey)))) ((recv (enc gy b (privk ca))) (recv (cat gy (enc gy b (privk ca)))) (send (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gy gy dhkey)))) (recv (enc "check" n (enc "dh" gy gy dhkey)))) ((send (enc gy b (privk ca)))) ((send (enc gy b (privk ca))))) (label 80) (parent 73) (realized) (shape) (maps ((0 1) ((a b) (b b) (ca ca) (gx gy) (gy gy) (n n) (dhkey dhkey)))) (origs (n (1 2)))) (defskeleton dhca (vars (dhkey skey) (n text) (gy akey) (b ca b-0 name)) (defstrand init 4 (dhkey dhkey) (n n) (gx gy) (h gy) (a b) (b b) (ca ca)) (defstrand resp 4 (dhkey dhkey) (n n) (gy gy) (h gy) (a b) (b b) (ca ca)) (defstrand ca 1 (gz gy) (subject b) (ca ca)) (defstrand init 4 (dhkey dhkey) (n n) (gx gy) (h gy) (a b) (b b-0) (ca ca)) (precedes ((1 2) (0 2)) ((1 2) (3 2)) ((2 0) (1 0)) ((2 0) (3 0)) ((3 3) (1 3))) (non-orig dhkey (invk gy) (privk ca)) (uniq-orig n) (operation encryption-test (displaced 4 2 ca 1) (enc gy a (privk ca-0)) (3 0)) (traces ((recv (enc gy b (privk ca))) (send (cat gy (enc gy b (privk ca)))) (recv (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gy gy dhkey)))) (send (enc "check" n (enc "dh" gy gy dhkey)))) ((recv (enc gy b (privk ca))) (recv (cat gy (enc gy b (privk ca)))) (send (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gy gy dhkey)))) (recv (enc "check" n (enc "dh" gy gy dhkey)))) ((send (enc gy b (privk ca)))) ((recv (enc gy b (privk ca))) (send (cat gy (enc gy b (privk ca)))) (recv (cat gy (enc gy b-0 (privk ca)) (enc n (enc "dh" gy gy dhkey)))) (send (enc "check" n (enc "dh" gy gy dhkey))))) (label 81) (parent 74) (unrealized (0 0) (3 2)) (comment "2 in cohort - 2 not yet seen")) (defskeleton dhca (vars (dhkey skey) (n text) (gy akey) (b ca a b-0 ca-0 name)) (defstrand init 4 (dhkey dhkey) (n n) (gx gy) (h gy) (a b) (b b) (ca ca)) (defstrand resp 4 (dhkey dhkey) (n n) (gy gy) (h gy) (a b) (b b) (ca ca)) (defstrand ca 1 (gz gy) (subject b) (ca ca)) (defstrand init 4 (dhkey dhkey) (n n) (gx gy) (h gy) (a a) (b b-0) (ca ca-0)) (defstrand ca 1 (gz gy) (subject a) (ca ca-0)) (precedes ((1 2) (0 2)) ((1 2) (3 2)) ((2 0) (1 0)) ((3 3) (1 3)) ((4 0) (3 0))) (non-orig dhkey (invk gy) (privk ca) (privk ca-0)) (uniq-orig n) (operation encryption-test (added-strand ca 1) (enc gy a (privk ca-0)) (3 0)) (traces ((recv (enc gy b (privk ca))) (send (cat gy (enc gy b (privk ca)))) (recv (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gy gy dhkey)))) (send (enc "check" n (enc "dh" gy gy dhkey)))) ((recv (enc gy b (privk ca))) (recv (cat gy (enc gy b (privk ca)))) (send (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gy gy dhkey)))) (recv (enc "check" n (enc "dh" gy gy dhkey)))) ((send (enc gy b (privk ca)))) ((recv (enc gy a (privk ca-0))) (send (cat gy (enc gy a (privk ca-0)))) (recv (cat gy (enc gy b-0 (privk ca-0)) (enc n (enc "dh" gy gy dhkey)))) (send (enc "check" n (enc "dh" gy gy dhkey)))) ((send (enc gy a (privk ca-0))))) (label 82) (parent 74) (unrealized (0 0) (3 2)) (comment "3 in cohort - 3 not yet seen")) (defskeleton dhca (vars (dhkey skey) (n text) (gy akey) (b ca name)) (defstrand init 4 (dhkey dhkey) (n n) (gx gy) (h gy) (a b) (b b) (ca ca)) (defstrand resp 4 (dhkey dhkey) (n n) (gy gy) (h gy) (a b) (b b) (ca ca)) (defstrand ca 1 (gz gy) (subject b) (ca ca)) (defstrand ca 1 (gz gy) (subject b) (ca ca)) (precedes ((0 3) (1 3)) ((1 2) (0 2)) ((2 0) (0 0)) ((2 0) (1 0)) ((3 0) (1 1))) (non-orig dhkey (invk gy) (privk ca)) (uniq-orig n) (operation encryption-test (displaced 4 2 ca 1) (enc gx a (privk ca)) (0 0)) (traces ((recv (enc gy b (privk ca))) (send (cat gy (enc gy b (privk ca)))) (recv (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gy gy dhkey)))) (send (enc "check" n (enc "dh" gy gy dhkey)))) ((recv (enc gy b (privk ca))) (recv (cat gy (enc gy b (privk ca)))) (send (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gy gy dhkey)))) (recv (enc "check" n (enc "dh" gy gy dhkey)))) ((send (enc gy b (privk ca)))) ((send (enc gy b (privk ca))))) (label 83) (parent 76) (seen 79) (realized) (comment "1 in cohort - 0 not yet seen")) (defskeleton dhca (vars (dhkey skey) (n text) (gx gy akey) (a b ca name)) (defstrand init 4 (dhkey dhkey) (n n) (gx gx) (h gy) (a a) (b b) (ca ca)) (defstrand resp 4 (dhkey dhkey) (n n) (gy gy) (h gx) (a a) (b b) (ca ca)) (defstrand ca 1 (gz gy) (subject b) (ca ca)) (defstrand ca 1 (gz gx) (subject a) (ca ca)) (precedes ((0 3) (1 3)) ((1 2) (0 2)) ((2 0) (1 0)) ((3 0) (0 0)) ((3 0) (1 1))) (non-orig dhkey (invk gx) (invk gy) (privk ca)) (uniq-orig n) (operation encryption-test (displaced 4 3 ca 1) (enc gx a (privk ca)) (0 0)) (traces ((recv (enc gx a (privk ca))) (send (cat gx (enc gx a (privk ca)))) (recv (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gx gy dhkey)))) (send (enc "check" n (enc "dh" gx gy dhkey)))) ((recv (enc gy b (privk ca))) (recv (cat gx (enc gx a (privk ca)))) (send (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gx gy dhkey)))) (recv (enc "check" n (enc "dh" gx gy dhkey)))) ((send (enc gy b (privk ca)))) ((send (enc gx a (privk ca))))) (label 84) (parent 76) (realized) (shape) (maps ((0 1) ((a a) (b b) (ca ca) (gx gx) (gy gy) (n n) (dhkey dhkey)))) (origs (n (1 2)))) (defskeleton dhca (vars (dhkey skey) (n text) (gx gy akey) (a b ca name)) (defstrand init 4 (dhkey dhkey) (n n) (gx gx) (h gy) (a a) (b b) (ca ca)) (defstrand resp 4 (dhkey dhkey) (n n) (gy gy) (h gx) (a a) (b b) (ca ca)) (defstrand ca 1 (gz gy) (subject b) (ca ca)) (defstrand ca 1 (gz gx) (subject a) (ca ca)) (defstrand ca 1 (gz gx) (subject a) (ca ca)) (precedes ((0 3) (1 3)) ((1 2) (0 2)) ((2 0) (1 0)) ((3 0) (1 1)) ((4 0) (0 0))) (non-orig dhkey (invk gx) (invk gy) (privk ca)) (uniq-orig n) (operation encryption-test (added-strand ca 1) (enc gx a (privk ca)) (0 0)) (traces ((recv (enc gx a (privk ca))) (send (cat gx (enc gx a (privk ca)))) (recv (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gx gy dhkey)))) (send (enc "check" n (enc "dh" gx gy dhkey)))) ((recv (enc gy b (privk ca))) (recv (cat gx (enc gx a (privk ca)))) (send (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gx gy dhkey)))) (recv (enc "check" n (enc "dh" gx gy dhkey)))) ((send (enc gy b (privk ca)))) ((send (enc gx a (privk ca)))) ((send (enc gx a (privk ca))))) (label 85) (parent 76) (realized) (shape) (maps ((0 1) ((a a) (b b) (ca ca) (gx gx) (gy gy) (n n) (dhkey dhkey)))) (origs (n (1 2)))) (defskeleton dhca (vars (dhkey skey) (n text) (gy akey) (a b ca b-0 name)) (defstrand init 4 (dhkey dhkey) (n n) (gx gy) (h gy) (a a) (b b) (ca ca)) (defstrand resp 4 (dhkey dhkey) (n n) (gy gy) (h gy) (a a) (b b) (ca ca)) (defstrand ca 1 (gz gy) (subject b) (ca ca)) (defstrand ca 1 (gz gy) (subject a) (ca ca)) (defstrand init 4 (dhkey dhkey) (n n) (gx gy) (h gy) (a b) (b b-0) (ca ca)) (precedes ((1 2) (0 2)) ((1 2) (4 2)) ((2 0) (1 0)) ((2 0) (4 0)) ((3 0) (1 1)) ((4 3) (1 3))) (non-orig dhkey (invk gy) (privk ca)) (uniq-orig n) (operation encryption-test (displaced 5 2 ca 1) (enc gx a-0 (privk ca-0)) (4 0)) (traces ((recv (enc gy a (privk ca))) (send (cat gy (enc gy a (privk ca)))) (recv (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gy gy dhkey)))) (send (enc "check" n (enc "dh" gy gy dhkey)))) ((recv (enc gy b (privk ca))) (recv (cat gy (enc gy a (privk ca)))) (send (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gy gy dhkey)))) (recv (enc "check" n (enc "dh" gy gy dhkey)))) ((send (enc gy b (privk ca)))) ((send (enc gy a (privk ca)))) ((recv (enc gy b (privk ca))) (send (cat gy (enc gy b (privk ca)))) (recv (cat gy (enc gy b-0 (privk ca)) (enc n (enc "dh" gy gy dhkey)))) (send (enc "check" n (enc "dh" gy gy dhkey))))) (label 86) (parent 77) (unrealized (0 0) (4 2)) (comment "3 in cohort - 3 not yet seen")) (defskeleton dhca (vars (dhkey skey) (n text) (gx gy akey) (a b ca b-0 name)) (defstrand init 4 (dhkey dhkey) (n n) (gx gx) (h gy) (a a) (b b) (ca ca)) (defstrand resp 4 (dhkey dhkey) (n n) (gy gy) (h gx) (a a) (b b) (ca ca)) (defstrand ca 1 (gz gy) (subject b) (ca ca)) (defstrand ca 1 (gz gx) (subject a) (ca ca)) (defstrand init 4 (dhkey dhkey) (n n) (gx gx) (h gy) (a a) (b b-0) (ca ca)) (precedes ((1 2) (0 2)) ((1 2) (4 2)) ((2 0) (1 0)) ((3 0) (1 1)) ((3 0) (4 0)) ((4 3) (1 3))) (non-orig dhkey (invk gx) (invk gy) (privk ca)) (uniq-orig n) (operation encryption-test (displaced 5 3 ca 1) (enc gx a-0 (privk ca-0)) (4 0)) (traces ((recv (enc gx a (privk ca))) (send (cat gx (enc gx a (privk ca)))) (recv (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gx gy dhkey)))) (send (enc "check" n (enc "dh" gx gy dhkey)))) ((recv (enc gy b (privk ca))) (recv (cat gx (enc gx a (privk ca)))) (send (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gx gy dhkey)))) (recv (enc "check" n (enc "dh" gx gy dhkey)))) ((send (enc gy b (privk ca)))) ((send (enc gx a (privk ca)))) ((recv (enc gx a (privk ca))) (send (cat gx (enc gx a (privk ca)))) (recv (cat gy (enc gy b-0 (privk ca)) (enc n (enc "dh" gx gy dhkey)))) (send (enc "check" n (enc "dh" gx gy dhkey))))) (label 87) (parent 77) (unrealized (0 0) (4 2)) (comment "3 in cohort - 3 not yet seen")) (defskeleton dhca (vars (dhkey skey) (n text) (gx gy akey) (a b ca a-0 b-0 ca-0 name)) (defstrand init 4 (dhkey dhkey) (n n) (gx gx) (h gy) (a a) (b b) (ca ca)) (defstrand resp 4 (dhkey dhkey) (n n) (gy gy) (h gx) (a a) (b b) (ca ca)) (defstrand ca 1 (gz gy) (subject b) (ca ca)) (defstrand ca 1 (gz gx) (subject a) (ca ca)) (defstrand init 4 (dhkey dhkey) (n n) (gx gx) (h gy) (a a-0) (b b-0) (ca ca-0)) (defstrand ca 1 (gz gx) (subject a-0) (ca ca-0)) (precedes ((1 2) (0 2)) ((1 2) (4 2)) ((2 0) (1 0)) ((3 0) (1 1)) ((4 3) (1 3)) ((5 0) (4 0))) (non-orig dhkey (invk gx) (invk gy) (privk ca) (privk ca-0)) (uniq-orig n) (operation encryption-test (added-strand ca 1) (enc gx a-0 (privk ca-0)) (4 0)) (traces ((recv (enc gx a (privk ca))) (send (cat gx (enc gx a (privk ca)))) (recv (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gx gy dhkey)))) (send (enc "check" n (enc "dh" gx gy dhkey)))) ((recv (enc gy b (privk ca))) (recv (cat gx (enc gx a (privk ca)))) (send (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gx gy dhkey)))) (recv (enc "check" n (enc "dh" gx gy dhkey)))) ((send (enc gy b (privk ca)))) ((send (enc gx a (privk ca)))) ((recv (enc gx a-0 (privk ca-0))) (send (cat gx (enc gx a-0 (privk ca-0)))) (recv (cat gy (enc gy b-0 (privk ca-0)) (enc n (enc "dh" gx gy dhkey)))) (send (enc "check" n (enc "dh" gx gy dhkey)))) ((send (enc gx a-0 (privk ca-0))))) (label 88) (parent 77) (unrealized (0 0) (4 2)) (comment "4 in cohort - 4 not yet seen")) (defskeleton dhca (vars (dhkey skey) (n text) (gy akey) (b ca name)) (defstrand init 4 (dhkey dhkey) (n n) (gx gy) (h gy) (a b) (b b) (ca ca)) (defstrand resp 4 (dhkey dhkey) (n n) (gy gy) (h gy) (a b) (b b) (ca ca)) (defstrand ca 1 (gz gy) (subject b) (ca ca)) (defstrand init 4 (dhkey dhkey) (n n) (gx gy) (h gy) (a b) (b b) (ca ca)) (precedes ((1 2) (0 2)) ((1 2) (3 2)) ((2 0) (1 0)) ((2 0) (3 0)) ((3 3) (1 3))) (non-orig dhkey (invk gy) (privk ca)) (uniq-orig n) (operation encryption-test (displaced 4 2 ca 1) (enc gy b-0 (privk ca)) (3 2)) (traces ((recv (enc gy b (privk ca))) (send (cat gy (enc gy b (privk ca)))) (recv (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gy gy dhkey)))) (send (enc "check" n (enc "dh" gy gy dhkey)))) ((recv (enc gy b (privk ca))) (recv (cat gy (enc gy b (privk ca)))) (send (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gy gy dhkey)))) (recv (enc "check" n (enc "dh" gy gy dhkey)))) ((send (enc gy b (privk ca)))) ((recv (enc gy b (privk ca))) (send (cat gy (enc gy b (privk ca)))) (recv (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gy gy dhkey)))) (send (enc "check" n (enc "dh" gy gy dhkey))))) (label 89) (parent 81) (unrealized (0 0)) (comment "2 in cohort - 2 not yet seen")) (defskeleton dhca (vars (dhkey skey) (n text) (gy akey) (b ca b-0 name)) (defstrand init 4 (dhkey dhkey) (n n) (gx gy) (h gy) (a b) (b b) (ca ca)) (defstrand resp 4 (dhkey dhkey) (n n) (gy gy) (h gy) (a b) (b b) (ca ca)) (defstrand ca 1 (gz gy) (subject b) (ca ca)) (defstrand init 4 (dhkey dhkey) (n n) (gx gy) (h gy) (a b) (b b-0) (ca ca)) (defstrand ca 1 (gz gy) (subject b-0) (ca ca)) (precedes ((1 2) (0 2)) ((1 2) (3 2)) ((2 0) (1 0)) ((2 0) (3 0)) ((3 3) (1 3)) ((4 0) (3 2))) (non-orig dhkey (invk gy) (privk ca)) (uniq-orig n) (operation encryption-test (added-strand ca 1) (enc gy b-0 (privk ca)) (3 2)) (traces ((recv (enc gy b (privk ca))) (send (cat gy (enc gy b (privk ca)))) (recv (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gy gy dhkey)))) (send (enc "check" n (enc "dh" gy gy dhkey)))) ((recv (enc gy b (privk ca))) (recv (cat gy (enc gy b (privk ca)))) (send (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gy gy dhkey)))) (recv (enc "check" n (enc "dh" gy gy dhkey)))) ((send (enc gy b (privk ca)))) ((recv (enc gy b (privk ca))) (send (cat gy (enc gy b (privk ca)))) (recv (cat gy (enc gy b-0 (privk ca)) (enc n (enc "dh" gy gy dhkey)))) (send (enc "check" n (enc "dh" gy gy dhkey)))) ((send (enc gy b-0 (privk ca))))) (label 90) (parent 81) (unrealized (0 0)) (comment "3 in cohort - 3 not yet seen")) (defskeleton dhca (vars (dhkey skey) (n text) (gy akey) (b ca a name)) (defstrand init 4 (dhkey dhkey) (n n) (gx gy) (h gy) (a b) (b b) (ca ca)) (defstrand resp 4 (dhkey dhkey) (n n) (gy gy) (h gy) (a b) (b b) (ca ca)) (defstrand ca 1 (gz gy) (subject b) (ca ca)) (defstrand init 4 (dhkey dhkey) (n n) (gx gy) (h gy) (a a) (b b) (ca ca)) (defstrand ca 1 (gz gy) (subject a) (ca ca)) (precedes ((1 2) (0 2)) ((1 2) (3 2)) ((2 0) (1 0)) ((3 3) (1 3)) ((4 0) (3 0))) (non-orig dhkey (invk gy) (privk ca)) (uniq-orig n) (operation encryption-test (displaced 5 2 ca 1) (enc gy b-0 (privk ca-0)) (3 2)) (traces ((recv (enc gy b (privk ca))) (send (cat gy (enc gy b (privk ca)))) (recv (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gy gy dhkey)))) (send (enc "check" n (enc "dh" gy gy dhkey)))) ((recv (enc gy b (privk ca))) (recv (cat gy (enc gy b (privk ca)))) (send (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gy gy dhkey)))) (recv (enc "check" n (enc "dh" gy gy dhkey)))) ((send (enc gy b (privk ca)))) ((recv (enc gy a (privk ca))) (send (cat gy (enc gy a (privk ca)))) (recv (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gy gy dhkey)))) (send (enc "check" n (enc "dh" gy gy dhkey)))) ((send (enc gy a (privk ca))))) (label 91) (parent 82) (unrealized (0 0)) (comment "3 in cohort - 3 not yet seen")) (defskeleton dhca (vars (dhkey skey) (n text) (gy akey) (b ca a ca-0 name)) (defstrand init 4 (dhkey dhkey) (n n) (gx gy) (h gy) (a b) (b b) (ca ca)) (defstrand resp 4 (dhkey dhkey) (n n) (gy gy) (h gy) (a b) (b b) (ca ca)) (defstrand ca 1 (gz gy) (subject b) (ca ca)) (defstrand init 4 (dhkey dhkey) (n n) (gx gy) (h gy) (a a) (b a) (ca ca-0)) (defstrand ca 1 (gz gy) (subject a) (ca ca-0)) (precedes ((1 2) (0 2)) ((1 2) (3 2)) ((2 0) (1 0)) ((3 3) (1 3)) ((4 0) (3 0))) (non-orig dhkey (invk gy) (privk ca) (privk ca-0)) (uniq-orig n) (operation encryption-test (displaced 5 4 ca 1) (enc gy b-0 (privk ca-0)) (3 2)) (traces ((recv (enc gy b (privk ca))) (send (cat gy (enc gy b (privk ca)))) (recv (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gy gy dhkey)))) (send (enc "check" n (enc "dh" gy gy dhkey)))) ((recv (enc gy b (privk ca))) (recv (cat gy (enc gy b (privk ca)))) (send (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gy gy dhkey)))) (recv (enc "check" n (enc "dh" gy gy dhkey)))) ((send (enc gy b (privk ca)))) ((recv (enc gy a (privk ca-0))) (send (cat gy (enc gy a (privk ca-0)))) (recv (cat gy (enc gy a (privk ca-0)) (enc n (enc "dh" gy gy dhkey)))) (send (enc "check" n (enc "dh" gy gy dhkey)))) ((send (enc gy a (privk ca-0))))) (label 92) (parent 82) (seen 110) (unrealized (0 0)) (comment "3 in cohort - 2 not yet seen")) (defskeleton dhca (vars (dhkey skey) (n text) (gy akey) (b ca a b-0 ca-0 name)) (defstrand init 4 (dhkey dhkey) (n n) (gx gy) (h gy) (a b) (b b) (ca ca)) (defstrand resp 4 (dhkey dhkey) (n n) (gy gy) (h gy) (a b) (b b) (ca ca)) (defstrand ca 1 (gz gy) (subject b) (ca ca)) (defstrand init 4 (dhkey dhkey) (n n) (gx gy) (h gy) (a a) (b b-0) (ca ca-0)) (defstrand ca 1 (gz gy) (subject a) (ca ca-0)) (defstrand ca 1 (gz gy) (subject b-0) (ca ca-0)) (precedes ((1 2) (0 2)) ((1 2) (3 2)) ((2 0) (1 0)) ((3 3) (1 3)) ((4 0) (3 0)) ((5 0) (3 2))) (non-orig dhkey (invk gy) (privk ca) (privk ca-0)) (uniq-orig n) (operation encryption-test (added-strand ca 1) (enc gy b-0 (privk ca-0)) (3 2)) (traces ((recv (enc gy b (privk ca))) (send (cat gy (enc gy b (privk ca)))) (recv (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gy gy dhkey)))) (send (enc "check" n (enc "dh" gy gy dhkey)))) ((recv (enc gy b (privk ca))) (recv (cat gy (enc gy b (privk ca)))) (send (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gy gy dhkey)))) (recv (enc "check" n (enc "dh" gy gy dhkey)))) ((send (enc gy b (privk ca)))) ((recv (enc gy a (privk ca-0))) (send (cat gy (enc gy a (privk ca-0)))) (recv (cat gy (enc gy b-0 (privk ca-0)) (enc n (enc "dh" gy gy dhkey)))) (send (enc "check" n (enc "dh" gy gy dhkey)))) ((send (enc gy a (privk ca-0)))) ((send (enc gy b-0 (privk ca-0))))) (label 93) (parent 82) (unrealized (0 0)) (comment "4 in cohort - 4 not yet seen")) (defskeleton dhca (vars (dhkey skey) (n text) (gy akey) (a b ca name)) (defstrand init 4 (dhkey dhkey) (n n) (gx gy) (h gy) (a a) (b b) (ca ca)) (defstrand resp 4 (dhkey dhkey) (n n) (gy gy) (h gy) (a a) (b b) (ca ca)) (defstrand ca 1 (gz gy) (subject b) (ca ca)) (defstrand ca 1 (gz gy) (subject a) (ca ca)) (defstrand init 4 (dhkey dhkey) (n n) (gx gy) (h gy) (a b) (b b) (ca ca)) (precedes ((1 2) (0 2)) ((1 2) (4 2)) ((2 0) (1 0)) ((2 0) (4 0)) ((3 0) (1 1)) ((4 3) (1 3))) (non-orig dhkey (invk gy) (privk ca)) (uniq-orig n) (operation encryption-test (displaced 5 2 ca 1) (enc gy b-0 (privk ca)) (4 2)) (traces ((recv (enc gy a (privk ca))) (send (cat gy (enc gy a (privk ca)))) (recv (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gy gy dhkey)))) (send (enc "check" n (enc "dh" gy gy dhkey)))) ((recv (enc gy b (privk ca))) (recv (cat gy (enc gy a (privk ca)))) (send (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gy gy dhkey)))) (recv (enc "check" n (enc "dh" gy gy dhkey)))) ((send (enc gy b (privk ca)))) ((send (enc gy a (privk ca)))) ((recv (enc gy b (privk ca))) (send (cat gy (enc gy b (privk ca)))) (recv (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gy gy dhkey)))) (send (enc "check" n (enc "dh" gy gy dhkey))))) (label 94) (parent 86) (unrealized (0 0)) (comment "3 in cohort - 3 not yet seen")) (defskeleton dhca (vars (dhkey skey) (n text) (gy akey) (a b ca name)) (defstrand init 4 (dhkey dhkey) (n n) (gx gy) (h gy) (a a) (b b) (ca ca)) (defstrand resp 4 (dhkey dhkey) (n n) (gy gy) (h gy) (a a) (b b) (ca ca)) (defstrand ca 1 (gz gy) (subject b) (ca ca)) (defstrand ca 1 (gz gy) (subject a) (ca ca)) (defstrand init 4 (dhkey dhkey) (n n) (gx gy) (h gy) (a b) (b a) (ca ca)) (precedes ((1 2) (0 2)) ((1 2) (4 2)) ((2 0) (1 0)) ((2 0) (4 0)) ((3 0) (1 1)) ((4 3) (1 3))) (non-orig dhkey (invk gy) (privk ca)) (uniq-orig n) (operation encryption-test (displaced 5 3 ca 1) (enc gy b-0 (privk ca)) (4 2)) (traces ((recv (enc gy a (privk ca))) (send (cat gy (enc gy a (privk ca)))) (recv (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gy gy dhkey)))) (send (enc "check" n (enc "dh" gy gy dhkey)))) ((recv (enc gy b (privk ca))) (recv (cat gy (enc gy a (privk ca)))) (send (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gy gy dhkey)))) (recv (enc "check" n (enc "dh" gy gy dhkey)))) ((send (enc gy b (privk ca)))) ((send (enc gy a (privk ca)))) ((recv (enc gy b (privk ca))) (send (cat gy (enc gy b (privk ca)))) (recv (cat gy (enc gy a (privk ca)) (enc n (enc "dh" gy gy dhkey)))) (send (enc "check" n (enc "dh" gy gy dhkey))))) (label 95) (parent 86) (seen 118) (unrealized (0 0)) (comment "3 in cohort - 2 not yet seen")) (defskeleton dhca (vars (dhkey skey) (n text) (gy akey) (a b ca b-0 name)) (defstrand init 4 (dhkey dhkey) (n n) (gx gy) (h gy) (a a) (b b) (ca ca)) (defstrand resp 4 (dhkey dhkey) (n n) (gy gy) (h gy) (a a) (b b) (ca ca)) (defstrand ca 1 (gz gy) (subject b) (ca ca)) (defstrand ca 1 (gz gy) (subject a) (ca ca)) (defstrand init 4 (dhkey dhkey) (n n) (gx gy) (h gy) (a b) (b b-0) (ca ca)) (defstrand ca 1 (gz gy) (subject b-0) (ca ca)) (precedes ((1 2) (0 2)) ((1 2) (4 2)) ((2 0) (1 0)) ((2 0) (4 0)) ((3 0) (1 1)) ((4 3) (1 3)) ((5 0) (4 2))) (non-orig dhkey (invk gy) (privk ca)) (uniq-orig n) (operation encryption-test (added-strand ca 1) (enc gy b-0 (privk ca)) (4 2)) (traces ((recv (enc gy a (privk ca))) (send (cat gy (enc gy a (privk ca)))) (recv (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gy gy dhkey)))) (send (enc "check" n (enc "dh" gy gy dhkey)))) ((recv (enc gy b (privk ca))) (recv (cat gy (enc gy a (privk ca)))) (send (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gy gy dhkey)))) (recv (enc "check" n (enc "dh" gy gy dhkey)))) ((send (enc gy b (privk ca)))) ((send (enc gy a (privk ca)))) ((recv (enc gy b (privk ca))) (send (cat gy (enc gy b (privk ca)))) (recv (cat gy (enc gy b-0 (privk ca)) (enc n (enc "dh" gy gy dhkey)))) (send (enc "check" n (enc "dh" gy gy dhkey)))) ((send (enc gy b-0 (privk ca))))) (label 96) (parent 86) (unrealized (0 0)) (comment "4 in cohort - 4 not yet seen")) (defskeleton dhca (vars (dhkey skey) (n text) (gx gy akey) (a b ca name)) (defstrand init 4 (dhkey dhkey) (n n) (gx gx) (h gy) (a a) (b b) (ca ca)) (defstrand resp 4 (dhkey dhkey) (n n) (gy gy) (h gx) (a a) (b b) (ca ca)) (defstrand ca 1 (gz gy) (subject b) (ca ca)) (defstrand ca 1 (gz gx) (subject a) (ca ca)) (defstrand init 4 (dhkey dhkey) (n n) (gx gx) (h gy) (a a) (b b) (ca ca)) (precedes ((1 2) (0 2)) ((1 2) (4 2)) ((2 0) (1 0)) ((3 0) (1 1)) ((3 0) (4 0)) ((4 3) (1 3))) (non-orig dhkey (invk gx) (invk gy) (privk ca)) (uniq-orig n) (operation encryption-test (displaced 5 2 ca 1) (enc gy b-0 (privk ca)) (4 2)) (traces ((recv (enc gx a (privk ca))) (send (cat gx (enc gx a (privk ca)))) (recv (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gx gy dhkey)))) (send (enc "check" n (enc "dh" gx gy dhkey)))) ((recv (enc gy b (privk ca))) (recv (cat gx (enc gx a (privk ca)))) (send (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gx gy dhkey)))) (recv (enc "check" n (enc "dh" gx gy dhkey)))) ((send (enc gy b (privk ca)))) ((send (enc gx a (privk ca)))) ((recv (enc gx a (privk ca))) (send (cat gx (enc gx a (privk ca)))) (recv (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gx gy dhkey)))) (send (enc "check" n (enc "dh" gx gy dhkey))))) (label 97) (parent 87) (unrealized (0 0)) (comment "3 in cohort - 3 not yet seen")) (defskeleton dhca (vars (dhkey skey) (n text) (gx akey) (a b ca name)) (defstrand init 4 (dhkey dhkey) (n n) (gx gx) (h gx) (a a) (b b) (ca ca)) (defstrand resp 4 (dhkey dhkey) (n n) (gy gx) (h gx) (a a) (b b) (ca ca)) (defstrand ca 1 (gz gx) (subject b) (ca ca)) (defstrand ca 1 (gz gx) (subject a) (ca ca)) (defstrand init 4 (dhkey dhkey) (n n) (gx gx) (h gx) (a a) (b a) (ca ca)) (precedes ((1 2) (0 2)) ((1 2) (4 2)) ((2 0) (1 0)) ((3 0) (1 1)) ((3 0) (4 0)) ((4 3) (1 3))) (non-orig dhkey (invk gx) (privk ca)) (uniq-orig n) (operation encryption-test (displaced 5 3 ca 1) (enc gy b-0 (privk ca)) (4 2)) (traces ((recv (enc gx a (privk ca))) (send (cat gx (enc gx a (privk ca)))) (recv (cat gx (enc gx b (privk ca)) (enc n (enc "dh" gx gx dhkey)))) (send (enc "check" n (enc "dh" gx gx dhkey)))) ((recv (enc gx b (privk ca))) (recv (cat gx (enc gx a (privk ca)))) (send (cat gx (enc gx b (privk ca)) (enc n (enc "dh" gx gx dhkey)))) (recv (enc "check" n (enc "dh" gx gx dhkey)))) ((send (enc gx b (privk ca)))) ((send (enc gx a (privk ca)))) ((recv (enc gx a (privk ca))) (send (cat gx (enc gx a (privk ca)))) (recv (cat gx (enc gx a (privk ca)) (enc n (enc "dh" gx gx dhkey)))) (send (enc "check" n (enc "dh" gx gx dhkey))))) (label 98) (parent 87) (seen 127) (unrealized (0 0)) (comment "3 in cohort - 2 not yet seen")) (defskeleton dhca (vars (dhkey skey) (n text) (gx gy akey) (a b ca b-0 name)) (defstrand init 4 (dhkey dhkey) (n n) (gx gx) (h gy) (a a) (b b) (ca ca)) (defstrand resp 4 (dhkey dhkey) (n n) (gy gy) (h gx) (a a) (b b) (ca ca)) (defstrand ca 1 (gz gy) (subject b) (ca ca)) (defstrand ca 1 (gz gx) (subject a) (ca ca)) (defstrand init 4 (dhkey dhkey) (n n) (gx gx) (h gy) (a a) (b b-0) (ca ca)) (defstrand ca 1 (gz gy) (subject b-0) (ca ca)) (precedes ((1 2) (0 2)) ((1 2) (4 2)) ((2 0) (1 0)) ((3 0) (1 1)) ((3 0) (4 0)) ((4 3) (1 3)) ((5 0) (4 2))) (non-orig dhkey (invk gx) (invk gy) (privk ca)) (uniq-orig n) (operation encryption-test (added-strand ca 1) (enc gy b-0 (privk ca)) (4 2)) (traces ((recv (enc gx a (privk ca))) (send (cat gx (enc gx a (privk ca)))) (recv (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gx gy dhkey)))) (send (enc "check" n (enc "dh" gx gy dhkey)))) ((recv (enc gy b (privk ca))) (recv (cat gx (enc gx a (privk ca)))) (send (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gx gy dhkey)))) (recv (enc "check" n (enc "dh" gx gy dhkey)))) ((send (enc gy b (privk ca)))) ((send (enc gx a (privk ca)))) ((recv (enc gx a (privk ca))) (send (cat gx (enc gx a (privk ca)))) (recv (cat gy (enc gy b-0 (privk ca)) (enc n (enc "dh" gx gy dhkey)))) (send (enc "check" n (enc "dh" gx gy dhkey)))) ((send (enc gy b-0 (privk ca))))) (label 99) (parent 87) (unrealized (0 0)) (comment "4 in cohort - 4 not yet seen")) (defskeleton dhca (vars (dhkey skey) (n text) (gx akey) (a b ca a-0 name)) (defstrand init 4 (dhkey dhkey) (n n) (gx gx) (h gx) (a a) (b b) (ca ca)) (defstrand resp 4 (dhkey dhkey) (n n) (gy gx) (h gx) (a a) (b b) (ca ca)) (defstrand ca 1 (gz gx) (subject b) (ca ca)) (defstrand ca 1 (gz gx) (subject a) (ca ca)) (defstrand init 4 (dhkey dhkey) (n n) (gx gx) (h gx) (a a-0) (b a) (ca ca)) (defstrand ca 1 (gz gx) (subject a-0) (ca ca)) (precedes ((1 2) (0 2)) ((1 2) (4 2)) ((2 0) (1 0)) ((3 0) (1 1)) ((4 3) (1 3)) ((5 0) (4 0))) (non-orig dhkey (invk gx) (privk ca)) (uniq-orig n) (operation encryption-test (displaced 6 3 ca 1) (enc gy b-0 (privk ca-0)) (4 2)) (traces ((recv (enc gx a (privk ca))) (send (cat gx (enc gx a (privk ca)))) (recv (cat gx (enc gx b (privk ca)) (enc n (enc "dh" gx gx dhkey)))) (send (enc "check" n (enc "dh" gx gx dhkey)))) ((recv (enc gx b (privk ca))) (recv (cat gx (enc gx a (privk ca)))) (send (cat gx (enc gx b (privk ca)) (enc n (enc "dh" gx gx dhkey)))) (recv (enc "check" n (enc "dh" gx gx dhkey)))) ((send (enc gx b (privk ca)))) ((send (enc gx a (privk ca)))) ((recv (enc gx a-0 (privk ca))) (send (cat gx (enc gx a-0 (privk ca)))) (recv (cat gx (enc gx a (privk ca)) (enc n (enc "dh" gx gx dhkey)))) (send (enc "check" n (enc "dh" gx gx dhkey)))) ((send (enc gx a-0 (privk ca))))) (label 100) (parent 88) (unrealized (0 0)) (comment "4 in cohort - 4 not yet seen")) (defskeleton dhca (vars (dhkey skey) (n text) (gx gy akey) (a b ca a-0 name)) (defstrand init 4 (dhkey dhkey) (n n) (gx gx) (h gy) (a a) (b b) (ca ca)) (defstrand resp 4 (dhkey dhkey) (n n) (gy gy) (h gx) (a a) (b b) (ca ca)) (defstrand ca 1 (gz gy) (subject b) (ca ca)) (defstrand ca 1 (gz gx) (subject a) (ca ca)) (defstrand init 4 (dhkey dhkey) (n n) (gx gx) (h gy) (a a-0) (b b) (ca ca)) (defstrand ca 1 (gz gx) (subject a-0) (ca ca)) (precedes ((1 2) (0 2)) ((1 2) (4 2)) ((2 0) (1 0)) ((3 0) (1 1)) ((4 3) (1 3)) ((5 0) (4 0))) (non-orig dhkey (invk gx) (invk gy) (privk ca)) (uniq-orig n) (operation encryption-test (displaced 6 2 ca 1) (enc gy b-0 (privk ca-0)) (4 2)) (traces ((recv (enc gx a (privk ca))) (send (cat gx (enc gx a (privk ca)))) (recv (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gx gy dhkey)))) (send (enc "check" n (enc "dh" gx gy dhkey)))) ((recv (enc gy b (privk ca))) (recv (cat gx (enc gx a (privk ca)))) (send (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gx gy dhkey)))) (recv (enc "check" n (enc "dh" gx gy dhkey)))) ((send (enc gy b (privk ca)))) ((send (enc gx a (privk ca)))) ((recv (enc gx a-0 (privk ca))) (send (cat gx (enc gx a-0 (privk ca)))) (recv (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gx gy dhkey)))) (send (enc "check" n (enc "dh" gx gy dhkey)))) ((send (enc gx a-0 (privk ca))))) (label 101) (parent 88) (seen 137) (unrealized (0 0)) (comment "4 in cohort - 3 not yet seen")) (defskeleton dhca (vars (dhkey skey) (n text) (gx akey) (a b ca a-0 ca-0 name)) (defstrand init 4 (dhkey dhkey) (n n) (gx gx) (h gx) (a a) (b b) (ca ca)) (defstrand resp 4 (dhkey dhkey) (n n) (gy gx) (h gx) (a a) (b b) (ca ca)) (defstrand ca 1 (gz gx) (subject b) (ca ca)) (defstrand ca 1 (gz gx) (subject a) (ca ca)) (defstrand init 4 (dhkey dhkey) (n n) (gx gx) (h gx) (a a-0) (b a-0) (ca ca-0)) (defstrand ca 1 (gz gx) (subject a-0) (ca ca-0)) (precedes ((1 2) (0 2)) ((1 2) (4 2)) ((2 0) (1 0)) ((3 0) (1 1)) ((4 3) (1 3)) ((5 0) (4 0))) (non-orig dhkey (invk gx) (privk ca) (privk ca-0)) (uniq-orig n) (operation encryption-test (displaced 6 5 ca 1) (enc gy b-0 (privk ca-0)) (4 2)) (traces ((recv (enc gx a (privk ca))) (send (cat gx (enc gx a (privk ca)))) (recv (cat gx (enc gx b (privk ca)) (enc n (enc "dh" gx gx dhkey)))) (send (enc "check" n (enc "dh" gx gx dhkey)))) ((recv (enc gx b (privk ca))) (recv (cat gx (enc gx a (privk ca)))) (send (cat gx (enc gx b (privk ca)) (enc n (enc "dh" gx gx dhkey)))) (recv (enc "check" n (enc "dh" gx gx dhkey)))) ((send (enc gx b (privk ca)))) ((send (enc gx a (privk ca)))) ((recv (enc gx a-0 (privk ca-0))) (send (cat gx (enc gx a-0 (privk ca-0)))) (recv (cat gx (enc gx a-0 (privk ca-0)) (enc n (enc "dh" gx gx dhkey)))) (send (enc "check" n (enc "dh" gx gx dhkey)))) ((send (enc gx a-0 (privk ca-0))))) (label 102) (parent 88) (seen 138) (unrealized (0 0)) (comment "4 in cohort - 3 not yet seen")) (defskeleton dhca (vars (dhkey skey) (n text) (gx gy akey) (a b ca a-0 b-0 ca-0 name)) (defstrand init 4 (dhkey dhkey) (n n) (gx gx) (h gy) (a a) (b b) (ca ca)) (defstrand resp 4 (dhkey dhkey) (n n) (gy gy) (h gx) (a a) (b b) (ca ca)) (defstrand ca 1 (gz gy) (subject b) (ca ca)) (defstrand ca 1 (gz gx) (subject a) (ca ca)) (defstrand init 4 (dhkey dhkey) (n n) (gx gx) (h gy) (a a-0) (b b-0) (ca ca-0)) (defstrand ca 1 (gz gx) (subject a-0) (ca ca-0)) (defstrand ca 1 (gz gy) (subject b-0) (ca ca-0)) (precedes ((1 2) (0 2)) ((1 2) (4 2)) ((2 0) (1 0)) ((3 0) (1 1)) ((4 3) (1 3)) ((5 0) (4 0)) ((6 0) (4 2))) (non-orig dhkey (invk gx) (invk gy) (privk ca) (privk ca-0)) (uniq-orig n) (operation encryption-test (added-strand ca 1) (enc gy b-0 (privk ca-0)) (4 2)) (traces ((recv (enc gx a (privk ca))) (send (cat gx (enc gx a (privk ca)))) (recv (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gx gy dhkey)))) (send (enc "check" n (enc "dh" gx gy dhkey)))) ((recv (enc gy b (privk ca))) (recv (cat gx (enc gx a (privk ca)))) (send (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gx gy dhkey)))) (recv (enc "check" n (enc "dh" gx gy dhkey)))) ((send (enc gy b (privk ca)))) ((send (enc gx a (privk ca)))) ((recv (enc gx a-0 (privk ca-0))) (send (cat gx (enc gx a-0 (privk ca-0)))) (recv (cat gy (enc gy b-0 (privk ca-0)) (enc n (enc "dh" gx gy dhkey)))) (send (enc "check" n (enc "dh" gx gy dhkey)))) ((send (enc gx a-0 (privk ca-0)))) ((send (enc gy b-0 (privk ca-0))))) (label 103) (parent 88) (unrealized (0 0)) (comment "5 in cohort - 5 not yet seen")) (defskeleton dhca (vars (dhkey skey) (n text) (gy akey) (b ca name)) (defstrand init 4 (dhkey dhkey) (n n) (gx gy) (h gy) (a b) (b b) (ca ca)) (defstrand resp 4 (dhkey dhkey) (n n) (gy gy) (h gy) (a b) (b b) (ca ca)) (defstrand ca 1 (gz gy) (subject b) (ca ca)) (defstrand init 4 (dhkey dhkey) (n n) (gx gy) (h gy) (a b) (b b) (ca ca)) (precedes ((1 2) (0 2)) ((1 2) (3 2)) ((2 0) (0 0)) ((2 0) (1 0)) ((2 0) (3 0)) ((3 3) (1 3))) (non-orig dhkey (invk gy) (privk ca)) (uniq-orig n) (operation encryption-test (displaced 4 2 ca 1) (enc gy b (privk ca)) (0 0)) (traces ((recv (enc gy b (privk ca))) (send (cat gy (enc gy b (privk ca)))) (recv (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gy gy dhkey)))) (send (enc "check" n (enc "dh" gy gy dhkey)))) ((recv (enc gy b (privk ca))) (recv (cat gy (enc gy b (privk ca)))) (send (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gy gy dhkey)))) (recv (enc "check" n (enc "dh" gy gy dhkey)))) ((send (enc gy b (privk ca)))) ((recv (enc gy b (privk ca))) (send (cat gy (enc gy b (privk ca)))) (recv (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gy gy dhkey)))) (send (enc "check" n (enc "dh" gy gy dhkey))))) (label 104) (parent 89) (realized) (shape) (maps ((0 1) ((a b) (b b) (ca ca) (gx gy) (gy gy) (n n) (dhkey dhkey)))) (origs (n (1 2)))) (defskeleton dhca (vars (dhkey skey) (n text) (gy akey) (b ca name)) (defstrand init 4 (dhkey dhkey) (n n) (gx gy) (h gy) (a b) (b b) (ca ca)) (defstrand resp 4 (dhkey dhkey) (n n) (gy gy) (h gy) (a b) (b b) (ca ca)) (defstrand ca 1 (gz gy) (subject b) (ca ca)) (defstrand init 4 (dhkey dhkey) (n n) (gx gy) (h gy) (a b) (b b) (ca ca)) (defstrand ca 1 (gz gy) (subject b) (ca ca)) (precedes ((1 2) (0 2)) ((1 2) (3 2)) ((2 0) (1 0)) ((2 0) (3 0)) ((3 3) (1 3)) ((4 0) (0 0))) (non-orig dhkey (invk gy) (privk ca)) (uniq-orig n) (operation encryption-test (added-strand ca 1) (enc gy b (privk ca)) (0 0)) (traces ((recv (enc gy b (privk ca))) (send (cat gy (enc gy b (privk ca)))) (recv (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gy gy dhkey)))) (send (enc "check" n (enc "dh" gy gy dhkey)))) ((recv (enc gy b (privk ca))) (recv (cat gy (enc gy b (privk ca)))) (send (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gy gy dhkey)))) (recv (enc "check" n (enc "dh" gy gy dhkey)))) ((send (enc gy b (privk ca)))) ((recv (enc gy b (privk ca))) (send (cat gy (enc gy b (privk ca)))) (recv (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gy gy dhkey)))) (send (enc "check" n (enc "dh" gy gy dhkey)))) ((send (enc gy b (privk ca))))) (label 105) (parent 89) (realized) (shape) (maps ((0 1) ((a b) (b b) (ca ca) (gx gy) (gy gy) (n n) (dhkey dhkey)))) (origs (n (1 2)))) (defskeleton dhca (vars (dhkey skey) (n text) (gy akey) (b ca b-0 name)) (defstrand init 4 (dhkey dhkey) (n n) (gx gy) (h gy) (a b) (b b) (ca ca)) (defstrand resp 4 (dhkey dhkey) (n n) (gy gy) (h gy) (a b) (b b) (ca ca)) (defstrand ca 1 (gz gy) (subject b) (ca ca)) (defstrand init 4 (dhkey dhkey) (n n) (gx gy) (h gy) (a b) (b b-0) (ca ca)) (defstrand ca 1 (gz gy) (subject b-0) (ca ca)) (precedes ((1 2) (0 2)) ((1 2) (3 2)) ((2 0) (0 0)) ((2 0) (1 0)) ((2 0) (3 0)) ((3 3) (1 3)) ((4 0) (3 2))) (non-orig dhkey (invk gy) (privk ca)) (uniq-orig n) (operation encryption-test (displaced 5 2 ca 1) (enc gy b (privk ca)) (0 0)) (traces ((recv (enc gy b (privk ca))) (send (cat gy (enc gy b (privk ca)))) (recv (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gy gy dhkey)))) (send (enc "check" n (enc "dh" gy gy dhkey)))) ((recv (enc gy b (privk ca))) (recv (cat gy (enc gy b (privk ca)))) (send (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gy gy dhkey)))) (recv (enc "check" n (enc "dh" gy gy dhkey)))) ((send (enc gy b (privk ca)))) ((recv (enc gy b (privk ca))) (send (cat gy (enc gy b (privk ca)))) (recv (cat gy (enc gy b-0 (privk ca)) (enc n (enc "dh" gy gy dhkey)))) (send (enc "check" n (enc "dh" gy gy dhkey)))) ((send (enc gy b-0 (privk ca))))) (label 106) (parent 90) (realized) (shape) (maps ((0 1) ((a b) (b b) (ca ca) (gx gy) (gy gy) (n n) (dhkey dhkey)))) (origs (n (1 2)))) (defskeleton dhca (vars (dhkey skey) (n text) (gy akey) (ca b name)) (defstrand init 4 (dhkey dhkey) (n n) (gx gy) (h gy) (a b) (b b) (ca ca)) (defstrand resp 4 (dhkey dhkey) (n n) (gy gy) (h gy) (a b) (b b) (ca ca)) (defstrand ca 1 (gz gy) (subject b) (ca ca)) (defstrand init 4 (dhkey dhkey) (n n) (gx gy) (h gy) (a b) (b b) (ca ca)) (defstrand ca 1 (gz gy) (subject b) (ca ca)) (precedes ((1 2) (0 2)) ((1 2) (3 2)) ((2 0) (1 0)) ((2 0) (3 0)) ((3 3) (1 3)) ((4 0) (0 0)) ((4 0) (3 2))) (non-orig dhkey (invk gy) (privk ca)) (uniq-orig n) (operation encryption-test (displaced 5 4 ca 1) (enc gy b-0 (privk ca)) (0 0)) (traces ((recv (enc gy b (privk ca))) (send (cat gy (enc gy b (privk ca)))) (recv (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gy gy dhkey)))) (send (enc "check" n (enc "dh" gy gy dhkey)))) ((recv (enc gy b (privk ca))) (recv (cat gy (enc gy b (privk ca)))) (send (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gy gy dhkey)))) (recv (enc "check" n (enc "dh" gy gy dhkey)))) ((send (enc gy b (privk ca)))) ((recv (enc gy b (privk ca))) (send (cat gy (enc gy b (privk ca)))) (recv (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gy gy dhkey)))) (send (enc "check" n (enc "dh" gy gy dhkey)))) ((send (enc gy b (privk ca))))) (label 107) (parent 90) (realized) (comment "1 in cohort - 1 not yet seen")) (defskeleton dhca (vars (dhkey skey) (n text) (gy akey) (b ca b-0 name)) (defstrand init 4 (dhkey dhkey) (n n) (gx gy) (h gy) (a b) (b b) (ca ca)) (defstrand resp 4 (dhkey dhkey) (n n) (gy gy) (h gy) (a b) (b b) (ca ca)) (defstrand ca 1 (gz gy) (subject b) (ca ca)) (defstrand init 4 (dhkey dhkey) (n n) (gx gy) (h gy) (a b) (b b-0) (ca ca)) (defstrand ca 1 (gz gy) (subject b-0) (ca ca)) (defstrand ca 1 (gz gy) (subject b) (ca ca)) (precedes ((1 2) (0 2)) ((1 2) (3 2)) ((2 0) (1 0)) ((2 0) (3 0)) ((3 3) (1 3)) ((4 0) (3 2)) ((5 0) (0 0))) (non-orig dhkey (invk gy) (privk ca)) (uniq-orig n) (operation encryption-test (added-strand ca 1) (enc gy b (privk ca)) (0 0)) (traces ((recv (enc gy b (privk ca))) (send (cat gy (enc gy b (privk ca)))) (recv (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gy gy dhkey)))) (send (enc "check" n (enc "dh" gy gy dhkey)))) ((recv (enc gy b (privk ca))) (recv (cat gy (enc gy b (privk ca)))) (send (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gy gy dhkey)))) (recv (enc "check" n (enc "dh" gy gy dhkey)))) ((send (enc gy b (privk ca)))) ((recv (enc gy b (privk ca))) (send (cat gy (enc gy b (privk ca)))) (recv (cat gy (enc gy b-0 (privk ca)) (enc n (enc "dh" gy gy dhkey)))) (send (enc "check" n (enc "dh" gy gy dhkey)))) ((send (enc gy b-0 (privk ca)))) ((send (enc gy b (privk ca))))) (label 108) (parent 90) (realized) (shape) (maps ((0 1) ((a b) (b b) (ca ca) (gx gy) (gy gy) (n n) (dhkey dhkey)))) (origs (n (1 2)))) (defskeleton dhca (vars (dhkey skey) (n text) (gy akey) (b ca a name)) (defstrand init 4 (dhkey dhkey) (n n) (gx gy) (h gy) (a b) (b b) (ca ca)) (defstrand resp 4 (dhkey dhkey) (n n) (gy gy) (h gy) (a b) (b b) (ca ca)) (defstrand ca 1 (gz gy) (subject b) (ca ca)) (defstrand init 4 (dhkey dhkey) (n n) (gx gy) (h gy) (a a) (b b) (ca ca)) (defstrand ca 1 (gz gy) (subject a) (ca ca)) (precedes ((1 2) (0 2)) ((1 2) (3 2)) ((2 0) (0 0)) ((2 0) (1 0)) ((3 3) (1 3)) ((4 0) (3 0))) (non-orig dhkey (invk gy) (privk ca)) (uniq-orig n) (operation encryption-test (displaced 5 2 ca 1) (enc gy b (privk ca)) (0 0)) (traces ((recv (enc gy b (privk ca))) (send (cat gy (enc gy b (privk ca)))) (recv (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gy gy dhkey)))) (send (enc "check" n (enc "dh" gy gy dhkey)))) ((recv (enc gy b (privk ca))) (recv (cat gy (enc gy b (privk ca)))) (send (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gy gy dhkey)))) (recv (enc "check" n (enc "dh" gy gy dhkey)))) ((send (enc gy b (privk ca)))) ((recv (enc gy a (privk ca))) (send (cat gy (enc gy a (privk ca)))) (recv (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gy gy dhkey)))) (send (enc "check" n (enc "dh" gy gy dhkey)))) ((send (enc gy a (privk ca))))) (label 109) (parent 91) (realized) (shape) (maps ((0 1) ((a b) (b b) (ca ca) (gx gy) (gy gy) (n n) (dhkey dhkey)))) (origs (n (1 2)))) (defskeleton dhca (vars (dhkey skey) (n text) (gy akey) (ca a name)) (defstrand init 4 (dhkey dhkey) (n n) (gx gy) (h gy) (a a) (b a) (ca ca)) (defstrand resp 4 (dhkey dhkey) (n n) (gy gy) (h gy) (a a) (b a) (ca ca)) (defstrand ca 1 (gz gy) (subject a) (ca ca)) (defstrand init 4 (dhkey dhkey) (n n) (gx gy) (h gy) (a a) (b a) (ca ca)) (defstrand ca 1 (gz gy) (subject a) (ca ca)) (precedes ((1 2) (0 2)) ((1 2) (3 2)) ((2 0) (1 0)) ((3 3) (1 3)) ((4 0) (0 0)) ((4 0) (3 0))) (non-orig dhkey (invk gy) (privk ca)) (uniq-orig n) (operation encryption-test (displaced 5 4 ca 1) (enc gy b (privk ca)) (0 0)) (traces ((recv (enc gy a (privk ca))) (send (cat gy (enc gy a (privk ca)))) (recv (cat gy (enc gy a (privk ca)) (enc n (enc "dh" gy gy dhkey)))) (send (enc "check" n (enc "dh" gy gy dhkey)))) ((recv (enc gy a (privk ca))) (recv (cat gy (enc gy a (privk ca)))) (send (cat gy (enc gy a (privk ca)) (enc n (enc "dh" gy gy dhkey)))) (recv (enc "check" n (enc "dh" gy gy dhkey)))) ((send (enc gy a (privk ca)))) ((recv (enc gy a (privk ca))) (send (cat gy (enc gy a (privk ca)))) (recv (cat gy (enc gy a (privk ca)) (enc n (enc "dh" gy gy dhkey)))) (send (enc "check" n (enc "dh" gy gy dhkey)))) ((send (enc gy a (privk ca))))) (label 110) (parent 91) (realized) (shape) (maps ((0 1) ((a a) (b a) (ca ca) (gx gy) (gy gy) (n n) (dhkey dhkey)))) (origs (n (1 2)))) (defskeleton dhca (vars (dhkey skey) (n text) (gy akey) (b ca a name)) (defstrand init 4 (dhkey dhkey) (n n) (gx gy) (h gy) (a b) (b b) (ca ca)) (defstrand resp 4 (dhkey dhkey) (n n) (gy gy) (h gy) (a b) (b b) (ca ca)) (defstrand ca 1 (gz gy) (subject b) (ca ca)) (defstrand init 4 (dhkey dhkey) (n n) (gx gy) (h gy) (a a) (b b) (ca ca)) (defstrand ca 1 (gz gy) (subject a) (ca ca)) (defstrand ca 1 (gz gy) (subject b) (ca ca)) (precedes ((1 2) (0 2)) ((1 2) (3 2)) ((2 0) (1 0)) ((3 3) (1 3)) ((4 0) (3 0)) ((5 0) (0 0))) (non-orig dhkey (invk gy) (privk ca)) (uniq-orig n) (operation encryption-test (added-strand ca 1) (enc gy b (privk ca)) (0 0)) (traces ((recv (enc gy b (privk ca))) (send (cat gy (enc gy b (privk ca)))) (recv (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gy gy dhkey)))) (send (enc "check" n (enc "dh" gy gy dhkey)))) ((recv (enc gy b (privk ca))) (recv (cat gy (enc gy b (privk ca)))) (send (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gy gy dhkey)))) (recv (enc "check" n (enc "dh" gy gy dhkey)))) ((send (enc gy b (privk ca)))) ((recv (enc gy a (privk ca))) (send (cat gy (enc gy a (privk ca)))) (recv (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gy gy dhkey)))) (send (enc "check" n (enc "dh" gy gy dhkey)))) ((send (enc gy a (privk ca)))) ((send (enc gy b (privk ca))))) (label 111) (parent 91) (realized) (shape) (maps ((0 1) ((a b) (b b) (ca ca) (gx gy) (gy gy) (n n) (dhkey dhkey)))) (origs (n (1 2)))) (defskeleton dhca (vars (dhkey skey) (n text) (gy akey) (b ca a ca-0 name)) (defstrand init 4 (dhkey dhkey) (n n) (gx gy) (h gy) (a b) (b b) (ca ca)) (defstrand resp 4 (dhkey dhkey) (n n) (gy gy) (h gy) (a b) (b b) (ca ca)) (defstrand ca 1 (gz gy) (subject b) (ca ca)) (defstrand init 4 (dhkey dhkey) (n n) (gx gy) (h gy) (a a) (b a) (ca ca-0)) (defstrand ca 1 (gz gy) (subject a) (ca ca-0)) (precedes ((1 2) (0 2)) ((1 2) (3 2)) ((2 0) (0 0)) ((2 0) (1 0)) ((3 3) (1 3)) ((4 0) (3 0))) (non-orig dhkey (invk gy) (privk ca) (privk ca-0)) (uniq-orig n) (operation encryption-test (displaced 5 2 ca 1) (enc gy b (privk ca)) (0 0)) (traces ((recv (enc gy b (privk ca))) (send (cat gy (enc gy b (privk ca)))) (recv (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gy gy dhkey)))) (send (enc "check" n (enc "dh" gy gy dhkey)))) ((recv (enc gy b (privk ca))) (recv (cat gy (enc gy b (privk ca)))) (send (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gy gy dhkey)))) (recv (enc "check" n (enc "dh" gy gy dhkey)))) ((send (enc gy b (privk ca)))) ((recv (enc gy a (privk ca-0))) (send (cat gy (enc gy a (privk ca-0)))) (recv (cat gy (enc gy a (privk ca-0)) (enc n (enc "dh" gy gy dhkey)))) (send (enc "check" n (enc "dh" gy gy dhkey)))) ((send (enc gy a (privk ca-0))))) (label 112) (parent 92) (realized) (shape) (maps ((0 1) ((a b) (b b) (ca ca) (gx gy) (gy gy) (n n) (dhkey dhkey)))) (origs (n (1 2)))) (defskeleton dhca (vars (dhkey skey) (n text) (gy akey) (b ca a ca-0 name)) (defstrand init 4 (dhkey dhkey) (n n) (gx gy) (h gy) (a b) (b b) (ca ca)) (defstrand resp 4 (dhkey dhkey) (n n) (gy gy) (h gy) (a b) (b b) (ca ca)) (defstrand ca 1 (gz gy) (subject b) (ca ca)) (defstrand init 4 (dhkey dhkey) (n n) (gx gy) (h gy) (a a) (b a) (ca ca-0)) (defstrand ca 1 (gz gy) (subject a) (ca ca-0)) (defstrand ca 1 (gz gy) (subject b) (ca ca)) (precedes ((1 2) (0 2)) ((1 2) (3 2)) ((2 0) (1 0)) ((3 3) (1 3)) ((4 0) (3 0)) ((5 0) (0 0))) (non-orig dhkey (invk gy) (privk ca) (privk ca-0)) (uniq-orig n) (operation encryption-test (added-strand ca 1) (enc gy b (privk ca)) (0 0)) (traces ((recv (enc gy b (privk ca))) (send (cat gy (enc gy b (privk ca)))) (recv (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gy gy dhkey)))) (send (enc "check" n (enc "dh" gy gy dhkey)))) ((recv (enc gy b (privk ca))) (recv (cat gy (enc gy b (privk ca)))) (send (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gy gy dhkey)))) (recv (enc "check" n (enc "dh" gy gy dhkey)))) ((send (enc gy b (privk ca)))) ((recv (enc gy a (privk ca-0))) (send (cat gy (enc gy a (privk ca-0)))) (recv (cat gy (enc gy a (privk ca-0)) (enc n (enc "dh" gy gy dhkey)))) (send (enc "check" n (enc "dh" gy gy dhkey)))) ((send (enc gy a (privk ca-0)))) ((send (enc gy b (privk ca))))) (label 113) (parent 92) (realized) (shape) (maps ((0 1) ((a b) (b b) (ca ca) (gx gy) (gy gy) (n n) (dhkey dhkey)))) (origs (n (1 2)))) (defskeleton dhca (vars (dhkey skey) (n text) (gy akey) (a b ca name)) (defstrand init 4 (dhkey dhkey) (n n) (gx gy) (h gy) (a a) (b a) (ca ca)) (defstrand resp 4 (dhkey dhkey) (n n) (gy gy) (h gy) (a a) (b a) (ca ca)) (defstrand ca 1 (gz gy) (subject a) (ca ca)) (defstrand init 4 (dhkey dhkey) (n n) (gx gy) (h gy) (a a) (b b) (ca ca)) (defstrand ca 1 (gz gy) (subject a) (ca ca)) (defstrand ca 1 (gz gy) (subject b) (ca ca)) (precedes ((1 2) (0 2)) ((1 2) (3 2)) ((2 0) (1 0)) ((3 3) (1 3)) ((4 0) (0 0)) ((4 0) (3 0)) ((5 0) (3 2))) (non-orig dhkey (invk gy) (privk ca)) (uniq-orig n) (operation encryption-test (displaced 6 4 ca 1) (enc gy b-0 (privk ca-0)) (0 0)) (traces ((recv (enc gy a (privk ca))) (send (cat gy (enc gy a (privk ca)))) (recv (cat gy (enc gy a (privk ca)) (enc n (enc "dh" gy gy dhkey)))) (send (enc "check" n (enc "dh" gy gy dhkey)))) ((recv (enc gy a (privk ca))) (recv (cat gy (enc gy a (privk ca)))) (send (cat gy (enc gy a (privk ca)) (enc n (enc "dh" gy gy dhkey)))) (recv (enc "check" n (enc "dh" gy gy dhkey)))) ((send (enc gy a (privk ca)))) ((recv (enc gy a (privk ca))) (send (cat gy (enc gy a (privk ca)))) (recv (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gy gy dhkey)))) (send (enc "check" n (enc "dh" gy gy dhkey)))) ((send (enc gy a (privk ca)))) ((send (enc gy b (privk ca))))) (label 114) (parent 93) (realized) (shape) (maps ((0 1) ((a a) (b a) (ca ca) (gx gy) (gy gy) (n n) (dhkey dhkey)))) (origs (n (1 2)))) (defskeleton dhca (vars (dhkey skey) (n text) (gy akey) (b ca a b-0 ca-0 name)) (defstrand init 4 (dhkey dhkey) (n n) (gx gy) (h gy) (a b) (b b) (ca ca)) (defstrand resp 4 (dhkey dhkey) (n n) (gy gy) (h gy) (a b) (b b) (ca ca)) (defstrand ca 1 (gz gy) (subject b) (ca ca)) (defstrand init 4 (dhkey dhkey) (n n) (gx gy) (h gy) (a a) (b b-0) (ca ca-0)) (defstrand ca 1 (gz gy) (subject a) (ca ca-0)) (defstrand ca 1 (gz gy) (subject b-0) (ca ca-0)) (precedes ((1 2) (0 2)) ((1 2) (3 2)) ((2 0) (0 0)) ((2 0) (1 0)) ((3 3) (1 3)) ((4 0) (3 0)) ((5 0) (3 2))) (non-orig dhkey (invk gy) (privk ca) (privk ca-0)) (uniq-orig n) (operation encryption-test (displaced 6 2 ca 1) (enc gy b (privk ca)) (0 0)) (traces ((recv (enc gy b (privk ca))) (send (cat gy (enc gy b (privk ca)))) (recv (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gy gy dhkey)))) (send (enc "check" n (enc "dh" gy gy dhkey)))) ((recv (enc gy b (privk ca))) (recv (cat gy (enc gy b (privk ca)))) (send (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gy gy dhkey)))) (recv (enc "check" n (enc "dh" gy gy dhkey)))) ((send (enc gy b (privk ca)))) ((recv (enc gy a (privk ca-0))) (send (cat gy (enc gy a (privk ca-0)))) (recv (cat gy (enc gy b-0 (privk ca-0)) (enc n (enc "dh" gy gy dhkey)))) (send (enc "check" n (enc "dh" gy gy dhkey)))) ((send (enc gy a (privk ca-0)))) ((send (enc gy b-0 (privk ca-0))))) (label 115) (parent 93) (realized) (shape) (maps ((0 1) ((a b) (b b) (ca ca) (gx gy) (gy gy) (n n) (dhkey dhkey)))) (origs (n (1 2)))) (defskeleton dhca (vars (dhkey skey) (n text) (gy akey) (a b ca name)) (defstrand init 4 (dhkey dhkey) (n n) (gx gy) (h gy) (a b) (b b) (ca ca)) (defstrand resp 4 (dhkey dhkey) (n n) (gy gy) (h gy) (a b) (b b) (ca ca)) (defstrand ca 1 (gz gy) (subject b) (ca ca)) (defstrand init 4 (dhkey dhkey) (n n) (gx gy) (h gy) (a a) (b b) (ca ca)) (defstrand ca 1 (gz gy) (subject a) (ca ca)) (defstrand ca 1 (gz gy) (subject b) (ca ca)) (precedes ((1 2) (0 2)) ((1 2) (3 2)) ((2 0) (1 0)) ((3 3) (1 3)) ((4 0) (3 0)) ((5 0) (0 0)) ((5 0) (3 2))) (non-orig dhkey (invk gy) (privk ca)) (uniq-orig n) (operation encryption-test (displaced 6 5 ca 1) (enc gy b-0 (privk ca-0)) (0 0)) (traces ((recv (enc gy b (privk ca))) (send (cat gy (enc gy b (privk ca)))) (recv (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gy gy dhkey)))) (send (enc "check" n (enc "dh" gy gy dhkey)))) ((recv (enc gy b (privk ca))) (recv (cat gy (enc gy b (privk ca)))) (send (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gy gy dhkey)))) (recv (enc "check" n (enc "dh" gy gy dhkey)))) ((send (enc gy b (privk ca)))) ((recv (enc gy a (privk ca))) (send (cat gy (enc gy a (privk ca)))) (recv (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gy gy dhkey)))) (send (enc "check" n (enc "dh" gy gy dhkey)))) ((send (enc gy a (privk ca)))) ((send (enc gy b (privk ca))))) (label 116) (parent 93) (realized) (comment "1 in cohort - 1 not yet seen")) (defskeleton dhca (vars (dhkey skey) (n text) (gy akey) (b ca a b-0 ca-0 name)) (defstrand init 4 (dhkey dhkey) (n n) (gx gy) (h gy) (a b) (b b) (ca ca)) (defstrand resp 4 (dhkey dhkey) (n n) (gy gy) (h gy) (a b) (b b) (ca ca)) (defstrand ca 1 (gz gy) (subject b) (ca ca)) (defstrand init 4 (dhkey dhkey) (n n) (gx gy) (h gy) (a a) (b b-0) (ca ca-0)) (defstrand ca 1 (gz gy) (subject a) (ca ca-0)) (defstrand ca 1 (gz gy) (subject b-0) (ca ca-0)) (defstrand ca 1 (gz gy) (subject b) (ca ca)) (precedes ((1 2) (0 2)) ((1 2) (3 2)) ((2 0) (1 0)) ((3 3) (1 3)) ((4 0) (3 0)) ((5 0) (3 2)) ((6 0) (0 0))) (non-orig dhkey (invk gy) (privk ca) (privk ca-0)) (uniq-orig n) (operation encryption-test (added-strand ca 1) (enc gy b (privk ca)) (0 0)) (traces ((recv (enc gy b (privk ca))) (send (cat gy (enc gy b (privk ca)))) (recv (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gy gy dhkey)))) (send (enc "check" n (enc "dh" gy gy dhkey)))) ((recv (enc gy b (privk ca))) (recv (cat gy (enc gy b (privk ca)))) (send (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gy gy dhkey)))) (recv (enc "check" n (enc "dh" gy gy dhkey)))) ((send (enc gy b (privk ca)))) ((recv (enc gy a (privk ca-0))) (send (cat gy (enc gy a (privk ca-0)))) (recv (cat gy (enc gy b-0 (privk ca-0)) (enc n (enc "dh" gy gy dhkey)))) (send (enc "check" n (enc "dh" gy gy dhkey)))) ((send (enc gy a (privk ca-0)))) ((send (enc gy b-0 (privk ca-0)))) ((send (enc gy b (privk ca))))) (label 117) (parent 93) (realized) (shape) (maps ((0 1) ((a b) (b b) (ca ca) (gx gy) (gy gy) (n n) (dhkey dhkey)))) (origs (n (1 2)))) (defskeleton dhca (vars (dhkey skey) (n text) (gy akey) (b ca name)) (defstrand init 4 (dhkey dhkey) (n n) (gx gy) (h gy) (a b) (b b) (ca ca)) (defstrand resp 4 (dhkey dhkey) (n n) (gy gy) (h gy) (a b) (b b) (ca ca)) (defstrand ca 1 (gz gy) (subject b) (ca ca)) (defstrand ca 1 (gz gy) (subject b) (ca ca)) (defstrand init 4 (dhkey dhkey) (n n) (gx gy) (h gy) (a b) (b b) (ca ca)) (precedes ((1 2) (0 2)) ((1 2) (4 2)) ((2 0) (0 0)) ((2 0) (1 0)) ((2 0) (4 0)) ((3 0) (1 1)) ((4 3) (1 3))) (non-orig dhkey (invk gy) (privk ca)) (uniq-orig n) (operation encryption-test (displaced 5 2 ca 1) (enc gy a (privk ca)) (0 0)) (traces ((recv (enc gy b (privk ca))) (send (cat gy (enc gy b (privk ca)))) (recv (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gy gy dhkey)))) (send (enc "check" n (enc "dh" gy gy dhkey)))) ((recv (enc gy b (privk ca))) (recv (cat gy (enc gy b (privk ca)))) (send (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gy gy dhkey)))) (recv (enc "check" n (enc "dh" gy gy dhkey)))) ((send (enc gy b (privk ca)))) ((send (enc gy b (privk ca)))) ((recv (enc gy b (privk ca))) (send (cat gy (enc gy b (privk ca)))) (recv (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gy gy dhkey)))) (send (enc "check" n (enc "dh" gy gy dhkey))))) (label 118) (parent 94) (seen 104) (realized) (comment "1 in cohort - 0 not yet seen")) (defskeleton dhca (vars (dhkey skey) (n text) (gy akey) (a b ca name)) (defstrand init 4 (dhkey dhkey) (n n) (gx gy) (h gy) (a a) (b b) (ca ca)) (defstrand resp 4 (dhkey dhkey) (n n) (gy gy) (h gy) (a a) (b b) (ca ca)) (defstrand ca 1 (gz gy) (subject b) (ca ca)) (defstrand ca 1 (gz gy) (subject a) (ca ca)) (defstrand init 4 (dhkey dhkey) (n n) (gx gy) (h gy) (a b) (b b) (ca ca)) (precedes ((1 2) (0 2)) ((1 2) (4 2)) ((2 0) (1 0)) ((2 0) (4 0)) ((3 0) (0 0)) ((3 0) (1 1)) ((4 3) (1 3))) (non-orig dhkey (invk gy) (privk ca)) (uniq-orig n) (operation encryption-test (displaced 5 3 ca 1) (enc gy a (privk ca)) (0 0)) (traces ((recv (enc gy a (privk ca))) (send (cat gy (enc gy a (privk ca)))) (recv (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gy gy dhkey)))) (send (enc "check" n (enc "dh" gy gy dhkey)))) ((recv (enc gy b (privk ca))) (recv (cat gy (enc gy a (privk ca)))) (send (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gy gy dhkey)))) (recv (enc "check" n (enc "dh" gy gy dhkey)))) ((send (enc gy b (privk ca)))) ((send (enc gy a (privk ca)))) ((recv (enc gy b (privk ca))) (send (cat gy (enc gy b (privk ca)))) (recv (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gy gy dhkey)))) (send (enc "check" n (enc "dh" gy gy dhkey))))) (label 119) (parent 94) (realized) (shape) (maps ((0 1) ((a a) (b b) (ca ca) (gx gy) (gy gy) (n n) (dhkey dhkey)))) (origs (n (1 2)))) (defskeleton dhca (vars (dhkey skey) (n text) (gy akey) (a b ca name)) (defstrand init 4 (dhkey dhkey) (n n) (gx gy) (h gy) (a a) (b b) (ca ca)) (defstrand resp 4 (dhkey dhkey) (n n) (gy gy) (h gy) (a a) (b b) (ca ca)) (defstrand ca 1 (gz gy) (subject b) (ca ca)) (defstrand ca 1 (gz gy) (subject a) (ca ca)) (defstrand init 4 (dhkey dhkey) (n n) (gx gy) (h gy) (a b) (b b) (ca ca)) (defstrand ca 1 (gz gy) (subject a) (ca ca)) (precedes ((1 2) (0 2)) ((1 2) (4 2)) ((2 0) (1 0)) ((2 0) (4 0)) ((3 0) (1 1)) ((4 3) (1 3)) ((5 0) (0 0))) (non-orig dhkey (invk gy) (privk ca)) (uniq-orig n) (operation encryption-test (added-strand ca 1) (enc gy a (privk ca)) (0 0)) (traces ((recv (enc gy a (privk ca))) (send (cat gy (enc gy a (privk ca)))) (recv (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gy gy dhkey)))) (send (enc "check" n (enc "dh" gy gy dhkey)))) ((recv (enc gy b (privk ca))) (recv (cat gy (enc gy a (privk ca)))) (send (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gy gy dhkey)))) (recv (enc "check" n (enc "dh" gy gy dhkey)))) ((send (enc gy b (privk ca)))) ((send (enc gy a (privk ca)))) ((recv (enc gy b (privk ca))) (send (cat gy (enc gy b (privk ca)))) (recv (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gy gy dhkey)))) (send (enc "check" n (enc "dh" gy gy dhkey)))) ((send (enc gy a (privk ca))))) (label 120) (parent 94) (realized) (shape) (maps ((0 1) ((a a) (b b) (ca ca) (gx gy) (gy gy) (n n) (dhkey dhkey)))) (origs (n (1 2)))) (defskeleton dhca (vars (dhkey skey) (n text) (gy akey) (a b ca name)) (defstrand init 4 (dhkey dhkey) (n n) (gx gy) (h gy) (a a) (b b) (ca ca)) (defstrand resp 4 (dhkey dhkey) (n n) (gy gy) (h gy) (a a) (b b) (ca ca)) (defstrand ca 1 (gz gy) (subject b) (ca ca)) (defstrand ca 1 (gz gy) (subject a) (ca ca)) (defstrand init 4 (dhkey dhkey) (n n) (gx gy) (h gy) (a b) (b a) (ca ca)) (precedes ((1 2) (0 2)) ((1 2) (4 2)) ((2 0) (1 0)) ((2 0) (4 0)) ((3 0) (0 0)) ((3 0) (1 1)) ((4 3) (1 3))) (non-orig dhkey (invk gy) (privk ca)) (uniq-orig n) (operation encryption-test (displaced 5 3 ca 1) (enc gy a (privk ca)) (0 0)) (traces ((recv (enc gy a (privk ca))) (send (cat gy (enc gy a (privk ca)))) (recv (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gy gy dhkey)))) (send (enc "check" n (enc "dh" gy gy dhkey)))) ((recv (enc gy b (privk ca))) (recv (cat gy (enc gy a (privk ca)))) (send (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gy gy dhkey)))) (recv (enc "check" n (enc "dh" gy gy dhkey)))) ((send (enc gy b (privk ca)))) ((send (enc gy a (privk ca)))) ((recv (enc gy b (privk ca))) (send (cat gy (enc gy b (privk ca)))) (recv (cat gy (enc gy a (privk ca)) (enc n (enc "dh" gy gy dhkey)))) (send (enc "check" n (enc "dh" gy gy dhkey))))) (label 121) (parent 95) (realized) (shape) (maps ((0 1) ((a a) (b b) (ca ca) (gx gy) (gy gy) (n n) (dhkey dhkey)))) (origs (n (1 2)))) (defskeleton dhca (vars (dhkey skey) (n text) (gy akey) (a b ca name)) (defstrand init 4 (dhkey dhkey) (n n) (gx gy) (h gy) (a a) (b b) (ca ca)) (defstrand resp 4 (dhkey dhkey) (n n) (gy gy) (h gy) (a a) (b b) (ca ca)) (defstrand ca 1 (gz gy) (subject b) (ca ca)) (defstrand ca 1 (gz gy) (subject a) (ca ca)) (defstrand init 4 (dhkey dhkey) (n n) (gx gy) (h gy) (a b) (b a) (ca ca)) (defstrand ca 1 (gz gy) (subject a) (ca ca)) (precedes ((1 2) (0 2)) ((1 2) (4 2)) ((2 0) (1 0)) ((2 0) (4 0)) ((3 0) (1 1)) ((4 3) (1 3)) ((5 0) (0 0))) (non-orig dhkey (invk gy) (privk ca)) (uniq-orig n) (operation encryption-test (added-strand ca 1) (enc gy a (privk ca)) (0 0)) (traces ((recv (enc gy a (privk ca))) (send (cat gy (enc gy a (privk ca)))) (recv (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gy gy dhkey)))) (send (enc "check" n (enc "dh" gy gy dhkey)))) ((recv (enc gy b (privk ca))) (recv (cat gy (enc gy a (privk ca)))) (send (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gy gy dhkey)))) (recv (enc "check" n (enc "dh" gy gy dhkey)))) ((send (enc gy b (privk ca)))) ((send (enc gy a (privk ca)))) ((recv (enc gy b (privk ca))) (send (cat gy (enc gy b (privk ca)))) (recv (cat gy (enc gy a (privk ca)) (enc n (enc "dh" gy gy dhkey)))) (send (enc "check" n (enc "dh" gy gy dhkey)))) ((send (enc gy a (privk ca))))) (label 122) (parent 95) (realized) (shape) (maps ((0 1) ((a a) (b b) (ca ca) (gx gy) (gy gy) (n n) (dhkey dhkey)))) (origs (n (1 2)))) (defskeleton dhca (vars (dhkey skey) (n text) (gy akey) (a b ca b-0 name)) (defstrand init 4 (dhkey dhkey) (n n) (gx gy) (h gy) (a a) (b b) (ca ca)) (defstrand resp 4 (dhkey dhkey) (n n) (gy gy) (h gy) (a a) (b b) (ca ca)) (defstrand ca 1 (gz gy) (subject b) (ca ca)) (defstrand ca 1 (gz gy) (subject a) (ca ca)) (defstrand init 4 (dhkey dhkey) (n n) (gx gy) (h gy) (a b) (b b-0) (ca ca)) (defstrand ca 1 (gz gy) (subject b-0) (ca ca)) (precedes ((1 2) (0 2)) ((1 2) (4 2)) ((2 0) (1 0)) ((2 0) (4 0)) ((3 0) (0 0)) ((3 0) (1 1)) ((4 3) (1 3)) ((5 0) (4 2))) (non-orig dhkey (invk gy) (privk ca)) (uniq-orig n) (operation encryption-test (displaced 6 3 ca 1) (enc gy a (privk ca)) (0 0)) (traces ((recv (enc gy a (privk ca))) (send (cat gy (enc gy a (privk ca)))) (recv (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gy gy dhkey)))) (send (enc "check" n (enc "dh" gy gy dhkey)))) ((recv (enc gy b (privk ca))) (recv (cat gy (enc gy a (privk ca)))) (send (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gy gy dhkey)))) (recv (enc "check" n (enc "dh" gy gy dhkey)))) ((send (enc gy b (privk ca)))) ((send (enc gy a (privk ca)))) ((recv (enc gy b (privk ca))) (send (cat gy (enc gy b (privk ca)))) (recv (cat gy (enc gy b-0 (privk ca)) (enc n (enc "dh" gy gy dhkey)))) (send (enc "check" n (enc "dh" gy gy dhkey)))) ((send (enc gy b-0 (privk ca))))) (label 123) (parent 96) (realized) (shape) (maps ((0 1) ((a a) (b b) (ca ca) (gx gy) (gy gy) (n n) (dhkey dhkey)))) (origs (n (1 2)))) (defskeleton dhca (vars (dhkey skey) (n text) (gy akey) (b ca b-0 name)) (defstrand init 4 (dhkey dhkey) (n n) (gx gy) (h gy) (a b) (b b) (ca ca)) (defstrand resp 4 (dhkey dhkey) (n n) (gy gy) (h gy) (a b) (b b) (ca ca)) (defstrand ca 1 (gz gy) (subject b) (ca ca)) (defstrand ca 1 (gz gy) (subject b) (ca ca)) (defstrand init 4 (dhkey dhkey) (n n) (gx gy) (h gy) (a b) (b b-0) (ca ca)) (defstrand ca 1 (gz gy) (subject b-0) (ca ca)) (precedes ((1 2) (0 2)) ((1 2) (4 2)) ((2 0) (0 0)) ((2 0) (1 0)) ((2 0) (4 0)) ((3 0) (1 1)) ((4 3) (1 3)) ((5 0) (4 2))) (non-orig dhkey (invk gy) (privk ca)) (uniq-orig n) (operation encryption-test (displaced 6 2 ca 1) (enc gy a (privk ca)) (0 0)) (traces ((recv (enc gy b (privk ca))) (send (cat gy (enc gy b (privk ca)))) (recv (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gy gy dhkey)))) (send (enc "check" n (enc "dh" gy gy dhkey)))) ((recv (enc gy b (privk ca))) (recv (cat gy (enc gy b (privk ca)))) (send (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gy gy dhkey)))) (recv (enc "check" n (enc "dh" gy gy dhkey)))) ((send (enc gy b (privk ca)))) ((send (enc gy b (privk ca)))) ((recv (enc gy b (privk ca))) (send (cat gy (enc gy b (privk ca)))) (recv (cat gy (enc gy b-0 (privk ca)) (enc n (enc "dh" gy gy dhkey)))) (send (enc "check" n (enc "dh" gy gy dhkey)))) ((send (enc gy b-0 (privk ca))))) (label 124) (parent 96) (seen 106) (realized) (comment "1 in cohort - 0 not yet seen")) (defskeleton dhca (vars (dhkey skey) (n text) (gy akey) (b ca b-0 name)) (defstrand init 4 (dhkey dhkey) (n n) (gx gy) (h gy) (a b-0) (b b) (ca ca)) (defstrand resp 4 (dhkey dhkey) (n n) (gy gy) (h gy) (a b-0) (b b) (ca ca)) (defstrand ca 1 (gz gy) (subject b) (ca ca)) (defstrand ca 1 (gz gy) (subject b-0) (ca ca)) (defstrand init 4 (dhkey dhkey) (n n) (gx gy) (h gy) (a b) (b b-0) (ca ca)) (defstrand ca 1 (gz gy) (subject b-0) (ca ca)) (precedes ((1 2) (0 2)) ((1 2) (4 2)) ((2 0) (1 0)) ((2 0) (4 0)) ((3 0) (1 1)) ((4 3) (1 3)) ((5 0) (0 0)) ((5 0) (4 2))) (non-orig dhkey (invk gy) (privk ca)) (uniq-orig n) (operation encryption-test (displaced 6 5 ca 1) (enc gy a (privk ca)) (0 0)) (traces ((recv (enc gy b-0 (privk ca))) (send (cat gy (enc gy b-0 (privk ca)))) (recv (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gy gy dhkey)))) (send (enc "check" n (enc "dh" gy gy dhkey)))) ((recv (enc gy b (privk ca))) (recv (cat gy (enc gy b-0 (privk ca)))) (send (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gy gy dhkey)))) (recv (enc "check" n (enc "dh" gy gy dhkey)))) ((send (enc gy b (privk ca)))) ((send (enc gy b-0 (privk ca)))) ((recv (enc gy b (privk ca))) (send (cat gy (enc gy b (privk ca)))) (recv (cat gy (enc gy b-0 (privk ca)) (enc n (enc "dh" gy gy dhkey)))) (send (enc "check" n (enc "dh" gy gy dhkey)))) ((send (enc gy b-0 (privk ca))))) (label 125) (parent 96) (realized) (comment "1 in cohort - 1 not yet seen")) (defskeleton dhca (vars (dhkey skey) (n text) (gy akey) (a b ca b-0 name)) (defstrand init 4 (dhkey dhkey) (n n) (gx gy) (h gy) (a a) (b b) (ca ca)) (defstrand resp 4 (dhkey dhkey) (n n) (gy gy) (h gy) (a a) (b b) (ca ca)) (defstrand ca 1 (gz gy) (subject b) (ca ca)) (defstrand ca 1 (gz gy) (subject a) (ca ca)) (defstrand init 4 (dhkey dhkey) (n n) (gx gy) (h gy) (a b) (b b-0) (ca ca)) (defstrand ca 1 (gz gy) (subject b-0) (ca ca)) (defstrand ca 1 (gz gy) (subject a) (ca ca)) (precedes ((1 2) (0 2)) ((1 2) (4 2)) ((2 0) (1 0)) ((2 0) (4 0)) ((3 0) (1 1)) ((4 3) (1 3)) ((5 0) (4 2)) ((6 0) (0 0))) (non-orig dhkey (invk gy) (privk ca)) (uniq-orig n) (operation encryption-test (added-strand ca 1) (enc gy a (privk ca)) (0 0)) (traces ((recv (enc gy a (privk ca))) (send (cat gy (enc gy a (privk ca)))) (recv (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gy gy dhkey)))) (send (enc "check" n (enc "dh" gy gy dhkey)))) ((recv (enc gy b (privk ca))) (recv (cat gy (enc gy a (privk ca)))) (send (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gy gy dhkey)))) (recv (enc "check" n (enc "dh" gy gy dhkey)))) ((send (enc gy b (privk ca)))) ((send (enc gy a (privk ca)))) ((recv (enc gy b (privk ca))) (send (cat gy (enc gy b (privk ca)))) (recv (cat gy (enc gy b-0 (privk ca)) (enc n (enc "dh" gy gy dhkey)))) (send (enc "check" n (enc "dh" gy gy dhkey)))) ((send (enc gy b-0 (privk ca)))) ((send (enc gy a (privk ca))))) (label 126) (parent 96) (realized) (shape) (maps ((0 1) ((a a) (b b) (ca ca) (gx gy) (gy gy) (n n) (dhkey dhkey)))) (origs (n (1 2)))) (defskeleton dhca (vars (dhkey skey) (n text) (gy akey) (b ca name)) (defstrand init 4 (dhkey dhkey) (n n) (gx gy) (h gy) (a b) (b b) (ca ca)) (defstrand resp 4 (dhkey dhkey) (n n) (gy gy) (h gy) (a b) (b b) (ca ca)) (defstrand ca 1 (gz gy) (subject b) (ca ca)) (defstrand ca 1 (gz gy) (subject b) (ca ca)) (defstrand init 4 (dhkey dhkey) (n n) (gx gy) (h gy) (a b) (b b) (ca ca)) (precedes ((1 2) (0 2)) ((1 2) (4 2)) ((2 0) (0 0)) ((2 0) (1 0)) ((3 0) (1 1)) ((3 0) (4 0)) ((4 3) (1 3))) (non-orig dhkey (invk gy) (privk ca)) (uniq-orig n) (operation encryption-test (displaced 5 2 ca 1) (enc gx a (privk ca)) (0 0)) (traces ((recv (enc gy b (privk ca))) (send (cat gy (enc gy b (privk ca)))) (recv (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gy gy dhkey)))) (send (enc "check" n (enc "dh" gy gy dhkey)))) ((recv (enc gy b (privk ca))) (recv (cat gy (enc gy b (privk ca)))) (send (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gy gy dhkey)))) (recv (enc "check" n (enc "dh" gy gy dhkey)))) ((send (enc gy b (privk ca)))) ((send (enc gy b (privk ca)))) ((recv (enc gy b (privk ca))) (send (cat gy (enc gy b (privk ca)))) (recv (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gy gy dhkey)))) (send (enc "check" n (enc "dh" gy gy dhkey))))) (label 127) (parent 97) (realized) (comment "1 in cohort - 1 not yet seen")) (defskeleton dhca (vars (dhkey skey) (n text) (gx gy akey) (a b ca name)) (defstrand init 4 (dhkey dhkey) (n n) (gx gx) (h gy) (a a) (b b) (ca ca)) (defstrand resp 4 (dhkey dhkey) (n n) (gy gy) (h gx) (a a) (b b) (ca ca)) (defstrand ca 1 (gz gy) (subject b) (ca ca)) (defstrand ca 1 (gz gx) (subject a) (ca ca)) (defstrand init 4 (dhkey dhkey) (n n) (gx gx) (h gy) (a a) (b b) (ca ca)) (precedes ((1 2) (0 2)) ((1 2) (4 2)) ((2 0) (1 0)) ((3 0) (0 0)) ((3 0) (1 1)) ((3 0) (4 0)) ((4 3) (1 3))) (non-orig dhkey (invk gx) (invk gy) (privk ca)) (uniq-orig n) (operation encryption-test (displaced 5 3 ca 1) (enc gx a (privk ca)) (0 0)) (traces ((recv (enc gx a (privk ca))) (send (cat gx (enc gx a (privk ca)))) (recv (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gx gy dhkey)))) (send (enc "check" n (enc "dh" gx gy dhkey)))) ((recv (enc gy b (privk ca))) (recv (cat gx (enc gx a (privk ca)))) (send (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gx gy dhkey)))) (recv (enc "check" n (enc "dh" gx gy dhkey)))) ((send (enc gy b (privk ca)))) ((send (enc gx a (privk ca)))) ((recv (enc gx a (privk ca))) (send (cat gx (enc gx a (privk ca)))) (recv (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gx gy dhkey)))) (send (enc "check" n (enc "dh" gx gy dhkey))))) (label 128) (parent 97) (realized) (shape) (maps ((0 1) ((a a) (b b) (ca ca) (gx gx) (gy gy) (n n) (dhkey dhkey)))) (origs (n (1 2)))) (defskeleton dhca (vars (dhkey skey) (n text) (gx gy akey) (a b ca name)) (defstrand init 4 (dhkey dhkey) (n n) (gx gx) (h gy) (a a) (b b) (ca ca)) (defstrand resp 4 (dhkey dhkey) (n n) (gy gy) (h gx) (a a) (b b) (ca ca)) (defstrand ca 1 (gz gy) (subject b) (ca ca)) (defstrand ca 1 (gz gx) (subject a) (ca ca)) (defstrand init 4 (dhkey dhkey) (n n) (gx gx) (h gy) (a a) (b b) (ca ca)) (defstrand ca 1 (gz gx) (subject a) (ca ca)) (precedes ((1 2) (0 2)) ((1 2) (4 2)) ((2 0) (1 0)) ((3 0) (1 1)) ((3 0) (4 0)) ((4 3) (1 3)) ((5 0) (0 0))) (non-orig dhkey (invk gx) (invk gy) (privk ca)) (uniq-orig n) (operation encryption-test (added-strand ca 1) (enc gx a (privk ca)) (0 0)) (traces ((recv (enc gx a (privk ca))) (send (cat gx (enc gx a (privk ca)))) (recv (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gx gy dhkey)))) (send (enc "check" n (enc "dh" gx gy dhkey)))) ((recv (enc gy b (privk ca))) (recv (cat gx (enc gx a (privk ca)))) (send (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gx gy dhkey)))) (recv (enc "check" n (enc "dh" gx gy dhkey)))) ((send (enc gy b (privk ca)))) ((send (enc gx a (privk ca)))) ((recv (enc gx a (privk ca))) (send (cat gx (enc gx a (privk ca)))) (recv (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gx gy dhkey)))) (send (enc "check" n (enc "dh" gx gy dhkey)))) ((send (enc gx a (privk ca))))) (label 129) (parent 97) (realized) (shape) (maps ((0 1) ((a a) (b b) (ca ca) (gx gx) (gy gy) (n n) (dhkey dhkey)))) (origs (n (1 2)))) (defskeleton dhca (vars (dhkey skey) (n text) (gx akey) (a b ca name)) (defstrand init 4 (dhkey dhkey) (n n) (gx gx) (h gx) (a a) (b b) (ca ca)) (defstrand resp 4 (dhkey dhkey) (n n) (gy gx) (h gx) (a a) (b b) (ca ca)) (defstrand ca 1 (gz gx) (subject b) (ca ca)) (defstrand ca 1 (gz gx) (subject a) (ca ca)) (defstrand init 4 (dhkey dhkey) (n n) (gx gx) (h gx) (a a) (b a) (ca ca)) (precedes ((1 2) (0 2)) ((1 2) (4 2)) ((2 0) (1 0)) ((3 0) (0 0)) ((3 0) (1 1)) ((3 0) (4 0)) ((4 3) (1 3))) (non-orig dhkey (invk gx) (privk ca)) (uniq-orig n) (operation encryption-test (displaced 5 3 ca 1) (enc gx a (privk ca)) (0 0)) (traces ((recv (enc gx a (privk ca))) (send (cat gx (enc gx a (privk ca)))) (recv (cat gx (enc gx b (privk ca)) (enc n (enc "dh" gx gx dhkey)))) (send (enc "check" n (enc "dh" gx gx dhkey)))) ((recv (enc gx b (privk ca))) (recv (cat gx (enc gx a (privk ca)))) (send (cat gx (enc gx b (privk ca)) (enc n (enc "dh" gx gx dhkey)))) (recv (enc "check" n (enc "dh" gx gx dhkey)))) ((send (enc gx b (privk ca)))) ((send (enc gx a (privk ca)))) ((recv (enc gx a (privk ca))) (send (cat gx (enc gx a (privk ca)))) (recv (cat gx (enc gx a (privk ca)) (enc n (enc "dh" gx gx dhkey)))) (send (enc "check" n (enc "dh" gx gx dhkey))))) (label 130) (parent 98) (realized) (shape) (maps ((0 1) ((a a) (b b) (ca ca) (gx gx) (gy gx) (n n) (dhkey dhkey)))) (origs (n (1 2)))) (defskeleton dhca (vars (dhkey skey) (n text) (gx akey) (a b ca name)) (defstrand init 4 (dhkey dhkey) (n n) (gx gx) (h gx) (a a) (b b) (ca ca)) (defstrand resp 4 (dhkey dhkey) (n n) (gy gx) (h gx) (a a) (b b) (ca ca)) (defstrand ca 1 (gz gx) (subject b) (ca ca)) (defstrand ca 1 (gz gx) (subject a) (ca ca)) (defstrand init 4 (dhkey dhkey) (n n) (gx gx) (h gx) (a a) (b a) (ca ca)) (defstrand ca 1 (gz gx) (subject a) (ca ca)) (precedes ((1 2) (0 2)) ((1 2) (4 2)) ((2 0) (1 0)) ((3 0) (1 1)) ((3 0) (4 0)) ((4 3) (1 3)) ((5 0) (0 0))) (non-orig dhkey (invk gx) (privk ca)) (uniq-orig n) (operation encryption-test (added-strand ca 1) (enc gx a (privk ca)) (0 0)) (traces ((recv (enc gx a (privk ca))) (send (cat gx (enc gx a (privk ca)))) (recv (cat gx (enc gx b (privk ca)) (enc n (enc "dh" gx gx dhkey)))) (send (enc "check" n (enc "dh" gx gx dhkey)))) ((recv (enc gx b (privk ca))) (recv (cat gx (enc gx a (privk ca)))) (send (cat gx (enc gx b (privk ca)) (enc n (enc "dh" gx gx dhkey)))) (recv (enc "check" n (enc "dh" gx gx dhkey)))) ((send (enc gx b (privk ca)))) ((send (enc gx a (privk ca)))) ((recv (enc gx a (privk ca))) (send (cat gx (enc gx a (privk ca)))) (recv (cat gx (enc gx a (privk ca)) (enc n (enc "dh" gx gx dhkey)))) (send (enc "check" n (enc "dh" gx gx dhkey)))) ((send (enc gx a (privk ca))))) (label 131) (parent 98) (realized) (shape) (maps ((0 1) ((a a) (b b) (ca ca) (gx gx) (gy gx) (n n) (dhkey dhkey)))) (origs (n (1 2)))) (defskeleton dhca (vars (dhkey skey) (n text) (gx gy akey) (a b ca b-0 name)) (defstrand init 4 (dhkey dhkey) (n n) (gx gx) (h gy) (a a) (b b) (ca ca)) (defstrand resp 4 (dhkey dhkey) (n n) (gy gy) (h gx) (a a) (b b) (ca ca)) (defstrand ca 1 (gz gy) (subject b) (ca ca)) (defstrand ca 1 (gz gx) (subject a) (ca ca)) (defstrand init 4 (dhkey dhkey) (n n) (gx gx) (h gy) (a a) (b b-0) (ca ca)) (defstrand ca 1 (gz gy) (subject b-0) (ca ca)) (precedes ((1 2) (0 2)) ((1 2) (4 2)) ((2 0) (1 0)) ((3 0) (0 0)) ((3 0) (1 1)) ((3 0) (4 0)) ((4 3) (1 3)) ((5 0) (4 2))) (non-orig dhkey (invk gx) (invk gy) (privk ca)) (uniq-orig n) (operation encryption-test (displaced 6 3 ca 1) (enc gx a (privk ca)) (0 0)) (traces ((recv (enc gx a (privk ca))) (send (cat gx (enc gx a (privk ca)))) (recv (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gx gy dhkey)))) (send (enc "check" n (enc "dh" gx gy dhkey)))) ((recv (enc gy b (privk ca))) (recv (cat gx (enc gx a (privk ca)))) (send (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gx gy dhkey)))) (recv (enc "check" n (enc "dh" gx gy dhkey)))) ((send (enc gy b (privk ca)))) ((send (enc gx a (privk ca)))) ((recv (enc gx a (privk ca))) (send (cat gx (enc gx a (privk ca)))) (recv (cat gy (enc gy b-0 (privk ca)) (enc n (enc "dh" gx gy dhkey)))) (send (enc "check" n (enc "dh" gx gy dhkey)))) ((send (enc gy b-0 (privk ca))))) (label 132) (parent 99) (realized) (shape) (maps ((0 1) ((a a) (b b) (ca ca) (gx gx) (gy gy) (n n) (dhkey dhkey)))) (origs (n (1 2)))) (defskeleton dhca (vars (dhkey skey) (n text) (gy akey) (b ca b-0 name)) (defstrand init 4 (dhkey dhkey) (n n) (gx gy) (h gy) (a b) (b b) (ca ca)) (defstrand resp 4 (dhkey dhkey) (n n) (gy gy) (h gy) (a b) (b b) (ca ca)) (defstrand ca 1 (gz gy) (subject b) (ca ca)) (defstrand ca 1 (gz gy) (subject b) (ca ca)) (defstrand init 4 (dhkey dhkey) (n n) (gx gy) (h gy) (a b) (b b-0) (ca ca)) (defstrand ca 1 (gz gy) (subject b-0) (ca ca)) (precedes ((1 2) (0 2)) ((1 2) (4 2)) ((2 0) (0 0)) ((2 0) (1 0)) ((3 0) (1 1)) ((3 0) (4 0)) ((4 3) (1 3)) ((5 0) (4 2))) (non-orig dhkey (invk gy) (privk ca)) (uniq-orig n) (operation encryption-test (displaced 6 2 ca 1) (enc gx a (privk ca)) (0 0)) (traces ((recv (enc gy b (privk ca))) (send (cat gy (enc gy b (privk ca)))) (recv (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gy gy dhkey)))) (send (enc "check" n (enc "dh" gy gy dhkey)))) ((recv (enc gy b (privk ca))) (recv (cat gy (enc gy b (privk ca)))) (send (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gy gy dhkey)))) (recv (enc "check" n (enc "dh" gy gy dhkey)))) ((send (enc gy b (privk ca)))) ((send (enc gy b (privk ca)))) ((recv (enc gy b (privk ca))) (send (cat gy (enc gy b (privk ca)))) (recv (cat gy (enc gy b-0 (privk ca)) (enc n (enc "dh" gy gy dhkey)))) (send (enc "check" n (enc "dh" gy gy dhkey)))) ((send (enc gy b-0 (privk ca))))) (label 133) (parent 99) (realized) (comment "1 in cohort - 1 not yet seen")) (defskeleton dhca (vars (dhkey skey) (n text) (gy akey) (b ca b-0 name)) (defstrand init 4 (dhkey dhkey) (n n) (gx gy) (h gy) (a b-0) (b b) (ca ca)) (defstrand resp 4 (dhkey dhkey) (n n) (gy gy) (h gy) (a b-0) (b b) (ca ca)) (defstrand ca 1 (gz gy) (subject b) (ca ca)) (defstrand ca 1 (gz gy) (subject b-0) (ca ca)) (defstrand init 4 (dhkey dhkey) (n n) (gx gy) (h gy) (a b-0) (b b-0) (ca ca)) (defstrand ca 1 (gz gy) (subject b-0) (ca ca)) (precedes ((1 2) (0 2)) ((1 2) (4 2)) ((2 0) (1 0)) ((3 0) (1 1)) ((3 0) (4 0)) ((4 3) (1 3)) ((5 0) (0 0)) ((5 0) (4 2))) (non-orig dhkey (invk gy) (privk ca)) (uniq-orig n) (operation encryption-test (displaced 6 5 ca 1) (enc gx a (privk ca)) (0 0)) (traces ((recv (enc gy b-0 (privk ca))) (send (cat gy (enc gy b-0 (privk ca)))) (recv (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gy gy dhkey)))) (send (enc "check" n (enc "dh" gy gy dhkey)))) ((recv (enc gy b (privk ca))) (recv (cat gy (enc gy b-0 (privk ca)))) (send (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gy gy dhkey)))) (recv (enc "check" n (enc "dh" gy gy dhkey)))) ((send (enc gy b (privk ca)))) ((send (enc gy b-0 (privk ca)))) ((recv (enc gy b-0 (privk ca))) (send (cat gy (enc gy b-0 (privk ca)))) (recv (cat gy (enc gy b-0 (privk ca)) (enc n (enc "dh" gy gy dhkey)))) (send (enc "check" n (enc "dh" gy gy dhkey)))) ((send (enc gy b-0 (privk ca))))) (label 134) (parent 99) (realized) (comment "1 in cohort - 1 not yet seen")) (defskeleton dhca (vars (dhkey skey) (n text) (gx gy akey) (a b ca b-0 name)) (defstrand init 4 (dhkey dhkey) (n n) (gx gx) (h gy) (a a) (b b) (ca ca)) (defstrand resp 4 (dhkey dhkey) (n n) (gy gy) (h gx) (a a) (b b) (ca ca)) (defstrand ca 1 (gz gy) (subject b) (ca ca)) (defstrand ca 1 (gz gx) (subject a) (ca ca)) (defstrand init 4 (dhkey dhkey) (n n) (gx gx) (h gy) (a a) (b b-0) (ca ca)) (defstrand ca 1 (gz gy) (subject b-0) (ca ca)) (defstrand ca 1 (gz gx) (subject a) (ca ca)) (precedes ((1 2) (0 2)) ((1 2) (4 2)) ((2 0) (1 0)) ((3 0) (1 1)) ((3 0) (4 0)) ((4 3) (1 3)) ((5 0) (4 2)) ((6 0) (0 0))) (non-orig dhkey (invk gx) (invk gy) (privk ca)) (uniq-orig n) (operation encryption-test (added-strand ca 1) (enc gx a (privk ca)) (0 0)) (traces ((recv (enc gx a (privk ca))) (send (cat gx (enc gx a (privk ca)))) (recv (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gx gy dhkey)))) (send (enc "check" n (enc "dh" gx gy dhkey)))) ((recv (enc gy b (privk ca))) (recv (cat gx (enc gx a (privk ca)))) (send (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gx gy dhkey)))) (recv (enc "check" n (enc "dh" gx gy dhkey)))) ((send (enc gy b (privk ca)))) ((send (enc gx a (privk ca)))) ((recv (enc gx a (privk ca))) (send (cat gx (enc gx a (privk ca)))) (recv (cat gy (enc gy b-0 (privk ca)) (enc n (enc "dh" gx gy dhkey)))) (send (enc "check" n (enc "dh" gx gy dhkey)))) ((send (enc gy b-0 (privk ca)))) ((send (enc gx a (privk ca))))) (label 135) (parent 99) (realized) (shape) (maps ((0 1) ((a a) (b b) (ca ca) (gx gx) (gy gy) (n n) (dhkey dhkey)))) (origs (n (1 2)))) (defskeleton dhca (vars (dhkey skey) (n text) (gx akey) (a b ca a-0 name)) (defstrand init 4 (dhkey dhkey) (n n) (gx gx) (h gx) (a a) (b b) (ca ca)) (defstrand resp 4 (dhkey dhkey) (n n) (gy gx) (h gx) (a a) (b b) (ca ca)) (defstrand ca 1 (gz gx) (subject b) (ca ca)) (defstrand ca 1 (gz gx) (subject a) (ca ca)) (defstrand init 4 (dhkey dhkey) (n n) (gx gx) (h gx) (a a-0) (b a) (ca ca)) (defstrand ca 1 (gz gx) (subject a-0) (ca ca)) (precedes ((1 2) (0 2)) ((1 2) (4 2)) ((2 0) (1 0)) ((3 0) (0 0)) ((3 0) (1 1)) ((4 3) (1 3)) ((5 0) (4 0))) (non-orig dhkey (invk gx) (privk ca)) (uniq-orig n) (operation encryption-test (displaced 6 3 ca 1) (enc gx a (privk ca)) (0 0)) (traces ((recv (enc gx a (privk ca))) (send (cat gx (enc gx a (privk ca)))) (recv (cat gx (enc gx b (privk ca)) (enc n (enc "dh" gx gx dhkey)))) (send (enc "check" n (enc "dh" gx gx dhkey)))) ((recv (enc gx b (privk ca))) (recv (cat gx (enc gx a (privk ca)))) (send (cat gx (enc gx b (privk ca)) (enc n (enc "dh" gx gx dhkey)))) (recv (enc "check" n (enc "dh" gx gx dhkey)))) ((send (enc gx b (privk ca)))) ((send (enc gx a (privk ca)))) ((recv (enc gx a-0 (privk ca))) (send (cat gx (enc gx a-0 (privk ca)))) (recv (cat gx (enc gx a (privk ca)) (enc n (enc "dh" gx gx dhkey)))) (send (enc "check" n (enc "dh" gx gx dhkey)))) ((send (enc gx a-0 (privk ca))))) (label 136) (parent 100) (realized) (shape) (maps ((0 1) ((a a) (b b) (ca ca) (gx gx) (gy gx) (n n) (dhkey dhkey)))) (origs (n (1 2)))) (defskeleton dhca (vars (dhkey skey) (n text) (gx akey) (b ca a name)) (defstrand init 4 (dhkey dhkey) (n n) (gx gx) (h gx) (a b) (b b) (ca ca)) (defstrand resp 4 (dhkey dhkey) (n n) (gy gx) (h gx) (a b) (b b) (ca ca)) (defstrand ca 1 (gz gx) (subject b) (ca ca)) (defstrand ca 1 (gz gx) (subject b) (ca ca)) (defstrand init 4 (dhkey dhkey) (n n) (gx gx) (h gx) (a a) (b b) (ca ca)) (defstrand ca 1 (gz gx) (subject a) (ca ca)) (precedes ((1 2) (0 2)) ((1 2) (4 2)) ((2 0) (0 0)) ((2 0) (1 0)) ((3 0) (1 1)) ((4 3) (1 3)) ((5 0) (4 0))) (non-orig dhkey (invk gx) (privk ca)) (uniq-orig n) (operation encryption-test (displaced 6 2 ca 1) (enc gx a-0 (privk ca)) (0 0)) (traces ((recv (enc gx b (privk ca))) (send (cat gx (enc gx b (privk ca)))) (recv (cat gx (enc gx b (privk ca)) (enc n (enc "dh" gx gx dhkey)))) (send (enc "check" n (enc "dh" gx gx dhkey)))) ((recv (enc gx b (privk ca))) (recv (cat gx (enc gx b (privk ca)))) (send (cat gx (enc gx b (privk ca)) (enc n (enc "dh" gx gx dhkey)))) (recv (enc "check" n (enc "dh" gx gx dhkey)))) ((send (enc gx b (privk ca)))) ((send (enc gx b (privk ca)))) ((recv (enc gx a (privk ca))) (send (cat gx (enc gx a (privk ca)))) (recv (cat gx (enc gx b (privk ca)) (enc n (enc "dh" gx gx dhkey)))) (send (enc "check" n (enc "dh" gx gx dhkey)))) ((send (enc gx a (privk ca))))) (label 137) (parent 100) (seen 109) (realized) (comment "1 in cohort - 0 not yet seen")) (defskeleton dhca (vars (dhkey skey) (n text) (gx akey) (b ca a name)) (defstrand init 4 (dhkey dhkey) (n n) (gx gx) (h gx) (a a) (b b) (ca ca)) (defstrand resp 4 (dhkey dhkey) (n n) (gy gx) (h gx) (a a) (b b) (ca ca)) (defstrand ca 1 (gz gx) (subject b) (ca ca)) (defstrand ca 1 (gz gx) (subject a) (ca ca)) (defstrand init 4 (dhkey dhkey) (n n) (gx gx) (h gx) (a a) (b a) (ca ca)) (defstrand ca 1 (gz gx) (subject a) (ca ca)) (precedes ((1 2) (0 2)) ((1 2) (4 2)) ((2 0) (1 0)) ((3 0) (1 1)) ((4 3) (1 3)) ((5 0) (0 0)) ((5 0) (4 0))) (non-orig dhkey (invk gx) (privk ca)) (uniq-orig n) (operation encryption-test (displaced 6 5 ca 1) (enc gx a-0 (privk ca)) (0 0)) (traces ((recv (enc gx a (privk ca))) (send (cat gx (enc gx a (privk ca)))) (recv (cat gx (enc gx b (privk ca)) (enc n (enc "dh" gx gx dhkey)))) (send (enc "check" n (enc "dh" gx gx dhkey)))) ((recv (enc gx b (privk ca))) (recv (cat gx (enc gx a (privk ca)))) (send (cat gx (enc gx b (privk ca)) (enc n (enc "dh" gx gx dhkey)))) (recv (enc "check" n (enc "dh" gx gx dhkey)))) ((send (enc gx b (privk ca)))) ((send (enc gx a (privk ca)))) ((recv (enc gx a (privk ca))) (send (cat gx (enc gx a (privk ca)))) (recv (cat gx (enc gx a (privk ca)) (enc n (enc "dh" gx gx dhkey)))) (send (enc "check" n (enc "dh" gx gx dhkey)))) ((send (enc gx a (privk ca))))) (label 138) (parent 100) (realized) (shape) (maps ((0 1) ((a a) (b b) (ca ca) (gx gx) (gy gx) (n n) (dhkey dhkey)))) (origs (n (1 2)))) (defskeleton dhca (vars (dhkey skey) (n text) (gx akey) (a b ca a-0 name)) (defstrand init 4 (dhkey dhkey) (n n) (gx gx) (h gx) (a a) (b b) (ca ca)) (defstrand resp 4 (dhkey dhkey) (n n) (gy gx) (h gx) (a a) (b b) (ca ca)) (defstrand ca 1 (gz gx) (subject b) (ca ca)) (defstrand ca 1 (gz gx) (subject a) (ca ca)) (defstrand init 4 (dhkey dhkey) (n n) (gx gx) (h gx) (a a-0) (b a) (ca ca)) (defstrand ca 1 (gz gx) (subject a-0) (ca ca)) (defstrand ca 1 (gz gx) (subject a) (ca ca)) (precedes ((1 2) (0 2)) ((1 2) (4 2)) ((2 0) (1 0)) ((3 0) (1 1)) ((4 3) (1 3)) ((5 0) (4 0)) ((6 0) (0 0))) (non-orig dhkey (invk gx) (privk ca)) (uniq-orig n) (operation encryption-test (added-strand ca 1) (enc gx a (privk ca)) (0 0)) (traces ((recv (enc gx a (privk ca))) (send (cat gx (enc gx a (privk ca)))) (recv (cat gx (enc gx b (privk ca)) (enc n (enc "dh" gx gx dhkey)))) (send (enc "check" n (enc "dh" gx gx dhkey)))) ((recv (enc gx b (privk ca))) (recv (cat gx (enc gx a (privk ca)))) (send (cat gx (enc gx b (privk ca)) (enc n (enc "dh" gx gx dhkey)))) (recv (enc "check" n (enc "dh" gx gx dhkey)))) ((send (enc gx b (privk ca)))) ((send (enc gx a (privk ca)))) ((recv (enc gx a-0 (privk ca))) (send (cat gx (enc gx a-0 (privk ca)))) (recv (cat gx (enc gx a (privk ca)) (enc n (enc "dh" gx gx dhkey)))) (send (enc "check" n (enc "dh" gx gx dhkey)))) ((send (enc gx a-0 (privk ca)))) ((send (enc gx a (privk ca))))) (label 139) (parent 100) (realized) (shape) (maps ((0 1) ((a a) (b b) (ca ca) (gx gx) (gy gx) (n n) (dhkey dhkey)))) (origs (n (1 2)))) (defskeleton dhca (vars (dhkey skey) (n text) (gx gy akey) (a b ca a-0 name)) (defstrand init 4 (dhkey dhkey) (n n) (gx gx) (h gy) (a a) (b b) (ca ca)) (defstrand resp 4 (dhkey dhkey) (n n) (gy gy) (h gx) (a a) (b b) (ca ca)) (defstrand ca 1 (gz gy) (subject b) (ca ca)) (defstrand ca 1 (gz gx) (subject a) (ca ca)) (defstrand init 4 (dhkey dhkey) (n n) (gx gx) (h gy) (a a-0) (b b) (ca ca)) (defstrand ca 1 (gz gx) (subject a-0) (ca ca)) (precedes ((1 2) (0 2)) ((1 2) (4 2)) ((2 0) (1 0)) ((3 0) (0 0)) ((3 0) (1 1)) ((4 3) (1 3)) ((5 0) (4 0))) (non-orig dhkey (invk gx) (invk gy) (privk ca)) (uniq-orig n) (operation encryption-test (displaced 6 3 ca 1) (enc gx a (privk ca)) (0 0)) (traces ((recv (enc gx a (privk ca))) (send (cat gx (enc gx a (privk ca)))) (recv (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gx gy dhkey)))) (send (enc "check" n (enc "dh" gx gy dhkey)))) ((recv (enc gy b (privk ca))) (recv (cat gx (enc gx a (privk ca)))) (send (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gx gy dhkey)))) (recv (enc "check" n (enc "dh" gx gy dhkey)))) ((send (enc gy b (privk ca)))) ((send (enc gx a (privk ca)))) ((recv (enc gx a-0 (privk ca))) (send (cat gx (enc gx a-0 (privk ca)))) (recv (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gx gy dhkey)))) (send (enc "check" n (enc "dh" gx gy dhkey)))) ((send (enc gx a-0 (privk ca))))) (label 140) (parent 101) (realized) (shape) (maps ((0 1) ((a a) (b b) (ca ca) (gx gx) (gy gy) (n n) (dhkey dhkey)))) (origs (n (1 2)))) (defskeleton dhca (vars (dhkey skey) (n text) (gx gy akey) (b ca a name)) (defstrand init 4 (dhkey dhkey) (n n) (gx gx) (h gy) (a a) (b b) (ca ca)) (defstrand resp 4 (dhkey dhkey) (n n) (gy gy) (h gx) (a a) (b b) (ca ca)) (defstrand ca 1 (gz gy) (subject b) (ca ca)) (defstrand ca 1 (gz gx) (subject a) (ca ca)) (defstrand init 4 (dhkey dhkey) (n n) (gx gx) (h gy) (a a) (b b) (ca ca)) (defstrand ca 1 (gz gx) (subject a) (ca ca)) (precedes ((1 2) (0 2)) ((1 2) (4 2)) ((2 0) (1 0)) ((3 0) (1 1)) ((4 3) (1 3)) ((5 0) (0 0)) ((5 0) (4 0))) (non-orig dhkey (invk gx) (invk gy) (privk ca)) (uniq-orig n) (operation encryption-test (displaced 6 5 ca 1) (enc gx a-0 (privk ca)) (0 0)) (traces ((recv (enc gx a (privk ca))) (send (cat gx (enc gx a (privk ca)))) (recv (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gx gy dhkey)))) (send (enc "check" n (enc "dh" gx gy dhkey)))) ((recv (enc gy b (privk ca))) (recv (cat gx (enc gx a (privk ca)))) (send (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gx gy dhkey)))) (recv (enc "check" n (enc "dh" gx gy dhkey)))) ((send (enc gy b (privk ca)))) ((send (enc gx a (privk ca)))) ((recv (enc gx a (privk ca))) (send (cat gx (enc gx a (privk ca)))) (recv (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gx gy dhkey)))) (send (enc "check" n (enc "dh" gx gy dhkey)))) ((send (enc gx a (privk ca))))) (label 141) (parent 101) (realized) (shape) (maps ((0 1) ((a a) (b b) (ca ca) (gx gx) (gy gy) (n n) (dhkey dhkey)))) (origs (n (1 2)))) (defskeleton dhca (vars (dhkey skey) (n text) (gx gy akey) (a b ca a-0 name)) (defstrand init 4 (dhkey dhkey) (n n) (gx gx) (h gy) (a a) (b b) (ca ca)) (defstrand resp 4 (dhkey dhkey) (n n) (gy gy) (h gx) (a a) (b b) (ca ca)) (defstrand ca 1 (gz gy) (subject b) (ca ca)) (defstrand ca 1 (gz gx) (subject a) (ca ca)) (defstrand init 4 (dhkey dhkey) (n n) (gx gx) (h gy) (a a-0) (b b) (ca ca)) (defstrand ca 1 (gz gx) (subject a-0) (ca ca)) (defstrand ca 1 (gz gx) (subject a) (ca ca)) (precedes ((1 2) (0 2)) ((1 2) (4 2)) ((2 0) (1 0)) ((3 0) (1 1)) ((4 3) (1 3)) ((5 0) (4 0)) ((6 0) (0 0))) (non-orig dhkey (invk gx) (invk gy) (privk ca)) (uniq-orig n) (operation encryption-test (added-strand ca 1) (enc gx a (privk ca)) (0 0)) (traces ((recv (enc gx a (privk ca))) (send (cat gx (enc gx a (privk ca)))) (recv (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gx gy dhkey)))) (send (enc "check" n (enc "dh" gx gy dhkey)))) ((recv (enc gy b (privk ca))) (recv (cat gx (enc gx a (privk ca)))) (send (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gx gy dhkey)))) (recv (enc "check" n (enc "dh" gx gy dhkey)))) ((send (enc gy b (privk ca)))) ((send (enc gx a (privk ca)))) ((recv (enc gx a-0 (privk ca))) (send (cat gx (enc gx a-0 (privk ca)))) (recv (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gx gy dhkey)))) (send (enc "check" n (enc "dh" gx gy dhkey)))) ((send (enc gx a-0 (privk ca)))) ((send (enc gx a (privk ca))))) (label 142) (parent 101) (realized) (shape) (maps ((0 1) ((a a) (b b) (ca ca) (gx gx) (gy gy) (n n) (dhkey dhkey)))) (origs (n (1 2)))) (defskeleton dhca (vars (dhkey skey) (n text) (gx akey) (a b ca a-0 ca-0 name)) (defstrand init 4 (dhkey dhkey) (n n) (gx gx) (h gx) (a a) (b b) (ca ca)) (defstrand resp 4 (dhkey dhkey) (n n) (gy gx) (h gx) (a a) (b b) (ca ca)) (defstrand ca 1 (gz gx) (subject b) (ca ca)) (defstrand ca 1 (gz gx) (subject a) (ca ca)) (defstrand init 4 (dhkey dhkey) (n n) (gx gx) (h gx) (a a-0) (b a-0) (ca ca-0)) (defstrand ca 1 (gz gx) (subject a-0) (ca ca-0)) (precedes ((1 2) (0 2)) ((1 2) (4 2)) ((2 0) (1 0)) ((3 0) (0 0)) ((3 0) (1 1)) ((4 3) (1 3)) ((5 0) (4 0))) (non-orig dhkey (invk gx) (privk ca) (privk ca-0)) (uniq-orig n) (operation encryption-test (displaced 6 3 ca 1) (enc gx a (privk ca)) (0 0)) (traces ((recv (enc gx a (privk ca))) (send (cat gx (enc gx a (privk ca)))) (recv (cat gx (enc gx b (privk ca)) (enc n (enc "dh" gx gx dhkey)))) (send (enc "check" n (enc "dh" gx gx dhkey)))) ((recv (enc gx b (privk ca))) (recv (cat gx (enc gx a (privk ca)))) (send (cat gx (enc gx b (privk ca)) (enc n (enc "dh" gx gx dhkey)))) (recv (enc "check" n (enc "dh" gx gx dhkey)))) ((send (enc gx b (privk ca)))) ((send (enc gx a (privk ca)))) ((recv (enc gx a-0 (privk ca-0))) (send (cat gx (enc gx a-0 (privk ca-0)))) (recv (cat gx (enc gx a-0 (privk ca-0)) (enc n (enc "dh" gx gx dhkey)))) (send (enc "check" n (enc "dh" gx gx dhkey)))) ((send (enc gx a-0 (privk ca-0))))) (label 143) (parent 102) (realized) (shape) (maps ((0 1) ((a a) (b b) (ca ca) (gx gx) (gy gx) (n n) (dhkey dhkey)))) (origs (n (1 2)))) (defskeleton dhca (vars (dhkey skey) (n text) (gx akey) (b ca a ca-0 name)) (defstrand init 4 (dhkey dhkey) (n n) (gx gx) (h gx) (a b) (b b) (ca ca)) (defstrand resp 4 (dhkey dhkey) (n n) (gy gx) (h gx) (a b) (b b) (ca ca)) (defstrand ca 1 (gz gx) (subject b) (ca ca)) (defstrand ca 1 (gz gx) (subject b) (ca ca)) (defstrand init 4 (dhkey dhkey) (n n) (gx gx) (h gx) (a a) (b a) (ca ca-0)) (defstrand ca 1 (gz gx) (subject a) (ca ca-0)) (precedes ((1 2) (0 2)) ((1 2) (4 2)) ((2 0) (0 0)) ((2 0) (1 0)) ((3 0) (1 1)) ((4 3) (1 3)) ((5 0) (4 0))) (non-orig dhkey (invk gx) (privk ca) (privk ca-0)) (uniq-orig n) (operation encryption-test (displaced 6 2 ca 1) (enc gx a-0 (privk ca)) (0 0)) (traces ((recv (enc gx b (privk ca))) (send (cat gx (enc gx b (privk ca)))) (recv (cat gx (enc gx b (privk ca)) (enc n (enc "dh" gx gx dhkey)))) (send (enc "check" n (enc "dh" gx gx dhkey)))) ((recv (enc gx b (privk ca))) (recv (cat gx (enc gx b (privk ca)))) (send (cat gx (enc gx b (privk ca)) (enc n (enc "dh" gx gx dhkey)))) (recv (enc "check" n (enc "dh" gx gx dhkey)))) ((send (enc gx b (privk ca)))) ((send (enc gx b (privk ca)))) ((recv (enc gx a (privk ca-0))) (send (cat gx (enc gx a (privk ca-0)))) (recv (cat gx (enc gx a (privk ca-0)) (enc n (enc "dh" gx gx dhkey)))) (send (enc "check" n (enc "dh" gx gx dhkey)))) ((send (enc gx a (privk ca-0))))) (label 144) (parent 102) (seen 112) (realized) (comment "1 in cohort - 0 not yet seen")) (defskeleton dhca (vars (dhkey skey) (n text) (gx akey) (a b ca a-0 ca-0 name)) (defstrand init 4 (dhkey dhkey) (n n) (gx gx) (h gx) (a a) (b b) (ca ca)) (defstrand resp 4 (dhkey dhkey) (n n) (gy gx) (h gx) (a a) (b b) (ca ca)) (defstrand ca 1 (gz gx) (subject b) (ca ca)) (defstrand ca 1 (gz gx) (subject a) (ca ca)) (defstrand init 4 (dhkey dhkey) (n n) (gx gx) (h gx) (a a-0) (b a-0) (ca ca-0)) (defstrand ca 1 (gz gx) (subject a-0) (ca ca-0)) (defstrand ca 1 (gz gx) (subject a) (ca ca)) (precedes ((1 2) (0 2)) ((1 2) (4 2)) ((2 0) (1 0)) ((3 0) (1 1)) ((4 3) (1 3)) ((5 0) (4 0)) ((6 0) (0 0))) (non-orig dhkey (invk gx) (privk ca) (privk ca-0)) (uniq-orig n) (operation encryption-test (added-strand ca 1) (enc gx a (privk ca)) (0 0)) (traces ((recv (enc gx a (privk ca))) (send (cat gx (enc gx a (privk ca)))) (recv (cat gx (enc gx b (privk ca)) (enc n (enc "dh" gx gx dhkey)))) (send (enc "check" n (enc "dh" gx gx dhkey)))) ((recv (enc gx b (privk ca))) (recv (cat gx (enc gx a (privk ca)))) (send (cat gx (enc gx b (privk ca)) (enc n (enc "dh" gx gx dhkey)))) (recv (enc "check" n (enc "dh" gx gx dhkey)))) ((send (enc gx b (privk ca)))) ((send (enc gx a (privk ca)))) ((recv (enc gx a-0 (privk ca-0))) (send (cat gx (enc gx a-0 (privk ca-0)))) (recv (cat gx (enc gx a-0 (privk ca-0)) (enc n (enc "dh" gx gx dhkey)))) (send (enc "check" n (enc "dh" gx gx dhkey)))) ((send (enc gx a-0 (privk ca-0)))) ((send (enc gx a (privk ca))))) (label 145) (parent 102) (realized) (shape) (maps ((0 1) ((a a) (b b) (ca ca) (gx gx) (gy gx) (n n) (dhkey dhkey)))) (origs (n (1 2)))) (defskeleton dhca (vars (dhkey skey) (n text) (gx gy akey) (a b ca a-0 b-0 ca-0 name)) (defstrand init 4 (dhkey dhkey) (n n) (gx gx) (h gy) (a a) (b b) (ca ca)) (defstrand resp 4 (dhkey dhkey) (n n) (gy gy) (h gx) (a a) (b b) (ca ca)) (defstrand ca 1 (gz gy) (subject b) (ca ca)) (defstrand ca 1 (gz gx) (subject a) (ca ca)) (defstrand init 4 (dhkey dhkey) (n n) (gx gx) (h gy) (a a-0) (b b-0) (ca ca-0)) (defstrand ca 1 (gz gx) (subject a-0) (ca ca-0)) (defstrand ca 1 (gz gy) (subject b-0) (ca ca-0)) (precedes ((1 2) (0 2)) ((1 2) (4 2)) ((2 0) (1 0)) ((3 0) (0 0)) ((3 0) (1 1)) ((4 3) (1 3)) ((5 0) (4 0)) ((6 0) (4 2))) (non-orig dhkey (invk gx) (invk gy) (privk ca) (privk ca-0)) (uniq-orig n) (operation encryption-test (displaced 7 3 ca 1) (enc gx a (privk ca)) (0 0)) (traces ((recv (enc gx a (privk ca))) (send (cat gx (enc gx a (privk ca)))) (recv (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gx gy dhkey)))) (send (enc "check" n (enc "dh" gx gy dhkey)))) ((recv (enc gy b (privk ca))) (recv (cat gx (enc gx a (privk ca)))) (send (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gx gy dhkey)))) (recv (enc "check" n (enc "dh" gx gy dhkey)))) ((send (enc gy b (privk ca)))) ((send (enc gx a (privk ca)))) ((recv (enc gx a-0 (privk ca-0))) (send (cat gx (enc gx a-0 (privk ca-0)))) (recv (cat gy (enc gy b-0 (privk ca-0)) (enc n (enc "dh" gx gy dhkey)))) (send (enc "check" n (enc "dh" gx gy dhkey)))) ((send (enc gx a-0 (privk ca-0)))) ((send (enc gy b-0 (privk ca-0))))) (label 146) (parent 103) (realized) (shape) (maps ((0 1) ((a a) (b b) (ca ca) (gx gx) (gy gy) (n n) (dhkey dhkey)))) (origs (n (1 2)))) (defskeleton dhca (vars (dhkey skey) (n text) (gy akey) (b ca a b-0 ca-0 name)) (defstrand init 4 (dhkey dhkey) (n n) (gx gy) (h gy) (a b) (b b) (ca ca)) (defstrand resp 4 (dhkey dhkey) (n n) (gy gy) (h gy) (a b) (b b) (ca ca)) (defstrand ca 1 (gz gy) (subject b) (ca ca)) (defstrand ca 1 (gz gy) (subject b) (ca ca)) (defstrand init 4 (dhkey dhkey) (n n) (gx gy) (h gy) (a a) (b b-0) (ca ca-0)) (defstrand ca 1 (gz gy) (subject a) (ca ca-0)) (defstrand ca 1 (gz gy) (subject b-0) (ca ca-0)) (precedes ((1 2) (0 2)) ((1 2) (4 2)) ((2 0) (0 0)) ((2 0) (1 0)) ((3 0) (1 1)) ((4 3) (1 3)) ((5 0) (4 0)) ((6 0) (4 2))) (non-orig dhkey (invk gy) (privk ca) (privk ca-0)) (uniq-orig n) (operation encryption-test (displaced 7 2 ca 1) (enc gx a-0 (privk ca)) (0 0)) (traces ((recv (enc gy b (privk ca))) (send (cat gy (enc gy b (privk ca)))) (recv (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gy gy dhkey)))) (send (enc "check" n (enc "dh" gy gy dhkey)))) ((recv (enc gy b (privk ca))) (recv (cat gy (enc gy b (privk ca)))) (send (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gy gy dhkey)))) (recv (enc "check" n (enc "dh" gy gy dhkey)))) ((send (enc gy b (privk ca)))) ((send (enc gy b (privk ca)))) ((recv (enc gy a (privk ca-0))) (send (cat gy (enc gy a (privk ca-0)))) (recv (cat gy (enc gy b-0 (privk ca-0)) (enc n (enc "dh" gy gy dhkey)))) (send (enc "check" n (enc "dh" gy gy dhkey)))) ((send (enc gy a (privk ca-0)))) ((send (enc gy b-0 (privk ca-0))))) (label 147) (parent 103) (seen 115) (realized) (comment "1 in cohort - 0 not yet seen")) (defskeleton dhca (vars (dhkey skey) (n text) (gx gy akey) (b a b-0 ca name)) (defstrand init 4 (dhkey dhkey) (n n) (gx gx) (h gy) (a a) (b b) (ca ca)) (defstrand resp 4 (dhkey dhkey) (n n) (gy gy) (h gx) (a a) (b b) (ca ca)) (defstrand ca 1 (gz gy) (subject b) (ca ca)) (defstrand ca 1 (gz gx) (subject a) (ca ca)) (defstrand init 4 (dhkey dhkey) (n n) (gx gx) (h gy) (a a) (b b-0) (ca ca)) (defstrand ca 1 (gz gx) (subject a) (ca ca)) (defstrand ca 1 (gz gy) (subject b-0) (ca ca)) (precedes ((1 2) (0 2)) ((1 2) (4 2)) ((2 0) (1 0)) ((3 0) (1 1)) ((4 3) (1 3)) ((5 0) (0 0)) ((5 0) (4 0)) ((6 0) (4 2))) (non-orig dhkey (invk gx) (invk gy) (privk ca)) (uniq-orig n) (operation encryption-test (displaced 7 5 ca 1) (enc gx a-0 (privk ca-0)) (0 0)) (traces ((recv (enc gx a (privk ca))) (send (cat gx (enc gx a (privk ca)))) (recv (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gx gy dhkey)))) (send (enc "check" n (enc "dh" gx gy dhkey)))) ((recv (enc gy b (privk ca))) (recv (cat gx (enc gx a (privk ca)))) (send (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gx gy dhkey)))) (recv (enc "check" n (enc "dh" gx gy dhkey)))) ((send (enc gy b (privk ca)))) ((send (enc gx a (privk ca)))) ((recv (enc gx a (privk ca))) (send (cat gx (enc gx a (privk ca)))) (recv (cat gy (enc gy b-0 (privk ca)) (enc n (enc "dh" gx gy dhkey)))) (send (enc "check" n (enc "dh" gx gy dhkey)))) ((send (enc gx a (privk ca)))) ((send (enc gy b-0 (privk ca))))) (label 148) (parent 103) (realized) (shape) (maps ((0 1) ((a a) (b b) (ca ca) (gx gx) (gy gy) (n n) (dhkey dhkey)))) (origs (n (1 2)))) (defskeleton dhca (vars (dhkey skey) (n text) (gy akey) (b a b-0 ca name)) (defstrand init 4 (dhkey dhkey) (n n) (gx gy) (h gy) (a b-0) (b b) (ca ca)) (defstrand resp 4 (dhkey dhkey) (n n) (gy gy) (h gy) (a b-0) (b b) (ca ca)) (defstrand ca 1 (gz gy) (subject b) (ca ca)) (defstrand ca 1 (gz gy) (subject b-0) (ca ca)) (defstrand init 4 (dhkey dhkey) (n n) (gx gy) (h gy) (a a) (b b-0) (ca ca)) (defstrand ca 1 (gz gy) (subject a) (ca ca)) (defstrand ca 1 (gz gy) (subject b-0) (ca ca)) (precedes ((1 2) (0 2)) ((1 2) (4 2)) ((2 0) (1 0)) ((3 0) (1 1)) ((4 3) (1 3)) ((5 0) (4 0)) ((6 0) (0 0)) ((6 0) (4 2))) (non-orig dhkey (invk gy) (privk ca)) (uniq-orig n) (operation encryption-test (displaced 7 6 ca 1) (enc gx a-0 (privk ca-0)) (0 0)) (traces ((recv (enc gy b-0 (privk ca))) (send (cat gy (enc gy b-0 (privk ca)))) (recv (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gy gy dhkey)))) (send (enc "check" n (enc "dh" gy gy dhkey)))) ((recv (enc gy b (privk ca))) (recv (cat gy (enc gy b-0 (privk ca)))) (send (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gy gy dhkey)))) (recv (enc "check" n (enc "dh" gy gy dhkey)))) ((send (enc gy b (privk ca)))) ((send (enc gy b-0 (privk ca)))) ((recv (enc gy a (privk ca))) (send (cat gy (enc gy a (privk ca)))) (recv (cat gy (enc gy b-0 (privk ca)) (enc n (enc "dh" gy gy dhkey)))) (send (enc "check" n (enc "dh" gy gy dhkey)))) ((send (enc gy a (privk ca)))) ((send (enc gy b-0 (privk ca))))) (label 149) (parent 103) (realized) (comment "1 in cohort - 1 not yet seen")) (defskeleton dhca (vars (dhkey skey) (n text) (gx gy akey) (a b ca a-0 b-0 ca-0 name)) (defstrand init 4 (dhkey dhkey) (n n) (gx gx) (h gy) (a a) (b b) (ca ca)) (defstrand resp 4 (dhkey dhkey) (n n) (gy gy) (h gx) (a a) (b b) (ca ca)) (defstrand ca 1 (gz gy) (subject b) (ca ca)) (defstrand ca 1 (gz gx) (subject a) (ca ca)) (defstrand init 4 (dhkey dhkey) (n n) (gx gx) (h gy) (a a-0) (b b-0) (ca ca-0)) (defstrand ca 1 (gz gx) (subject a-0) (ca ca-0)) (defstrand ca 1 (gz gy) (subject b-0) (ca ca-0)) (defstrand ca 1 (gz gx) (subject a) (ca ca)) (precedes ((1 2) (0 2)) ((1 2) (4 2)) ((2 0) (1 0)) ((3 0) (1 1)) ((4 3) (1 3)) ((5 0) (4 0)) ((6 0) (4 2)) ((7 0) (0 0))) (non-orig dhkey (invk gx) (invk gy) (privk ca) (privk ca-0)) (uniq-orig n) (operation encryption-test (added-strand ca 1) (enc gx a (privk ca)) (0 0)) (traces ((recv (enc gx a (privk ca))) (send (cat gx (enc gx a (privk ca)))) (recv (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gx gy dhkey)))) (send (enc "check" n (enc "dh" gx gy dhkey)))) ((recv (enc gy b (privk ca))) (recv (cat gx (enc gx a (privk ca)))) (send (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gx gy dhkey)))) (recv (enc "check" n (enc "dh" gx gy dhkey)))) ((send (enc gy b (privk ca)))) ((send (enc gx a (privk ca)))) ((recv (enc gx a-0 (privk ca-0))) (send (cat gx (enc gx a-0 (privk ca-0)))) (recv (cat gy (enc gy b-0 (privk ca-0)) (enc n (enc "dh" gx gy dhkey)))) (send (enc "check" n (enc "dh" gx gy dhkey)))) ((send (enc gx a-0 (privk ca-0)))) ((send (enc gy b-0 (privk ca-0)))) ((send (enc gx a (privk ca))))) (label 150) (parent 103) (realized) (shape) (maps ((0 1) ((a a) (b b) (ca ca) (gx gx) (gy gy) (n n) (dhkey dhkey)))) (origs (n (1 2)))) (defskeleton dhca (vars (dhkey skey) (n text) (gy akey) (ca b name)) (defstrand init 4 (dhkey dhkey) (n n) (gx gy) (h gy) (a b) (b b) (ca ca)) (defstrand resp 4 (dhkey dhkey) (n n) (gy gy) (h gy) (a b) (b b) (ca ca)) (defstrand ca 1 (gz gy) (subject b) (ca ca)) (defstrand init 4 (dhkey dhkey) (n n) (gx gy) (h gy) (a b) (b b) (ca ca)) (defstrand ca 1 (gz gy) (subject b) (ca ca)) (precedes ((1 2) (0 2)) ((1 2) (3 2)) ((2 0) (1 0)) ((2 0) (3 0)) ((3 3) (1 3)) ((4 0) (0 0)) ((4 0) (1 3))) (non-orig dhkey (invk gy) (privk ca)) (uniq-orig n) (operation generalization weakened ((4 0) (3 2))) (traces ((recv (enc gy b (privk ca))) (send (cat gy (enc gy b (privk ca)))) (recv (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gy gy dhkey)))) (send (enc "check" n (enc "dh" gy gy dhkey)))) ((recv (enc gy b (privk ca))) (recv (cat gy (enc gy b (privk ca)))) (send (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gy gy dhkey)))) (recv (enc "check" n (enc "dh" gy gy dhkey)))) ((send (enc gy b (privk ca)))) ((recv (enc gy b (privk ca))) (send (cat gy (enc gy b (privk ca)))) (recv (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gy gy dhkey)))) (send (enc "check" n (enc "dh" gy gy dhkey)))) ((send (enc gy b (privk ca))))) (label 151) (parent 107) (seen 105) (realized) (comment "1 in cohort - 0 not yet seen")) (defskeleton dhca (vars (dhkey skey) (n text) (gy akey) (a b ca name)) (defstrand init 4 (dhkey dhkey) (n n) (gx gy) (h gy) (a b) (b b) (ca ca)) (defstrand resp 4 (dhkey dhkey) (n n) (gy gy) (h gy) (a b) (b b) (ca ca)) (defstrand ca 1 (gz gy) (subject b) (ca ca)) (defstrand init 4 (dhkey dhkey) (n n) (gx gy) (h gy) (a a) (b b) (ca ca)) (defstrand ca 1 (gz gy) (subject a) (ca ca)) (defstrand ca 1 (gz gy) (subject b) (ca ca)) (precedes ((1 2) (0 2)) ((1 2) (3 2)) ((2 0) (1 0)) ((3 3) (1 3)) ((4 0) (3 0)) ((5 0) (0 0)) ((5 0) (1 3))) (non-orig dhkey (invk gy) (privk ca)) (uniq-orig n) (operation generalization weakened ((5 0) (3 2))) (traces ((recv (enc gy b (privk ca))) (send (cat gy (enc gy b (privk ca)))) (recv (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gy gy dhkey)))) (send (enc "check" n (enc "dh" gy gy dhkey)))) ((recv (enc gy b (privk ca))) (recv (cat gy (enc gy b (privk ca)))) (send (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gy gy dhkey)))) (recv (enc "check" n (enc "dh" gy gy dhkey)))) ((send (enc gy b (privk ca)))) ((recv (enc gy a (privk ca))) (send (cat gy (enc gy a (privk ca)))) (recv (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gy gy dhkey)))) (send (enc "check" n (enc "dh" gy gy dhkey)))) ((send (enc gy a (privk ca)))) ((send (enc gy b (privk ca))))) (label 152) (parent 116) (seen 111) (realized) (comment "1 in cohort - 0 not yet seen")) (defskeleton dhca (vars (dhkey skey) (n text) (gy akey) (b ca b-0 name)) (defstrand init 4 (dhkey dhkey) (n n) (gx gy) (h gy) (a b-0) (b b) (ca ca)) (defstrand resp 4 (dhkey dhkey) (n n) (gy gy) (h gy) (a b-0) (b b) (ca ca)) (defstrand ca 1 (gz gy) (subject b) (ca ca)) (defstrand ca 1 (gz gy) (subject b-0) (ca ca)) (defstrand init 4 (dhkey dhkey) (n n) (gx gy) (h gy) (a b) (b b-0) (ca ca)) (defstrand ca 1 (gz gy) (subject b-0) (ca ca)) (precedes ((1 2) (0 2)) ((1 2) (4 2)) ((2 0) (1 0)) ((2 0) (4 0)) ((3 0) (1 1)) ((4 3) (1 3)) ((5 0) (0 0)) ((5 0) (1 3))) (non-orig dhkey (invk gy) (privk ca)) (uniq-orig n) (operation generalization weakened ((5 0) (4 2))) (traces ((recv (enc gy b-0 (privk ca))) (send (cat gy (enc gy b-0 (privk ca)))) (recv (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gy gy dhkey)))) (send (enc "check" n (enc "dh" gy gy dhkey)))) ((recv (enc gy b (privk ca))) (recv (cat gy (enc gy b-0 (privk ca)))) (send (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gy gy dhkey)))) (recv (enc "check" n (enc "dh" gy gy dhkey)))) ((send (enc gy b (privk ca)))) ((send (enc gy b-0 (privk ca)))) ((recv (enc gy b (privk ca))) (send (cat gy (enc gy b (privk ca)))) (recv (cat gy (enc gy b-0 (privk ca)) (enc n (enc "dh" gy gy dhkey)))) (send (enc "check" n (enc "dh" gy gy dhkey)))) ((send (enc gy b-0 (privk ca))))) (label 153) (parent 125) (seen 122) (realized) (comment "1 in cohort - 0 not yet seen")) (defskeleton dhca (vars (dhkey skey) (n text) (gy akey) (b ca name)) (defstrand init 4 (dhkey dhkey) (n n) (gx gy) (h gy) (a b) (b b) (ca ca)) (defstrand resp 4 (dhkey dhkey) (n n) (gy gy) (h gy) (a b) (b b) (ca ca)) (defstrand ca 1 (gz gy) (subject b) (ca ca)) (defstrand ca 1 (gz gy) (subject b) (ca ca)) (defstrand init 4 (dhkey dhkey) (n n) (gx gy) (h gy) (a b) (b b) (ca ca)) (precedes ((1 2) (0 2)) ((1 2) (4 2)) ((2 0) (0 0)) ((2 0) (1 0)) ((3 0) (0 2)) ((3 0) (4 0)) ((4 3) (1 3))) (non-orig dhkey (invk gy) (privk ca)) (uniq-orig n) (operation generalization weakened ((3 0) (1 1))) (traces ((recv (enc gy b (privk ca))) (send (cat gy (enc gy b (privk ca)))) (recv (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gy gy dhkey)))) (send (enc "check" n (enc "dh" gy gy dhkey)))) ((recv (enc gy b (privk ca))) (recv (cat gy (enc gy b (privk ca)))) (send (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gy gy dhkey)))) (recv (enc "check" n (enc "dh" gy gy dhkey)))) ((send (enc gy b (privk ca)))) ((send (enc gy b (privk ca)))) ((recv (enc gy b (privk ca))) (send (cat gy (enc gy b (privk ca)))) (recv (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gy gy dhkey)))) (send (enc "check" n (enc "dh" gy gy dhkey))))) (label 154) (parent 127) (realized) (comment "1 in cohort - 1 not yet seen")) (defskeleton dhca (vars (dhkey skey) (n text) (gy akey) (b ca b-0 name)) (defstrand init 4 (dhkey dhkey) (n n) (gx gy) (h gy) (a b) (b b) (ca ca)) (defstrand resp 4 (dhkey dhkey) (n n) (gy gy) (h gy) (a b) (b b) (ca ca)) (defstrand ca 1 (gz gy) (subject b) (ca ca)) (defstrand ca 1 (gz gy) (subject b) (ca ca)) (defstrand init 4 (dhkey dhkey) (n n) (gx gy) (h gy) (a b) (b b-0) (ca ca)) (defstrand ca 1 (gz gy) (subject b-0) (ca ca)) (precedes ((1 2) (0 2)) ((1 2) (4 2)) ((2 0) (0 0)) ((2 0) (1 0)) ((3 0) (0 2)) ((3 0) (4 0)) ((4 3) (1 3)) ((5 0) (4 2))) (non-orig dhkey (invk gy) (privk ca)) (uniq-orig n) (operation generalization weakened ((3 0) (1 1))) (traces ((recv (enc gy b (privk ca))) (send (cat gy (enc gy b (privk ca)))) (recv (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gy gy dhkey)))) (send (enc "check" n (enc "dh" gy gy dhkey)))) ((recv (enc gy b (privk ca))) (recv (cat gy (enc gy b (privk ca)))) (send (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gy gy dhkey)))) (recv (enc "check" n (enc "dh" gy gy dhkey)))) ((send (enc gy b (privk ca)))) ((send (enc gy b (privk ca)))) ((recv (enc gy b (privk ca))) (send (cat gy (enc gy b (privk ca)))) (recv (cat gy (enc gy b-0 (privk ca)) (enc n (enc "dh" gy gy dhkey)))) (send (enc "check" n (enc "dh" gy gy dhkey)))) ((send (enc gy b-0 (privk ca))))) (label 155) (parent 133) (realized) (comment "1 in cohort - 1 not yet seen")) (defskeleton dhca (vars (dhkey skey) (n text) (gy akey) (b ca b-0 name)) (defstrand init 4 (dhkey dhkey) (n n) (gx gy) (h gy) (a b-0) (b b) (ca ca)) (defstrand resp 4 (dhkey dhkey) (n n) (gy gy) (h gy) (a b-0) (b b) (ca ca)) (defstrand ca 1 (gz gy) (subject b) (ca ca)) (defstrand ca 1 (gz gy) (subject b-0) (ca ca)) (defstrand init 4 (dhkey dhkey) (n n) (gx gy) (h gy) (a b-0) (b b-0) (ca ca)) (defstrand ca 1 (gz gy) (subject b-0) (ca ca)) (precedes ((1 2) (0 2)) ((1 2) (4 2)) ((2 0) (1 0)) ((3 0) (1 1)) ((3 0) (4 0)) ((4 3) (1 3)) ((5 0) (0 0)) ((5 0) (1 3))) (non-orig dhkey (invk gy) (privk ca)) (uniq-orig n) (operation generalization weakened ((5 0) (4 2))) (traces ((recv (enc gy b-0 (privk ca))) (send (cat gy (enc gy b-0 (privk ca)))) (recv (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gy gy dhkey)))) (send (enc "check" n (enc "dh" gy gy dhkey)))) ((recv (enc gy b (privk ca))) (recv (cat gy (enc gy b-0 (privk ca)))) (send (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gy gy dhkey)))) (recv (enc "check" n (enc "dh" gy gy dhkey)))) ((send (enc gy b (privk ca)))) ((send (enc gy b-0 (privk ca)))) ((recv (enc gy b-0 (privk ca))) (send (cat gy (enc gy b-0 (privk ca)))) (recv (cat gy (enc gy b-0 (privk ca)) (enc n (enc "dh" gy gy dhkey)))) (send (enc "check" n (enc "dh" gy gy dhkey)))) ((send (enc gy b-0 (privk ca))))) (label 156) (parent 134) (seen 131) (realized) (comment "1 in cohort - 0 not yet seen")) (defskeleton dhca (vars (dhkey skey) (n text) (gy akey) (b a b-0 ca name)) (defstrand init 4 (dhkey dhkey) (n n) (gx gy) (h gy) (a b-0) (b b) (ca ca)) (defstrand resp 4 (dhkey dhkey) (n n) (gy gy) (h gy) (a b-0) (b b) (ca ca)) (defstrand ca 1 (gz gy) (subject b) (ca ca)) (defstrand ca 1 (gz gy) (subject b-0) (ca ca)) (defstrand init 4 (dhkey dhkey) (n n) (gx gy) (h gy) (a a) (b b-0) (ca ca)) (defstrand ca 1 (gz gy) (subject a) (ca ca)) (defstrand ca 1 (gz gy) (subject b-0) (ca ca)) (precedes ((1 2) (0 2)) ((1 2) (4 2)) ((2 0) (1 0)) ((3 0) (1 1)) ((4 3) (1 3)) ((5 0) (4 0)) ((6 0) (0 0)) ((6 0) (1 3))) (non-orig dhkey (invk gy) (privk ca)) (uniq-orig n) (operation generalization weakened ((6 0) (4 2))) (traces ((recv (enc gy b-0 (privk ca))) (send (cat gy (enc gy b-0 (privk ca)))) (recv (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gy gy dhkey)))) (send (enc "check" n (enc "dh" gy gy dhkey)))) ((recv (enc gy b (privk ca))) (recv (cat gy (enc gy b-0 (privk ca)))) (send (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gy gy dhkey)))) (recv (enc "check" n (enc "dh" gy gy dhkey)))) ((send (enc gy b (privk ca)))) ((send (enc gy b-0 (privk ca)))) ((recv (enc gy a (privk ca))) (send (cat gy (enc gy a (privk ca)))) (recv (cat gy (enc gy b-0 (privk ca)) (enc n (enc "dh" gy gy dhkey)))) (send (enc "check" n (enc "dh" gy gy dhkey)))) ((send (enc gy a (privk ca)))) ((send (enc gy b-0 (privk ca))))) (label 157) (parent 149) (seen 139) (realized) (comment "1 in cohort - 0 not yet seen")) (defskeleton dhca (vars (dhkey skey) (n text) (gy akey) (b ca name)) (defstrand init 4 (dhkey dhkey) (n n) (gx gy) (h gy) (a b) (b b) (ca ca)) (defstrand resp 4 (dhkey dhkey) (n n) (gy gy) (h gy) (a b) (b b) (ca ca)) (defstrand ca 1 (gz gy) (subject b) (ca ca)) (defstrand ca 1 (gz gy) (subject b) (ca ca)) (defstrand init 4 (dhkey dhkey) (n n) (gx gy) (h gy) (a b) (b b) (ca ca)) (precedes ((1 2) (0 2)) ((1 2) (4 2)) ((2 0) (0 0)) ((2 0) (1 0)) ((3 0) (4 0)) ((4 3) (1 3))) (non-orig dhkey (invk gy) (privk ca)) (uniq-orig n) (operation generalization weakened ((3 0) (0 2))) (traces ((recv (enc gy b (privk ca))) (send (cat gy (enc gy b (privk ca)))) (recv (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gy gy dhkey)))) (send (enc "check" n (enc "dh" gy gy dhkey)))) ((recv (enc gy b (privk ca))) (recv (cat gy (enc gy b (privk ca)))) (send (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gy gy dhkey)))) (recv (enc "check" n (enc "dh" gy gy dhkey)))) ((send (enc gy b (privk ca)))) ((send (enc gy b (privk ca)))) ((recv (enc gy b (privk ca))) (send (cat gy (enc gy b (privk ca)))) (recv (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gy gy dhkey)))) (send (enc "check" n (enc "dh" gy gy dhkey))))) (label 158) (parent 154) (seen 109) (realized) (comment "1 in cohort - 0 not yet seen")) (defskeleton dhca (vars (dhkey skey) (n text) (gy akey) (b ca b-0 name)) (defstrand init 4 (dhkey dhkey) (n n) (gx gy) (h gy) (a b) (b b) (ca ca)) (defstrand resp 4 (dhkey dhkey) (n n) (gy gy) (h gy) (a b) (b b) (ca ca)) (defstrand ca 1 (gz gy) (subject b) (ca ca)) (defstrand ca 1 (gz gy) (subject b) (ca ca)) (defstrand init 4 (dhkey dhkey) (n n) (gx gy) (h gy) (a b) (b b-0) (ca ca)) (defstrand ca 1 (gz gy) (subject b-0) (ca ca)) (precedes ((1 2) (0 2)) ((1 2) (4 2)) ((2 0) (0 0)) ((2 0) (1 0)) ((3 0) (4 0)) ((4 3) (1 3)) ((5 0) (4 2))) (non-orig dhkey (invk gy) (privk ca)) (uniq-orig n) (operation generalization weakened ((3 0) (0 2))) (traces ((recv (enc gy b (privk ca))) (send (cat gy (enc gy b (privk ca)))) (recv (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gy gy dhkey)))) (send (enc "check" n (enc "dh" gy gy dhkey)))) ((recv (enc gy b (privk ca))) (recv (cat gy (enc gy b (privk ca)))) (send (cat gy (enc gy b (privk ca)) (enc n (enc "dh" gy gy dhkey)))) (recv (enc "check" n (enc "dh" gy gy dhkey)))) ((send (enc gy b (privk ca)))) ((send (enc gy b (privk ca)))) ((recv (enc gy b (privk ca))) (send (cat gy (enc gy b (privk ca)))) (recv (cat gy (enc gy b-0 (privk ca)) (enc n (enc "dh" gy gy dhkey)))) (send (enc "check" n (enc "dh" gy gy dhkey)))) ((send (enc gy b-0 (privk ca))))) (label 159) (parent 155) (realized) (shape) (maps ((0 1) ((a b) (b b) (ca ca) (gx gy) (gy gy) (n n) (dhkey dhkey)))) (origs (n (1 2)))) (comment "Nothing left to do")