(herald "IADH: unified model (UM)" (bound 20) (algebra diffie-hellman)) (comment "CPSA 3.2.2") (comment "All input read from iadh_um.scm") (comment "Strand count bounded at 20") (defprotocol iadh-um diffie-hellman (defrole init (vars (l e expn) (hl he base) (A B CA name) (key data)) (trace (recv (enc "cert" (exp (gen) l) A (privk CA))) (recv (enc "cert" hl B (privk CA))) (send (exp (gen) e)) (recv he) (send key)) (non-orig (privk CA)) (fn-of (foo ((hash (exp hl l) (exp he e)) key))) (neq (he (gen)) (hl (exp (gen) l)))) (defrole ltkgen (vars (P name) (l expn)) (trace (send (enc "cert-req" P (exp (gen) l) (privk P)))) (fn-of ("principal-of" (P (exp (gen) l))))) (defrole ca-gen (vars (P CA name) (h base)) (trace (recv (enc "cert-req" P h (privk P))) (send (enc "cert" h P (privk CA)))) (non-orig (privk P)) (fn-of ("principal-of" (P h))) (neq (h (gen))))) (defskeleton iadh-um (vars (key data) (A B CA A-0 B-0 CA-0 P P-0 name) (hl he hl-0 he-0 base) (e ep l lp expn)) (defstrand init 5 (key key) (A A) (B B) (CA CA) (hl hl) (he he) (l l) (e e)) (defstrand init 5 (key key) (A A-0) (B B-0) (CA CA-0) (hl hl-0) (he he-0) (l lp) (e ep)) (defstrand ltkgen 1 (P P) (l l)) (defstrand ltkgen 1 (P P-0) (l lp)) (fn-of ("principal-of" (P-0 (exp (gen) lp)) (P (exp (gen) l))) (foo ((hash (exp hl-0 lp) (exp he-0 ep)) key) ((hash (exp hl l) (exp he e)) key))) (neq (hl-0 (exp (gen) lp)) (he-0 (gen)) (hl (exp (gen) l)) (he (gen))) (non-orig (privk CA) (privk CA-0)) (uniq-gen e ep l lp) (traces ((recv (enc "cert" (exp (gen) l) A (privk CA))) (recv (enc "cert" hl B (privk CA))) (send (exp (gen) e)) (recv he) (send key)) ((recv (enc "cert" (exp (gen) lp) A-0 (privk CA-0))) (recv (enc "cert" hl-0 B-0 (privk CA-0))) (send (exp (gen) ep)) (recv he-0) (send key)) ((send (enc "cert-req" P (exp (gen) l) (privk P)))) ((send (enc "cert-req" P-0 (exp (gen) lp) (privk P-0))))) (label 0) (unrealized (0 0) (0 1) (1 0) (1 1)) (preskeleton) (comment "Not a skeleton")) (defskeleton iadh-um (vars (key data) (A B CA A-0 B-0 CA-0 P P-0 name) (hl he base) (l lp e ep expn)) (defstrand init 5 (key key) (A A) (B B) (CA CA) (hl hl) (he he) (l l) (e e)) (defstrand init 5 (key key) (A A-0) (B B-0) (CA CA-0) (hl (exp hl (mul l (rec lp)))) (he (exp he (mul e (rec ep)))) (l lp) (e ep)) (defstrand ltkgen 1 (P P) (l l)) (defstrand ltkgen 1 (P P-0) (l lp)) (precedes ((0 2) (1 3)) ((2 0) (0 0)) ((2 0) (1 1)) ((3 0) (1 0))) (fn-of ("principal-of" (P-0 (exp (gen) lp)) (P (exp (gen) l))) (foo ((hash (exp hl l) (exp he e)) key))) (neq ((exp hl (mul l (rec lp))) (exp (gen) lp)) ((exp he (mul e (rec ep))) (gen)) (hl (exp (gen) l)) (he (gen))) (non-orig (privk CA) (privk CA-0)) (uniq-gen l lp e ep) (traces ((recv (enc "cert" (exp (gen) l) A (privk CA))) (recv (enc "cert" hl B (privk CA))) (send (exp (gen) e)) (recv he) (send key)) ((recv (enc "cert" (exp (gen) lp) A-0 (privk CA-0))) (recv (enc "cert" (exp hl (mul l (rec lp))) B-0 (privk CA-0))) (send (exp (gen) ep)) (recv (exp he (mul e (rec ep)))) (send key)) ((send (enc "cert-req" P (exp (gen) l) (privk P)))) ((send (enc "cert-req" P-0 (exp (gen) lp) (privk P-0))))) (label 1) (parent 0) (unrealized (0 0) (0 1) (1 0) (1 1) (1 3)) (origs) (comment "1 in cohort - 1 not yet seen")) (defskeleton iadh-um (vars (key data) (A B CA A-0 B-0 CA-0 P name) (hl he base) (e ep lp expn)) (defstrand init 5 (key key) (A A) (B B) (CA CA) (hl hl) (he he) (l lp) (e e)) (defstrand init 5 (key key) (A A-0) (B B-0) (CA CA-0) (hl hl) (he (exp he (mul e (rec ep)))) (l lp) (e ep)) (defstrand ltkgen 1 (P P) (l lp)) (precedes ((0 2) (1 3)) ((2 0) (0 0)) ((2 0) (1 0))) (fn-of ("principal-of" (P (exp (gen) lp))) (foo ((hash (exp hl lp) (exp he e)) key))) (neq (hl (exp (gen) lp)) ((exp he (mul e (rec ep))) (gen)) (he (gen))) (non-orig (privk CA) (privk CA-0)) (uniq-gen e ep lp) (operation collapsed 3 2) (traces ((recv (enc "cert" (exp (gen) lp) A (privk CA))) (recv (enc "cert" hl B (privk CA))) (send (exp (gen) e)) (recv he) (send key)) ((recv (enc "cert" (exp (gen) lp) A-0 (privk CA-0))) (recv (enc "cert" hl B-0 (privk CA-0))) (send (exp (gen) ep)) (recv (exp he (mul e (rec ep)))) (send key)) ((send (enc "cert-req" P (exp (gen) lp) (privk P))))) (label 2) (parent 1) (unrealized (0 0) (0 1) (1 0) (1 1) (1 3)) (comment "1 in cohort - 1 not yet seen")) (defskeleton iadh-um (vars (key data) (A B CA P name) (hl he base) (lp ep expn)) (defstrand init 5 (key key) (A A) (B B) (CA CA) (hl hl) (he he) (l lp) (e ep)) (defstrand ltkgen 1 (P P) (l lp)) (precedes ((1 0) (0 0))) (fn-of ("principal-of" (P (exp (gen) lp))) (foo ((hash (exp hl lp) (exp he ep)) key))) (neq (hl (exp (gen) lp)) (he (gen))) (non-orig (privk CA)) (uniq-gen lp ep) (operation collapsed 1 0) (traces ((recv (enc "cert" (exp (gen) lp) A (privk CA))) (recv (enc "cert" hl B (privk CA))) (send (exp (gen) ep)) (recv he) (send key)) ((send (enc "cert-req" P (exp (gen) lp) (privk P))))) (label 3) (parent 2) (unrealized (0 0) (0 1)) (comment "1 in cohort - 1 not yet seen")) (defskeleton iadh-um (vars (key data) (A B CA B-0 CA-0 P P-0 name) (hl he base) (l lp e ep expn)) (defstrand init 5 (key key) (A A) (B B) (CA CA) (hl hl) (he he) (l l) (e e)) (defstrand init 5 (key key) (A P-0) (B B-0) (CA CA-0) (hl (exp hl (mul l (rec lp)))) (he (exp he (mul e (rec ep)))) (l lp) (e ep)) (defstrand ltkgen 1 (P P) (l l)) (defstrand ltkgen 1 (P P-0) (l lp)) (defstrand ca-gen 2 (P P-0) (CA CA-0) (h (exp (gen) lp))) (precedes ((0 2) (1 3)) ((2 0) (0 0)) ((2 0) (1 1)) ((3 0) (4 0)) ((4 1) (1 0))) (fn-of ("principal-of" (P-0 (exp (gen) lp)) (P (exp (gen) l))) (foo ((hash (exp hl l) (exp he e)) key))) (neq ((exp (gen) lp) (gen)) ((exp hl (mul l (rec lp))) (exp (gen) lp)) ((exp he (mul e (rec ep))) (gen)) (hl (exp (gen) l)) (he (gen))) (non-orig (privk CA) (privk CA-0) (privk P-0)) (uniq-gen l lp e ep) (operation encryption-test (added-strand ca-gen 2) (enc "cert" (exp (gen) lp) P-0 (privk CA-0)) (1 0)) (traces ((recv (enc "cert" (exp (gen) l) A (privk CA))) (recv (enc "cert" hl B (privk CA))) (send (exp (gen) e)) (recv he) (send key)) ((recv (enc "cert" (exp (gen) lp) P-0 (privk CA-0))) (recv (enc "cert" (exp hl (mul l (rec lp))) B-0 (privk CA-0))) (send (exp (gen) ep)) (recv (exp he (mul e (rec ep)))) (send key)) ((send (enc "cert-req" P (exp (gen) l) (privk P)))) ((send (enc "cert-req" P-0 (exp (gen) lp) (privk P-0)))) ((recv (enc "cert-req" P-0 (exp (gen) lp) (privk P-0))) (send (enc "cert" (exp (gen) lp) P-0 (privk CA-0))))) (label 4) (parent 1) (unrealized (0 0) (0 1) (1 1) (1 3)) (comment "1 in cohort - 1 not yet seen")) (defskeleton iadh-um (vars (key data) (A B CA B-0 CA-0 P name) (hl he base) (e ep lp expn)) (defstrand init 5 (key key) (A A) (B B) (CA CA) (hl hl) (he he) (l lp) (e e)) (defstrand init 5 (key key) (A P) (B B-0) (CA CA-0) (hl hl) (he (exp he (mul e (rec ep)))) (l lp) (e ep)) (defstrand ltkgen 1 (P P) (l lp)) (defstrand ca-gen 2 (P P) (CA CA-0) (h (exp (gen) lp))) (precedes ((0 2) (1 3)) ((2 0) (0 0)) ((2 0) (3 0)) ((3 1) (1 0))) (fn-of ("principal-of" (P (exp (gen) lp))) (foo ((hash (exp hl lp) (exp he e)) key))) (neq ((exp (gen) lp) (gen)) (hl (exp (gen) lp)) ((exp he (mul e (rec ep))) (gen)) (he (gen))) (non-orig (privk CA) (privk CA-0) (privk P)) (uniq-gen e ep lp) (operation encryption-test (added-strand ca-gen 2) (enc "cert" (exp (gen) lp) P (privk CA-0)) (1 0)) (traces ((recv (enc "cert" (exp (gen) lp) A (privk CA))) (recv (enc "cert" hl B (privk CA))) (send (exp (gen) e)) (recv he) (send key)) ((recv (enc "cert" (exp (gen) lp) P (privk CA-0))) (recv (enc "cert" hl B-0 (privk CA-0))) (send (exp (gen) ep)) (recv (exp he (mul e (rec ep)))) (send key)) ((send (enc "cert-req" P (exp (gen) lp) (privk P)))) ((recv (enc "cert-req" P (exp (gen) lp) (privk P))) (send (enc "cert" (exp (gen) lp) P (privk CA-0))))) (label 5) (parent 2) (unrealized (0 0) (0 1) (1 1) (1 3)) (origs) (comment "1 in cohort - 1 not yet seen")) (defskeleton iadh-um (vars (key data) (B CA P name) (hl he base) (lp ep expn)) (defstrand init 5 (key key) (A P) (B B) (CA CA) (hl hl) (he he) (l lp) (e ep)) (defstrand ltkgen 1 (P P) (l lp)) (defstrand ca-gen 2 (P P) (CA CA) (h (exp (gen) lp))) (precedes ((1 0) (2 0)) ((2 1) (0 0))) (fn-of ("principal-of" (P (exp (gen) lp))) (foo ((hash (exp hl lp) (exp he ep)) key))) (neq ((exp (gen) lp) (gen)) (hl (exp (gen) lp)) (he (gen))) (non-orig (privk CA) (privk P)) (uniq-gen lp ep) (operation encryption-test (added-strand ca-gen 2) (enc "cert" (exp (gen) lp) P (privk CA)) (0 0)) (traces ((recv (enc "cert" (exp (gen) lp) P (privk CA))) (recv (enc "cert" hl B (privk CA))) (send (exp (gen) ep)) (recv he) (send key)) ((send (enc "cert-req" P (exp (gen) lp) (privk P)))) ((recv (enc "cert-req" P (exp (gen) lp) (privk P))) (send (enc "cert" (exp (gen) lp) P (privk CA))))) (label 6) (parent 3) (unrealized (0 1)) (comment "1 in cohort - 1 not yet seen")) (defskeleton iadh-um (vars (key data) (A B CA B-0 CA-0 P P-0 name) (hl he base) (e ep l lp expn)) (defstrand init 5 (key key) (A A) (B B) (CA CA) (hl hl) (he he) (l l) (e e)) (defstrand init 5 (key key) (A P-0) (B B-0) (CA CA-0) (hl (exp hl (mul l (rec lp)))) (he (exp he (mul e (rec ep)))) (l lp) (e ep)) (defstrand ltkgen 1 (P P) (l l)) (defstrand ltkgen 1 (P P-0) (l lp)) (defstrand ca-gen 2 (P P-0) (CA CA-0) (h (exp (gen) lp))) (defstrand ca-gen 2 (P B-0) (CA CA-0) (h (exp hl (mul l (rec lp))))) (precedes ((0 2) (1 3)) ((2 0) (0 0)) ((2 0) (5 0)) ((3 0) (4 0)) ((3 0) (5 0)) ((4 1) (1 0)) ((5 1) (1 1))) (fn-of ("principal-of" (B-0 (exp hl (mul l (rec lp)))) (P-0 (exp (gen) lp)) (P (exp (gen) l))) (foo ((hash (exp hl l) (exp he e)) key))) (neq ((exp hl (mul l (rec lp))) (gen)) ((exp (gen) lp) (gen)) ((exp hl (mul l (rec lp))) (exp (gen) lp)) ((exp he (mul e (rec ep))) (gen)) (hl (exp (gen) l)) (he (gen))) (non-orig (privk CA) (privk B-0) (privk CA-0) (privk P-0)) (uniq-gen e ep l lp) (operation encryption-test (added-strand ca-gen 2) (enc "cert" (exp hl (mul l (rec lp))) B-0 (privk CA-0)) (1 1)) (traces ((recv (enc "cert" (exp (gen) l) A (privk CA))) (recv (enc "cert" hl B (privk CA))) (send (exp (gen) e)) (recv he) (send key)) ((recv (enc "cert" (exp (gen) lp) P-0 (privk CA-0))) (recv (enc "cert" (exp hl (mul l (rec lp))) B-0 (privk CA-0))) (send (exp (gen) ep)) (recv (exp he (mul e (rec ep)))) (send key)) ((send (enc "cert-req" P (exp (gen) l) (privk P)))) ((send (enc "cert-req" P-0 (exp (gen) lp) (privk P-0)))) ((recv (enc "cert-req" P-0 (exp (gen) lp) (privk P-0))) (send (enc "cert" (exp (gen) lp) P-0 (privk CA-0)))) ((recv (enc "cert-req" B-0 (exp hl (mul l (rec lp))) (privk B-0))) (send (enc "cert" (exp hl (mul l (rec lp))) B-0 (privk CA-0))))) (label 7) (parent 4) (unrealized (0 0) (0 1) (1 3) (5 0)) (comment "2 in cohort - 2 not yet seen")) (defskeleton iadh-um (vars (key data) (A B CA B-0 CA-0 P name) (hl he base) (e ep lp expn)) (defstrand init 5 (key key) (A A) (B B) (CA CA) (hl hl) (he he) (l lp) (e e)) (defstrand init 5 (key key) (A P) (B B-0) (CA CA-0) (hl hl) (he (exp he (mul e (rec ep)))) (l lp) (e ep)) (defstrand ltkgen 1 (P P) (l lp)) (defstrand ca-gen 2 (P P) (CA CA-0) (h (exp (gen) lp))) (defstrand ca-gen 2 (P B-0) (CA CA-0) (h hl)) (precedes ((0 2) (1 3)) ((2 0) (0 0)) ((2 0) (3 0)) ((3 1) (1 0)) ((4 1) (1 1))) (fn-of ("principal-of" (B-0 hl) (P (exp (gen) lp))) (foo ((hash (exp hl lp) (exp he e)) key))) (neq (hl (gen)) ((exp (gen) lp) (gen)) (hl (exp (gen) lp)) ((exp he (mul e (rec ep))) (gen)) (he (gen))) (non-orig (privk CA) (privk B-0) (privk CA-0) (privk P)) (uniq-gen e ep lp) (operation encryption-test (added-strand ca-gen 2) (enc "cert" hl B-0 (privk CA-0)) (1 1)) (traces ((recv (enc "cert" (exp (gen) lp) A (privk CA))) (recv (enc "cert" hl B (privk CA))) (send (exp (gen) e)) (recv he) (send key)) ((recv (enc "cert" (exp (gen) lp) P (privk CA-0))) (recv (enc "cert" hl B-0 (privk CA-0))) (send (exp (gen) ep)) (recv (exp he (mul e (rec ep)))) (send key)) ((send (enc "cert-req" P (exp (gen) lp) (privk P)))) ((recv (enc "cert-req" P (exp (gen) lp) (privk P))) (send (enc "cert" (exp (gen) lp) P (privk CA-0)))) ((recv (enc "cert-req" B-0 hl (privk B-0))) (send (enc "cert" hl B-0 (privk CA-0))))) (label 8) (parent 5) (unrealized (0 0) (0 1) (1 3) (4 0)) (comment "1 in cohort - 1 not yet seen")) (defskeleton iadh-um (vars (key data) (B CA P name) (hl he base) (lp ep expn)) (defstrand init 5 (key key) (A P) (B B) (CA CA) (hl hl) (he he) (l lp) (e ep)) (defstrand ltkgen 1 (P P) (l lp)) (defstrand ca-gen 2 (P P) (CA CA) (h (exp (gen) lp))) (defstrand ca-gen 2 (P B) (CA CA) (h hl)) (precedes ((1 0) (2 0)) ((2 1) (0 0)) ((3 1) (0 1))) (fn-of ("principal-of" (B hl) (P (exp (gen) lp))) (foo ((hash (exp hl lp) (exp he ep)) key))) (neq (hl (gen)) ((exp (gen) lp) (gen)) (hl (exp (gen) lp)) (he (gen))) (non-orig (privk B) (privk CA) (privk P)) (uniq-gen lp ep) (operation encryption-test (added-strand ca-gen 2) (enc "cert" hl B (privk CA)) (0 1)) (traces ((recv (enc "cert" (exp (gen) lp) P (privk CA))) (recv (enc "cert" hl B (privk CA))) (send (exp (gen) ep)) (recv he) (send key)) ((send (enc "cert-req" P (exp (gen) lp) (privk P)))) ((recv (enc "cert-req" P (exp (gen) lp) (privk P))) (send (enc "cert" (exp (gen) lp) P (privk CA)))) ((recv (enc "cert-req" B hl (privk B))) (send (enc "cert" hl B (privk CA))))) (label 9) (parent 6) (unrealized (3 0)) (origs) (comment "1 in cohort - 1 not yet seen")) (defskeleton iadh-um (vars (key data) (A B CA CA-0 P P-0 name) (he base) (e ep lp l expn)) (defstrand init 5 (key key) (A A) (B B) (CA CA) (hl (exp (gen) lp)) (he he) (l l) (e e)) (defstrand init 5 (key key) (A P-0) (B P) (CA CA-0) (hl (exp (gen) l)) (he (exp he (mul e (rec ep)))) (l lp) (e ep)) (defstrand ltkgen 1 (P P) (l l)) (defstrand ltkgen 1 (P P-0) (l lp)) (defstrand ca-gen 2 (P P-0) (CA CA-0) (h (exp (gen) lp))) (defstrand ca-gen 2 (P P) (CA CA-0) (h (exp (gen) l))) (precedes ((0 2) (1 3)) ((2 0) (0 0)) ((2 0) (5 0)) ((3 0) (0 1)) ((3 0) (4 0)) ((3 0) (5 0)) ((4 1) (1 0)) ((5 1) (1 1))) (fn-of ("principal-of" (P (exp (gen) l)) (P-0 (exp (gen) lp))) (foo ((hash (exp (gen) (mul lp l)) (exp he e)) key))) (neq ((exp (gen) l) (gen)) ((exp (gen) lp) (gen)) ((exp (gen) l) (exp (gen) lp)) ((exp he (mul e (rec ep))) (gen)) ((exp (gen) lp) (exp (gen) l)) (he (gen))) (non-orig (privk CA) (privk CA-0) (privk P) (privk P-0)) (uniq-gen e ep lp l) (operation encryption-test (displaced 6 2 ltkgen 1) (enc "cert-req" B-0 (exp (gen) l-0) (privk B-0)) (5 0)) (traces ((recv (enc "cert" (exp (gen) l) A (privk CA))) (recv (enc "cert" (exp (gen) lp) B (privk CA))) (send (exp (gen) e)) (recv he) (send key)) ((recv (enc "cert" (exp (gen) lp) P-0 (privk CA-0))) (recv (enc "cert" (exp (gen) l) P (privk CA-0))) (send (exp (gen) ep)) (recv (exp he (mul e (rec ep)))) (send key)) ((send (enc "cert-req" P (exp (gen) l) (privk P)))) ((send (enc "cert-req" P-0 (exp (gen) lp) (privk P-0)))) ((recv (enc "cert-req" P-0 (exp (gen) lp) (privk P-0))) (send (enc "cert" (exp (gen) lp) P-0 (privk CA-0)))) ((recv (enc "cert-req" P (exp (gen) l) (privk P))) (send (enc "cert" (exp (gen) l) P (privk CA-0))))) (label 10) (parent 7) (unrealized (0 0) (0 1) (1 3)) (comment "1 in cohort - 1 not yet seen")) (defskeleton iadh-um (vars (key data) (A B CA B-0 CA-0 P P-0 name) (he base) (e ep l lp l-0 expn)) (defstrand init 5 (key key) (A A) (B B) (CA CA) (hl (exp (gen) (mul (rec l) lp l-0))) (he he) (l l) (e e)) (defstrand init 5 (key key) (A P-0) (B B-0) (CA CA-0) (hl (exp (gen) l-0)) (he (exp he (mul e (rec ep)))) (l lp) (e ep)) (defstrand ltkgen 1 (P P) (l l)) (defstrand ltkgen 1 (P P-0) (l lp)) (defstrand ca-gen 2 (P P-0) (CA CA-0) (h (exp (gen) lp))) (defstrand ca-gen 2 (P B-0) (CA CA-0) (h (exp (gen) l-0))) (defstrand ltkgen 1 (P B-0) (l l-0)) (precedes ((0 2) (1 3)) ((2 0) (0 0)) ((2 0) (5 0)) ((3 0) (0 1)) ((3 0) (4 0)) ((3 0) (5 0)) ((4 1) (1 0)) ((5 1) (1 1)) ((6 0) (5 0))) (fn-of ("principal-of" (B-0 (exp (gen) l-0)) (P-0 (exp (gen) lp)) (P (exp (gen) l))) (foo ((hash (exp (gen) (mul lp l-0)) (exp he e)) key))) (neq ((exp (gen) l-0) (gen)) ((exp (gen) lp) (gen)) ((exp (gen) l-0) (exp (gen) lp)) ((exp he (mul e (rec ep))) (gen)) ((exp (gen) (mul (rec l) lp l-0)) (exp (gen) l)) (he (gen))) (non-orig (privk CA) (privk B-0) (privk CA-0) (privk P-0)) (uniq-gen e ep l lp) (operation encryption-test (added-strand ltkgen 1) (enc "cert-req" B-0 (exp (gen) l-0) (privk B-0)) (5 0)) (traces ((recv (enc "cert" (exp (gen) l) A (privk CA))) (recv (enc "cert" (exp (gen) (mul (rec l) lp l-0)) B (privk CA))) (send (exp (gen) e)) (recv he) (send key)) ((recv (enc "cert" (exp (gen) lp) P-0 (privk CA-0))) (recv (enc "cert" (exp (gen) l-0) B-0 (privk CA-0))) (send (exp (gen) ep)) (recv (exp he (mul e (rec ep)))) (send key)) ((send (enc "cert-req" P (exp (gen) l) (privk P)))) ((send (enc "cert-req" P-0 (exp (gen) lp) (privk P-0)))) ((recv (enc "cert-req" P-0 (exp (gen) lp) (privk P-0))) (send (enc "cert" (exp (gen) lp) P-0 (privk CA-0)))) ((recv (enc "cert-req" B-0 (exp (gen) l-0) (privk B-0))) (send (enc "cert" (exp (gen) l-0) B-0 (privk CA-0)))) ((send (enc "cert-req" B-0 (exp (gen) l-0) (privk B-0))))) (label 11) (parent 7) (unrealized (0 0) (0 1) (1 3)) (comment "1 in cohort - 1 not yet seen")) (defskeleton iadh-um (vars (key data) (A B CA B-0 CA-0 P name) (he base) (e ep lp l expn)) (defstrand init 5 (key key) (A A) (B B) (CA CA) (hl (exp (gen) l)) (he he) (l lp) (e e)) (defstrand init 5 (key key) (A P) (B B-0) (CA CA-0) (hl (exp (gen) l)) (he (exp he (mul e (rec ep)))) (l lp) (e ep)) (defstrand ltkgen 1 (P P) (l lp)) (defstrand ca-gen 2 (P P) (CA CA-0) (h (exp (gen) lp))) (defstrand ca-gen 2 (P B-0) (CA CA-0) (h (exp (gen) l))) (defstrand ltkgen 1 (P B-0) (l l)) (precedes ((0 2) (1 3)) ((2 0) (0 0)) ((2 0) (3 0)) ((3 1) (1 0)) ((4 1) (1 1)) ((5 0) (4 0))) (fn-of ("principal-of" (B-0 (exp (gen) l)) (P (exp (gen) lp))) (foo ((hash (exp (gen) (mul lp l)) (exp he e)) key))) (neq ((exp (gen) l) (gen)) ((exp (gen) lp) (gen)) ((exp (gen) l) (exp (gen) lp)) ((exp he (mul e (rec ep))) (gen)) (he (gen))) (non-orig (privk CA) (privk B-0) (privk CA-0) (privk P)) (uniq-gen e ep lp) (operation encryption-test (added-strand ltkgen 1) (enc "cert-req" B-0 (exp (gen) l) (privk B-0)) (4 0)) (traces ((recv (enc "cert" (exp (gen) lp) A (privk CA))) (recv (enc "cert" (exp (gen) l) B (privk CA))) (send (exp (gen) e)) (recv he) (send key)) ((recv (enc "cert" (exp (gen) lp) P (privk CA-0))) (recv (enc "cert" (exp (gen) l) B-0 (privk CA-0))) (send (exp (gen) ep)) (recv (exp he (mul e (rec ep)))) (send key)) ((send (enc "cert-req" P (exp (gen) lp) (privk P)))) ((recv (enc "cert-req" P (exp (gen) lp) (privk P))) (send (enc "cert" (exp (gen) lp) P (privk CA-0)))) ((recv (enc "cert-req" B-0 (exp (gen) l) (privk B-0))) (send (enc "cert" (exp (gen) l) B-0 (privk CA-0)))) ((send (enc "cert-req" B-0 (exp (gen) l) (privk B-0))))) (label 12) (parent 8) (unrealized (0 0) (0 1) (1 3)) (comment "1 in cohort - 1 not yet seen")) (defskeleton iadh-um (vars (key data) (B CA P name) (he base) (lp ep l expn)) (defstrand init 5 (key key) (A P) (B B) (CA CA) (hl (exp (gen) l)) (he he) (l lp) (e ep)) (defstrand ltkgen 1 (P P) (l lp)) (defstrand ca-gen 2 (P P) (CA CA) (h (exp (gen) lp))) (defstrand ca-gen 2 (P B) (CA CA) (h (exp (gen) l))) (defstrand ltkgen 1 (P B) (l l)) (precedes ((1 0) (2 0)) ((2 1) (0 0)) ((3 1) (0 1)) ((4 0) (3 0))) (fn-of ("principal-of" (B (exp (gen) l)) (P (exp (gen) lp))) (foo ((hash (exp (gen) (mul lp l)) (exp he ep)) key))) (neq ((exp (gen) l) (gen)) ((exp (gen) lp) (gen)) ((exp (gen) l) (exp (gen) lp)) (he (gen))) (non-orig (privk B) (privk CA) (privk P)) (uniq-gen lp ep) (operation encryption-test (added-strand ltkgen 1) (enc "cert-req" B (exp (gen) l) (privk B)) (3 0)) (traces ((recv (enc "cert" (exp (gen) lp) P (privk CA))) (recv (enc "cert" (exp (gen) l) B (privk CA))) (send (exp (gen) ep)) (recv he) (send key)) ((send (enc "cert-req" P (exp (gen) lp) (privk P)))) ((recv (enc "cert-req" P (exp (gen) lp) (privk P))) (send (enc "cert" (exp (gen) lp) P (privk CA)))) ((recv (enc "cert-req" B (exp (gen) l) (privk B))) (send (enc "cert" (exp (gen) l) B (privk CA)))) ((send (enc "cert-req" B (exp (gen) l) (privk B))))) (label 13) (parent 9) (unrealized) (shape) (maps) (origs)) (defskeleton iadh-um (vars (key data) (A B CA CA-0 P P-0 name) (e ep lp l expn) (l-0 expr)) (defstrand init 5 (key key) (A A) (B B) (CA CA) (hl (exp (gen) lp)) (he (exp (gen) (mul (rec e) ep l l-0))) (l l) (e e)) (defstrand init 5 (key key) (A P-0) (B P) (CA CA-0) (hl (exp (gen) l)) (he (exp (gen) (mul l l-0))) (l lp) (e ep)) (defstrand ltkgen 1 (P P) (l l)) (defstrand ltkgen 1 (P P-0) (l lp)) (defstrand ca-gen 2 (P P-0) (CA CA-0) (h (exp (gen) lp))) (defstrand ca-gen 2 (P P) (CA CA-0) (h (exp (gen) l))) (precedes ((0 2) (1 3)) ((1 2) (0 3)) ((2 0) (0 0)) ((2 0) (5 0)) ((3 0) (0 1)) ((3 0) (4 0)) ((3 0) (5 0)) ((4 1) (1 0)) ((5 1) (1 1))) (fn-of ("principal-of" (P (exp (gen) l)) (P-0 (exp (gen) lp))) (foo ((hash (exp (gen) (mul lp l)) (exp (gen) (mul ep l l-0))) key))) (neq ((exp (gen) l) (gen)) ((exp (gen) lp) (gen)) ((exp (gen) l) (exp (gen) lp)) ((exp (gen) (mul l l-0)) (gen)) ((exp (gen) lp) (exp (gen) l)) ((exp (gen) (mul (rec e) ep l l-0)) (gen))) (non-orig (privk CA) (privk CA-0) (privk P) (privk P-0)) (uniq-gen e ep lp l) (operation nonce-test (algebra-contracted (he (exp (gen) (mul (rec e) ep l l-0)))) (exp (gen) (mul l l-0)) (1 3)) (traces ((recv (enc "cert" (exp (gen) l) A (privk CA))) (recv (enc "cert" (exp (gen) lp) B (privk CA))) (send (exp (gen) e)) (recv (exp (gen) (mul (rec e) ep l l-0))) (send key)) ((recv (enc "cert" (exp (gen) lp) P-0 (privk CA-0))) (recv (enc "cert" (exp (gen) l) P (privk CA-0))) (send (exp (gen) ep)) (recv (exp (gen) (mul l l-0))) (send key)) ((send (enc "cert-req" P (exp (gen) l) (privk P)))) ((send (enc "cert-req" P-0 (exp (gen) lp) (privk P-0)))) ((recv (enc "cert-req" P-0 (exp (gen) lp) (privk P-0))) (send (enc "cert" (exp (gen) lp) P-0 (privk CA-0)))) ((recv (enc "cert-req" P (exp (gen) l) (privk P))) (send (enc "cert" (exp (gen) l) P (privk CA-0))))) (label 14) (parent 10) (unrealized (0 0) (0 1) (0 3)) (comment "2 in cohort - 2 not yet seen")) (defskeleton iadh-um (vars (key data) (A B CA B-0 CA-0 P P-0 name) (e ep l lp l-0 expn) (l-1 expr)) (defstrand init 5 (key key) (A A) (B B) (CA CA) (hl (exp (gen) (mul (rec l) lp l-0))) (he (exp (gen) (mul (rec e) ep l-0 l-1))) (l l) (e e)) (defstrand init 5 (key key) (A P-0) (B B-0) (CA CA-0) (hl (exp (gen) l-0)) (he (exp (gen) (mul l-0 l-1))) (l lp) (e ep)) (defstrand ltkgen 1 (P P) (l l)) (defstrand ltkgen 1 (P P-0) (l lp)) (defstrand ca-gen 2 (P P-0) (CA CA-0) (h (exp (gen) lp))) (defstrand ca-gen 2 (P B-0) (CA CA-0) (h (exp (gen) l-0))) (defstrand ltkgen 1 (P B-0) (l l-0)) (precedes ((0 2) (1 3)) ((1 2) (0 3)) ((2 0) (0 0)) ((2 0) (5 0)) ((3 0) (0 1)) ((3 0) (4 0)) ((3 0) (5 0)) ((4 1) (1 0)) ((5 1) (1 1)) ((6 0) (5 0))) (fn-of ("principal-of" (B-0 (exp (gen) l-0)) (P-0 (exp (gen) lp)) (P (exp (gen) l))) (foo ((hash (exp (gen) (mul lp l-0)) (exp (gen) (mul ep l-0 l-1))) key))) (neq ((exp (gen) l-0) (gen)) ((exp (gen) lp) (gen)) ((exp (gen) l-0) (exp (gen) lp)) ((exp (gen) (mul l-0 l-1)) (gen)) ((exp (gen) (mul (rec l) lp l-0)) (exp (gen) l)) ((exp (gen) (mul (rec e) ep l-0 l-1)) (gen))) (non-orig (privk CA) (privk B-0) (privk CA-0) (privk P-0)) (uniq-gen e ep l lp) (operation nonce-test (algebra-contracted (he (exp (gen) (mul (rec e) ep l-0 l-1)))) (exp (gen) (mul l-0 l-1)) (1 3)) (traces ((recv (enc "cert" (exp (gen) l) A (privk CA))) (recv (enc "cert" (exp (gen) (mul (rec l) lp l-0)) B (privk CA))) (send (exp (gen) e)) (recv (exp (gen) (mul (rec e) ep l-0 l-1))) (send key)) ((recv (enc "cert" (exp (gen) lp) P-0 (privk CA-0))) (recv (enc "cert" (exp (gen) l-0) B-0 (privk CA-0))) (send (exp (gen) ep)) (recv (exp (gen) (mul l-0 l-1))) (send key)) ((send (enc "cert-req" P (exp (gen) l) (privk P)))) ((send (enc "cert-req" P-0 (exp (gen) lp) (privk P-0)))) ((recv (enc "cert-req" P-0 (exp (gen) lp) (privk P-0))) (send (enc "cert" (exp (gen) lp) P-0 (privk CA-0)))) ((recv (enc "cert-req" B-0 (exp (gen) l-0) (privk B-0))) (send (enc "cert" (exp (gen) l-0) B-0 (privk CA-0)))) ((send (enc "cert-req" B-0 (exp (gen) l-0) (privk B-0))))) (label 15) (parent 11) (unrealized (0 0) (0 1) (0 3)) (comment "1 in cohort - 1 not yet seen")) (defskeleton iadh-um (vars (key data) (A B CA B-0 CA-0 P name) (e ep lp l expn) (l-0 expr)) (defstrand init 5 (key key) (A A) (B B) (CA CA) (hl (exp (gen) l)) (he (exp (gen) (mul (rec e) ep l l-0))) (l lp) (e e)) (defstrand init 5 (key key) (A P) (B B-0) (CA CA-0) (hl (exp (gen) l)) (he (exp (gen) (mul l l-0))) (l lp) (e ep)) (defstrand ltkgen 1 (P P) (l lp)) (defstrand ca-gen 2 (P P) (CA CA-0) (h (exp (gen) lp))) (defstrand ca-gen 2 (P B-0) (CA CA-0) (h (exp (gen) l))) (defstrand ltkgen 1 (P B-0) (l l)) (precedes ((0 2) (1 3)) ((1 2) (0 3)) ((2 0) (0 0)) ((2 0) (3 0)) ((3 1) (1 0)) ((4 1) (1 1)) ((5 0) (4 0))) (fn-of ("principal-of" (B-0 (exp (gen) l)) (P (exp (gen) lp))) (foo ((hash (exp (gen) (mul lp l)) (exp (gen) (mul ep l l-0))) key))) (neq ((exp (gen) l) (gen)) ((exp (gen) lp) (gen)) ((exp (gen) l) (exp (gen) lp)) ((exp (gen) (mul l l-0)) (gen)) ((exp (gen) (mul (rec e) ep l l-0)) (gen))) (non-orig (privk CA) (privk B-0) (privk CA-0) (privk P)) (uniq-gen e ep lp) (operation nonce-test (algebra-contracted (he (exp (gen) (mul (rec e) ep l l-0)))) (exp (gen) (mul l l-0)) (1 3)) (traces ((recv (enc "cert" (exp (gen) lp) A (privk CA))) (recv (enc "cert" (exp (gen) l) B (privk CA))) (send (exp (gen) e)) (recv (exp (gen) (mul (rec e) ep l l-0))) (send key)) ((recv (enc "cert" (exp (gen) lp) P (privk CA-0))) (recv (enc "cert" (exp (gen) l) B-0 (privk CA-0))) (send (exp (gen) ep)) (recv (exp (gen) (mul l l-0))) (send key)) ((send (enc "cert-req" P (exp (gen) lp) (privk P)))) ((recv (enc "cert-req" P (exp (gen) lp) (privk P))) (send (enc "cert" (exp (gen) lp) P (privk CA-0)))) ((recv (enc "cert-req" B-0 (exp (gen) l) (privk B-0))) (send (enc "cert" (exp (gen) l) B-0 (privk CA-0)))) ((send (enc "cert-req" B-0 (exp (gen) l) (privk B-0))))) (label 16) (parent 12) (unrealized (0 0) (0 1) (0 3)) (comment "2 in cohort - 2 not yet seen")) (defskeleton iadh-um (vars (key data) (B CA P P-0 name) (e ep lp l expn) (l-0 expr)) (defstrand init 5 (key key) (A P) (B B) (CA CA) (hl (exp (gen) lp)) (he (exp (gen) (mul (rec e) ep l l-0))) (l l) (e e)) (defstrand init 5 (key key) (A P-0) (B P) (CA CA) (hl (exp (gen) l)) (he (exp (gen) (mul l l-0))) (l lp) (e ep)) (defstrand ltkgen 1 (P P) (l l)) (defstrand ltkgen 1 (P P-0) (l lp)) (defstrand ca-gen 2 (P P-0) (CA CA) (h (exp (gen) lp))) (defstrand ca-gen 2 (P P) (CA CA) (h (exp (gen) l))) (precedes ((0 2) (1 3)) ((1 2) (0 3)) ((2 0) (5 0)) ((3 0) (4 0)) ((3 0) (5 0)) ((4 1) (1 0)) ((5 1) (0 0)) ((5 1) (1 1))) (fn-of ("principal-of" (P (exp (gen) l)) (P-0 (exp (gen) lp))) (foo ((hash (exp (gen) (mul lp l)) (exp (gen) (mul ep l l-0))) key))) (neq ((exp (gen) l) (gen)) ((exp (gen) lp) (gen)) ((exp (gen) l) (exp (gen) lp)) ((exp (gen) (mul l l-0)) (gen)) ((exp (gen) lp) (exp (gen) l)) ((exp (gen) (mul (rec e) ep l l-0)) (gen))) (non-orig (privk CA) (privk P) (privk P-0)) (uniq-gen e ep lp l) (operation encryption-test (displaced 6 5 ca-gen 2) (enc "cert" (exp (gen) l) A (privk CA-0)) (0 0)) (traces ((recv (enc "cert" (exp (gen) l) P (privk CA))) (recv (enc "cert" (exp (gen) lp) B (privk CA))) (send (exp (gen) e)) (recv (exp (gen) (mul (rec e) ep l l-0))) (send key)) ((recv (enc "cert" (exp (gen) lp) P-0 (privk CA))) (recv (enc "cert" (exp (gen) l) P (privk CA))) (send (exp (gen) ep)) (recv (exp (gen) (mul l l-0))) (send key)) ((send (enc "cert-req" P (exp (gen) l) (privk P)))) ((send (enc "cert-req" P-0 (exp (gen) lp) (privk P-0)))) ((recv (enc "cert-req" P-0 (exp (gen) lp) (privk P-0))) (send (enc "cert" (exp (gen) lp) P-0 (privk CA)))) ((recv (enc "cert-req" P (exp (gen) l) (privk P))) (send (enc "cert" (exp (gen) l) P (privk CA))))) (label 17) (parent 14) (unrealized (0 1) (0 3)) (comment "2 in cohort - 2 not yet seen")) (defskeleton iadh-um (vars (key data) (B CA CA-0 P P-0 name) (e ep lp l expn) (l-0 expr)) (defstrand init 5 (key key) (A P) (B B) (CA CA) (hl (exp (gen) lp)) (he (exp (gen) (mul (rec e) ep l l-0))) (l l) (e e)) (defstrand init 5 (key key) (A P-0) (B P) (CA CA-0) (hl (exp (gen) l)) (he (exp (gen) (mul l l-0))) (l lp) (e ep)) (defstrand ltkgen 1 (P P) (l l)) (defstrand ltkgen 1 (P P-0) (l lp)) (defstrand ca-gen 2 (P P-0) (CA CA-0) (h (exp (gen) lp))) (defstrand ca-gen 2 (P P) (CA CA-0) (h (exp (gen) l))) (defstrand ca-gen 2 (P P) (CA CA) (h (exp (gen) l))) (precedes ((0 2) (1 3)) ((1 2) (0 3)) ((2 0) (5 0)) ((2 0) (6 0)) ((3 0) (0 1)) ((3 0) (4 0)) ((3 0) (5 0)) ((4 1) (1 0)) ((5 1) (1 1)) ((6 1) (0 0))) (fn-of ("principal-of" (P (exp (gen) l)) (P-0 (exp (gen) lp))) (foo ((hash (exp (gen) (mul lp l)) (exp (gen) (mul ep l l-0))) key))) (neq ((exp (gen) l) (gen)) ((exp (gen) lp) (gen)) ((exp (gen) l) (exp (gen) lp)) ((exp (gen) (mul l l-0)) (gen)) ((exp (gen) lp) (exp (gen) l)) ((exp (gen) (mul (rec e) ep l l-0)) (gen))) (non-orig (privk CA) (privk CA-0) (privk P) (privk P-0)) (uniq-gen e ep lp l) (operation encryption-test (added-strand ca-gen 2) (enc "cert" (exp (gen) l) P (privk CA)) (0 0)) (traces ((recv (enc "cert" (exp (gen) l) P (privk CA))) (recv (enc "cert" (exp (gen) lp) B (privk CA))) (send (exp (gen) e)) (recv (exp (gen) (mul (rec e) ep l l-0))) (send key)) ((recv (enc "cert" (exp (gen) lp) P-0 (privk CA-0))) (recv (enc "cert" (exp (gen) l) P (privk CA-0))) (send (exp (gen) ep)) (recv (exp (gen) (mul l l-0))) (send key)) ((send (enc "cert-req" P (exp (gen) l) (privk P)))) ((send (enc "cert-req" P-0 (exp (gen) lp) (privk P-0)))) ((recv (enc "cert-req" P-0 (exp (gen) lp) (privk P-0))) (send (enc "cert" (exp (gen) lp) P-0 (privk CA-0)))) ((recv (enc "cert-req" P (exp (gen) l) (privk P))) (send (enc "cert" (exp (gen) l) P (privk CA-0)))) ((recv (enc "cert-req" P (exp (gen) l) (privk P))) (send (enc "cert" (exp (gen) l) P (privk CA))))) (label 18) (parent 14) (unrealized (0 1) (0 3)) (comment "2 in cohort - 2 not yet seen")) (defskeleton iadh-um (vars (key data) (B CA B-0 CA-0 P P-0 name) (e ep l lp l-0 expn) (l-1 expr)) (defstrand init 5 (key key) (A P) (B B) (CA CA) (hl (exp (gen) (mul (rec l) lp l-0))) (he (exp (gen) (mul (rec e) ep l-0 l-1))) (l l) (e e)) (defstrand init 5 (key key) (A P-0) (B B-0) (CA CA-0) (hl (exp (gen) l-0)) (he (exp (gen) (mul l-0 l-1))) (l lp) (e ep)) (defstrand ltkgen 1 (P P) (l l)) (defstrand ltkgen 1 (P P-0) (l lp)) (defstrand ca-gen 2 (P P-0) (CA CA-0) (h (exp (gen) lp))) (defstrand ca-gen 2 (P B-0) (CA CA-0) (h (exp (gen) l-0))) (defstrand ltkgen 1 (P B-0) (l l-0)) (defstrand ca-gen 2 (P P) (CA CA) (h (exp (gen) l))) (precedes ((0 2) (1 3)) ((1 2) (0 3)) ((2 0) (5 0)) ((2 0) (7 0)) ((3 0) (0 1)) ((3 0) (4 0)) ((3 0) (5 0)) ((4 1) (1 0)) ((5 1) (1 1)) ((6 0) (5 0)) ((7 1) (0 0))) (fn-of ("principal-of" (P (exp (gen) l)) (B-0 (exp (gen) l-0)) (P-0 (exp (gen) lp))) (foo ((hash (exp (gen) (mul lp l-0)) (exp (gen) (mul ep l-0 l-1))) key))) (neq ((exp (gen) l) (gen)) ((exp (gen) l-0) (gen)) ((exp (gen) lp) (gen)) ((exp (gen) l-0) (exp (gen) lp)) ((exp (gen) (mul l-0 l-1)) (gen)) ((exp (gen) (mul (rec l) lp l-0)) (exp (gen) l)) ((exp (gen) (mul (rec e) ep l-0 l-1)) (gen))) (non-orig (privk CA) (privk B-0) (privk CA-0) (privk P) (privk P-0)) (uniq-gen e ep l lp) (operation encryption-test (added-strand ca-gen 2) (enc "cert" (exp (gen) l) P (privk CA)) (0 0)) (traces ((recv (enc "cert" (exp (gen) l) P (privk CA))) (recv (enc "cert" (exp (gen) (mul (rec l) lp l-0)) B (privk CA))) (send (exp (gen) e)) (recv (exp (gen) (mul (rec e) ep l-0 l-1))) (send key)) ((recv (enc "cert" (exp (gen) lp) P-0 (privk CA-0))) (recv (enc "cert" (exp (gen) l-0) B-0 (privk CA-0))) (send (exp (gen) ep)) (recv (exp (gen) (mul l-0 l-1))) (send key)) ((send (enc "cert-req" P (exp (gen) l) (privk P)))) ((send (enc "cert-req" P-0 (exp (gen) lp) (privk P-0)))) ((recv (enc "cert-req" P-0 (exp (gen) lp) (privk P-0))) (send (enc "cert" (exp (gen) lp) P-0 (privk CA-0)))) ((recv (enc "cert-req" B-0 (exp (gen) l-0) (privk B-0))) (send (enc "cert" (exp (gen) l-0) B-0 (privk CA-0)))) ((send (enc "cert-req" B-0 (exp (gen) l-0) (privk B-0)))) ((recv (enc "cert-req" P (exp (gen) l) (privk P))) (send (enc "cert" (exp (gen) l) P (privk CA))))) (label 19) (parent 15) (unrealized (0 1) (0 3)) (comment "1 in cohort - 1 not yet seen")) (defskeleton iadh-um (vars (key data) (B B-0 CA P name) (e ep lp l expn) (l-0 expr)) (defstrand init 5 (key key) (A P) (B B) (CA CA) (hl (exp (gen) l)) (he (exp (gen) (mul (rec e) ep l l-0))) (l lp) (e e)) (defstrand init 5 (key key) (A P) (B B-0) (CA CA) (hl (exp (gen) l)) (he (exp (gen) (mul l l-0))) (l lp) (e ep)) (defstrand ltkgen 1 (P P) (l lp)) (defstrand ca-gen 2 (P P) (CA CA) (h (exp (gen) lp))) (defstrand ca-gen 2 (P B-0) (CA CA) (h (exp (gen) l))) (defstrand ltkgen 1 (P B-0) (l l)) (precedes ((0 2) (1 3)) ((1 2) (0 3)) ((2 0) (3 0)) ((3 1) (0 0)) ((3 1) (1 0)) ((4 1) (1 1)) ((5 0) (4 0))) (fn-of ("principal-of" (P (exp (gen) lp)) (B-0 (exp (gen) l))) (foo ((hash (exp (gen) (mul lp l)) (exp (gen) (mul ep l l-0))) key))) (neq ((exp (gen) lp) (gen)) ((exp (gen) l) (gen)) ((exp (gen) l) (exp (gen) lp)) ((exp (gen) (mul l l-0)) (gen)) ((exp (gen) (mul (rec e) ep l l-0)) (gen))) (non-orig (privk B-0) (privk CA) (privk P)) (uniq-gen e ep lp) (operation encryption-test (displaced 6 3 ca-gen 2) (enc "cert" (exp (gen) lp) A (privk CA-0)) (0 0)) (traces ((recv (enc "cert" (exp (gen) lp) P (privk CA))) (recv (enc "cert" (exp (gen) l) B (privk CA))) (send (exp (gen) e)) (recv (exp (gen) (mul (rec e) ep l l-0))) (send key)) ((recv (enc "cert" (exp (gen) lp) P (privk CA))) (recv (enc "cert" (exp (gen) l) B-0 (privk CA))) (send (exp (gen) ep)) (recv (exp (gen) (mul l l-0))) (send key)) ((send (enc "cert-req" P (exp (gen) lp) (privk P)))) ((recv (enc "cert-req" P (exp (gen) lp) (privk P))) (send (enc "cert" (exp (gen) lp) P (privk CA)))) ((recv (enc "cert-req" B-0 (exp (gen) l) (privk B-0))) (send (enc "cert" (exp (gen) l) B-0 (privk CA)))) ((send (enc "cert-req" B-0 (exp (gen) l) (privk B-0))))) (label 20) (parent 16) (unrealized (0 1) (0 3)) (comment "2 in cohort - 2 not yet seen")) (defskeleton iadh-um (vars (key data) (B CA B-0 CA-0 P name) (e ep lp l expn) (l-0 expr)) (defstrand init 5 (key key) (A P) (B B) (CA CA) (hl (exp (gen) l)) (he (exp (gen) (mul (rec e) ep l l-0))) (l lp) (e e)) (defstrand init 5 (key key) (A P) (B B-0) (CA CA-0) (hl (exp (gen) l)) (he (exp (gen) (mul l l-0))) (l lp) (e ep)) (defstrand ltkgen 1 (P P) (l lp)) (defstrand ca-gen 2 (P P) (CA CA-0) (h (exp (gen) lp))) (defstrand ca-gen 2 (P B-0) (CA CA-0) (h (exp (gen) l))) (defstrand ltkgen 1 (P B-0) (l l)) (defstrand ca-gen 2 (P P) (CA CA) (h (exp (gen) lp))) (precedes ((0 2) (1 3)) ((1 2) (0 3)) ((2 0) (3 0)) ((2 0) (6 0)) ((3 1) (1 0)) ((4 1) (1 1)) ((5 0) (4 0)) ((6 1) (0 0))) (fn-of ("principal-of" (P (exp (gen) lp)) (B-0 (exp (gen) l))) (foo ((hash (exp (gen) (mul lp l)) (exp (gen) (mul ep l l-0))) key))) (neq ((exp (gen) lp) (gen)) ((exp (gen) l) (gen)) ((exp (gen) l) (exp (gen) lp)) ((exp (gen) (mul l l-0)) (gen)) ((exp (gen) (mul (rec e) ep l l-0)) (gen))) (non-orig (privk CA) (privk B-0) (privk CA-0) (privk P)) (uniq-gen e ep lp) (operation encryption-test (added-strand ca-gen 2) (enc "cert" (exp (gen) lp) P (privk CA)) (0 0)) (traces ((recv (enc "cert" (exp (gen) lp) P (privk CA))) (recv (enc "cert" (exp (gen) l) B (privk CA))) (send (exp (gen) e)) (recv (exp (gen) (mul (rec e) ep l l-0))) (send key)) ((recv (enc "cert" (exp (gen) lp) P (privk CA-0))) (recv (enc "cert" (exp (gen) l) B-0 (privk CA-0))) (send (exp (gen) ep)) (recv (exp (gen) (mul l l-0))) (send key)) ((send (enc "cert-req" P (exp (gen) lp) (privk P)))) ((recv (enc "cert-req" P (exp (gen) lp) (privk P))) (send (enc "cert" (exp (gen) lp) P (privk CA-0)))) ((recv (enc "cert-req" B-0 (exp (gen) l) (privk B-0))) (send (enc "cert" (exp (gen) l) B-0 (privk CA-0)))) ((send (enc "cert-req" B-0 (exp (gen) l) (privk B-0)))) ((recv (enc "cert-req" P (exp (gen) lp) (privk P))) (send (enc "cert" (exp (gen) lp) P (privk CA))))) (label 21) (parent 16) (unrealized (0 1) (0 3)) (comment "2 in cohort - 2 not yet seen")) (defskeleton iadh-um (vars (key data) (CA P P-0 name) (e ep lp l expn) (l-0 expr)) (defstrand init 5 (key key) (A P) (B P-0) (CA CA) (hl (exp (gen) lp)) (he (exp (gen) (mul (rec e) ep l l-0))) (l l) (e e)) (defstrand init 5 (key key) (A P-0) (B P) (CA CA) (hl (exp (gen) l)) (he (exp (gen) (mul l l-0))) (l lp) (e ep)) (defstrand ltkgen 1 (P P) (l l)) (defstrand ltkgen 1 (P P-0) (l lp)) (defstrand ca-gen 2 (P P-0) (CA CA) (h (exp (gen) lp))) (defstrand ca-gen 2 (P P) (CA CA) (h (exp (gen) l))) (precedes ((0 2) (1 3)) ((1 2) (0 3)) ((2 0) (5 0)) ((3 0) (4 0)) ((3 0) (5 0)) ((4 1) (0 1)) ((4 1) (1 0)) ((5 1) (0 0)) ((5 1) (1 1))) (fn-of ("principal-of" (P-0 (exp (gen) lp)) (P (exp (gen) l))) (foo ((hash (exp (gen) (mul lp l)) (exp (gen) (mul ep l l-0))) key))) (neq ((exp (gen) lp) (gen)) ((exp (gen) l) (gen)) ((exp (gen) l) (exp (gen) lp)) ((exp (gen) (mul l l-0)) (gen)) ((exp (gen) lp) (exp (gen) l)) ((exp (gen) (mul (rec e) ep l l-0)) (gen))) (non-orig (privk CA) (privk P) (privk P-0)) (uniq-gen e ep lp l) (operation encryption-test (displaced 6 4 ca-gen 2) (enc "cert" (exp (gen) lp) B (privk CA)) (0 1)) (traces ((recv (enc "cert" (exp (gen) l) P (privk CA))) (recv (enc "cert" (exp (gen) lp) P-0 (privk CA))) (send (exp (gen) e)) (recv (exp (gen) (mul (rec e) ep l l-0))) (send key)) ((recv (enc "cert" (exp (gen) lp) P-0 (privk CA))) (recv (enc "cert" (exp (gen) l) P (privk CA))) (send (exp (gen) ep)) (recv (exp (gen) (mul l l-0))) (send key)) ((send (enc "cert-req" P (exp (gen) l) (privk P)))) ((send (enc "cert-req" P-0 (exp (gen) lp) (privk P-0)))) ((recv (enc "cert-req" P-0 (exp (gen) lp) (privk P-0))) (send (enc "cert" (exp (gen) lp) P-0 (privk CA)))) ((recv (enc "cert-req" P (exp (gen) l) (privk P))) (send (enc "cert" (exp (gen) l) P (privk CA))))) (label 22) (parent 17) (unrealized (0 3)) (comment "1 in cohort - 1 not yet seen")) (defskeleton iadh-um (vars (key data) (CA P P-0 name) (e ep lp l expn) (l-0 expr)) (defstrand init 5 (key key) (A P) (B P-0) (CA CA) (hl (exp (gen) lp)) (he (exp (gen) (mul (rec e) ep l l-0))) (l l) (e e)) (defstrand init 5 (key key) (A P-0) (B P) (CA CA) (hl (exp (gen) l)) (he (exp (gen) (mul l l-0))) (l lp) (e ep)) (defstrand ltkgen 1 (P P) (l l)) (defstrand ltkgen 1 (P P-0) (l lp)) (defstrand ca-gen 2 (P P-0) (CA CA) (h (exp (gen) lp))) (defstrand ca-gen 2 (P P) (CA CA) (h (exp (gen) l))) (defstrand ca-gen 2 (P P-0) (CA CA) (h (exp (gen) lp))) (precedes ((0 2) (1 3)) ((1 2) (0 3)) ((2 0) (5 0)) ((3 0) (4 0)) ((3 0) (5 0)) ((3 0) (6 0)) ((4 1) (1 0)) ((5 1) (0 0)) ((5 1) (1 1)) ((6 1) (0 1))) (fn-of ("principal-of" (P-0 (exp (gen) lp)) (P (exp (gen) l))) (foo ((hash (exp (gen) (mul lp l)) (exp (gen) (mul ep l l-0))) key))) (neq ((exp (gen) lp) (gen)) ((exp (gen) l) (gen)) ((exp (gen) l) (exp (gen) lp)) ((exp (gen) (mul l l-0)) (gen)) ((exp (gen) lp) (exp (gen) l)) ((exp (gen) (mul (rec e) ep l l-0)) (gen))) (non-orig (privk CA) (privk P) (privk P-0)) (uniq-gen e ep lp l) (operation encryption-test (added-strand ca-gen 2) (enc "cert" (exp (gen) lp) P-0 (privk CA)) (0 1)) (traces ((recv (enc "cert" (exp (gen) l) P (privk CA))) (recv (enc "cert" (exp (gen) lp) P-0 (privk CA))) (send (exp (gen) e)) (recv (exp (gen) (mul (rec e) ep l l-0))) (send key)) ((recv (enc "cert" (exp (gen) lp) P-0 (privk CA))) (recv (enc "cert" (exp (gen) l) P (privk CA))) (send (exp (gen) ep)) (recv (exp (gen) (mul l l-0))) (send key)) ((send (enc "cert-req" P (exp (gen) l) (privk P)))) ((send (enc "cert-req" P-0 (exp (gen) lp) (privk P-0)))) ((recv (enc "cert-req" P-0 (exp (gen) lp) (privk P-0))) (send (enc "cert" (exp (gen) lp) P-0 (privk CA)))) ((recv (enc "cert-req" P (exp (gen) l) (privk P))) (send (enc "cert" (exp (gen) l) P (privk CA)))) ((recv (enc "cert-req" P-0 (exp (gen) lp) (privk P-0))) (send (enc "cert" (exp (gen) lp) P-0 (privk CA))))) (label 23) (parent 17) (unrealized (0 3)) (comment "1 in cohort - 1 not yet seen")) (defskeleton iadh-um (vars (key data) (CA P P-0 name) (e ep lp l expn) (l-0 expr)) (defstrand init 5 (key key) (A P) (B P-0) (CA CA) (hl (exp (gen) lp)) (he (exp (gen) (mul (rec e) ep l l-0))) (l l) (e e)) (defstrand init 5 (key key) (A P-0) (B P) (CA CA) (hl (exp (gen) l)) (he (exp (gen) (mul l l-0))) (l lp) (e ep)) (defstrand ltkgen 1 (P P) (l l)) (defstrand ltkgen 1 (P P-0) (l lp)) (defstrand ca-gen 2 (P P-0) (CA CA) (h (exp (gen) lp))) (defstrand ca-gen 2 (P P) (CA CA) (h (exp (gen) l))) (defstrand ca-gen 2 (P P) (CA CA) (h (exp (gen) l))) (precedes ((0 2) (1 3)) ((1 2) (0 3)) ((2 0) (5 0)) ((2 0) (6 0)) ((3 0) (4 0)) ((3 0) (5 0)) ((4 1) (0 1)) ((4 1) (1 0)) ((5 1) (1 1)) ((6 1) (0 0))) (fn-of ("principal-of" (P-0 (exp (gen) lp)) (P (exp (gen) l))) (foo ((hash (exp (gen) (mul lp l)) (exp (gen) (mul ep l l-0))) key))) (neq ((exp (gen) lp) (gen)) ((exp (gen) l) (gen)) ((exp (gen) l) (exp (gen) lp)) ((exp (gen) (mul l l-0)) (gen)) ((exp (gen) lp) (exp (gen) l)) ((exp (gen) (mul (rec e) ep l l-0)) (gen))) (non-orig (privk CA) (privk P) (privk P-0)) (uniq-gen e ep lp l) (operation encryption-test (displaced 7 4 ca-gen 2) (enc "cert" (exp (gen) lp) B (privk CA-0)) (0 1)) (traces ((recv (enc "cert" (exp (gen) l) P (privk CA))) (recv (enc "cert" (exp (gen) lp) P-0 (privk CA))) (send (exp (gen) e)) (recv (exp (gen) (mul (rec e) ep l l-0))) (send key)) ((recv (enc "cert" (exp (gen) lp) P-0 (privk CA))) (recv (enc "cert" (exp (gen) l) P (privk CA))) (send (exp (gen) ep)) (recv (exp (gen) (mul l l-0))) (send key)) ((send (enc "cert-req" P (exp (gen) l) (privk P)))) ((send (enc "cert-req" P-0 (exp (gen) lp) (privk P-0)))) ((recv (enc "cert-req" P-0 (exp (gen) lp) (privk P-0))) (send (enc "cert" (exp (gen) lp) P-0 (privk CA)))) ((recv (enc "cert-req" P (exp (gen) l) (privk P))) (send (enc "cert" (exp (gen) l) P (privk CA)))) ((recv (enc "cert-req" P (exp (gen) l) (privk P))) (send (enc "cert" (exp (gen) l) P (privk CA))))) (label 24) (parent 18) (unrealized (0 3)) (comment "1 in cohort - 1 not yet seen")) (defskeleton iadh-um (vars (key data) (CA CA-0 P P-0 name) (e ep lp l expn) (l-0 expr)) (defstrand init 5 (key key) (A P) (B P-0) (CA CA) (hl (exp (gen) lp)) (he (exp (gen) (mul (rec e) ep l l-0))) (l l) (e e)) (defstrand init 5 (key key) (A P-0) (B P) (CA CA-0) (hl (exp (gen) l)) (he (exp (gen) (mul l l-0))) (l lp) (e ep)) (defstrand ltkgen 1 (P P) (l l)) (defstrand ltkgen 1 (P P-0) (l lp)) (defstrand ca-gen 2 (P P-0) (CA CA-0) (h (exp (gen) lp))) (defstrand ca-gen 2 (P P) (CA CA-0) (h (exp (gen) l))) (defstrand ca-gen 2 (P P) (CA CA) (h (exp (gen) l))) (defstrand ca-gen 2 (P P-0) (CA CA) (h (exp (gen) lp))) (precedes ((0 2) (1 3)) ((1 2) (0 3)) ((2 0) (5 0)) ((2 0) (6 0)) ((3 0) (4 0)) ((3 0) (5 0)) ((3 0) (7 0)) ((4 1) (1 0)) ((5 1) (1 1)) ((6 1) (0 0)) ((7 1) (0 1))) (fn-of ("principal-of" (P-0 (exp (gen) lp)) (P (exp (gen) l))) (foo ((hash (exp (gen) (mul lp l)) (exp (gen) (mul ep l l-0))) key))) (neq ((exp (gen) lp) (gen)) ((exp (gen) l) (gen)) ((exp (gen) l) (exp (gen) lp)) ((exp (gen) (mul l l-0)) (gen)) ((exp (gen) lp) (exp (gen) l)) ((exp (gen) (mul (rec e) ep l l-0)) (gen))) (non-orig (privk CA) (privk CA-0) (privk P) (privk P-0)) (uniq-gen e ep lp l) (operation encryption-test (added-strand ca-gen 2) (enc "cert" (exp (gen) lp) P-0 (privk CA)) (0 1)) (traces ((recv (enc "cert" (exp (gen) l) P (privk CA))) (recv (enc "cert" (exp (gen) lp) P-0 (privk CA))) (send (exp (gen) e)) (recv (exp (gen) (mul (rec e) ep l l-0))) (send key)) ((recv (enc "cert" (exp (gen) lp) P-0 (privk CA-0))) (recv (enc "cert" (exp (gen) l) P (privk CA-0))) (send (exp (gen) ep)) (recv (exp (gen) (mul l l-0))) (send key)) ((send (enc "cert-req" P (exp (gen) l) (privk P)))) ((send (enc "cert-req" P-0 (exp (gen) lp) (privk P-0)))) ((recv (enc "cert-req" P-0 (exp (gen) lp) (privk P-0))) (send (enc "cert" (exp (gen) lp) P-0 (privk CA-0)))) ((recv (enc "cert-req" P (exp (gen) l) (privk P))) (send (enc "cert" (exp (gen) l) P (privk CA-0)))) ((recv (enc "cert-req" P (exp (gen) l) (privk P))) (send (enc "cert" (exp (gen) l) P (privk CA)))) ((recv (enc "cert-req" P-0 (exp (gen) lp) (privk P-0))) (send (enc "cert" (exp (gen) lp) P-0 (privk CA))))) (label 25) (parent 18) (unrealized (0 3)) (comment "1 in cohort - 1 not yet seen")) (defskeleton iadh-um (vars (key data) (B CA B-0 CA-0 P P-0 name) (e ep l lp l-0 expn) (l-1 expr)) (defstrand init 5 (key key) (A P) (B B) (CA CA) (hl (exp (gen) (mul (rec l) lp l-0))) (he (exp (gen) (mul (rec e) ep l-0 l-1))) (l l) (e e)) (defstrand init 5 (key key) (A P-0) (B B-0) (CA CA-0) (hl (exp (gen) l-0)) (he (exp (gen) (mul l-0 l-1))) (l lp) (e ep)) (defstrand ltkgen 1 (P P) (l l)) (defstrand ltkgen 1 (P P-0) (l lp)) (defstrand ca-gen 2 (P P-0) (CA CA-0) (h (exp (gen) lp))) (defstrand ca-gen 2 (P B-0) (CA CA-0) (h (exp (gen) l-0))) (defstrand ltkgen 1 (P B-0) (l l-0)) (defstrand ca-gen 2 (P P) (CA CA) (h (exp (gen) l))) (defstrand ca-gen 2 (P B) (CA CA) (h (exp (gen) (mul (rec l) lp l-0)))) (precedes ((0 2) (1 3)) ((1 2) (0 3)) ((2 0) (5 0)) ((2 0) (7 0)) ((2 0) (8 0)) ((3 0) (4 0)) ((3 0) (5 0)) ((3 0) (8 0)) ((4 1) (1 0)) ((5 1) (1 1)) ((6 0) (5 0)) ((7 1) (0 0)) ((8 1) (0 1))) (fn-of ("principal-of" (B (exp (gen) (mul (rec l) lp l-0))) (P (exp (gen) l)) (B-0 (exp (gen) l-0)) (P-0 (exp (gen) lp))) (foo ((hash (exp (gen) (mul lp l-0)) (exp (gen) (mul ep l-0 l-1))) key))) (neq ((exp (gen) (mul (rec l) lp l-0)) (gen)) ((exp (gen) l) (gen)) ((exp (gen) l-0) (gen)) ((exp (gen) lp) (gen)) ((exp (gen) l-0) (exp (gen) lp)) ((exp (gen) (mul l-0 l-1)) (gen)) ((exp (gen) (mul (rec l) lp l-0)) (exp (gen) l)) ((exp (gen) (mul (rec e) ep l-0 l-1)) (gen))) (non-orig (privk B) (privk CA) (privk B-0) (privk CA-0) (privk P) (privk P-0)) (uniq-gen e ep l lp) (operation encryption-test (added-strand ca-gen 2) (enc "cert" (exp (gen) (mul (rec l) lp l-0)) B (privk CA)) (0 1)) (traces ((recv (enc "cert" (exp (gen) l) P (privk CA))) (recv (enc "cert" (exp (gen) (mul (rec l) lp l-0)) B (privk CA))) (send (exp (gen) e)) (recv (exp (gen) (mul (rec e) ep l-0 l-1))) (send key)) ((recv (enc "cert" (exp (gen) lp) P-0 (privk CA-0))) (recv (enc "cert" (exp (gen) l-0) B-0 (privk CA-0))) (send (exp (gen) ep)) (recv (exp (gen) (mul l-0 l-1))) (send key)) ((send (enc "cert-req" P (exp (gen) l) (privk P)))) ((send (enc "cert-req" P-0 (exp (gen) lp) (privk P-0)))) ((recv (enc "cert-req" P-0 (exp (gen) lp) (privk P-0))) (send (enc "cert" (exp (gen) lp) P-0 (privk CA-0)))) ((recv (enc "cert-req" B-0 (exp (gen) l-0) (privk B-0))) (send (enc "cert" (exp (gen) l-0) B-0 (privk CA-0)))) ((send (enc "cert-req" B-0 (exp (gen) l-0) (privk B-0)))) ((recv (enc "cert-req" P (exp (gen) l) (privk P))) (send (enc "cert" (exp (gen) l) P (privk CA)))) ((recv (enc "cert-req" B (exp (gen) (mul (rec l) lp l-0)) (privk B))) (send (enc "cert" (exp (gen) (mul (rec l) lp l-0)) B (privk CA))))) (label 26) (parent 19) (unrealized (0 3) (8 0)) (comment "empty cohort")) (defskeleton iadh-um (vars (key data) (B CA P name) (e ep lp l expn) (l-0 expr)) (defstrand init 5 (key key) (A P) (B B) (CA CA) (hl (exp (gen) l)) (he (exp (gen) (mul (rec e) ep l l-0))) (l lp) (e e)) (defstrand init 5 (key key) (A P) (B B) (CA CA) (hl (exp (gen) l)) (he (exp (gen) (mul l l-0))) (l lp) (e ep)) (defstrand ltkgen 1 (P P) (l lp)) (defstrand ca-gen 2 (P P) (CA CA) (h (exp (gen) lp))) (defstrand ca-gen 2 (P B) (CA CA) (h (exp (gen) l))) (defstrand ltkgen 1 (P B) (l l)) (precedes ((0 2) (1 3)) ((1 2) (0 3)) ((2 0) (3 0)) ((3 1) (0 0)) ((3 1) (1 0)) ((4 1) (0 1)) ((4 1) (1 1)) ((5 0) (4 0))) (fn-of ("principal-of" (B (exp (gen) l)) (P (exp (gen) lp))) (foo ((hash (exp (gen) (mul lp l)) (exp (gen) (mul ep l l-0))) key))) (neq ((exp (gen) l) (gen)) ((exp (gen) lp) (gen)) ((exp (gen) l) (exp (gen) lp)) ((exp (gen) (mul l l-0)) (gen)) ((exp (gen) (mul (rec e) ep l l-0)) (gen))) (non-orig (privk B) (privk CA) (privk P)) (uniq-gen e ep lp) (operation encryption-test (displaced 6 4 ca-gen 2) (enc "cert" (exp (gen) l) B-0 (privk CA)) (0 1)) (traces ((recv (enc "cert" (exp (gen) lp) P (privk CA))) (recv (enc "cert" (exp (gen) l) B (privk CA))) (send (exp (gen) e)) (recv (exp (gen) (mul (rec e) ep l l-0))) (send key)) ((recv (enc "cert" (exp (gen) lp) P (privk CA))) (recv (enc "cert" (exp (gen) l) B (privk CA))) (send (exp (gen) ep)) (recv (exp (gen) (mul l l-0))) (send key)) ((send (enc "cert-req" P (exp (gen) lp) (privk P)))) ((recv (enc "cert-req" P (exp (gen) lp) (privk P))) (send (enc "cert" (exp (gen) lp) P (privk CA)))) ((recv (enc "cert-req" B (exp (gen) l) (privk B))) (send (enc "cert" (exp (gen) l) B (privk CA)))) ((send (enc "cert-req" B (exp (gen) l) (privk B))))) (label 27) (parent 20) (seen 27) (unrealized (0 3)) (comment "1 in cohort - 0 not yet seen")) (defskeleton iadh-um (vars (key data) (B CA P name) (e ep lp l expn) (l-0 expr)) (defstrand init 5 (key key) (A P) (B B) (CA CA) (hl (exp (gen) l)) (he (exp (gen) (mul (rec e) ep l l-0))) (l lp) (e e)) (defstrand init 5 (key key) (A P) (B B) (CA CA) (hl (exp (gen) l)) (he (exp (gen) (mul l l-0))) (l lp) (e ep)) (defstrand ltkgen 1 (P P) (l lp)) (defstrand ca-gen 2 (P P) (CA CA) (h (exp (gen) lp))) (defstrand ca-gen 2 (P B) (CA CA) (h (exp (gen) l))) (defstrand ltkgen 1 (P B) (l l)) (defstrand ca-gen 2 (P B) (CA CA) (h (exp (gen) l))) (precedes ((0 2) (1 3)) ((1 2) (0 3)) ((2 0) (3 0)) ((3 1) (0 0)) ((3 1) (1 0)) ((4 1) (1 1)) ((5 0) (4 0)) ((6 1) (0 1))) (fn-of ("principal-of" (B (exp (gen) l)) (P (exp (gen) lp))) (foo ((hash (exp (gen) (mul lp l)) (exp (gen) (mul ep l l-0))) key))) (neq ((exp (gen) l) (gen)) ((exp (gen) lp) (gen)) ((exp (gen) l) (exp (gen) lp)) ((exp (gen) (mul l l-0)) (gen)) ((exp (gen) (mul (rec e) ep l l-0)) (gen))) (non-orig (privk B) (privk CA) (privk P)) (uniq-gen e ep lp) (operation encryption-test (added-strand ca-gen 2) (enc "cert" (exp (gen) l) B (privk CA)) (0 1)) (traces ((recv (enc "cert" (exp (gen) lp) P (privk CA))) (recv (enc "cert" (exp (gen) l) B (privk CA))) (send (exp (gen) e)) (recv (exp (gen) (mul (rec e) ep l l-0))) (send key)) ((recv (enc "cert" (exp (gen) lp) P (privk CA))) (recv (enc "cert" (exp (gen) l) B (privk CA))) (send (exp (gen) ep)) (recv (exp (gen) (mul l l-0))) (send key)) ((send (enc "cert-req" P (exp (gen) lp) (privk P)))) ((recv (enc "cert-req" P (exp (gen) lp) (privk P))) (send (enc "cert" (exp (gen) lp) P (privk CA)))) ((recv (enc "cert-req" B (exp (gen) l) (privk B))) (send (enc "cert" (exp (gen) l) B (privk CA)))) ((send (enc "cert-req" B (exp (gen) l) (privk B)))) ((recv (enc "cert-req" B (exp (gen) l) (privk B))) (send (enc "cert" (exp (gen) l) B (privk CA))))) (label 28) (parent 20) (unrealized (0 3) (6 0)) (comment "2 in cohort - 2 not yet seen")) (defskeleton iadh-um (vars (key data) (B CA P name) (e ep lp l expn) (l-0 expr)) (defstrand init 5 (key key) (A P) (B B) (CA CA) (hl (exp (gen) l)) (he (exp (gen) (mul (rec e) ep l l-0))) (l lp) (e e)) (defstrand init 5 (key key) (A P) (B B) (CA CA) (hl (exp (gen) l)) (he (exp (gen) (mul l l-0))) (l lp) (e ep)) (defstrand ltkgen 1 (P P) (l lp)) (defstrand ca-gen 2 (P P) (CA CA) (h (exp (gen) lp))) (defstrand ca-gen 2 (P B) (CA CA) (h (exp (gen) l))) (defstrand ltkgen 1 (P B) (l l)) (defstrand ca-gen 2 (P P) (CA CA) (h (exp (gen) lp))) (precedes ((0 2) (1 3)) ((1 2) (0 3)) ((2 0) (3 0)) ((2 0) (6 0)) ((3 1) (1 0)) ((4 1) (0 1)) ((4 1) (1 1)) ((5 0) (4 0)) ((6 1) (0 0))) (fn-of ("principal-of" (B (exp (gen) l)) (P (exp (gen) lp))) (foo ((hash (exp (gen) (mul lp l)) (exp (gen) (mul ep l l-0))) key))) (neq ((exp (gen) l) (gen)) ((exp (gen) lp) (gen)) ((exp (gen) l) (exp (gen) lp)) ((exp (gen) (mul l l-0)) (gen)) ((exp (gen) (mul (rec e) ep l l-0)) (gen))) (non-orig (privk B) (privk CA) (privk P)) (uniq-gen e ep lp) (operation encryption-test (displaced 7 4 ca-gen 2) (enc "cert" (exp (gen) l) B-0 (privk CA-0)) (0 1)) (traces ((recv (enc "cert" (exp (gen) lp) P (privk CA))) (recv (enc "cert" (exp (gen) l) B (privk CA))) (send (exp (gen) e)) (recv (exp (gen) (mul (rec e) ep l l-0))) (send key)) ((recv (enc "cert" (exp (gen) lp) P (privk CA))) (recv (enc "cert" (exp (gen) l) B (privk CA))) (send (exp (gen) ep)) (recv (exp (gen) (mul l l-0))) (send key)) ((send (enc "cert-req" P (exp (gen) lp) (privk P)))) ((recv (enc "cert-req" P (exp (gen) lp) (privk P))) (send (enc "cert" (exp (gen) lp) P (privk CA)))) ((recv (enc "cert-req" B (exp (gen) l) (privk B))) (send (enc "cert" (exp (gen) l) B (privk CA)))) ((send (enc "cert-req" B (exp (gen) l) (privk B)))) ((recv (enc "cert-req" P (exp (gen) lp) (privk P))) (send (enc "cert" (exp (gen) lp) P (privk CA))))) (label 29) (parent 21) (unrealized (0 3)) (comment "1 in cohort - 1 not yet seen")) (defskeleton iadh-um (vars (key data) (CA B CA-0 P name) (e ep lp l expn) (l-0 expr)) (defstrand init 5 (key key) (A P) (B B) (CA CA) (hl (exp (gen) l)) (he (exp (gen) (mul (rec e) ep l l-0))) (l lp) (e e)) (defstrand init 5 (key key) (A P) (B B) (CA CA-0) (hl (exp (gen) l)) (he (exp (gen) (mul l l-0))) (l lp) (e ep)) (defstrand ltkgen 1 (P P) (l lp)) (defstrand ca-gen 2 (P P) (CA CA-0) (h (exp (gen) lp))) (defstrand ca-gen 2 (P B) (CA CA-0) (h (exp (gen) l))) (defstrand ltkgen 1 (P B) (l l)) (defstrand ca-gen 2 (P P) (CA CA) (h (exp (gen) lp))) (defstrand ca-gen 2 (P B) (CA CA) (h (exp (gen) l))) (precedes ((0 2) (1 3)) ((1 2) (0 3)) ((2 0) (3 0)) ((2 0) (6 0)) ((3 1) (1 0)) ((4 1) (1 1)) ((5 0) (4 0)) ((6 1) (0 0)) ((7 1) (0 1))) (fn-of ("principal-of" (B (exp (gen) l)) (P (exp (gen) lp))) (foo ((hash (exp (gen) (mul lp l)) (exp (gen) (mul ep l l-0))) key))) (neq ((exp (gen) l) (gen)) ((exp (gen) lp) (gen)) ((exp (gen) l) (exp (gen) lp)) ((exp (gen) (mul l l-0)) (gen)) ((exp (gen) (mul (rec e) ep l l-0)) (gen))) (non-orig (privk CA) (privk B) (privk CA-0) (privk P)) (uniq-gen e ep lp) (operation encryption-test (added-strand ca-gen 2) (enc "cert" (exp (gen) l) B (privk CA)) (0 1)) (traces ((recv (enc "cert" (exp (gen) lp) P (privk CA))) (recv (enc "cert" (exp (gen) l) B (privk CA))) (send (exp (gen) e)) (recv (exp (gen) (mul (rec e) ep l l-0))) (send key)) ((recv (enc "cert" (exp (gen) lp) P (privk CA-0))) (recv (enc "cert" (exp (gen) l) B (privk CA-0))) (send (exp (gen) ep)) (recv (exp (gen) (mul l l-0))) (send key)) ((send (enc "cert-req" P (exp (gen) lp) (privk P)))) ((recv (enc "cert-req" P (exp (gen) lp) (privk P))) (send (enc "cert" (exp (gen) lp) P (privk CA-0)))) ((recv (enc "cert-req" B (exp (gen) l) (privk B))) (send (enc "cert" (exp (gen) l) B (privk CA-0)))) ((send (enc "cert-req" B (exp (gen) l) (privk B)))) ((recv (enc "cert-req" P (exp (gen) lp) (privk P))) (send (enc "cert" (exp (gen) lp) P (privk CA)))) ((recv (enc "cert-req" B (exp (gen) l) (privk B))) (send (enc "cert" (exp (gen) l) B (privk CA))))) (label 30) (parent 21) (unrealized (0 3) (7 0)) (comment "2 in cohort - 2 not yet seen")) (defskeleton iadh-um (vars (key data) (CA P P-0 name) (lp l e ep expn) (l-0 expr)) (defstrand init 5 (key key) (A P) (B P-0) (CA CA) (hl (exp (gen) lp)) (he (exp (gen) (mul l l-0))) (l l) (e e)) (defstrand init 5 (key key) (A P-0) (B P) (CA CA) (hl (exp (gen) l)) (he (exp (gen) (mul l e (rec ep) l-0))) (l lp) (e ep)) (defstrand ltkgen 1 (P P) (l l)) (defstrand ltkgen 1 (P P-0) (l lp)) (defstrand ca-gen 2 (P P-0) (CA CA) (h (exp (gen) lp))) (defstrand ca-gen 2 (P P) (CA CA) (h (exp (gen) l))) (precedes ((0 2) (1 3)) ((1 2) (0 3)) ((2 0) (5 0)) ((3 0) (4 0)) ((3 0) (5 0)) ((4 1) (0 1)) ((4 1) (1 0)) ((5 1) (0 0)) ((5 1) (1 1))) (fn-of ("principal-of" (P-0 (exp (gen) lp)) (P (exp (gen) l))) (foo ((hash (exp (gen) (mul lp l)) (exp (gen) (mul l e l-0))) key))) (neq ((exp (gen) lp) (gen)) ((exp (gen) l) (gen)) ((exp (gen) l) (exp (gen) lp)) ((exp (gen) (mul l e (rec ep) l-0)) (gen)) ((exp (gen) lp) (exp (gen) l)) ((exp (gen) (mul l l-0)) (gen))) (non-orig (privk CA) (privk P) (privk P-0)) (uniq-gen lp l e ep) (operation nonce-test (algebra-contracted (e-0 e) (ep-0 ep) (l-1 (mul e (rec ep) l-0)) (l-2 l-0)) (exp (gen) (mul l l-0)) (0 3)) (traces ((recv (enc "cert" (exp (gen) l) P (privk CA))) (recv (enc "cert" (exp (gen) lp) P-0 (privk CA))) (send (exp (gen) e)) (recv (exp (gen) (mul l l-0))) (send key)) ((recv (enc "cert" (exp (gen) lp) P-0 (privk CA))) (recv (enc "cert" (exp (gen) l) P (privk CA))) (send (exp (gen) ep)) (recv (exp (gen) (mul l e (rec ep) l-0))) (send key)) ((send (enc "cert-req" P (exp (gen) l) (privk P)))) ((send (enc "cert-req" P-0 (exp (gen) lp) (privk P-0)))) ((recv (enc "cert-req" P-0 (exp (gen) lp) (privk P-0))) (send (enc "cert" (exp (gen) lp) P-0 (privk CA)))) ((recv (enc "cert-req" P (exp (gen) l) (privk P))) (send (enc "cert" (exp (gen) l) P (privk CA))))) (label 31) (parent 22) (unrealized (1 3)) (comment "1 in cohort - 1 not yet seen")) (defskeleton iadh-um (vars (key data) (CA P P-0 name) (lp l e ep expn) (l-0 expr)) (defstrand init 5 (key key) (A P) (B P-0) (CA CA) (hl (exp (gen) lp)) (he (exp (gen) (mul l l-0))) (l l) (e e)) (defstrand init 5 (key key) (A P-0) (B P) (CA CA) (hl (exp (gen) l)) (he (exp (gen) (mul l e (rec ep) l-0))) (l lp) (e ep)) (defstrand ltkgen 1 (P P) (l l)) (defstrand ltkgen 1 (P P-0) (l lp)) (defstrand ca-gen 2 (P P-0) (CA CA) (h (exp (gen) lp))) (defstrand ca-gen 2 (P P) (CA CA) (h (exp (gen) l))) (defstrand ca-gen 2 (P P-0) (CA CA) (h (exp (gen) lp))) (precedes ((0 2) (1 3)) ((1 2) (0 3)) ((2 0) (5 0)) ((3 0) (4 0)) ((3 0) (5 0)) ((3 0) (6 0)) ((4 1) (1 0)) ((5 1) (0 0)) ((5 1) (1 1)) ((6 1) (0 1))) (fn-of ("principal-of" (P-0 (exp (gen) lp)) (P (exp (gen) l))) (foo ((hash (exp (gen) (mul lp l)) (exp (gen) (mul l e l-0))) key))) (neq ((exp (gen) lp) (gen)) ((exp (gen) l) (gen)) ((exp (gen) l) (exp (gen) lp)) ((exp (gen) (mul l e (rec ep) l-0)) (gen)) ((exp (gen) lp) (exp (gen) l)) ((exp (gen) (mul l l-0)) (gen))) (non-orig (privk CA) (privk P) (privk P-0)) (uniq-gen lp l e ep) (operation nonce-test (algebra-contracted (e-0 e) (ep-0 ep) (l-1 (mul e (rec ep) l-0)) (l-2 l-0)) (exp (gen) (mul l l-0)) (0 3)) (traces ((recv (enc "cert" (exp (gen) l) P (privk CA))) (recv (enc "cert" (exp (gen) lp) P-0 (privk CA))) (send (exp (gen) e)) (recv (exp (gen) (mul l l-0))) (send key)) ((recv (enc "cert" (exp (gen) lp) P-0 (privk CA))) (recv (enc "cert" (exp (gen) l) P (privk CA))) (send (exp (gen) ep)) (recv (exp (gen) (mul l e (rec ep) l-0))) (send key)) ((send (enc "cert-req" P (exp (gen) l) (privk P)))) ((send (enc "cert-req" P-0 (exp (gen) lp) (privk P-0)))) ((recv (enc "cert-req" P-0 (exp (gen) lp) (privk P-0))) (send (enc "cert" (exp (gen) lp) P-0 (privk CA)))) ((recv (enc "cert-req" P (exp (gen) l) (privk P))) (send (enc "cert" (exp (gen) l) P (privk CA)))) ((recv (enc "cert-req" P-0 (exp (gen) lp) (privk P-0))) (send (enc "cert" (exp (gen) lp) P-0 (privk CA))))) (label 32) (parent 23) (unrealized (1 3)) (comment "1 in cohort - 1 not yet seen")) (defskeleton iadh-um (vars (key data) (CA P P-0 name) (lp l e ep expn) (l-0 expr)) (defstrand init 5 (key key) (A P) (B P-0) (CA CA) (hl (exp (gen) lp)) (he (exp (gen) (mul l l-0))) (l l) (e e)) (defstrand init 5 (key key) (A P-0) (B P) (CA CA) (hl (exp (gen) l)) (he (exp (gen) (mul l e (rec ep) l-0))) (l lp) (e ep)) (defstrand ltkgen 1 (P P) (l l)) (defstrand ltkgen 1 (P P-0) (l lp)) (defstrand ca-gen 2 (P P-0) (CA CA) (h (exp (gen) lp))) (defstrand ca-gen 2 (P P) (CA CA) (h (exp (gen) l))) (defstrand ca-gen 2 (P P) (CA CA) (h (exp (gen) l))) (precedes ((0 2) (1 3)) ((1 2) (0 3)) ((2 0) (5 0)) ((2 0) (6 0)) ((3 0) (4 0)) ((3 0) (5 0)) ((4 1) (0 1)) ((4 1) (1 0)) ((5 1) (1 1)) ((6 1) (0 0))) (fn-of ("principal-of" (P-0 (exp (gen) lp)) (P (exp (gen) l))) (foo ((hash (exp (gen) (mul lp l)) (exp (gen) (mul l e l-0))) key))) (neq ((exp (gen) lp) (gen)) ((exp (gen) l) (gen)) ((exp (gen) l) (exp (gen) lp)) ((exp (gen) (mul l e (rec ep) l-0)) (gen)) ((exp (gen) lp) (exp (gen) l)) ((exp (gen) (mul l l-0)) (gen))) (non-orig (privk CA) (privk P) (privk P-0)) (uniq-gen lp l e ep) (operation nonce-test (algebra-contracted (e-0 e) (ep-0 ep) (l-1 (mul e (rec ep) l-0)) (l-2 l-0)) (exp (gen) (mul l l-0)) (0 3)) (traces ((recv (enc "cert" (exp (gen) l) P (privk CA))) (recv (enc "cert" (exp (gen) lp) P-0 (privk CA))) (send (exp (gen) e)) (recv (exp (gen) (mul l l-0))) (send key)) ((recv (enc "cert" (exp (gen) lp) P-0 (privk CA))) (recv (enc "cert" (exp (gen) l) P (privk CA))) (send (exp (gen) ep)) (recv (exp (gen) (mul l e (rec ep) l-0))) (send key)) ((send (enc "cert-req" P (exp (gen) l) (privk P)))) ((send (enc "cert-req" P-0 (exp (gen) lp) (privk P-0)))) ((recv (enc "cert-req" P-0 (exp (gen) lp) (privk P-0))) (send (enc "cert" (exp (gen) lp) P-0 (privk CA)))) ((recv (enc "cert-req" P (exp (gen) l) (privk P))) (send (enc "cert" (exp (gen) l) P (privk CA)))) ((recv (enc "cert-req" P (exp (gen) l) (privk P))) (send (enc "cert" (exp (gen) l) P (privk CA))))) (label 33) (parent 24) (unrealized (1 3)) (comment "1 in cohort - 1 not yet seen")) (defskeleton iadh-um (vars (key data) (CA CA-0 P P-0 name) (lp l e ep expn) (l-0 expr)) (defstrand init 5 (key key) (A P) (B P-0) (CA CA) (hl (exp (gen) lp)) (he (exp (gen) (mul l l-0))) (l l) (e e)) (defstrand init 5 (key key) (A P-0) (B P) (CA CA-0) (hl (exp (gen) l)) (he (exp (gen) (mul l e (rec ep) l-0))) (l lp) (e ep)) (defstrand ltkgen 1 (P P) (l l)) (defstrand ltkgen 1 (P P-0) (l lp)) (defstrand ca-gen 2 (P P-0) (CA CA-0) (h (exp (gen) lp))) (defstrand ca-gen 2 (P P) (CA CA-0) (h (exp (gen) l))) (defstrand ca-gen 2 (P P) (CA CA) (h (exp (gen) l))) (defstrand ca-gen 2 (P P-0) (CA CA) (h (exp (gen) lp))) (precedes ((0 2) (1 3)) ((1 2) (0 3)) ((2 0) (5 0)) ((2 0) (6 0)) ((3 0) (4 0)) ((3 0) (5 0)) ((3 0) (7 0)) ((4 1) (1 0)) ((5 1) (1 1)) ((6 1) (0 0)) ((7 1) (0 1))) (fn-of ("principal-of" (P-0 (exp (gen) lp)) (P (exp (gen) l))) (foo ((hash (exp (gen) (mul lp l)) (exp (gen) (mul l e l-0))) key))) (neq ((exp (gen) lp) (gen)) ((exp (gen) l) (gen)) ((exp (gen) l) (exp (gen) lp)) ((exp (gen) (mul l e (rec ep) l-0)) (gen)) ((exp (gen) lp) (exp (gen) l)) ((exp (gen) (mul l l-0)) (gen))) (non-orig (privk CA) (privk CA-0) (privk P) (privk P-0)) (uniq-gen lp l e ep) (operation nonce-test (algebra-contracted (e-0 e) (ep-0 ep) (l-1 (mul e (rec ep) l-0)) (l-2 l-0)) (exp (gen) (mul l l-0)) (0 3)) (traces ((recv (enc "cert" (exp (gen) l) P (privk CA))) (recv (enc "cert" (exp (gen) lp) P-0 (privk CA))) (send (exp (gen) e)) (recv (exp (gen) (mul l l-0))) (send key)) ((recv (enc "cert" (exp (gen) lp) P-0 (privk CA-0))) (recv (enc "cert" (exp (gen) l) P (privk CA-0))) (send (exp (gen) ep)) (recv (exp (gen) (mul l e (rec ep) l-0))) (send key)) ((send (enc "cert-req" P (exp (gen) l) (privk P)))) ((send (enc "cert-req" P-0 (exp (gen) lp) (privk P-0)))) ((recv (enc "cert-req" P-0 (exp (gen) lp) (privk P-0))) (send (enc "cert" (exp (gen) lp) P-0 (privk CA-0)))) ((recv (enc "cert-req" P (exp (gen) l) (privk P))) (send (enc "cert" (exp (gen) l) P (privk CA-0)))) ((recv (enc "cert-req" P (exp (gen) l) (privk P))) (send (enc "cert" (exp (gen) l) P (privk CA)))) ((recv (enc "cert-req" P-0 (exp (gen) lp) (privk P-0))) (send (enc "cert" (exp (gen) lp) P-0 (privk CA))))) (label 34) (parent 25) (unrealized (1 3)) (comment "1 in cohort - 1 not yet seen")) (defskeleton iadh-um (vars (key data) (B CA P name) (e ep lp expn) (l expr) (l-0 expn)) (defstrand init 5 (key key) (A P) (B B) (CA CA) (hl (exp (gen) l-0)) (he (exp (gen) (mul (rec e) ep l l-0))) (l lp) (e e)) (defstrand init 5 (key key) (A P) (B B) (CA CA) (hl (exp (gen) l-0)) (he (exp (gen) (mul l l-0))) (l lp) (e ep)) (defstrand ltkgen 1 (P P) (l lp)) (defstrand ca-gen 2 (P P) (CA CA) (h (exp (gen) lp))) (defstrand ca-gen 2 (P B) (CA CA) (h (exp (gen) l-0))) (defstrand ltkgen 1 (P B) (l l-0)) (defstrand ca-gen 2 (P B) (CA CA) (h (exp (gen) l-0))) (precedes ((0 2) (1 3)) ((1 2) (0 3)) ((2 0) (3 0)) ((3 1) (0 0)) ((3 1) (1 0)) ((4 1) (1 1)) ((5 0) (4 0)) ((5 0) (6 0)) ((6 1) (0 1))) (fn-of ("principal-of" (B (exp (gen) l-0)) (P (exp (gen) lp))) (foo ((hash (exp (gen) (mul lp l-0)) (exp (gen) (mul ep l l-0))) key))) (neq ((exp (gen) l-0) (gen)) ((exp (gen) lp) (gen)) ((exp (gen) l-0) (exp (gen) lp)) ((exp (gen) (mul l l-0)) (gen)) ((exp (gen) (mul (rec e) ep l l-0)) (gen))) (non-orig (privk B) (privk CA) (privk P)) (uniq-gen e ep lp) (operation encryption-test (displaced 7 5 ltkgen 1) (enc "cert-req" B (exp (gen) l-0) (privk B)) (6 0)) (traces ((recv (enc "cert" (exp (gen) lp) P (privk CA))) (recv (enc "cert" (exp (gen) l-0) B (privk CA))) (send (exp (gen) e)) (recv (exp (gen) (mul (rec e) ep l l-0))) (send key)) ((recv (enc "cert" (exp (gen) lp) P (privk CA))) (recv (enc "cert" (exp (gen) l-0) B (privk CA))) (send (exp (gen) ep)) (recv (exp (gen) (mul l l-0))) (send key)) ((send (enc "cert-req" P (exp (gen) lp) (privk P)))) ((recv (enc "cert-req" P (exp (gen) lp) (privk P))) (send (enc "cert" (exp (gen) lp) P (privk CA)))) ((recv (enc "cert-req" B (exp (gen) l-0) (privk B))) (send (enc "cert" (exp (gen) l-0) B (privk CA)))) ((send (enc "cert-req" B (exp (gen) l-0) (privk B)))) ((recv (enc "cert-req" B (exp (gen) l-0) (privk B))) (send (enc "cert" (exp (gen) l-0) B (privk CA))))) (label 35) (parent 28) (unrealized (0 3)) (comment "1 in cohort - 1 not yet seen")) (defskeleton iadh-um (vars (key data) (B CA P name) (e ep lp expn) (l expr) (l-0 expn)) (defstrand init 5 (key key) (A P) (B B) (CA CA) (hl (exp (gen) l-0)) (he (exp (gen) (mul (rec e) ep l l-0))) (l lp) (e e)) (defstrand init 5 (key key) (A P) (B B) (CA CA) (hl (exp (gen) l-0)) (he (exp (gen) (mul l l-0))) (l lp) (e ep)) (defstrand ltkgen 1 (P P) (l lp)) (defstrand ca-gen 2 (P P) (CA CA) (h (exp (gen) lp))) (defstrand ca-gen 2 (P B) (CA CA) (h (exp (gen) l-0))) (defstrand ltkgen 1 (P B) (l l-0)) (defstrand ca-gen 2 (P B) (CA CA) (h (exp (gen) l-0))) (defstrand ltkgen 1 (P B) (l l-0)) (precedes ((0 2) (1 3)) ((1 2) (0 3)) ((2 0) (3 0)) ((3 1) (0 0)) ((3 1) (1 0)) ((4 1) (1 1)) ((5 0) (4 0)) ((6 1) (0 1)) ((7 0) (6 0))) (fn-of ("principal-of" (B (exp (gen) l-0)) (P (exp (gen) lp))) (foo ((hash (exp (gen) (mul lp l-0)) (exp (gen) (mul ep l l-0))) key))) (neq ((exp (gen) l-0) (gen)) ((exp (gen) lp) (gen)) ((exp (gen) l-0) (exp (gen) lp)) ((exp (gen) (mul l l-0)) (gen)) ((exp (gen) (mul (rec e) ep l l-0)) (gen))) (non-orig (privk B) (privk CA) (privk P)) (uniq-gen e ep lp) (operation encryption-test (added-strand ltkgen 1) (enc "cert-req" B (exp (gen) l-0) (privk B)) (6 0)) (traces ((recv (enc "cert" (exp (gen) lp) P (privk CA))) (recv (enc "cert" (exp (gen) l-0) B (privk CA))) (send (exp (gen) e)) (recv (exp (gen) (mul (rec e) ep l l-0))) (send key)) ((recv (enc "cert" (exp (gen) lp) P (privk CA))) (recv (enc "cert" (exp (gen) l-0) B (privk CA))) (send (exp (gen) ep)) (recv (exp (gen) (mul l l-0))) (send key)) ((send (enc "cert-req" P (exp (gen) lp) (privk P)))) ((recv (enc "cert-req" P (exp (gen) lp) (privk P))) (send (enc "cert" (exp (gen) lp) P (privk CA)))) ((recv (enc "cert-req" B (exp (gen) l-0) (privk B))) (send (enc "cert" (exp (gen) l-0) B (privk CA)))) ((send (enc "cert-req" B (exp (gen) l-0) (privk B)))) ((recv (enc "cert-req" B (exp (gen) l-0) (privk B))) (send (enc "cert" (exp (gen) l-0) B (privk CA)))) ((send (enc "cert-req" B (exp (gen) l-0) (privk B))))) (label 36) (parent 28) (unrealized (0 3)) (comment "1 in cohort - 1 not yet seen")) (defskeleton iadh-um (vars (key data) (B CA P name) (ep lp e l expn) (ep-0 expr)) (defstrand init 5 (key key) (A P) (B B) (CA CA) (hl (exp (gen) l)) (he (exp (gen) (mul ep ep-0))) (l lp) (e e)) (defstrand init 5 (key key) (A P) (B B) (CA CA) (hl (exp (gen) l)) (he (exp (gen) (mul e ep-0))) (l lp) (e ep)) (defstrand ltkgen 1 (P P) (l lp)) (defstrand ca-gen 2 (P P) (CA CA) (h (exp (gen) lp))) (defstrand ca-gen 2 (P B) (CA CA) (h (exp (gen) l))) (defstrand ltkgen 1 (P B) (l l)) (precedes ((0 2) (1 3)) ((1 2) (0 3)) ((2 0) (0 0)) ((2 0) (3 0)) ((3 1) (1 0)) ((4 1) (0 1)) ((4 1) (1 1)) ((5 0) (4 0))) (fn-of ("principal-of" (B (exp (gen) l)) (P (exp (gen) lp))) (foo ((hash (exp (gen) (mul lp l)) (exp (gen) (mul ep e ep-0))) key))) (neq ((exp (gen) l) (gen)) ((exp (gen) lp) (gen)) ((exp (gen) l) (exp (gen) lp)) ((exp (gen) (mul e ep-0)) (gen)) ((exp (gen) (mul ep ep-0)) (gen))) (non-orig (privk B) (privk CA) (privk P)) (uniq-gen ep lp e) (operation nonce-test (algebra-contracted (e-0 e) (l-0 l) (l-1 (mul e (rec l) ep-0)) (ep-1 ep-0)) (exp (gen) (mul ep ep-0)) (0 3)) (traces ((recv (enc "cert" (exp (gen) lp) P (privk CA))) (recv (enc "cert" (exp (gen) l) B (privk CA))) (send (exp (gen) e)) (recv (exp (gen) (mul ep ep-0))) (send key)) ((recv (enc "cert" (exp (gen) lp) P (privk CA))) (recv (enc "cert" (exp (gen) l) B (privk CA))) (send (exp (gen) ep)) (recv (exp (gen) (mul e ep-0))) (send key)) ((send (enc "cert-req" P (exp (gen) lp) (privk P)))) ((recv (enc "cert-req" P (exp (gen) lp) (privk P))) (send (enc "cert" (exp (gen) lp) P (privk CA)))) ((recv (enc "cert-req" B (exp (gen) l) (privk B))) (send (enc "cert" (exp (gen) l) B (privk CA)))) ((send (enc "cert-req" B (exp (gen) l) (privk B))))) (label 37) (parent 29) (unrealized (0 0)) (comment "1 in cohort - 1 not yet seen")) (defskeleton iadh-um (vars (key data) (CA B CA-0 P name) (e ep lp expn) (l expr) (l-0 expn)) (defstrand init 5 (key key) (A P) (B B) (CA CA) (hl (exp (gen) l-0)) (he (exp (gen) (mul (rec e) ep l l-0))) (l lp) (e e)) (defstrand init 5 (key key) (A P) (B B) (CA CA-0) (hl (exp (gen) l-0)) (he (exp (gen) (mul l l-0))) (l lp) (e ep)) (defstrand ltkgen 1 (P P) (l lp)) (defstrand ca-gen 2 (P P) (CA CA-0) (h (exp (gen) lp))) (defstrand ca-gen 2 (P B) (CA CA-0) (h (exp (gen) l-0))) (defstrand ltkgen 1 (P B) (l l-0)) (defstrand ca-gen 2 (P P) (CA CA) (h (exp (gen) lp))) (defstrand ca-gen 2 (P B) (CA CA) (h (exp (gen) l-0))) (precedes ((0 2) (1 3)) ((1 2) (0 3)) ((2 0) (3 0)) ((2 0) (6 0)) ((3 1) (1 0)) ((4 1) (1 1)) ((5 0) (4 0)) ((5 0) (7 0)) ((6 1) (0 0)) ((7 1) (0 1))) (fn-of ("principal-of" (B (exp (gen) l-0)) (P (exp (gen) lp))) (foo ((hash (exp (gen) (mul lp l-0)) (exp (gen) (mul ep l l-0))) key))) (neq ((exp (gen) l-0) (gen)) ((exp (gen) lp) (gen)) ((exp (gen) l-0) (exp (gen) lp)) ((exp (gen) (mul l l-0)) (gen)) ((exp (gen) (mul (rec e) ep l l-0)) (gen))) (non-orig (privk CA) (privk B) (privk CA-0) (privk P)) (uniq-gen e ep lp) (operation encryption-test (displaced 8 5 ltkgen 1) (enc "cert-req" B (exp (gen) l-0) (privk B)) (7 0)) (traces ((recv (enc "cert" (exp (gen) lp) P (privk CA))) (recv (enc "cert" (exp (gen) l-0) B (privk CA))) (send (exp (gen) e)) (recv (exp (gen) (mul (rec e) ep l l-0))) (send key)) ((recv (enc "cert" (exp (gen) lp) P (privk CA-0))) (recv (enc "cert" (exp (gen) l-0) B (privk CA-0))) (send (exp (gen) ep)) (recv (exp (gen) (mul l l-0))) (send key)) ((send (enc "cert-req" P (exp (gen) lp) (privk P)))) ((recv (enc "cert-req" P (exp (gen) lp) (privk P))) (send (enc "cert" (exp (gen) lp) P (privk CA-0)))) ((recv (enc "cert-req" B (exp (gen) l-0) (privk B))) (send (enc "cert" (exp (gen) l-0) B (privk CA-0)))) ((send (enc "cert-req" B (exp (gen) l-0) (privk B)))) ((recv (enc "cert-req" P (exp (gen) lp) (privk P))) (send (enc "cert" (exp (gen) lp) P (privk CA)))) ((recv (enc "cert-req" B (exp (gen) l-0) (privk B))) (send (enc "cert" (exp (gen) l-0) B (privk CA))))) (label 38) (parent 30) (seen 38) (unrealized (0 3)) (comment "1 in cohort - 0 not yet seen")) (defskeleton iadh-um (vars (key data) (CA B CA-0 P name) (e ep lp expn) (l expr) (l-0 expn)) (defstrand init 5 (key key) (A P) (B B) (CA CA) (hl (exp (gen) l-0)) (he (exp (gen) (mul (rec e) ep l l-0))) (l lp) (e e)) (defstrand init 5 (key key) (A P) (B B) (CA CA-0) (hl (exp (gen) l-0)) (he (exp (gen) (mul l l-0))) (l lp) (e ep)) (defstrand ltkgen 1 (P P) (l lp)) (defstrand ca-gen 2 (P P) (CA CA-0) (h (exp (gen) lp))) (defstrand ca-gen 2 (P B) (CA CA-0) (h (exp (gen) l-0))) (defstrand ltkgen 1 (P B) (l l-0)) (defstrand ca-gen 2 (P P) (CA CA) (h (exp (gen) lp))) (defstrand ca-gen 2 (P B) (CA CA) (h (exp (gen) l-0))) (defstrand ltkgen 1 (P B) (l l-0)) (precedes ((0 2) (1 3)) ((1 2) (0 3)) ((2 0) (3 0)) ((2 0) (6 0)) ((3 1) (1 0)) ((4 1) (1 1)) ((5 0) (4 0)) ((6 1) (0 0)) ((7 1) (0 1)) ((8 0) (7 0))) (fn-of ("principal-of" (B (exp (gen) l-0)) (P (exp (gen) lp))) (foo ((hash (exp (gen) (mul lp l-0)) (exp (gen) (mul ep l l-0))) key))) (neq ((exp (gen) l-0) (gen)) ((exp (gen) lp) (gen)) ((exp (gen) l-0) (exp (gen) lp)) ((exp (gen) (mul l l-0)) (gen)) ((exp (gen) (mul (rec e) ep l l-0)) (gen))) (non-orig (privk CA) (privk B) (privk CA-0) (privk P)) (uniq-gen e ep lp) (operation encryption-test (added-strand ltkgen 1) (enc "cert-req" B (exp (gen) l-0) (privk B)) (7 0)) (traces ((recv (enc "cert" (exp (gen) lp) P (privk CA))) (recv (enc "cert" (exp (gen) l-0) B (privk CA))) (send (exp (gen) e)) (recv (exp (gen) (mul (rec e) ep l l-0))) (send key)) ((recv (enc "cert" (exp (gen) lp) P (privk CA-0))) (recv (enc "cert" (exp (gen) l-0) B (privk CA-0))) (send (exp (gen) ep)) (recv (exp (gen) (mul l l-0))) (send key)) ((send (enc "cert-req" P (exp (gen) lp) (privk P)))) ((recv (enc "cert-req" P (exp (gen) lp) (privk P))) (send (enc "cert" (exp (gen) lp) P (privk CA-0)))) ((recv (enc "cert-req" B (exp (gen) l-0) (privk B))) (send (enc "cert" (exp (gen) l-0) B (privk CA-0)))) ((send (enc "cert-req" B (exp (gen) l-0) (privk B)))) ((recv (enc "cert-req" P (exp (gen) lp) (privk P))) (send (enc "cert" (exp (gen) lp) P (privk CA)))) ((recv (enc "cert-req" B (exp (gen) l-0) (privk B))) (send (enc "cert" (exp (gen) l-0) B (privk CA)))) ((send (enc "cert-req" B (exp (gen) l-0) (privk B))))) (label 39) (parent 30) (unrealized (0 3)) (comment "1 in cohort - 1 not yet seen")) (defskeleton iadh-um (vars (key data) (CA P P-0 name) (lp l e ep expn) (ep-0 expr)) (defstrand init 5 (key key) (A P) (B P-0) (CA CA) (hl (exp (gen) lp)) (he (exp (gen) (mul (rec e) ep ep ep-0))) (l l) (e e)) (defstrand init 5 (key key) (A P-0) (B P) (CA CA) (hl (exp (gen) l)) (he (exp (gen) (mul ep ep-0))) (l lp) (e ep)) (defstrand ltkgen 1 (P P) (l l)) (defstrand ltkgen 1 (P P-0) (l lp)) (defstrand ca-gen 2 (P P-0) (CA CA) (h (exp (gen) lp))) (defstrand ca-gen 2 (P P) (CA CA) (h (exp (gen) l))) (precedes ((0 2) (1 3)) ((1 2) (0 3)) ((2 0) (5 0)) ((3 0) (4 0)) ((3 0) (5 0)) ((4 1) (0 1)) ((4 1) (1 0)) ((5 1) (0 0)) ((5 1) (1 1))) (fn-of ("principal-of" (P-0 (exp (gen) lp)) (P (exp (gen) l))) (foo ((hash (exp (gen) (mul lp l)) (exp (gen) (mul ep ep ep-0))) key))) (neq ((exp (gen) lp) (gen)) ((exp (gen) l) (gen)) ((exp (gen) l) (exp (gen) lp)) ((exp (gen) (mul ep ep-0)) (gen)) ((exp (gen) lp) (exp (gen) l)) ((exp (gen) (mul (rec e) ep ep ep-0)) (gen))) (non-orig (privk CA) (privk P) (privk P-0)) (uniq-gen lp l e ep) (operation nonce-test (algebra-contracted (l-0 l) (e-0 e) (ep-1 ep) (l-1 (mul (rec l) (rec e) ep ep ep-0)) (ep-2 ep-0)) (exp (gen) (mul ep ep-0)) (1 3)) (traces ((recv (enc "cert" (exp (gen) l) P (privk CA))) (recv (enc "cert" (exp (gen) lp) P-0 (privk CA))) (send (exp (gen) e)) (recv (exp (gen) (mul (rec e) ep ep ep-0))) (send key)) ((recv (enc "cert" (exp (gen) lp) P-0 (privk CA))) (recv (enc "cert" (exp (gen) l) P (privk CA))) (send (exp (gen) ep)) (recv (exp (gen) (mul ep ep-0))) (send key)) ((send (enc "cert-req" P (exp (gen) l) (privk P)))) ((send (enc "cert-req" P-0 (exp (gen) lp) (privk P-0)))) ((recv (enc "cert-req" P-0 (exp (gen) lp) (privk P-0))) (send (enc "cert" (exp (gen) lp) P-0 (privk CA)))) ((recv (enc "cert-req" P (exp (gen) l) (privk P))) (send (enc "cert" (exp (gen) l) P (privk CA))))) (label 40) (parent 31) (unrealized (0 3)) (comment "1 in cohort - 1 not yet seen")) (defskeleton iadh-um (vars (key data) (CA P P-0 name) (lp l e ep expn) (ep-0 expr)) (defstrand init 5 (key key) (A P) (B P-0) (CA CA) (hl (exp (gen) lp)) (he (exp (gen) (mul (rec e) ep ep ep-0))) (l l) (e e)) (defstrand init 5 (key key) (A P-0) (B P) (CA CA) (hl (exp (gen) l)) (he (exp (gen) (mul ep ep-0))) (l lp) (e ep)) (defstrand ltkgen 1 (P P) (l l)) (defstrand ltkgen 1 (P P-0) (l lp)) (defstrand ca-gen 2 (P P-0) (CA CA) (h (exp (gen) lp))) (defstrand ca-gen 2 (P P) (CA CA) (h (exp (gen) l))) (defstrand ca-gen 2 (P P-0) (CA CA) (h (exp (gen) lp))) (precedes ((0 2) (1 3)) ((1 2) (0 3)) ((2 0) (5 0)) ((3 0) (4 0)) ((3 0) (5 0)) ((3 0) (6 0)) ((4 1) (1 0)) ((5 1) (0 0)) ((5 1) (1 1)) ((6 1) (0 1))) (fn-of ("principal-of" (P-0 (exp (gen) lp)) (P (exp (gen) l))) (foo ((hash (exp (gen) (mul lp l)) (exp (gen) (mul ep ep ep-0))) key))) (neq ((exp (gen) lp) (gen)) ((exp (gen) l) (gen)) ((exp (gen) l) (exp (gen) lp)) ((exp (gen) (mul ep ep-0)) (gen)) ((exp (gen) lp) (exp (gen) l)) ((exp (gen) (mul (rec e) ep ep ep-0)) (gen))) (non-orig (privk CA) (privk P) (privk P-0)) (uniq-gen lp l e ep) (operation nonce-test (algebra-contracted (l-0 l) (e-0 e) (ep-1 ep) (l-1 (mul (rec l) (rec e) ep ep ep-0)) (ep-2 ep-0)) (exp (gen) (mul ep ep-0)) (1 3)) (traces ((recv (enc "cert" (exp (gen) l) P (privk CA))) (recv (enc "cert" (exp (gen) lp) P-0 (privk CA))) (send (exp (gen) e)) (recv (exp (gen) (mul (rec e) ep ep ep-0))) (send key)) ((recv (enc "cert" (exp (gen) lp) P-0 (privk CA))) (recv (enc "cert" (exp (gen) l) P (privk CA))) (send (exp (gen) ep)) (recv (exp (gen) (mul ep ep-0))) (send key)) ((send (enc "cert-req" P (exp (gen) l) (privk P)))) ((send (enc "cert-req" P-0 (exp (gen) lp) (privk P-0)))) ((recv (enc "cert-req" P-0 (exp (gen) lp) (privk P-0))) (send (enc "cert" (exp (gen) lp) P-0 (privk CA)))) ((recv (enc "cert-req" P (exp (gen) l) (privk P))) (send (enc "cert" (exp (gen) l) P (privk CA)))) ((recv (enc "cert-req" P-0 (exp (gen) lp) (privk P-0))) (send (enc "cert" (exp (gen) lp) P-0 (privk CA))))) (label 41) (parent 32) (unrealized (0 3)) (comment "1 in cohort - 1 not yet seen")) (defskeleton iadh-um (vars (key data) (CA P P-0 name) (lp l e ep expn) (ep-0 expr)) (defstrand init 5 (key key) (A P) (B P-0) (CA CA) (hl (exp (gen) lp)) (he (exp (gen) (mul (rec e) ep ep ep-0))) (l l) (e e)) (defstrand init 5 (key key) (A P-0) (B P) (CA CA) (hl (exp (gen) l)) (he (exp (gen) (mul ep ep-0))) (l lp) (e ep)) (defstrand ltkgen 1 (P P) (l l)) (defstrand ltkgen 1 (P P-0) (l lp)) (defstrand ca-gen 2 (P P-0) (CA CA) (h (exp (gen) lp))) (defstrand ca-gen 2 (P P) (CA CA) (h (exp (gen) l))) (defstrand ca-gen 2 (P P) (CA CA) (h (exp (gen) l))) (precedes ((0 2) (1 3)) ((1 2) (0 3)) ((2 0) (5 0)) ((2 0) (6 0)) ((3 0) (4 0)) ((3 0) (5 0)) ((4 1) (0 1)) ((4 1) (1 0)) ((5 1) (1 1)) ((6 1) (0 0))) (fn-of ("principal-of" (P-0 (exp (gen) lp)) (P (exp (gen) l))) (foo ((hash (exp (gen) (mul lp l)) (exp (gen) (mul ep ep ep-0))) key))) (neq ((exp (gen) lp) (gen)) ((exp (gen) l) (gen)) ((exp (gen) l) (exp (gen) lp)) ((exp (gen) (mul ep ep-0)) (gen)) ((exp (gen) lp) (exp (gen) l)) ((exp (gen) (mul (rec e) ep ep ep-0)) (gen))) (non-orig (privk CA) (privk P) (privk P-0)) (uniq-gen lp l e ep) (operation nonce-test (algebra-contracted (l-0 l) (e-0 e) (ep-1 ep) (l-1 (mul (rec l) (rec e) ep ep ep-0)) (ep-2 ep-0)) (exp (gen) (mul ep ep-0)) (1 3)) (traces ((recv (enc "cert" (exp (gen) l) P (privk CA))) (recv (enc "cert" (exp (gen) lp) P-0 (privk CA))) (send (exp (gen) e)) (recv (exp (gen) (mul (rec e) ep ep ep-0))) (send key)) ((recv (enc "cert" (exp (gen) lp) P-0 (privk CA))) (recv (enc "cert" (exp (gen) l) P (privk CA))) (send (exp (gen) ep)) (recv (exp (gen) (mul ep ep-0))) (send key)) ((send (enc "cert-req" P (exp (gen) l) (privk P)))) ((send (enc "cert-req" P-0 (exp (gen) lp) (privk P-0)))) ((recv (enc "cert-req" P-0 (exp (gen) lp) (privk P-0))) (send (enc "cert" (exp (gen) lp) P-0 (privk CA)))) ((recv (enc "cert-req" P (exp (gen) l) (privk P))) (send (enc "cert" (exp (gen) l) P (privk CA)))) ((recv (enc "cert-req" P (exp (gen) l) (privk P))) (send (enc "cert" (exp (gen) l) P (privk CA))))) (label 42) (parent 33) (unrealized (0 3)) (comment "1 in cohort - 1 not yet seen")) (defskeleton iadh-um (vars (key data) (CA CA-0 P P-0 name) (lp l e ep expn) (ep-0 expr)) (defstrand init 5 (key key) (A P) (B P-0) (CA CA) (hl (exp (gen) lp)) (he (exp (gen) (mul (rec e) ep ep ep-0))) (l l) (e e)) (defstrand init 5 (key key) (A P-0) (B P) (CA CA-0) (hl (exp (gen) l)) (he (exp (gen) (mul ep ep-0))) (l lp) (e ep)) (defstrand ltkgen 1 (P P) (l l)) (defstrand ltkgen 1 (P P-0) (l lp)) (defstrand ca-gen 2 (P P-0) (CA CA-0) (h (exp (gen) lp))) (defstrand ca-gen 2 (P P) (CA CA-0) (h (exp (gen) l))) (defstrand ca-gen 2 (P P) (CA CA) (h (exp (gen) l))) (defstrand ca-gen 2 (P P-0) (CA CA) (h (exp (gen) lp))) (precedes ((0 2) (1 3)) ((1 2) (0 3)) ((2 0) (5 0)) ((2 0) (6 0)) ((3 0) (4 0)) ((3 0) (5 0)) ((3 0) (7 0)) ((4 1) (1 0)) ((5 1) (1 1)) ((6 1) (0 0)) ((7 1) (0 1))) (fn-of ("principal-of" (P-0 (exp (gen) lp)) (P (exp (gen) l))) (foo ((hash (exp (gen) (mul lp l)) (exp (gen) (mul ep ep ep-0))) key))) (neq ((exp (gen) lp) (gen)) ((exp (gen) l) (gen)) ((exp (gen) l) (exp (gen) lp)) ((exp (gen) (mul ep ep-0)) (gen)) ((exp (gen) lp) (exp (gen) l)) ((exp (gen) (mul (rec e) ep ep ep-0)) (gen))) (non-orig (privk CA) (privk CA-0) (privk P) (privk P-0)) (uniq-gen lp l e ep) (operation nonce-test (algebra-contracted (l-0 l) (e-0 e) (ep-1 ep) (l-1 (mul (rec l) (rec e) ep ep ep-0)) (ep-2 ep-0)) (exp (gen) (mul ep ep-0)) (1 3)) (traces ((recv (enc "cert" (exp (gen) l) P (privk CA))) (recv (enc "cert" (exp (gen) lp) P-0 (privk CA))) (send (exp (gen) e)) (recv (exp (gen) (mul (rec e) ep ep ep-0))) (send key)) ((recv (enc "cert" (exp (gen) lp) P-0 (privk CA-0))) (recv (enc "cert" (exp (gen) l) P (privk CA-0))) (send (exp (gen) ep)) (recv (exp (gen) (mul ep ep-0))) (send key)) ((send (enc "cert-req" P (exp (gen) l) (privk P)))) ((send (enc "cert-req" P-0 (exp (gen) lp) (privk P-0)))) ((recv (enc "cert-req" P-0 (exp (gen) lp) (privk P-0))) (send (enc "cert" (exp (gen) lp) P-0 (privk CA-0)))) ((recv (enc "cert-req" P (exp (gen) l) (privk P))) (send (enc "cert" (exp (gen) l) P (privk CA-0)))) ((recv (enc "cert-req" P (exp (gen) l) (privk P))) (send (enc "cert" (exp (gen) l) P (privk CA)))) ((recv (enc "cert-req" P-0 (exp (gen) lp) (privk P-0))) (send (enc "cert" (exp (gen) lp) P-0 (privk CA))))) (label 43) (parent 34) (unrealized (0 3)) (comment "1 in cohort - 1 not yet seen")) (defskeleton iadh-um (vars (key data) (B CA P name) (ep lp e l expn) (ep-0 expr)) (defstrand init 5 (key key) (A P) (B B) (CA CA) (hl (exp (gen) l)) (he (exp (gen) (mul ep ep-0))) (l lp) (e e)) (defstrand init 5 (key key) (A P) (B B) (CA CA) (hl (exp (gen) l)) (he (exp (gen) (mul e ep-0))) (l lp) (e ep)) (defstrand ltkgen 1 (P P) (l lp)) (defstrand ca-gen 2 (P P) (CA CA) (h (exp (gen) lp))) (defstrand ca-gen 2 (P B) (CA CA) (h (exp (gen) l))) (defstrand ltkgen 1 (P B) (l l)) (precedes ((0 2) (1 3)) ((1 2) (0 3)) ((2 0) (3 0)) ((3 1) (0 0)) ((3 1) (1 0)) ((4 1) (1 1)) ((5 0) (0 1)) ((5 0) (4 0))) (fn-of ("principal-of" (B (exp (gen) l)) (P (exp (gen) lp))) (foo ((hash (exp (gen) (mul lp l)) (exp (gen) (mul ep e ep-0))) key))) (neq ((exp (gen) l) (gen)) ((exp (gen) lp) (gen)) ((exp (gen) l) (exp (gen) lp)) ((exp (gen) (mul e ep-0)) (gen)) ((exp (gen) (mul ep ep-0)) (gen))) (non-orig (privk B) (privk CA) (privk P)) (uniq-gen ep lp e) (operation nonce-test (algebra-contracted (e-0 e) (l-0 (mul e (rec l) ep-0)) (l-1 l) (ep-1 ep-0)) (exp (gen) (mul ep ep-0)) (0 3)) (traces ((recv (enc "cert" (exp (gen) lp) P (privk CA))) (recv (enc "cert" (exp (gen) l) B (privk CA))) (send (exp (gen) e)) (recv (exp (gen) (mul ep ep-0))) (send key)) ((recv (enc "cert" (exp (gen) lp) P (privk CA))) (recv (enc "cert" (exp (gen) l) B (privk CA))) (send (exp (gen) ep)) (recv (exp (gen) (mul e ep-0))) (send key)) ((send (enc "cert-req" P (exp (gen) lp) (privk P)))) ((recv (enc "cert-req" P (exp (gen) lp) (privk P))) (send (enc "cert" (exp (gen) lp) P (privk CA)))) ((recv (enc "cert-req" B (exp (gen) l) (privk B))) (send (enc "cert" (exp (gen) l) B (privk CA)))) ((send (enc "cert-req" B (exp (gen) l) (privk B))))) (label 44) (parent 35) (seen 46) (unrealized (0 1)) (comment "2 in cohort - 1 not yet seen")) (defskeleton iadh-um (vars (key data) (B CA P name) (ep lp e l expn) (ep-0 expr)) (defstrand init 5 (key key) (A P) (B B) (CA CA) (hl (exp (gen) l)) (he (exp (gen) (mul ep ep-0))) (l lp) (e e)) (defstrand init 5 (key key) (A P) (B B) (CA CA) (hl (exp (gen) l)) (he (exp (gen) (mul e ep-0))) (l lp) (e ep)) (defstrand ltkgen 1 (P P) (l lp)) (defstrand ca-gen 2 (P P) (CA CA) (h (exp (gen) lp))) (defstrand ca-gen 2 (P B) (CA CA) (h (exp (gen) l))) (defstrand ltkgen 1 (P B) (l l)) (defstrand ca-gen 2 (P B) (CA CA) (h (exp (gen) l))) (precedes ((0 2) (1 3)) ((1 2) (0 3)) ((2 0) (3 0)) ((3 1) (0 0)) ((3 1) (1 0)) ((4 1) (1 1)) ((5 0) (4 0)) ((6 1) (0 1))) (fn-of ("principal-of" (B (exp (gen) l)) (P (exp (gen) lp))) (foo ((hash (exp (gen) (mul lp l)) (exp (gen) (mul ep e ep-0))) key))) (neq ((exp (gen) l) (gen)) ((exp (gen) lp) (gen)) ((exp (gen) l) (exp (gen) lp)) ((exp (gen) (mul e ep-0)) (gen)) ((exp (gen) (mul ep ep-0)) (gen))) (non-orig (privk B) (privk CA) (privk P)) (uniq-gen ep lp e) (operation nonce-test (algebra-contracted (e-0 e) (l-0 (mul e (rec l) ep-0)) (l-1 l) (ep-1 ep-0)) (exp (gen) (mul ep ep-0)) (0 3)) (traces ((recv (enc "cert" (exp (gen) lp) P (privk CA))) (recv (enc "cert" (exp (gen) l) B (privk CA))) (send (exp (gen) e)) (recv (exp (gen) (mul ep ep-0))) (send key)) ((recv (enc "cert" (exp (gen) lp) P (privk CA))) (recv (enc "cert" (exp (gen) l) B (privk CA))) (send (exp (gen) ep)) (recv (exp (gen) (mul e ep-0))) (send key)) ((send (enc "cert-req" P (exp (gen) lp) (privk P)))) ((recv (enc "cert-req" P (exp (gen) lp) (privk P))) (send (enc "cert" (exp (gen) lp) P (privk CA)))) ((recv (enc "cert-req" B (exp (gen) l) (privk B))) (send (enc "cert" (exp (gen) l) B (privk CA)))) ((send (enc "cert-req" B (exp (gen) l) (privk B)))) ((recv (enc "cert-req" B (exp (gen) l) (privk B))) (send (enc "cert" (exp (gen) l) B (privk CA))))) (label 45) (parent 36) (seen 44) (unrealized (6 0)) (comment "1 in cohort - 0 not yet seen")) (defskeleton iadh-um (vars (key data) (B CA P name) (ep lp e l expn) (ep-0 expr)) (defstrand init 5 (key key) (A P) (B B) (CA CA) (hl (exp (gen) l)) (he (exp (gen) (mul ep ep-0))) (l lp) (e e)) (defstrand init 5 (key key) (A P) (B B) (CA CA) (hl (exp (gen) l)) (he (exp (gen) (mul e ep-0))) (l lp) (e ep)) (defstrand ltkgen 1 (P P) (l lp)) (defstrand ca-gen 2 (P P) (CA CA) (h (exp (gen) lp))) (defstrand ca-gen 2 (P B) (CA CA) (h (exp (gen) l))) (defstrand ltkgen 1 (P B) (l l)) (precedes ((0 2) (1 3)) ((1 2) (0 3)) ((2 0) (3 0)) ((3 1) (0 0)) ((3 1) (1 0)) ((4 1) (0 1)) ((4 1) (1 1)) ((5 0) (4 0))) (fn-of ("principal-of" (P (exp (gen) lp)) (B (exp (gen) l))) (foo ((hash (exp (gen) (mul lp l)) (exp (gen) (mul ep e ep-0))) key))) (neq ((exp (gen) lp) (gen)) ((exp (gen) l) (gen)) ((exp (gen) l) (exp (gen) lp)) ((exp (gen) (mul e ep-0)) (gen)) ((exp (gen) (mul ep ep-0)) (gen))) (non-orig (privk B) (privk CA) (privk P)) (uniq-gen ep lp e) (operation encryption-test (displaced 6 3 ca-gen 2) (enc "cert" (exp (gen) lp) P (privk CA)) (0 0)) (traces ((recv (enc "cert" (exp (gen) lp) P (privk CA))) (recv (enc "cert" (exp (gen) l) B (privk CA))) (send (exp (gen) e)) (recv (exp (gen) (mul ep ep-0))) (send key)) ((recv (enc "cert" (exp (gen) lp) P (privk CA))) (recv (enc "cert" (exp (gen) l) B (privk CA))) (send (exp (gen) ep)) (recv (exp (gen) (mul e ep-0))) (send key)) ((send (enc "cert-req" P (exp (gen) lp) (privk P)))) ((recv (enc "cert-req" P (exp (gen) lp) (privk P))) (send (enc "cert" (exp (gen) lp) P (privk CA)))) ((recv (enc "cert-req" B (exp (gen) l) (privk B))) (send (enc "cert" (exp (gen) l) B (privk CA)))) ((send (enc "cert-req" B (exp (gen) l) (privk B))))) (label 46) (parent 37) (unrealized) (shape) (maps ((0 1 2 2) ((key key) (hl (exp (gen) l)) (he (exp (gen) (mul ep ep-0))) (A P) (B B) (CA CA) (A-0 P) (B-0 B) (CA-0 CA) (P P) (P-0 P) (l lp) (lp lp) (e e) (ep ep)))) (origs)) (defskeleton iadh-um (vars (key data) (CA B CA-0 P name) (ep lp e l expn) (ep-0 expr)) (defstrand init 5 (key key) (A P) (B B) (CA CA) (hl (exp (gen) l)) (he (exp (gen) (mul ep ep-0))) (l lp) (e e)) (defstrand init 5 (key key) (A P) (B B) (CA CA-0) (hl (exp (gen) l)) (he (exp (gen) (mul e ep-0))) (l lp) (e ep)) (defstrand ltkgen 1 (P P) (l lp)) (defstrand ca-gen 2 (P P) (CA CA-0) (h (exp (gen) lp))) (defstrand ca-gen 2 (P B) (CA CA-0) (h (exp (gen) l))) (defstrand ltkgen 1 (P B) (l l)) (defstrand ca-gen 2 (P P) (CA CA) (h (exp (gen) lp))) (defstrand ca-gen 2 (P B) (CA CA) (h (exp (gen) l))) (precedes ((0 2) (1 3)) ((1 2) (0 3)) ((2 0) (3 0)) ((2 0) (6 0)) ((3 1) (1 0)) ((4 1) (1 1)) ((5 0) (4 0)) ((6 1) (0 0)) ((7 1) (0 1))) (fn-of ("principal-of" (B (exp (gen) l)) (P (exp (gen) lp))) (foo ((hash (exp (gen) (mul lp l)) (exp (gen) (mul ep e ep-0))) key))) (neq ((exp (gen) l) (gen)) ((exp (gen) lp) (gen)) ((exp (gen) l) (exp (gen) lp)) ((exp (gen) (mul e ep-0)) (gen)) ((exp (gen) (mul ep ep-0)) (gen))) (non-orig (privk CA) (privk B) (privk CA-0) (privk P)) (uniq-gen ep lp e) (operation nonce-test (algebra-contracted (e-0 e) (l-0 (mul e (rec l) ep-0)) (l-1 l) (ep-1 ep-0)) (exp (gen) (mul ep ep-0)) (0 3)) (traces ((recv (enc "cert" (exp (gen) lp) P (privk CA))) (recv (enc "cert" (exp (gen) l) B (privk CA))) (send (exp (gen) e)) (recv (exp (gen) (mul ep ep-0))) (send key)) ((recv (enc "cert" (exp (gen) lp) P (privk CA-0))) (recv (enc "cert" (exp (gen) l) B (privk CA-0))) (send (exp (gen) ep)) (recv (exp (gen) (mul e ep-0))) (send key)) ((send (enc "cert-req" P (exp (gen) lp) (privk P)))) ((recv (enc "cert-req" P (exp (gen) lp) (privk P))) (send (enc "cert" (exp (gen) lp) P (privk CA-0)))) ((recv (enc "cert-req" B (exp (gen) l) (privk B))) (send (enc "cert" (exp (gen) l) B (privk CA-0)))) ((send (enc "cert-req" B (exp (gen) l) (privk B)))) ((recv (enc "cert-req" P (exp (gen) lp) (privk P))) (send (enc "cert" (exp (gen) lp) P (privk CA)))) ((recv (enc "cert-req" B (exp (gen) l) (privk B))) (send (enc "cert" (exp (gen) l) B (privk CA))))) (label 47) (parent 39) (unrealized (7 0)) (comment "1 in cohort - 1 not yet seen")) (defskeleton iadh-um (vars (key data) (CA P P-0 name) (lp l e ep expn) (ep-0 expr)) (defstrand init 5 (key key) (A P) (B P-0) (CA CA) (hl (exp (gen) lp)) (he (exp (gen) (mul ep ep-0))) (l l) (e e)) (defstrand init 5 (key key) (A P-0) (B P) (CA CA) (hl (exp (gen) l)) (he (exp (gen) (mul e ep-0))) (l lp) (e ep)) (defstrand ltkgen 1 (P P) (l l)) (defstrand ltkgen 1 (P P-0) (l lp)) (defstrand ca-gen 2 (P P-0) (CA CA) (h (exp (gen) lp))) (defstrand ca-gen 2 (P P) (CA CA) (h (exp (gen) l))) (precedes ((0 2) (1 3)) ((1 2) (0 3)) ((2 0) (5 0)) ((3 0) (4 0)) ((3 0) (5 0)) ((4 1) (0 1)) ((4 1) (1 0)) ((5 1) (0 0)) ((5 1) (1 1))) (fn-of ("principal-of" (P-0 (exp (gen) lp)) (P (exp (gen) l))) (foo ((hash (exp (gen) (mul lp l)) (exp (gen) (mul e ep ep-0))) key))) (neq ((exp (gen) lp) (gen)) ((exp (gen) l) (gen)) ((exp (gen) l) (exp (gen) lp)) ((exp (gen) (mul e ep-0)) (gen)) ((exp (gen) lp) (exp (gen) l)) ((exp (gen) (mul ep ep-0)) (gen))) (non-orig (privk CA) (privk P) (privk P-0)) (uniq-gen lp l e ep) (operation nonce-test (algebra-contracted (e-0 e) (ep-1 ep) (ep-2 (mul e (rec ep) ep-0)) (ep-3 ep-0)) (exp (gen) (mul ep ep-0)) (0 3)) (traces ((recv (enc "cert" (exp (gen) l) P (privk CA))) (recv (enc "cert" (exp (gen) lp) P-0 (privk CA))) (send (exp (gen) e)) (recv (exp (gen) (mul ep ep-0))) (send key)) ((recv (enc "cert" (exp (gen) lp) P-0 (privk CA))) (recv (enc "cert" (exp (gen) l) P (privk CA))) (send (exp (gen) ep)) (recv (exp (gen) (mul e ep-0))) (send key)) ((send (enc "cert-req" P (exp (gen) l) (privk P)))) ((send (enc "cert-req" P-0 (exp (gen) lp) (privk P-0)))) ((recv (enc "cert-req" P-0 (exp (gen) lp) (privk P-0))) (send (enc "cert" (exp (gen) lp) P-0 (privk CA)))) ((recv (enc "cert-req" P (exp (gen) l) (privk P))) (send (enc "cert" (exp (gen) l) P (privk CA))))) (label 48) (parent 40) (unrealized) (comment "1 in cohort - 1 not yet seen")) (defskeleton iadh-um (vars (key data) (CA P P-0 name) (lp l e ep expn) (ep-0 expr)) (defstrand init 5 (key key) (A P) (B P-0) (CA CA) (hl (exp (gen) lp)) (he (exp (gen) (mul ep ep-0))) (l l) (e e)) (defstrand init 5 (key key) (A P-0) (B P) (CA CA) (hl (exp (gen) l)) (he (exp (gen) (mul e ep-0))) (l lp) (e ep)) (defstrand ltkgen 1 (P P) (l l)) (defstrand ltkgen 1 (P P-0) (l lp)) (defstrand ca-gen 2 (P P-0) (CA CA) (h (exp (gen) lp))) (defstrand ca-gen 2 (P P) (CA CA) (h (exp (gen) l))) (defstrand ca-gen 2 (P P-0) (CA CA) (h (exp (gen) lp))) (precedes ((0 2) (1 3)) ((1 2) (0 3)) ((2 0) (5 0)) ((3 0) (4 0)) ((3 0) (5 0)) ((3 0) (6 0)) ((4 1) (1 0)) ((5 1) (0 0)) ((5 1) (1 1)) ((6 1) (0 1))) (fn-of ("principal-of" (P-0 (exp (gen) lp)) (P (exp (gen) l))) (foo ((hash (exp (gen) (mul lp l)) (exp (gen) (mul e ep ep-0))) key))) (neq ((exp (gen) lp) (gen)) ((exp (gen) l) (gen)) ((exp (gen) l) (exp (gen) lp)) ((exp (gen) (mul e ep-0)) (gen)) ((exp (gen) lp) (exp (gen) l)) ((exp (gen) (mul ep ep-0)) (gen))) (non-orig (privk CA) (privk P) (privk P-0)) (uniq-gen lp l e ep) (operation nonce-test (algebra-contracted (e-0 e) (ep-1 ep) (ep-2 (mul e (rec ep) ep-0)) (ep-3 ep-0)) (exp (gen) (mul ep ep-0)) (0 3)) (traces ((recv (enc "cert" (exp (gen) l) P (privk CA))) (recv (enc "cert" (exp (gen) lp) P-0 (privk CA))) (send (exp (gen) e)) (recv (exp (gen) (mul ep ep-0))) (send key)) ((recv (enc "cert" (exp (gen) lp) P-0 (privk CA))) (recv (enc "cert" (exp (gen) l) P (privk CA))) (send (exp (gen) ep)) (recv (exp (gen) (mul e ep-0))) (send key)) ((send (enc "cert-req" P (exp (gen) l) (privk P)))) ((send (enc "cert-req" P-0 (exp (gen) lp) (privk P-0)))) ((recv (enc "cert-req" P-0 (exp (gen) lp) (privk P-0))) (send (enc "cert" (exp (gen) lp) P-0 (privk CA)))) ((recv (enc "cert-req" P (exp (gen) l) (privk P))) (send (enc "cert" (exp (gen) l) P (privk CA)))) ((recv (enc "cert-req" P-0 (exp (gen) lp) (privk P-0))) (send (enc "cert" (exp (gen) lp) P-0 (privk CA))))) (label 49) (parent 41) (unrealized) (comment "1 in cohort - 1 not yet seen")) (defskeleton iadh-um (vars (key data) (CA P P-0 name) (lp l e ep expn) (ep-0 expr)) (defstrand init 5 (key key) (A P) (B P-0) (CA CA) (hl (exp (gen) lp)) (he (exp (gen) (mul ep ep-0))) (l l) (e e)) (defstrand init 5 (key key) (A P-0) (B P) (CA CA) (hl (exp (gen) l)) (he (exp (gen) (mul e ep-0))) (l lp) (e ep)) (defstrand ltkgen 1 (P P) (l l)) (defstrand ltkgen 1 (P P-0) (l lp)) (defstrand ca-gen 2 (P P-0) (CA CA) (h (exp (gen) lp))) (defstrand ca-gen 2 (P P) (CA CA) (h (exp (gen) l))) (defstrand ca-gen 2 (P P) (CA CA) (h (exp (gen) l))) (precedes ((0 2) (1 3)) ((1 2) (0 3)) ((2 0) (5 0)) ((2 0) (6 0)) ((3 0) (4 0)) ((3 0) (5 0)) ((4 1) (0 1)) ((4 1) (1 0)) ((5 1) (1 1)) ((6 1) (0 0))) (fn-of ("principal-of" (P-0 (exp (gen) lp)) (P (exp (gen) l))) (foo ((hash (exp (gen) (mul lp l)) (exp (gen) (mul e ep ep-0))) key))) (neq ((exp (gen) lp) (gen)) ((exp (gen) l) (gen)) ((exp (gen) l) (exp (gen) lp)) ((exp (gen) (mul e ep-0)) (gen)) ((exp (gen) lp) (exp (gen) l)) ((exp (gen) (mul ep ep-0)) (gen))) (non-orig (privk CA) (privk P) (privk P-0)) (uniq-gen lp l e ep) (operation nonce-test (algebra-contracted (e-0 e) (ep-1 ep) (ep-2 (mul e (rec ep) ep-0)) (ep-3 ep-0)) (exp (gen) (mul ep ep-0)) (0 3)) (traces ((recv (enc "cert" (exp (gen) l) P (privk CA))) (recv (enc "cert" (exp (gen) lp) P-0 (privk CA))) (send (exp (gen) e)) (recv (exp (gen) (mul ep ep-0))) (send key)) ((recv (enc "cert" (exp (gen) lp) P-0 (privk CA))) (recv (enc "cert" (exp (gen) l) P (privk CA))) (send (exp (gen) ep)) (recv (exp (gen) (mul e ep-0))) (send key)) ((send (enc "cert-req" P (exp (gen) l) (privk P)))) ((send (enc "cert-req" P-0 (exp (gen) lp) (privk P-0)))) ((recv (enc "cert-req" P-0 (exp (gen) lp) (privk P-0))) (send (enc "cert" (exp (gen) lp) P-0 (privk CA)))) ((recv (enc "cert-req" P (exp (gen) l) (privk P))) (send (enc "cert" (exp (gen) l) P (privk CA)))) ((recv (enc "cert-req" P (exp (gen) l) (privk P))) (send (enc "cert" (exp (gen) l) P (privk CA))))) (label 50) (parent 42) (unrealized) (comment "1 in cohort - 1 not yet seen")) (defskeleton iadh-um (vars (key data) (CA CA-0 P P-0 name) (lp l e ep expn) (ep-0 expr)) (defstrand init 5 (key key) (A P) (B P-0) (CA CA) (hl (exp (gen) lp)) (he (exp (gen) (mul ep ep-0))) (l l) (e e)) (defstrand init 5 (key key) (A P-0) (B P) (CA CA-0) (hl (exp (gen) l)) (he (exp (gen) (mul e ep-0))) (l lp) (e ep)) (defstrand ltkgen 1 (P P) (l l)) (defstrand ltkgen 1 (P P-0) (l lp)) (defstrand ca-gen 2 (P P-0) (CA CA-0) (h (exp (gen) lp))) (defstrand ca-gen 2 (P P) (CA CA-0) (h (exp (gen) l))) (defstrand ca-gen 2 (P P) (CA CA) (h (exp (gen) l))) (defstrand ca-gen 2 (P P-0) (CA CA) (h (exp (gen) lp))) (precedes ((0 2) (1 3)) ((1 2) (0 3)) ((2 0) (5 0)) ((2 0) (6 0)) ((3 0) (4 0)) ((3 0) (5 0)) ((3 0) (7 0)) ((4 1) (1 0)) ((5 1) (1 1)) ((6 1) (0 0)) ((7 1) (0 1))) (fn-of ("principal-of" (P-0 (exp (gen) lp)) (P (exp (gen) l))) (foo ((hash (exp (gen) (mul lp l)) (exp (gen) (mul e ep ep-0))) key))) (neq ((exp (gen) lp) (gen)) ((exp (gen) l) (gen)) ((exp (gen) l) (exp (gen) lp)) ((exp (gen) (mul e ep-0)) (gen)) ((exp (gen) lp) (exp (gen) l)) ((exp (gen) (mul ep ep-0)) (gen))) (non-orig (privk CA) (privk CA-0) (privk P) (privk P-0)) (uniq-gen lp l e ep) (operation nonce-test (algebra-contracted (e-0 e) (ep-1 ep) (ep-2 (mul e (rec ep) ep-0)) (ep-3 ep-0)) (exp (gen) (mul ep ep-0)) (0 3)) (traces ((recv (enc "cert" (exp (gen) l) P (privk CA))) (recv (enc "cert" (exp (gen) lp) P-0 (privk CA))) (send (exp (gen) e)) (recv (exp (gen) (mul ep ep-0))) (send key)) ((recv (enc "cert" (exp (gen) lp) P-0 (privk CA-0))) (recv (enc "cert" (exp (gen) l) P (privk CA-0))) (send (exp (gen) ep)) (recv (exp (gen) (mul e ep-0))) (send key)) ((send (enc "cert-req" P (exp (gen) l) (privk P)))) ((send (enc "cert-req" P-0 (exp (gen) lp) (privk P-0)))) ((recv (enc "cert-req" P-0 (exp (gen) lp) (privk P-0))) (send (enc "cert" (exp (gen) lp) P-0 (privk CA-0)))) ((recv (enc "cert-req" P (exp (gen) l) (privk P))) (send (enc "cert" (exp (gen) l) P (privk CA-0)))) ((recv (enc "cert-req" P (exp (gen) l) (privk P))) (send (enc "cert" (exp (gen) l) P (privk CA)))) ((recv (enc "cert-req" P-0 (exp (gen) lp) (privk P-0))) (send (enc "cert" (exp (gen) lp) P-0 (privk CA))))) (label 51) (parent 43) (unrealized) (comment "1 in cohort - 1 not yet seen")) (defskeleton iadh-um (vars (key data) (B CA P name) (ep lp e l expn) (ep-0 expr)) (defstrand init 5 (key key) (A P) (B B) (CA CA) (hl (exp (gen) l)) (he (exp (gen) (mul ep ep-0))) (l lp) (e e)) (defstrand init 5 (key key) (A P) (B B) (CA CA) (hl (exp (gen) l)) (he (exp (gen) (mul e ep-0))) (l lp) (e ep)) (defstrand ltkgen 1 (P P) (l lp)) (defstrand ca-gen 2 (P P) (CA CA) (h (exp (gen) lp))) (defstrand ca-gen 2 (P B) (CA CA) (h (exp (gen) l))) (defstrand ltkgen 1 (P B) (l l)) (defstrand ca-gen 2 (P B) (CA CA) (h (exp (gen) l))) (precedes ((0 2) (1 3)) ((1 2) (0 3)) ((2 0) (3 0)) ((3 1) (0 0)) ((3 1) (1 0)) ((4 1) (1 1)) ((5 0) (0 1)) ((5 0) (4 0)) ((6 1) (0 1))) (fn-of ("principal-of" (B (exp (gen) l)) (P (exp (gen) lp))) (foo ((hash (exp (gen) (mul lp l)) (exp (gen) (mul ep e ep-0))) key))) (neq ((exp (gen) l) (gen)) ((exp (gen) lp) (gen)) ((exp (gen) l) (exp (gen) lp)) ((exp (gen) (mul e ep-0)) (gen)) ((exp (gen) (mul ep ep-0)) (gen))) (non-orig (privk B) (privk CA) (privk P)) (uniq-gen ep lp e) (operation encryption-test (added-strand ca-gen 2) (enc "cert" (exp (gen) l) B (privk CA)) (0 1)) (traces ((recv (enc "cert" (exp (gen) lp) P (privk CA))) (recv (enc "cert" (exp (gen) l) B (privk CA))) (send (exp (gen) e)) (recv (exp (gen) (mul ep ep-0))) (send key)) ((recv (enc "cert" (exp (gen) lp) P (privk CA))) (recv (enc "cert" (exp (gen) l) B (privk CA))) (send (exp (gen) ep)) (recv (exp (gen) (mul e ep-0))) (send key)) ((send (enc "cert-req" P (exp (gen) lp) (privk P)))) ((recv (enc "cert-req" P (exp (gen) lp) (privk P))) (send (enc "cert" (exp (gen) lp) P (privk CA)))) ((recv (enc "cert-req" B (exp (gen) l) (privk B))) (send (enc "cert" (exp (gen) l) B (privk CA)))) ((send (enc "cert-req" B (exp (gen) l) (privk B)))) ((recv (enc "cert-req" B (exp (gen) l) (privk B))) (send (enc "cert" (exp (gen) l) B (privk CA))))) (label 52) (parent 44) (seen 44) (unrealized (6 0)) (comment "1 in cohort - 0 not yet seen")) (defskeleton iadh-um (vars (key data) (CA B CA-0 P name) (ep lp e expn) (ep-0 expr) (l expn)) (defstrand init 5 (key key) (A P) (B B) (CA CA) (hl (exp (gen) l)) (he (exp (gen) (mul ep ep-0))) (l lp) (e e)) (defstrand init 5 (key key) (A P) (B B) (CA CA-0) (hl (exp (gen) l)) (he (exp (gen) (mul e ep-0))) (l lp) (e ep)) (defstrand ltkgen 1 (P P) (l lp)) (defstrand ca-gen 2 (P P) (CA CA-0) (h (exp (gen) lp))) (defstrand ca-gen 2 (P B) (CA CA-0) (h (exp (gen) l))) (defstrand ltkgen 1 (P B) (l l)) (defstrand ca-gen 2 (P P) (CA CA) (h (exp (gen) lp))) (defstrand ca-gen 2 (P B) (CA CA) (h (exp (gen) l))) (precedes ((0 2) (1 3)) ((1 2) (0 3)) ((2 0) (3 0)) ((2 0) (6 0)) ((3 1) (1 0)) ((4 1) (1 1)) ((5 0) (4 0)) ((5 0) (7 0)) ((6 1) (0 0)) ((7 1) (0 1))) (fn-of ("principal-of" (B (exp (gen) l)) (P (exp (gen) lp))) (foo ((hash (exp (gen) (mul lp l)) (exp (gen) (mul ep e ep-0))) key))) (neq ((exp (gen) l) (gen)) ((exp (gen) lp) (gen)) ((exp (gen) l) (exp (gen) lp)) ((exp (gen) (mul e ep-0)) (gen)) ((exp (gen) (mul ep ep-0)) (gen))) (non-orig (privk CA) (privk B) (privk CA-0) (privk P)) (uniq-gen ep lp e) (operation encryption-test (displaced 8 5 ltkgen 1) (enc "cert-req" B (exp (gen) l) (privk B)) (7 0)) (traces ((recv (enc "cert" (exp (gen) lp) P (privk CA))) (recv (enc "cert" (exp (gen) l) B (privk CA))) (send (exp (gen) e)) (recv (exp (gen) (mul ep ep-0))) (send key)) ((recv (enc "cert" (exp (gen) lp) P (privk CA-0))) (recv (enc "cert" (exp (gen) l) B (privk CA-0))) (send (exp (gen) ep)) (recv (exp (gen) (mul e ep-0))) (send key)) ((send (enc "cert-req" P (exp (gen) lp) (privk P)))) ((recv (enc "cert-req" P (exp (gen) lp) (privk P))) (send (enc "cert" (exp (gen) lp) P (privk CA-0)))) ((recv (enc "cert-req" B (exp (gen) l) (privk B))) (send (enc "cert" (exp (gen) l) B (privk CA-0)))) ((send (enc "cert-req" B (exp (gen) l) (privk B)))) ((recv (enc "cert-req" P (exp (gen) lp) (privk P))) (send (enc "cert" (exp (gen) lp) P (privk CA)))) ((recv (enc "cert-req" B (exp (gen) l) (privk B))) (send (enc "cert" (exp (gen) l) B (privk CA))))) (label 53) (parent 47) (unrealized) (shape) (maps ((0 1 2 2) ((key key) (hl (exp (gen) l)) (he (exp (gen) (mul ep ep-0))) (A P) (B B) (CA CA) (A-0 P) (B-0 B) (CA-0 CA-0) (P P) (P-0 P) (l lp) (lp lp) (e e) (ep ep)))) (origs)) (defskeleton iadh-um (vars (key data) (CA P P-0 name) (lp l e ep expn) (ep-0 expr)) (defstrand init 5 (key key) (A P) (B P-0) (CA CA) (hl (exp (gen) lp)) (he (exp (gen) (mul ep ep-0))) (l l) (e e)) (defstrand init 5 (key key) (A P-0) (B P) (CA CA) (hl (exp (gen) l)) (he (exp (gen) (mul e ep-0))) (l lp) (e ep)) (defstrand ltkgen 1 (P P) (l l)) (defstrand ltkgen 1 (P P-0) (l lp)) (defstrand ca-gen 2 (P P-0) (CA CA) (h (exp (gen) lp))) (defstrand ca-gen 2 (P P) (CA CA) (h (exp (gen) l))) (precedes ((0 2) (1 3)) ((1 2) (0 3)) ((2 0) (5 0)) ((3 0) (0 0)) ((3 0) (4 0)) ((4 1) (0 1)) ((4 1) (1 0)) ((5 1) (0 0)) ((5 1) (1 1))) (fn-of ("principal-of" (P-0 (exp (gen) lp)) (P (exp (gen) l))) (foo ((hash (exp (gen) (mul lp l)) (exp (gen) (mul e ep ep-0))) key))) (neq ((exp (gen) lp) (gen)) ((exp (gen) l) (gen)) ((exp (gen) l) (exp (gen) lp)) ((exp (gen) (mul e ep-0)) (gen)) ((exp (gen) lp) (exp (gen) l)) ((exp (gen) (mul ep ep-0)) (gen))) (non-orig (privk CA) (privk P) (privk P-0)) (uniq-gen lp l e ep) (operation generalization weakened ((3 0) (5 0))) (traces ((recv (enc "cert" (exp (gen) l) P (privk CA))) (recv (enc "cert" (exp (gen) lp) P-0 (privk CA))) (send (exp (gen) e)) (recv (exp (gen) (mul ep ep-0))) (send key)) ((recv (enc "cert" (exp (gen) lp) P-0 (privk CA))) (recv (enc "cert" (exp (gen) l) P (privk CA))) (send (exp (gen) ep)) (recv (exp (gen) (mul e ep-0))) (send key)) ((send (enc "cert-req" P (exp (gen) l) (privk P)))) ((send (enc "cert-req" P-0 (exp (gen) lp) (privk P-0)))) ((recv (enc "cert-req" P-0 (exp (gen) lp) (privk P-0))) (send (enc "cert" (exp (gen) lp) P-0 (privk CA)))) ((recv (enc "cert-req" P (exp (gen) l) (privk P))) (send (enc "cert" (exp (gen) l) P (privk CA))))) (label 54) (parent 48) (unrealized) (comment "1 in cohort - 1 not yet seen")) (defskeleton iadh-um (vars (key data) (CA P P-0 name) (lp l e ep expn) (ep-0 expr)) (defstrand init 5 (key key) (A P) (B P-0) (CA CA) (hl (exp (gen) lp)) (he (exp (gen) (mul ep ep-0))) (l l) (e e)) (defstrand init 5 (key key) (A P-0) (B P) (CA CA) (hl (exp (gen) l)) (he (exp (gen) (mul e ep-0))) (l lp) (e ep)) (defstrand ltkgen 1 (P P) (l l)) (defstrand ltkgen 1 (P P-0) (l lp)) (defstrand ca-gen 2 (P P-0) (CA CA) (h (exp (gen) lp))) (defstrand ca-gen 2 (P P) (CA CA) (h (exp (gen) l))) (defstrand ca-gen 2 (P P-0) (CA CA) (h (exp (gen) lp))) (precedes ((0 2) (1 3)) ((1 2) (0 3)) ((2 0) (5 0)) ((3 0) (0 0)) ((3 0) (4 0)) ((3 0) (6 0)) ((4 1) (1 0)) ((5 1) (0 0)) ((5 1) (1 1)) ((6 1) (0 1))) (fn-of ("principal-of" (P-0 (exp (gen) lp)) (P (exp (gen) l))) (foo ((hash (exp (gen) (mul lp l)) (exp (gen) (mul e ep ep-0))) key))) (neq ((exp (gen) lp) (gen)) ((exp (gen) l) (gen)) ((exp (gen) l) (exp (gen) lp)) ((exp (gen) (mul e ep-0)) (gen)) ((exp (gen) lp) (exp (gen) l)) ((exp (gen) (mul ep ep-0)) (gen))) (non-orig (privk CA) (privk P) (privk P-0)) (uniq-gen lp l e ep) (operation generalization weakened ((3 0) (5 0))) (traces ((recv (enc "cert" (exp (gen) l) P (privk CA))) (recv (enc "cert" (exp (gen) lp) P-0 (privk CA))) (send (exp (gen) e)) (recv (exp (gen) (mul ep ep-0))) (send key)) ((recv (enc "cert" (exp (gen) lp) P-0 (privk CA))) (recv (enc "cert" (exp (gen) l) P (privk CA))) (send (exp (gen) ep)) (recv (exp (gen) (mul e ep-0))) (send key)) ((send (enc "cert-req" P (exp (gen) l) (privk P)))) ((send (enc "cert-req" P-0 (exp (gen) lp) (privk P-0)))) ((recv (enc "cert-req" P-0 (exp (gen) lp) (privk P-0))) (send (enc "cert" (exp (gen) lp) P-0 (privk CA)))) ((recv (enc "cert-req" P (exp (gen) l) (privk P))) (send (enc "cert" (exp (gen) l) P (privk CA)))) ((recv (enc "cert-req" P-0 (exp (gen) lp) (privk P-0))) (send (enc "cert" (exp (gen) lp) P-0 (privk CA))))) (label 55) (parent 49) (seen 56) (unrealized) (comment "1 in cohort - 0 not yet seen")) (defskeleton iadh-um (vars (key data) (CA P P-0 name) (lp l e ep expn) (ep-0 expr)) (defstrand init 5 (key key) (A P) (B P-0) (CA CA) (hl (exp (gen) lp)) (he (exp (gen) (mul ep ep-0))) (l l) (e e)) (defstrand init 5 (key key) (A P-0) (B P) (CA CA) (hl (exp (gen) l)) (he (exp (gen) (mul e ep-0))) (l lp) (e ep)) (defstrand ltkgen 1 (P P) (l l)) (defstrand ltkgen 1 (P P-0) (l lp)) (defstrand ca-gen 2 (P P-0) (CA CA) (h (exp (gen) lp))) (defstrand ca-gen 2 (P P) (CA CA) (h (exp (gen) l))) (defstrand ca-gen 2 (P P) (CA CA) (h (exp (gen) l))) (precedes ((0 2) (1 3)) ((1 2) (0 3)) ((2 0) (5 0)) ((2 0) (6 0)) ((3 0) (4 0)) ((4 1) (0 1)) ((4 1) (1 0)) ((5 1) (1 1)) ((6 1) (0 0))) (fn-of ("principal-of" (P-0 (exp (gen) lp)) (P (exp (gen) l))) (foo ((hash (exp (gen) (mul lp l)) (exp (gen) (mul e ep ep-0))) key))) (neq ((exp (gen) lp) (gen)) ((exp (gen) l) (gen)) ((exp (gen) l) (exp (gen) lp)) ((exp (gen) (mul e ep-0)) (gen)) ((exp (gen) lp) (exp (gen) l)) ((exp (gen) (mul ep ep-0)) (gen))) (non-orig (privk CA) (privk P) (privk P-0)) (uniq-gen lp l e ep) (operation generalization weakened ((3 0) (5 0))) (traces ((recv (enc "cert" (exp (gen) l) P (privk CA))) (recv (enc "cert" (exp (gen) lp) P-0 (privk CA))) (send (exp (gen) e)) (recv (exp (gen) (mul ep ep-0))) (send key)) ((recv (enc "cert" (exp (gen) lp) P-0 (privk CA))) (recv (enc "cert" (exp (gen) l) P (privk CA))) (send (exp (gen) ep)) (recv (exp (gen) (mul e ep-0))) (send key)) ((send (enc "cert-req" P (exp (gen) l) (privk P)))) ((send (enc "cert-req" P-0 (exp (gen) lp) (privk P-0)))) ((recv (enc "cert-req" P-0 (exp (gen) lp) (privk P-0))) (send (enc "cert" (exp (gen) lp) P-0 (privk CA)))) ((recv (enc "cert-req" P (exp (gen) l) (privk P))) (send (enc "cert" (exp (gen) l) P (privk CA)))) ((recv (enc "cert-req" P (exp (gen) l) (privk P))) (send (enc "cert" (exp (gen) l) P (privk CA))))) (label 56) (parent 50) (unrealized) (shape) (maps ((0 1 2 3) ((key key) (hl (exp (gen) lp)) (he (exp (gen) (mul ep ep-0))) (A P) (B P-0) (CA CA) (A-0 P-0) (B-0 P) (CA-0 CA) (P P) (P-0 P-0) (l l) (lp lp) (e e) (ep ep)))) (origs)) (defskeleton iadh-um (vars (key data) (CA CA-0 P P-0 name) (lp l e ep expn) (ep-0 expr)) (defstrand init 5 (key key) (A P) (B P-0) (CA CA) (hl (exp (gen) lp)) (he (exp (gen) (mul ep ep-0))) (l l) (e e)) (defstrand init 5 (key key) (A P-0) (B P) (CA CA-0) (hl (exp (gen) l)) (he (exp (gen) (mul e ep-0))) (l lp) (e ep)) (defstrand ltkgen 1 (P P) (l l)) (defstrand ltkgen 1 (P P-0) (l lp)) (defstrand ca-gen 2 (P P-0) (CA CA-0) (h (exp (gen) lp))) (defstrand ca-gen 2 (P P) (CA CA-0) (h (exp (gen) l))) (defstrand ca-gen 2 (P P) (CA CA) (h (exp (gen) l))) (defstrand ca-gen 2 (P P-0) (CA CA) (h (exp (gen) lp))) (precedes ((0 2) (1 3)) ((1 2) (0 3)) ((2 0) (5 0)) ((2 0) (6 0)) ((3 0) (4 0)) ((3 0) (7 0)) ((4 1) (1 0)) ((5 1) (1 1)) ((6 1) (0 0)) ((7 1) (0 1))) (fn-of ("principal-of" (P-0 (exp (gen) lp)) (P (exp (gen) l))) (foo ((hash (exp (gen) (mul lp l)) (exp (gen) (mul e ep ep-0))) key))) (neq ((exp (gen) lp) (gen)) ((exp (gen) l) (gen)) ((exp (gen) l) (exp (gen) lp)) ((exp (gen) (mul e ep-0)) (gen)) ((exp (gen) lp) (exp (gen) l)) ((exp (gen) (mul ep ep-0)) (gen))) (non-orig (privk CA) (privk CA-0) (privk P) (privk P-0)) (uniq-gen lp l e ep) (operation generalization weakened ((3 0) (5 0))) (traces ((recv (enc "cert" (exp (gen) l) P (privk CA))) (recv (enc "cert" (exp (gen) lp) P-0 (privk CA))) (send (exp (gen) e)) (recv (exp (gen) (mul ep ep-0))) (send key)) ((recv (enc "cert" (exp (gen) lp) P-0 (privk CA-0))) (recv (enc "cert" (exp (gen) l) P (privk CA-0))) (send (exp (gen) ep)) (recv (exp (gen) (mul e ep-0))) (send key)) ((send (enc "cert-req" P (exp (gen) l) (privk P)))) ((send (enc "cert-req" P-0 (exp (gen) lp) (privk P-0)))) ((recv (enc "cert-req" P-0 (exp (gen) lp) (privk P-0))) (send (enc "cert" (exp (gen) lp) P-0 (privk CA-0)))) ((recv (enc "cert-req" P (exp (gen) l) (privk P))) (send (enc "cert" (exp (gen) l) P (privk CA-0)))) ((recv (enc "cert-req" P (exp (gen) l) (privk P))) (send (enc "cert" (exp (gen) l) P (privk CA)))) ((recv (enc "cert-req" P-0 (exp (gen) lp) (privk P-0))) (send (enc "cert" (exp (gen) lp) P-0 (privk CA))))) (label 57) (parent 51) (unrealized) (shape) (maps ((0 1 2 3) ((key key) (hl (exp (gen) lp)) (he (exp (gen) (mul ep ep-0))) (A P) (B P-0) (CA CA) (A-0 P-0) (B-0 P) (CA-0 CA-0) (P P) (P-0 P-0) (l l) (lp lp) (e e) (ep ep)))) (origs)) (defskeleton iadh-um (vars (key data) (CA P P-0 name) (lp l e ep expn) (ep-0 expr)) (defstrand init 5 (key key) (A P) (B P-0) (CA CA) (hl (exp (gen) lp)) (he (exp (gen) (mul ep ep-0))) (l l) (e e)) (defstrand init 5 (key key) (A P-0) (B P) (CA CA) (hl (exp (gen) l)) (he (exp (gen) (mul e ep-0))) (l lp) (e ep)) (defstrand ltkgen 1 (P P) (l l)) (defstrand ltkgen 1 (P P-0) (l lp)) (defstrand ca-gen 2 (P P-0) (CA CA) (h (exp (gen) lp))) (defstrand ca-gen 2 (P P) (CA CA) (h (exp (gen) l))) (precedes ((0 2) (1 3)) ((1 2) (0 3)) ((2 0) (5 0)) ((3 0) (4 0)) ((4 1) (0 1)) ((4 1) (1 0)) ((5 1) (0 0)) ((5 1) (1 1))) (fn-of ("principal-of" (P-0 (exp (gen) lp)) (P (exp (gen) l))) (foo ((hash (exp (gen) (mul lp l)) (exp (gen) (mul e ep ep-0))) key))) (neq ((exp (gen) lp) (gen)) ((exp (gen) l) (gen)) ((exp (gen) l) (exp (gen) lp)) ((exp (gen) (mul e ep-0)) (gen)) ((exp (gen) lp) (exp (gen) l)) ((exp (gen) (mul ep ep-0)) (gen))) (non-orig (privk CA) (privk P) (privk P-0)) (uniq-gen lp l e ep) (operation generalization weakened ((3 0) (0 0))) (traces ((recv (enc "cert" (exp (gen) l) P (privk CA))) (recv (enc "cert" (exp (gen) lp) P-0 (privk CA))) (send (exp (gen) e)) (recv (exp (gen) (mul ep ep-0))) (send key)) ((recv (enc "cert" (exp (gen) lp) P-0 (privk CA))) (recv (enc "cert" (exp (gen) l) P (privk CA))) (send (exp (gen) ep)) (recv (exp (gen) (mul e ep-0))) (send key)) ((send (enc "cert-req" P (exp (gen) l) (privk P)))) ((send (enc "cert-req" P-0 (exp (gen) lp) (privk P-0)))) ((recv (enc "cert-req" P-0 (exp (gen) lp) (privk P-0))) (send (enc "cert" (exp (gen) lp) P-0 (privk CA)))) ((recv (enc "cert-req" P (exp (gen) l) (privk P))) (send (enc "cert" (exp (gen) l) P (privk CA))))) (label 58) (parent 54) (unrealized) (shape) (maps ((0 1 2 3) ((key key) (hl (exp (gen) lp)) (he (exp (gen) (mul ep ep-0))) (A P) (B P-0) (CA CA) (A-0 P-0) (B-0 P) (CA-0 CA) (P P) (P-0 P-0) (l l) (lp lp) (e e) (ep ep)))) (origs)) (comment "Nothing left to do") (defprotocol iadh-um diffie-hellman (defrole init (vars (l e expn) (hl he base) (A B CA name) (key data)) (trace (recv (enc "cert" (exp (gen) l) A (privk CA))) (recv (enc "cert" hl B (privk CA))) (send (exp (gen) e)) (recv he) (send key)) (non-orig (privk CA)) (fn-of (foo ((hash (exp hl l) (exp he e)) key))) (neq (he (gen)) (hl (exp (gen) l)))) (defrole ltkgen (vars (P name) (l expn)) (trace (send (enc "cert-req" P (exp (gen) l) (privk P)))) (fn-of ("principal-of" (P (exp (gen) l))))) (defrole ca-gen (vars (P CA name) (h base)) (trace (recv (enc "cert-req" P h (privk P))) (send (enc "cert" h P (privk CA)))) (non-orig (privk P)) (fn-of ("principal-of" (P h))) (neq (h (gen))))) (defskeleton iadh-um (vars (A B CA P P-0 name) (he base) (e l lp expn)) (defstrand init 4 (A A) (B B) (CA CA) (hl (exp (gen) lp)) (he he) (l l) (e e)) (defstrand ltkgen 1 (P P) (l l)) (defstrand ltkgen 1 (P P-0) (l lp)) (deflistener (hash (exp (gen) (mul l lp)) (exp he e))) (fn-of ("principal-of" (P-0 (exp (gen) lp)) (P (exp (gen) l)))) (neq ((exp (gen) lp) (exp (gen) l)) (he (gen))) (non-orig (privk CA)) (uniq-gen e l lp) (traces ((recv (enc "cert" (exp (gen) l) A (privk CA))) (recv (enc "cert" (exp (gen) lp) B (privk CA))) (send (exp (gen) e)) (recv he)) ((send (enc "cert-req" P (exp (gen) l) (privk P)))) ((send (enc "cert-req" P-0 (exp (gen) lp) (privk P-0)))) ((recv (hash (exp (gen) (mul l lp)) (exp he e))) (send (hash (exp (gen) (mul l lp)) (exp he e))))) (label 59) (unrealized (0 0) (0 1) (3 0)) (preskeleton) (comment "Not a skeleton")) (defskeleton iadh-um (vars (A B CA P P-0 name) (he base) (e l lp expn)) (defstrand init 4 (A A) (B B) (CA CA) (hl (exp (gen) lp)) (he he) (l l) (e e)) (defstrand ltkgen 1 (P P) (l l)) (defstrand ltkgen 1 (P P-0) (l lp)) (deflistener (hash (exp (gen) (mul l lp)) (exp he e))) (precedes ((0 2) (3 0)) ((1 0) (0 0)) ((2 0) (0 1))) (fn-of ("principal-of" (P-0 (exp (gen) lp)) (P (exp (gen) l)))) (neq ((exp (gen) lp) (exp (gen) l)) (he (gen))) (non-orig (privk CA)) (uniq-gen e l lp) (traces ((recv (enc "cert" (exp (gen) l) A (privk CA))) (recv (enc "cert" (exp (gen) lp) B (privk CA))) (send (exp (gen) e)) (recv he)) ((send (enc "cert-req" P (exp (gen) l) (privk P)))) ((send (enc "cert-req" P-0 (exp (gen) lp) (privk P-0)))) ((recv (hash (exp (gen) (mul l lp)) (exp he e))) (send (hash (exp (gen) (mul l lp)) (exp he e))))) (label 60) (parent 59) (unrealized (0 0) (0 1) (3 0)) (origs) (comment "1 in cohort - 1 not yet seen")) (defskeleton iadh-um (vars (A B CA P P-0 name) (he base) (e l lp expn)) (defstrand init 4 (A A) (B B) (CA CA) (hl (exp (gen) lp)) (he he) (l l) (e e)) (defstrand ltkgen 1 (P P) (l l)) (defstrand ltkgen 1 (P P-0) (l lp)) (deflistener (hash (exp (gen) (mul l lp)) (exp he e))) (deflistener (cat (exp (gen) (mul l lp)) (exp he e))) (precedes ((0 2) (4 0)) ((1 0) (0 0)) ((2 0) (0 1)) ((4 1) (3 0))) (fn-of ("principal-of" (P-0 (exp (gen) lp)) (P (exp (gen) l)))) (neq ((exp (gen) lp) (exp (gen) l)) (he (gen))) (non-orig (privk CA)) (uniq-gen e l lp) (operation encryption-test (added-listener (cat (exp (gen) (mul l lp)) (exp he e))) (hash (exp (gen) (mul l lp)) (exp he e)) (3 0)) (traces ((recv (enc "cert" (exp (gen) l) A (privk CA))) (recv (enc "cert" (exp (gen) lp) B (privk CA))) (send (exp (gen) e)) (recv he)) ((send (enc "cert-req" P (exp (gen) l) (privk P)))) ((send (enc "cert-req" P-0 (exp (gen) lp) (privk P-0)))) ((recv (hash (exp (gen) (mul l lp)) (exp he e))) (send (hash (exp (gen) (mul l lp)) (exp he e)))) ((recv (cat (exp (gen) (mul l lp)) (exp he e))) (send (cat (exp (gen) (mul l lp)) (exp he e))))) (label 61) (parent 60) (unrealized (0 0) (0 1) (4 0)) (comment "empty cohort")) (comment "Nothing left to do") (defprotocol iadh-um diffie-hellman (defrole init (vars (l e expn) (hl he base) (A B CA name) (key data)) (trace (recv (enc "cert" (exp (gen) l) A (privk CA))) (recv (enc "cert" hl B (privk CA))) (send (exp (gen) e)) (recv he) (send key)) (non-orig (privk CA)) (fn-of (foo ((hash (exp hl l) (exp he e)) key))) (neq (he (gen)) (hl (exp (gen) l)))) (defrole ltkgen (vars (P name) (l expn)) (trace (send (enc "cert-req" P (exp (gen) l) (privk P)))) (fn-of ("principal-of" (P (exp (gen) l))))) (defrole ca-gen (vars (P CA name) (h base)) (trace (recv (enc "cert-req" P h (privk P))) (send (enc "cert" h P (privk CA)))) (non-orig (privk P)) (fn-of ("principal-of" (P h))) (neq (h (gen))))) (defskeleton iadh-um (vars (A B CA P P-0 name) (he base) (e l lp expn)) (defstrand init 4 (A A) (B B) (CA CA) (hl (exp (gen) lp)) (he he) (l l) (e e)) (defstrand ltkgen 1 (P P) (l l)) (defstrand ltkgen 1 (P P-0) (l lp)) (deflistener (hash (exp (gen) (mul l lp)) (exp he e))) (fn-of ("principal-of" (P-0 (exp (gen) lp)) (P (exp (gen) l)))) (neq ((exp (gen) lp) (exp (gen) l)) (he (gen))) (non-orig (privk CA)) (uniq-gen l lp) (traces ((recv (enc "cert" (exp (gen) l) A (privk CA))) (recv (enc "cert" (exp (gen) lp) B (privk CA))) (send (exp (gen) e)) (recv he)) ((send (enc "cert-req" P (exp (gen) l) (privk P)))) ((send (enc "cert-req" P-0 (exp (gen) lp) (privk P-0)))) ((recv (hash (exp (gen) (mul l lp)) (exp he e))) (send (hash (exp (gen) (mul l lp)) (exp he e))))) (label 62) (unrealized (0 0) (0 1) (3 0)) (preskeleton) (comment "Not a skeleton")) (defskeleton iadh-um (vars (A B CA P P-0 name) (he base) (e l lp expn)) (defstrand init 4 (A A) (B B) (CA CA) (hl (exp (gen) lp)) (he he) (l l) (e e)) (defstrand ltkgen 1 (P P) (l l)) (defstrand ltkgen 1 (P P-0) (l lp)) (deflistener (hash (exp (gen) (mul l lp)) (exp he e))) (precedes ((1 0) (0 0)) ((1 0) (3 0)) ((2 0) (0 1)) ((2 0) (3 0))) (fn-of ("principal-of" (P-0 (exp (gen) lp)) (P (exp (gen) l)))) (neq ((exp (gen) lp) (exp (gen) l)) (he (gen))) (non-orig (privk CA)) (uniq-gen l lp) (traces ((recv (enc "cert" (exp (gen) l) A (privk CA))) (recv (enc "cert" (exp (gen) lp) B (privk CA))) (send (exp (gen) e)) (recv he)) ((send (enc "cert-req" P (exp (gen) l) (privk P)))) ((send (enc "cert-req" P-0 (exp (gen) lp) (privk P-0)))) ((recv (hash (exp (gen) (mul l lp)) (exp he e))) (send (hash (exp (gen) (mul l lp)) (exp he e))))) (label 63) (parent 62) (unrealized (0 0) (0 1) (3 0)) (origs) (comment "1 in cohort - 1 not yet seen")) (defskeleton iadh-um (vars (A B CA P P-0 name) (he base) (e l lp expn)) (defstrand init 4 (A A) (B B) (CA CA) (hl (exp (gen) lp)) (he he) (l l) (e e)) (defstrand ltkgen 1 (P P) (l l)) (defstrand ltkgen 1 (P P-0) (l lp)) (deflistener (hash (exp (gen) (mul l lp)) (exp he e))) (deflistener (cat (exp (gen) (mul l lp)) (exp he e))) (precedes ((1 0) (0 0)) ((1 0) (4 0)) ((2 0) (0 1)) ((2 0) (4 0)) ((4 1) (3 0))) (fn-of ("principal-of" (P-0 (exp (gen) lp)) (P (exp (gen) l)))) (neq ((exp (gen) lp) (exp (gen) l)) (he (gen))) (non-orig (privk CA)) (uniq-gen l lp) (operation encryption-test (added-listener (cat (exp (gen) (mul l lp)) (exp he e))) (hash (exp (gen) (mul l lp)) (exp he e)) (3 0)) (traces ((recv (enc "cert" (exp (gen) l) A (privk CA))) (recv (enc "cert" (exp (gen) lp) B (privk CA))) (send (exp (gen) e)) (recv he)) ((send (enc "cert-req" P (exp (gen) l) (privk P)))) ((send (enc "cert-req" P-0 (exp (gen) lp) (privk P-0)))) ((recv (hash (exp (gen) (mul l lp)) (exp he e))) (send (hash (exp (gen) (mul l lp)) (exp he e)))) ((recv (cat (exp (gen) (mul l lp)) (exp he e))) (send (cat (exp (gen) (mul l lp)) (exp he e))))) (label 64) (parent 63) (unrealized (0 0) (0 1) (4 0)) (comment "empty cohort")) (comment "Nothing left to do") (defprotocol iadh-um diffie-hellman (defrole init (vars (l e expn) (hl he base) (A B CA name) (key data)) (trace (recv (enc "cert" (exp (gen) l) A (privk CA))) (recv (enc "cert" hl B (privk CA))) (send (exp (gen) e)) (recv he) (send key)) (non-orig (privk CA)) (fn-of (foo ((hash (exp hl l) (exp he e)) key))) (neq (he (gen)) (hl (exp (gen) l)))) (defrole ltkgen (vars (P name) (l expn)) (trace (send (enc "cert-req" P (exp (gen) l) (privk P)))) (fn-of ("principal-of" (P (exp (gen) l))))) (defrole ca-gen (vars (P CA name) (h base)) (trace (recv (enc "cert-req" P h (privk P))) (send (enc "cert" h P (privk CA)))) (non-orig (privk P)) (fn-of ("principal-of" (P h))) (neq (h (gen))))) (defskeleton iadh-um (vars (A B CA P name) (he base) (e l lp l-0 expn)) (defstrand init 4 (A A) (B B) (CA CA) (hl (exp (gen) lp)) (he he) (l l-0) (e e)) (defstrand ltkgen 1 (P P) (l lp)) (deflistener (hash (exp (gen) (mul l lp)) (exp he e))) (fn-of ("principal-of" (P (exp (gen) lp)))) (neq ((exp (gen) lp) (exp (gen) l-0)) (he (gen))) (non-orig (privk CA)) (uniq-gen e lp) (traces ((recv (enc "cert" (exp (gen) l-0) A (privk CA))) (recv (enc "cert" (exp (gen) lp) B (privk CA))) (send (exp (gen) e)) (recv he)) ((send (enc "cert-req" P (exp (gen) lp) (privk P)))) ((recv (hash (exp (gen) (mul l lp)) (exp he e))) (send (hash (exp (gen) (mul l lp)) (exp he e))))) (label 65) (unrealized (0 0) (0 1) (2 0)) (preskeleton) (comment "Not a skeleton")) (defskeleton iadh-um (vars (A B CA P name) (he base) (e l lp l-0 expn)) (defstrand init 4 (A A) (B B) (CA CA) (hl (exp (gen) lp)) (he he) (l l-0) (e e)) (defstrand ltkgen 1 (P P) (l lp)) (deflistener (hash (exp (gen) (mul l lp)) (exp he e))) (precedes ((0 2) (2 0)) ((1 0) (0 1))) (fn-of ("principal-of" (P (exp (gen) lp)))) (neq ((exp (gen) lp) (exp (gen) l-0)) (he (gen))) (non-orig (privk CA)) (uniq-gen e lp) (traces ((recv (enc "cert" (exp (gen) l-0) A (privk CA))) (recv (enc "cert" (exp (gen) lp) B (privk CA))) (send (exp (gen) e)) (recv he)) ((send (enc "cert-req" P (exp (gen) lp) (privk P)))) ((recv (hash (exp (gen) (mul l lp)) (exp he e))) (send (hash (exp (gen) (mul l lp)) (exp he e))))) (label 66) (parent 65) (unrealized (0 0) (0 1) (2 0)) (origs) (comment "1 in cohort - 1 not yet seen")) (defskeleton iadh-um (vars (A B CA P name) (he base) (e l lp l-0 expn)) (defstrand init 4 (A A) (B B) (CA CA) (hl (exp (gen) lp)) (he he) (l l-0) (e e)) (defstrand ltkgen 1 (P P) (l lp)) (deflistener (hash (exp (gen) (mul l lp)) (exp he e))) (deflistener (cat (exp (gen) (mul l lp)) (exp he e))) (precedes ((0 2) (3 0)) ((1 0) (0 1)) ((3 1) (2 0))) (fn-of ("principal-of" (P (exp (gen) lp)))) (neq ((exp (gen) lp) (exp (gen) l-0)) (he (gen))) (non-orig (privk CA)) (uniq-gen e lp) (operation encryption-test (added-listener (cat (exp (gen) (mul l lp)) (exp he e))) (hash (exp (gen) (mul l lp)) (exp he e)) (2 0)) (traces ((recv (enc "cert" (exp (gen) l-0) A (privk CA))) (recv (enc "cert" (exp (gen) lp) B (privk CA))) (send (exp (gen) e)) (recv he)) ((send (enc "cert-req" P (exp (gen) lp) (privk P)))) ((recv (hash (exp (gen) (mul l lp)) (exp he e))) (send (hash (exp (gen) (mul l lp)) (exp he e)))) ((recv (cat (exp (gen) (mul l lp)) (exp he e))) (send (cat (exp (gen) (mul l lp)) (exp he e))))) (label 67) (parent 66) (unrealized (0 0) (0 1) (3 0)) (comment "1 in cohort - 1 not yet seen")) (defskeleton iadh-um (vars (A B CA P name) (e l lp l-0 expn) (lp-0 expr)) (defstrand init 4 (A A) (B B) (CA CA) (hl (exp (gen) lp)) (he (exp (gen) (mul (rec e) lp lp-0))) (l l-0) (e e)) (defstrand ltkgen 1 (P P) (l lp)) (deflistener (hash (exp (gen) (mul l lp)) (exp (gen) (mul lp lp-0)))) (deflistener (cat (exp (gen) (mul l lp)) (exp (gen) (mul lp lp-0)))) (precedes ((0 2) (3 0)) ((1 0) (0 1)) ((3 1) (2 0))) (fn-of ("principal-of" (P (exp (gen) lp)))) (neq ((exp (gen) lp) (exp (gen) l-0)) ((exp (gen) (mul (rec e) lp lp-0)) (gen))) (non-orig (privk CA)) (uniq-gen e lp) (operation nonce-test (algebra-contracted (he (exp (gen) (mul (rec e) lp lp-0)))) (exp (gen) (mul lp lp-0)) (3 0) (exp (gen) e)) (traces ((recv (enc "cert" (exp (gen) l-0) A (privk CA))) (recv (enc "cert" (exp (gen) lp) B (privk CA))) (send (exp (gen) e)) (recv (exp (gen) (mul (rec e) lp lp-0)))) ((send (enc "cert-req" P (exp (gen) lp) (privk P)))) ((recv (hash (exp (gen) (mul l lp)) (exp (gen) (mul lp lp-0)))) (send (hash (exp (gen) (mul l lp)) (exp (gen) (mul lp lp-0))))) ((recv (cat (exp (gen) (mul l lp)) (exp (gen) (mul lp lp-0)))) (send (cat (exp (gen) (mul l lp)) (exp (gen) (mul lp lp-0)))))) (label 68) (parent 67) (unrealized (0 0) (0 1) (0 3)) (comment "1 in cohort - 1 not yet seen")) (defskeleton iadh-um (vars (A B CA P name) (e l lp l-0 expn) (lp-0 expr)) (defstrand init 4 (A A) (B B) (CA CA) (hl (exp (gen) lp)) (he (exp (gen) (mul (rec e) lp lp-0))) (l l-0) (e e)) (defstrand ltkgen 1 (P P) (l lp)) (deflistener (hash (exp (gen) (mul l lp)) (exp (gen) (mul lp lp-0)))) (deflistener (cat (exp (gen) (mul l lp)) (exp (gen) (mul lp lp-0)))) (defstrand ca-gen 2 (P A) (CA CA) (h (exp (gen) l-0))) (precedes ((0 2) (3 0)) ((1 0) (0 1)) ((3 1) (2 0)) ((4 1) (0 0))) (fn-of ("principal-of" (A (exp (gen) l-0)) (P (exp (gen) lp)))) (neq ((exp (gen) l-0) (gen)) ((exp (gen) lp) (exp (gen) l-0)) ((exp (gen) (mul (rec e) lp lp-0)) (gen))) (non-orig (privk A) (privk CA)) (uniq-gen e lp) (operation encryption-test (added-strand ca-gen 2) (enc "cert" (exp (gen) l-0) A (privk CA)) (0 0)) (traces ((recv (enc "cert" (exp (gen) l-0) A (privk CA))) (recv (enc "cert" (exp (gen) lp) B (privk CA))) (send (exp (gen) e)) (recv (exp (gen) (mul (rec e) lp lp-0)))) ((send (enc "cert-req" P (exp (gen) lp) (privk P)))) ((recv (hash (exp (gen) (mul l lp)) (exp (gen) (mul lp lp-0)))) (send (hash (exp (gen) (mul l lp)) (exp (gen) (mul lp lp-0))))) ((recv (cat (exp (gen) (mul l lp)) (exp (gen) (mul lp lp-0)))) (send (cat (exp (gen) (mul l lp)) (exp (gen) (mul lp lp-0))))) ((recv (enc "cert-req" A (exp (gen) l-0) (privk A))) (send (enc "cert" (exp (gen) l-0) A (privk CA))))) (label 69) (parent 68) (unrealized (0 1) (0 3) (4 0)) (comment "1 in cohort - 1 not yet seen")) (defskeleton iadh-um (vars (A B CA P name) (e l lp expn) (lp-0 expr) (l-0 expn)) (defstrand init 4 (A A) (B B) (CA CA) (hl (exp (gen) lp)) (he (exp (gen) (mul (rec e) lp lp-0))) (l l-0) (e e)) (defstrand ltkgen 1 (P P) (l lp)) (deflistener (hash (exp (gen) (mul l lp)) (exp (gen) (mul lp lp-0)))) (deflistener (cat (exp (gen) (mul l lp)) (exp (gen) (mul lp lp-0)))) (defstrand ca-gen 2 (P A) (CA CA) (h (exp (gen) l-0))) (defstrand ltkgen 1 (P A) (l l-0)) (precedes ((0 2) (3 0)) ((1 0) (0 1)) ((3 1) (2 0)) ((4 1) (0 0)) ((5 0) (4 0))) (fn-of ("principal-of" (A (exp (gen) l-0)) (P (exp (gen) lp)))) (neq ((exp (gen) l-0) (gen)) ((exp (gen) lp) (exp (gen) l-0)) ((exp (gen) (mul (rec e) lp lp-0)) (gen))) (non-orig (privk A) (privk CA)) (uniq-gen e lp) (operation encryption-test (added-strand ltkgen 1) (enc "cert-req" A (exp (gen) l-0) (privk A)) (4 0)) (traces ((recv (enc "cert" (exp (gen) l-0) A (privk CA))) (recv (enc "cert" (exp (gen) lp) B (privk CA))) (send (exp (gen) e)) (recv (exp (gen) (mul (rec e) lp lp-0)))) ((send (enc "cert-req" P (exp (gen) lp) (privk P)))) ((recv (hash (exp (gen) (mul l lp)) (exp (gen) (mul lp lp-0)))) (send (hash (exp (gen) (mul l lp)) (exp (gen) (mul lp lp-0))))) ((recv (cat (exp (gen) (mul l lp)) (exp (gen) (mul lp lp-0)))) (send (cat (exp (gen) (mul l lp)) (exp (gen) (mul lp lp-0))))) ((recv (enc "cert-req" A (exp (gen) l-0) (privk A))) (send (enc "cert" (exp (gen) l-0) A (privk CA)))) ((send (enc "cert-req" A (exp (gen) l-0) (privk A))))) (label 70) (parent 69) (unrealized (0 1) (0 3)) (comment "1 in cohort - 1 not yet seen")) (defskeleton iadh-um (vars (A CA P name) (e l lp expn) (lp-0 expr) (l-0 expn)) (defstrand init 4 (A A) (B P) (CA CA) (hl (exp (gen) lp)) (he (exp (gen) (mul (rec e) lp lp-0))) (l l-0) (e e)) (defstrand ltkgen 1 (P P) (l lp)) (deflistener (hash (exp (gen) (mul l lp)) (exp (gen) (mul lp lp-0)))) (deflistener (cat (exp (gen) (mul l lp)) (exp (gen) (mul lp lp-0)))) (defstrand ca-gen 2 (P A) (CA CA) (h (exp (gen) l-0))) (defstrand ltkgen 1 (P A) (l l-0)) (defstrand ca-gen 2 (P P) (CA CA) (h (exp (gen) lp))) (precedes ((0 2) (3 0)) ((1 0) (6 0)) ((3 1) (2 0)) ((4 1) (0 0)) ((5 0) (4 0)) ((6 1) (0 1))) (fn-of ("principal-of" (P (exp (gen) lp)) (A (exp (gen) l-0)))) (neq ((exp (gen) lp) (gen)) ((exp (gen) l-0) (gen)) ((exp (gen) lp) (exp (gen) l-0)) ((exp (gen) (mul (rec e) lp lp-0)) (gen))) (non-orig (privk A) (privk CA) (privk P)) (uniq-gen e lp) (operation encryption-test (added-strand ca-gen 2) (enc "cert" (exp (gen) lp) P (privk CA)) (0 1)) (traces ((recv (enc "cert" (exp (gen) l-0) A (privk CA))) (recv (enc "cert" (exp (gen) lp) P (privk CA))) (send (exp (gen) e)) (recv (exp (gen) (mul (rec e) lp lp-0)))) ((send (enc "cert-req" P (exp (gen) lp) (privk P)))) ((recv (hash (exp (gen) (mul l lp)) (exp (gen) (mul lp lp-0)))) (send (hash (exp (gen) (mul l lp)) (exp (gen) (mul lp lp-0))))) ((recv (cat (exp (gen) (mul l lp)) (exp (gen) (mul lp lp-0)))) (send (cat (exp (gen) (mul l lp)) (exp (gen) (mul lp lp-0))))) ((recv (enc "cert-req" A (exp (gen) l-0) (privk A))) (send (enc "cert" (exp (gen) l-0) A (privk CA)))) ((send (enc "cert-req" A (exp (gen) l-0) (privk A)))) ((recv (enc "cert-req" P (exp (gen) lp) (privk P))) (send (enc "cert" (exp (gen) lp) P (privk CA))))) (label 71) (parent 70) (unrealized (0 3)) (comment "1 in cohort - 1 not yet seen")) (defskeleton iadh-um (vars (A CA P name) (l e lp l-0 expn) (l-1 expr)) (defstrand init 4 (A A) (B P) (CA CA) (hl (exp (gen) lp)) (he (exp (gen) (mul l-0 l-1))) (l l-0) (e e)) (defstrand ltkgen 1 (P P) (l lp)) (deflistener (hash (exp (gen) (mul l lp)) (exp (gen) (mul e l-0 l-1)))) (deflistener (cat (exp (gen) (mul l lp)) (exp (gen) (mul e l-0 l-1)))) (defstrand ca-gen 2 (P A) (CA CA) (h (exp (gen) l-0))) (defstrand ltkgen 1 (P A) (l l-0)) (defstrand ca-gen 2 (P P) (CA CA) (h (exp (gen) lp))) (precedes ((0 2) (3 0)) ((1 0) (6 0)) ((3 1) (2 0)) ((4 1) (0 0)) ((5 0) (4 0)) ((6 1) (0 1))) (fn-of ("principal-of" (P (exp (gen) lp)) (A (exp (gen) l-0)))) (neq ((exp (gen) lp) (gen)) ((exp (gen) l-0) (gen)) ((exp (gen) lp) (exp (gen) l-0)) ((exp (gen) (mul l-0 l-1)) (gen))) (non-orig (privk A) (privk CA) (privk P)) (uniq-gen e lp) (operation nonce-test (algebra-contracted (e-0 e) (lp-0 lp) (lp-1 (mul e (rec lp) l-0 l-1)) (l-2 l-0) (l-3 l-1)) (exp (gen) (mul l-0 l-1)) (0 3)) (traces ((recv (enc "cert" (exp (gen) l-0) A (privk CA))) (recv (enc "cert" (exp (gen) lp) P (privk CA))) (send (exp (gen) e)) (recv (exp (gen) (mul l-0 l-1)))) ((send (enc "cert-req" P (exp (gen) lp) (privk P)))) ((recv (hash (exp (gen) (mul l lp)) (exp (gen) (mul e l-0 l-1)))) (send (hash (exp (gen) (mul l lp)) (exp (gen) (mul e l-0 l-1))))) ((recv (cat (exp (gen) (mul l lp)) (exp (gen) (mul e l-0 l-1)))) (send (cat (exp (gen) (mul l lp)) (exp (gen) (mul e l-0 l-1))))) ((recv (enc "cert-req" A (exp (gen) l-0) (privk A))) (send (enc "cert" (exp (gen) l-0) A (privk CA)))) ((send (enc "cert-req" A (exp (gen) l-0) (privk A)))) ((recv (enc "cert-req" P (exp (gen) lp) (privk P))) (send (enc "cert" (exp (gen) lp) P (privk CA))))) (label 72) (parent 71) (unrealized) (comment "1 in cohort - 1 not yet seen")) (defskeleton iadh-um (vars (A CA P name) (l e lp l-0 expn) (l-1 expr)) (defstrand init 4 (A A) (B P) (CA CA) (hl (exp (gen) lp)) (he (exp (gen) (mul l-0 l-1))) (l l-0) (e e)) (defstrand ltkgen 1 (P P) (l lp)) (deflistener (hash (exp (gen) (mul l lp)) (exp (gen) (mul e l-0 l-1)))) (defstrand ca-gen 2 (P A) (CA CA) (h (exp (gen) l-0))) (defstrand ltkgen 1 (P A) (l l-0)) (defstrand ca-gen 2 (P P) (CA CA) (h (exp (gen) lp))) (precedes ((0 2) (2 0)) ((1 0) (5 0)) ((3 1) (0 0)) ((4 0) (3 0)) ((5 1) (0 1))) (fn-of ("principal-of" (P (exp (gen) lp)) (A (exp (gen) l-0)))) (neq ((exp (gen) lp) (gen)) ((exp (gen) l-0) (gen)) ((exp (gen) lp) (exp (gen) l-0)) ((exp (gen) (mul l-0 l-1)) (gen))) (non-orig (privk A) (privk CA) (privk P)) (uniq-gen e lp) (operation generalization deleted (3 0)) (traces ((recv (enc "cert" (exp (gen) l-0) A (privk CA))) (recv (enc "cert" (exp (gen) lp) P (privk CA))) (send (exp (gen) e)) (recv (exp (gen) (mul l-0 l-1)))) ((send (enc "cert-req" P (exp (gen) lp) (privk P)))) ((recv (hash (exp (gen) (mul l lp)) (exp (gen) (mul e l-0 l-1)))) (send (hash (exp (gen) (mul l lp)) (exp (gen) (mul e l-0 l-1))))) ((recv (enc "cert-req" A (exp (gen) l-0) (privk A))) (send (enc "cert" (exp (gen) l-0) A (privk CA)))) ((send (enc "cert-req" A (exp (gen) l-0) (privk A)))) ((recv (enc "cert-req" P (exp (gen) lp) (privk P))) (send (enc "cert" (exp (gen) lp) P (privk CA))))) (label 73) (parent 72) (unrealized) (shape) (maps ((0 1 2) ((he (exp (gen) (mul l-0 l-1))) (e e) (l l) (lp lp) (l-0 l-0) (A A) (B P) (CA CA) (P P)))) (origs)) (comment "Nothing left to do") (defprotocol iadh-um diffie-hellman (defrole init (vars (l e expn) (hl he base) (A B CA name) (key data)) (trace (recv (enc "cert" (exp (gen) l) A (privk CA))) (recv (enc "cert" hl B (privk CA))) (send (exp (gen) e)) (recv he) (send key)) (non-orig (privk CA)) (fn-of (foo ((hash (exp hl l) (exp he e)) key))) (neq (he (gen)) (hl (exp (gen) l)))) (defrole ltkgen (vars (P name) (l expn)) (trace (send (enc "cert-req" P (exp (gen) l) (privk P)))) (fn-of ("principal-of" (P (exp (gen) l))))) (defrole ca-gen (vars (P CA name) (h base)) (trace (recv (enc "cert-req" P h (privk P))) (send (enc "cert" h P (privk CA)))) (non-orig (privk P)) (fn-of ("principal-of" (P h))) (neq (h (gen))))) (defskeleton iadh-um (vars (A B CA P name) (he hl base) (e l expn)) (defstrand init 4 (A A) (B B) (CA CA) (hl hl) (he he) (l l) (e e)) (defstrand ltkgen 1 (P P) (l l)) (deflistener (hash (exp hl l) (exp he e))) (fn-of ("principal-of" (P (exp (gen) l)))) (neq (hl (exp (gen) l)) (he (gen))) (non-orig (privk CA)) (uniq-gen e l) (traces ((recv (enc "cert" (exp (gen) l) A (privk CA))) (recv (enc "cert" hl B (privk CA))) (send (exp (gen) e)) (recv he)) ((send (enc "cert-req" P (exp (gen) l) (privk P)))) ((recv (hash (exp hl l) (exp he e))) (send (hash (exp hl l) (exp he e))))) (label 74) (unrealized (0 0) (0 1) (2 0)) (preskeleton) (comment "Not a skeleton")) (defskeleton iadh-um (vars (A B CA P name) (he hl base) (e l expn)) (defstrand init 4 (A A) (B B) (CA CA) (hl hl) (he he) (l l) (e e)) (defstrand ltkgen 1 (P P) (l l)) (deflistener (hash (exp hl l) (exp he e))) (precedes ((0 2) (2 0)) ((1 0) (0 0))) (fn-of ("principal-of" (P (exp (gen) l)))) (neq (hl (exp (gen) l)) (he (gen))) (non-orig (privk CA)) (uniq-gen e l) (traces ((recv (enc "cert" (exp (gen) l) A (privk CA))) (recv (enc "cert" hl B (privk CA))) (send (exp (gen) e)) (recv he)) ((send (enc "cert-req" P (exp (gen) l) (privk P)))) ((recv (hash (exp hl l) (exp he e))) (send (hash (exp hl l) (exp he e))))) (label 75) (parent 74) (unrealized (0 0) (0 1) (2 0)) (origs) (comment "1 in cohort - 1 not yet seen")) (defskeleton iadh-um (vars (A B CA P name) (he hl base) (e l expn)) (defstrand init 4 (A A) (B B) (CA CA) (hl hl) (he he) (l l) (e e)) (defstrand ltkgen 1 (P P) (l l)) (deflistener (hash (exp hl l) (exp he e))) (deflistener (cat (exp hl l) (exp he e))) (precedes ((0 2) (3 0)) ((1 0) (0 0)) ((3 1) (2 0))) (fn-of ("principal-of" (P (exp (gen) l)))) (neq (hl (exp (gen) l)) (he (gen))) (non-orig (privk CA)) (uniq-gen e l) (operation encryption-test (added-listener (cat (exp hl l) (exp he e))) (hash (exp hl l) (exp he e)) (2 0)) (traces ((recv (enc "cert" (exp (gen) l) A (privk CA))) (recv (enc "cert" hl B (privk CA))) (send (exp (gen) e)) (recv he)) ((send (enc "cert-req" P (exp (gen) l) (privk P)))) ((recv (hash (exp hl l) (exp he e))) (send (hash (exp hl l) (exp he e)))) ((recv (cat (exp hl l) (exp he e))) (send (cat (exp hl l) (exp he e))))) (label 76) (parent 75) (unrealized (0 0) (0 1) (3 0)) (comment "1 in cohort - 1 not yet seen")) (defskeleton iadh-um (vars (A B CA P name) (he base) (e l expn) (l-0 expr)) (defstrand init 4 (A A) (B B) (CA CA) (hl (exp (gen) l-0)) (he he) (l l) (e e)) (defstrand ltkgen 1 (P P) (l l)) (deflistener (hash (exp (gen) (mul l l-0)) (exp he e))) (deflistener (cat (exp (gen) (mul l l-0)) (exp he e))) (precedes ((0 2) (3 0)) ((1 0) (0 0)) ((3 1) (2 0))) (fn-of ("principal-of" (P (exp (gen) l)))) (neq ((exp (gen) l-0) (exp (gen) l)) (he (gen))) (non-orig (privk CA)) (uniq-gen e l) (operation nonce-test (algebra-contracted (hl (exp (gen) l-0))) (exp (gen) (mul l l-0)) (3 0) (exp (gen) l)) (traces ((recv (enc "cert" (exp (gen) l) A (privk CA))) (recv (enc "cert" (exp (gen) l-0) B (privk CA))) (send (exp (gen) e)) (recv he)) ((send (enc "cert-req" P (exp (gen) l) (privk P)))) ((recv (hash (exp (gen) (mul l l-0)) (exp he e))) (send (hash (exp (gen) (mul l l-0)) (exp he e)))) ((recv (cat (exp (gen) (mul l l-0)) (exp he e))) (send (cat (exp (gen) (mul l l-0)) (exp he e))))) (label 77) (parent 76) (unrealized (0 0) (0 1) (3 0)) (comment "1 in cohort - 1 not yet seen")) (defskeleton iadh-um (vars (A B CA P name) (e l expn) (l-0 l-1 expr)) (defstrand init 4 (A A) (B B) (CA CA) (hl (exp (gen) l-0)) (he (exp (gen) (mul (rec e) l l-1))) (l l) (e e)) (defstrand ltkgen 1 (P P) (l l)) (deflistener (hash (exp (gen) (mul l l-0)) (exp (gen) (mul l l-1)))) (deflistener (cat (exp (gen) (mul l l-0)) (exp (gen) (mul l l-1)))) (precedes ((0 2) (3 0)) ((1 0) (0 0)) ((3 1) (2 0))) (fn-of ("principal-of" (P (exp (gen) l)))) (neq ((exp (gen) l-0) (exp (gen) l)) ((exp (gen) (mul (rec e) l l-1)) (gen))) (non-orig (privk CA)) (uniq-gen e l) (operation nonce-test (algebra-contracted (he (exp (gen) (mul (rec e) l l-1)))) (exp (gen) (mul l l-1)) (3 0) (exp (gen) e)) (traces ((recv (enc "cert" (exp (gen) l) A (privk CA))) (recv (enc "cert" (exp (gen) l-0) B (privk CA))) (send (exp (gen) e)) (recv (exp (gen) (mul (rec e) l l-1)))) ((send (enc "cert-req" P (exp (gen) l) (privk P)))) ((recv (hash (exp (gen) (mul l l-0)) (exp (gen) (mul l l-1)))) (send (hash (exp (gen) (mul l l-0)) (exp (gen) (mul l l-1))))) ((recv (cat (exp (gen) (mul l l-0)) (exp (gen) (mul l l-1)))) (send (cat (exp (gen) (mul l l-0)) (exp (gen) (mul l l-1)))))) (label 78) (parent 77) (unrealized (0 0) (0 1) (0 3)) (comment "1 in cohort - 1 not yet seen")) (defskeleton iadh-um (vars (B CA P name) (e l expn) (l-0 l-1 expr)) (defstrand init 4 (A P) (B B) (CA CA) (hl (exp (gen) l-0)) (he (exp (gen) (mul (rec e) l l-1))) (l l) (e e)) (defstrand ltkgen 1 (P P) (l l)) (deflistener (hash (exp (gen) (mul l l-0)) (exp (gen) (mul l l-1)))) (deflistener (cat (exp (gen) (mul l l-0)) (exp (gen) (mul l l-1)))) (defstrand ca-gen 2 (P P) (CA CA) (h (exp (gen) l))) (precedes ((0 2) (3 0)) ((1 0) (4 0)) ((3 1) (2 0)) ((4 1) (0 0))) (fn-of ("principal-of" (P (exp (gen) l)))) (neq ((exp (gen) l) (gen)) ((exp (gen) l-0) (exp (gen) l)) ((exp (gen) (mul (rec e) l l-1)) (gen))) (non-orig (privk CA) (privk P)) (uniq-gen e l) (operation encryption-test (added-strand ca-gen 2) (enc "cert" (exp (gen) l) P (privk CA)) (0 0)) (traces ((recv (enc "cert" (exp (gen) l) P (privk CA))) (recv (enc "cert" (exp (gen) l-0) B (privk CA))) (send (exp (gen) e)) (recv (exp (gen) (mul (rec e) l l-1)))) ((send (enc "cert-req" P (exp (gen) l) (privk P)))) ((recv (hash (exp (gen) (mul l l-0)) (exp (gen) (mul l l-1)))) (send (hash (exp (gen) (mul l l-0)) (exp (gen) (mul l l-1))))) ((recv (cat (exp (gen) (mul l l-0)) (exp (gen) (mul l l-1)))) (send (cat (exp (gen) (mul l l-0)) (exp (gen) (mul l l-1))))) ((recv (enc "cert-req" P (exp (gen) l) (privk P))) (send (enc "cert" (exp (gen) l) P (privk CA))))) (label 79) (parent 78) (unrealized (0 1) (0 3)) (comment "1 in cohort - 1 not yet seen")) (defskeleton iadh-um (vars (B CA P name) (e l expn) (l-0 l-1 expr)) (defstrand init 4 (A P) (B B) (CA CA) (hl (exp (gen) l-0)) (he (exp (gen) (mul (rec e) l l-1))) (l l) (e e)) (defstrand ltkgen 1 (P P) (l l)) (deflistener (hash (exp (gen) (mul l l-0)) (exp (gen) (mul l l-1)))) (deflistener (cat (exp (gen) (mul l l-0)) (exp (gen) (mul l l-1)))) (defstrand ca-gen 2 (P P) (CA CA) (h (exp (gen) l))) (defstrand ca-gen 2 (P B) (CA CA) (h (exp (gen) l-0))) (precedes ((0 2) (3 0)) ((1 0) (4 0)) ((3 1) (2 0)) ((4 1) (0 0)) ((5 1) (0 1))) (fn-of ("principal-of" (B (exp (gen) l-0)) (P (exp (gen) l)))) (neq ((exp (gen) l-0) (gen)) ((exp (gen) l) (gen)) ((exp (gen) l-0) (exp (gen) l)) ((exp (gen) (mul (rec e) l l-1)) (gen))) (non-orig (privk B) (privk CA) (privk P)) (uniq-gen e l) (operation encryption-test (added-strand ca-gen 2) (enc "cert" (exp (gen) l-0) B (privk CA)) (0 1)) (traces ((recv (enc "cert" (exp (gen) l) P (privk CA))) (recv (enc "cert" (exp (gen) l-0) B (privk CA))) (send (exp (gen) e)) (recv (exp (gen) (mul (rec e) l l-1)))) ((send (enc "cert-req" P (exp (gen) l) (privk P)))) ((recv (hash (exp (gen) (mul l l-0)) (exp (gen) (mul l l-1)))) (send (hash (exp (gen) (mul l l-0)) (exp (gen) (mul l l-1))))) ((recv (cat (exp (gen) (mul l l-0)) (exp (gen) (mul l l-1)))) (send (cat (exp (gen) (mul l l-0)) (exp (gen) (mul l l-1))))) ((recv (enc "cert-req" P (exp (gen) l) (privk P))) (send (enc "cert" (exp (gen) l) P (privk CA)))) ((recv (enc "cert-req" B (exp (gen) l-0) (privk B))) (send (enc "cert" (exp (gen) l-0) B (privk CA))))) (label 80) (parent 79) (unrealized (0 3) (5 0)) (comment "1 in cohort - 1 not yet seen")) (defskeleton iadh-um (vars (B CA P name) (e l expn) (l-0 expr) (l-1 expn)) (defstrand init 4 (A P) (B B) (CA CA) (hl (exp (gen) l-1)) (he (exp (gen) (mul (rec e) l l-0))) (l l) (e e)) (defstrand ltkgen 1 (P P) (l l)) (deflistener (hash (exp (gen) (mul l l-1)) (exp (gen) (mul l l-0)))) (deflistener (cat (exp (gen) (mul l l-1)) (exp (gen) (mul l l-0)))) (defstrand ca-gen 2 (P P) (CA CA) (h (exp (gen) l))) (defstrand ca-gen 2 (P B) (CA CA) (h (exp (gen) l-1))) (defstrand ltkgen 1 (P B) (l l-1)) (precedes ((0 2) (3 0)) ((1 0) (4 0)) ((3 1) (2 0)) ((4 1) (0 0)) ((5 1) (0 1)) ((6 0) (5 0))) (fn-of ("principal-of" (B (exp (gen) l-1)) (P (exp (gen) l)))) (neq ((exp (gen) l-1) (gen)) ((exp (gen) l) (gen)) ((exp (gen) l-1) (exp (gen) l)) ((exp (gen) (mul (rec e) l l-0)) (gen))) (non-orig (privk B) (privk CA) (privk P)) (uniq-gen e l) (operation encryption-test (added-strand ltkgen 1) (enc "cert-req" B (exp (gen) l-1) (privk B)) (5 0)) (traces ((recv (enc "cert" (exp (gen) l) P (privk CA))) (recv (enc "cert" (exp (gen) l-1) B (privk CA))) (send (exp (gen) e)) (recv (exp (gen) (mul (rec e) l l-0)))) ((send (enc "cert-req" P (exp (gen) l) (privk P)))) ((recv (hash (exp (gen) (mul l l-1)) (exp (gen) (mul l l-0)))) (send (hash (exp (gen) (mul l l-1)) (exp (gen) (mul l l-0))))) ((recv (cat (exp (gen) (mul l l-1)) (exp (gen) (mul l l-0)))) (send (cat (exp (gen) (mul l l-1)) (exp (gen) (mul l l-0))))) ((recv (enc "cert-req" P (exp (gen) l) (privk P))) (send (enc "cert" (exp (gen) l) P (privk CA)))) ((recv (enc "cert-req" B (exp (gen) l-1) (privk B))) (send (enc "cert" (exp (gen) l-1) B (privk CA)))) ((send (enc "cert-req" B (exp (gen) l-1) (privk B))))) (label 81) (parent 80) (unrealized (0 3)) (comment "1 in cohort - 1 not yet seen")) (defskeleton iadh-um (vars (B CA P name) (e l l-0 expn) (l-1 expr)) (defstrand init 4 (A P) (B B) (CA CA) (hl (exp (gen) l-0)) (he (exp (gen) (mul l-0 l-1))) (l l) (e e)) (defstrand ltkgen 1 (P P) (l l)) (deflistener (hash (exp (gen) (mul l l-0)) (exp (gen) (mul e l-0 l-1)))) (deflistener (cat (exp (gen) (mul l l-0)) (exp (gen) (mul e l-0 l-1)))) (defstrand ca-gen 2 (P P) (CA CA) (h (exp (gen) l))) (defstrand ca-gen 2 (P B) (CA CA) (h (exp (gen) l-0))) (defstrand ltkgen 1 (P B) (l l-0)) (precedes ((0 2) (3 0)) ((1 0) (4 0)) ((3 1) (2 0)) ((4 1) (0 0)) ((5 1) (0 1)) ((6 0) (5 0))) (fn-of ("principal-of" (B (exp (gen) l-0)) (P (exp (gen) l)))) (neq ((exp (gen) l-0) (gen)) ((exp (gen) l) (gen)) ((exp (gen) l-0) (exp (gen) l)) ((exp (gen) (mul l-0 l-1)) (gen))) (non-orig (privk B) (privk CA) (privk P)) (uniq-gen e l) (operation nonce-test (algebra-contracted (e-0 e) (l-2 l) (l-3 (mul e (rec l) l-0 l-1)) (l-4 l-0) (l-5 l-1)) (exp (gen) (mul l-0 l-1)) (0 3)) (traces ((recv (enc "cert" (exp (gen) l) P (privk CA))) (recv (enc "cert" (exp (gen) l-0) B (privk CA))) (send (exp (gen) e)) (recv (exp (gen) (mul l-0 l-1)))) ((send (enc "cert-req" P (exp (gen) l) (privk P)))) ((recv (hash (exp (gen) (mul l l-0)) (exp (gen) (mul e l-0 l-1)))) (send (hash (exp (gen) (mul l l-0)) (exp (gen) (mul e l-0 l-1))))) ((recv (cat (exp (gen) (mul l l-0)) (exp (gen) (mul e l-0 l-1)))) (send (cat (exp (gen) (mul l l-0)) (exp (gen) (mul e l-0 l-1))))) ((recv (enc "cert-req" P (exp (gen) l) (privk P))) (send (enc "cert" (exp (gen) l) P (privk CA)))) ((recv (enc "cert-req" B (exp (gen) l-0) (privk B))) (send (enc "cert" (exp (gen) l-0) B (privk CA)))) ((send (enc "cert-req" B (exp (gen) l-0) (privk B))))) (label 82) (parent 81) (unrealized) (comment "1 in cohort - 1 not yet seen")) (defskeleton iadh-um (vars (B CA P name) (e l l-0 expn) (l-1 expr)) (defstrand init 4 (A P) (B B) (CA CA) (hl (exp (gen) l-0)) (he (exp (gen) (mul l-0 l-1))) (l l) (e e)) (defstrand ltkgen 1 (P P) (l l)) (deflistener (hash (exp (gen) (mul l l-0)) (exp (gen) (mul e l-0 l-1)))) (defstrand ca-gen 2 (P P) (CA CA) (h (exp (gen) l))) (defstrand ca-gen 2 (P B) (CA CA) (h (exp (gen) l-0))) (defstrand ltkgen 1 (P B) (l l-0)) (precedes ((0 2) (2 0)) ((1 0) (3 0)) ((3 1) (0 0)) ((4 1) (0 1)) ((5 0) (4 0))) (fn-of ("principal-of" (B (exp (gen) l-0)) (P (exp (gen) l)))) (neq ((exp (gen) l-0) (gen)) ((exp (gen) l) (gen)) ((exp (gen) l-0) (exp (gen) l)) ((exp (gen) (mul l-0 l-1)) (gen))) (non-orig (privk B) (privk CA) (privk P)) (uniq-gen e l) (operation generalization deleted (3 0)) (traces ((recv (enc "cert" (exp (gen) l) P (privk CA))) (recv (enc "cert" (exp (gen) l-0) B (privk CA))) (send (exp (gen) e)) (recv (exp (gen) (mul l-0 l-1)))) ((send (enc "cert-req" P (exp (gen) l) (privk P)))) ((recv (hash (exp (gen) (mul l l-0)) (exp (gen) (mul e l-0 l-1)))) (send (hash (exp (gen) (mul l l-0)) (exp (gen) (mul e l-0 l-1))))) ((recv (enc "cert-req" P (exp (gen) l) (privk P))) (send (enc "cert" (exp (gen) l) P (privk CA)))) ((recv (enc "cert-req" B (exp (gen) l-0) (privk B))) (send (enc "cert" (exp (gen) l-0) B (privk CA)))) ((send (enc "cert-req" B (exp (gen) l-0) (privk B))))) (label 83) (parent 82) (unrealized) (shape) (maps ((0 1 2) ((he (exp (gen) (mul l-0 l-1))) (hl (exp (gen) l-0)) (e e) (l l) (A P) (B B) (CA CA) (P P)))) (origs)) (comment "Nothing left to do") (defprotocol iadh-um diffie-hellman (defrole init (vars (l e expn) (hl he base) (A B CA name) (key data)) (trace (recv (enc "cert" (exp (gen) l) A (privk CA))) (recv (enc "cert" hl B (privk CA))) (send (exp (gen) e)) (recv he) (send key)) (non-orig (privk CA)) (fn-of (foo ((hash (exp hl l) (exp he e)) key))) (neq (he (gen)) (hl (exp (gen) l)))) (defrole ltkgen (vars (P name) (l expn)) (trace (send (enc "cert-req" P (exp (gen) l) (privk P)))) (fn-of ("principal-of" (P (exp (gen) l))))) (defrole ca-gen (vars (P CA name) (h base)) (trace (recv (enc "cert-req" P h (privk P))) (send (enc "cert" h P (privk CA)))) (non-orig (privk P)) (fn-of ("principal-of" (P h))) (neq (h (gen))))) (defskeleton iadh-um (vars (A B CA name) (he hl base) (e l expn)) (defstrand init 4 (A A) (B B) (CA CA) (hl hl) (he he) (l l) (e e)) (deflistener (hash (exp hl l) (exp he e))) (neq (hl (exp (gen) l)) (he (gen))) (non-orig (privk CA)) (uniq-gen e) (traces ((recv (enc "cert" (exp (gen) l) A (privk CA))) (recv (enc "cert" hl B (privk CA))) (send (exp (gen) e)) (recv he)) ((recv (hash (exp hl l) (exp he e))) (send (hash (exp hl l) (exp he e))))) (label 84) (unrealized (0 0) (0 1) (1 0)) (preskeleton) (comment "Not a skeleton")) (defskeleton iadh-um (vars (A B CA name) (he hl base) (e l expn)) (defstrand init 4 (A A) (B B) (CA CA) (hl hl) (he he) (l l) (e e)) (deflistener (hash (exp hl l) (exp he e))) (precedes ((0 2) (1 0))) (neq (hl (exp (gen) l)) (he (gen))) (non-orig (privk CA)) (uniq-gen e) (traces ((recv (enc "cert" (exp (gen) l) A (privk CA))) (recv (enc "cert" hl B (privk CA))) (send (exp (gen) e)) (recv he)) ((recv (hash (exp hl l) (exp he e))) (send (hash (exp hl l) (exp he e))))) (label 85) (parent 84) (unrealized (0 0) (0 1) (1 0)) (origs) (comment "1 in cohort - 1 not yet seen")) (defskeleton iadh-um (vars (A B CA name) (he hl base) (e l expn)) (defstrand init 4 (A A) (B B) (CA CA) (hl hl) (he he) (l l) (e e)) (deflistener (hash (exp hl l) (exp he e))) (deflistener (cat (exp hl l) (exp he e))) (precedes ((0 2) (2 0)) ((2 1) (1 0))) (neq (hl (exp (gen) l)) (he (gen))) (non-orig (privk CA)) (uniq-gen e) (operation encryption-test (added-listener (cat (exp hl l) (exp he e))) (hash (exp hl l) (exp he e)) (1 0)) (traces ((recv (enc "cert" (exp (gen) l) A (privk CA))) (recv (enc "cert" hl B (privk CA))) (send (exp (gen) e)) (recv he)) ((recv (hash (exp hl l) (exp he e))) (send (hash (exp hl l) (exp he e)))) ((recv (cat (exp hl l) (exp he e))) (send (cat (exp hl l) (exp he e))))) (label 86) (parent 85) (unrealized (0 0) (0 1) (2 0)) (comment "1 in cohort - 1 not yet seen")) (defskeleton iadh-um (vars (A B CA name) (hl base) (e l expn) (e-0 expr)) (defstrand init 4 (A A) (B B) (CA CA) (hl hl) (he (exp (gen) e-0)) (l l) (e e)) (deflistener (hash (exp hl l) (exp (gen) (mul e e-0)))) (deflistener (cat (exp hl l) (exp (gen) (mul e e-0)))) (precedes ((0 2) (2 0)) ((2 1) (1 0))) (neq (hl (exp (gen) l)) ((exp (gen) e-0) (gen))) (non-orig (privk CA)) (uniq-gen e) (operation nonce-test (algebra-contracted (he (exp (gen) e-0))) (exp (gen) (mul e e-0)) (2 0) (exp (gen) e)) (traces ((recv (enc "cert" (exp (gen) l) A (privk CA))) (recv (enc "cert" hl B (privk CA))) (send (exp (gen) e)) (recv (exp (gen) e-0))) ((recv (hash (exp hl l) (exp (gen) (mul e e-0)))) (send (hash (exp hl l) (exp (gen) (mul e e-0))))) ((recv (cat (exp hl l) (exp (gen) (mul e e-0)))) (send (cat (exp hl l) (exp (gen) (mul e e-0)))))) (label 87) (parent 86) (unrealized (0 0) (0 1)) (comment "1 in cohort - 1 not yet seen")) (defskeleton iadh-um (vars (A B CA name) (hl base) (e l expn) (e-0 expr)) (defstrand init 4 (A A) (B B) (CA CA) (hl hl) (he (exp (gen) e-0)) (l l) (e e)) (deflistener (hash (exp hl l) (exp (gen) (mul e e-0)))) (deflistener (cat (exp hl l) (exp (gen) (mul e e-0)))) (defstrand ca-gen 2 (P A) (CA CA) (h (exp (gen) l))) (precedes ((0 2) (2 0)) ((2 1) (1 0)) ((3 1) (0 0))) (fn-of ("principal-of" (A (exp (gen) l)))) (neq ((exp (gen) l) (gen)) (hl (exp (gen) l)) ((exp (gen) e-0) (gen))) (non-orig (privk A) (privk CA)) (uniq-gen e) (operation encryption-test (added-strand ca-gen 2) (enc "cert" (exp (gen) l) A (privk CA)) (0 0)) (traces ((recv (enc "cert" (exp (gen) l) A (privk CA))) (recv (enc "cert" hl B (privk CA))) (send (exp (gen) e)) (recv (exp (gen) e-0))) ((recv (hash (exp hl l) (exp (gen) (mul e e-0)))) (send (hash (exp hl l) (exp (gen) (mul e e-0))))) ((recv (cat (exp hl l) (exp (gen) (mul e e-0)))) (send (cat (exp hl l) (exp (gen) (mul e e-0))))) ((recv (enc "cert-req" A (exp (gen) l) (privk A))) (send (enc "cert" (exp (gen) l) A (privk CA))))) (label 88) (parent 87) (unrealized (0 1) (3 0)) (comment "1 in cohort - 1 not yet seen")) (defskeleton iadh-um (vars (A B CA name) (hl base) (e expn) (e-0 expr) (l expn)) (defstrand init 4 (A A) (B B) (CA CA) (hl hl) (he (exp (gen) e-0)) (l l) (e e)) (deflistener (hash (exp hl l) (exp (gen) (mul e e-0)))) (deflistener (cat (exp hl l) (exp (gen) (mul e e-0)))) (defstrand ca-gen 2 (P A) (CA CA) (h (exp (gen) l))) (defstrand ltkgen 1 (P A) (l l)) (precedes ((0 2) (2 0)) ((2 1) (1 0)) ((3 1) (0 0)) ((4 0) (3 0))) (fn-of ("principal-of" (A (exp (gen) l)))) (neq ((exp (gen) l) (gen)) (hl (exp (gen) l)) ((exp (gen) e-0) (gen))) (non-orig (privk A) (privk CA)) (uniq-gen e) (operation encryption-test (added-strand ltkgen 1) (enc "cert-req" A (exp (gen) l) (privk A)) (3 0)) (traces ((recv (enc "cert" (exp (gen) l) A (privk CA))) (recv (enc "cert" hl B (privk CA))) (send (exp (gen) e)) (recv (exp (gen) e-0))) ((recv (hash (exp hl l) (exp (gen) (mul e e-0)))) (send (hash (exp hl l) (exp (gen) (mul e e-0))))) ((recv (cat (exp hl l) (exp (gen) (mul e e-0)))) (send (cat (exp hl l) (exp (gen) (mul e e-0))))) ((recv (enc "cert-req" A (exp (gen) l) (privk A))) (send (enc "cert" (exp (gen) l) A (privk CA)))) ((send (enc "cert-req" A (exp (gen) l) (privk A))))) (label 89) (parent 88) (unrealized (0 1)) (comment "1 in cohort - 1 not yet seen")) (defskeleton iadh-um (vars (A B CA name) (hl base) (e expn) (e-0 expr) (l expn)) (defstrand init 4 (A A) (B B) (CA CA) (hl hl) (he (exp (gen) e-0)) (l l) (e e)) (deflistener (hash (exp hl l) (exp (gen) (mul e e-0)))) (deflistener (cat (exp hl l) (exp (gen) (mul e e-0)))) (defstrand ca-gen 2 (P A) (CA CA) (h (exp (gen) l))) (defstrand ltkgen 1 (P A) (l l)) (defstrand ca-gen 2 (P B) (CA CA) (h hl)) (precedes ((0 2) (2 0)) ((2 1) (1 0)) ((3 1) (0 0)) ((4 0) (3 0)) ((5 1) (0 1))) (fn-of ("principal-of" (B hl) (A (exp (gen) l)))) (neq (hl (gen)) ((exp (gen) l) (gen)) (hl (exp (gen) l)) ((exp (gen) e-0) (gen))) (non-orig (privk A) (privk B) (privk CA)) (uniq-gen e) (operation encryption-test (added-strand ca-gen 2) (enc "cert" hl B (privk CA)) (0 1)) (traces ((recv (enc "cert" (exp (gen) l) A (privk CA))) (recv (enc "cert" hl B (privk CA))) (send (exp (gen) e)) (recv (exp (gen) e-0))) ((recv (hash (exp hl l) (exp (gen) (mul e e-0)))) (send (hash (exp hl l) (exp (gen) (mul e e-0))))) ((recv (cat (exp hl l) (exp (gen) (mul e e-0)))) (send (cat (exp hl l) (exp (gen) (mul e e-0))))) ((recv (enc "cert-req" A (exp (gen) l) (privk A))) (send (enc "cert" (exp (gen) l) A (privk CA)))) ((send (enc "cert-req" A (exp (gen) l) (privk A)))) ((recv (enc "cert-req" B hl (privk B))) (send (enc "cert" hl B (privk CA))))) (label 90) (parent 89) (unrealized (5 0)) (comment "1 in cohort - 1 not yet seen")) (defskeleton iadh-um (vars (A B CA name) (e expn) (e-0 expr) (l l-0 expn)) (defstrand init 4 (A A) (B B) (CA CA) (hl (exp (gen) l-0)) (he (exp (gen) e-0)) (l l) (e e)) (deflistener (hash (exp (gen) (mul l l-0)) (exp (gen) (mul e e-0)))) (deflistener (cat (exp (gen) (mul l l-0)) (exp (gen) (mul e e-0)))) (defstrand ca-gen 2 (P A) (CA CA) (h (exp (gen) l))) (defstrand ltkgen 1 (P A) (l l)) (defstrand ca-gen 2 (P B) (CA CA) (h (exp (gen) l-0))) (defstrand ltkgen 1 (P B) (l l-0)) (precedes ((0 2) (2 0)) ((2 1) (1 0)) ((3 1) (0 0)) ((4 0) (3 0)) ((5 1) (0 1)) ((6 0) (5 0))) (fn-of ("principal-of" (B (exp (gen) l-0)) (A (exp (gen) l)))) (neq ((exp (gen) l-0) (gen)) ((exp (gen) l) (gen)) ((exp (gen) l-0) (exp (gen) l)) ((exp (gen) e-0) (gen))) (non-orig (privk A) (privk B) (privk CA)) (uniq-gen e) (operation encryption-test (added-strand ltkgen 1) (enc "cert-req" B (exp (gen) l-0) (privk B)) (5 0)) (traces ((recv (enc "cert" (exp (gen) l) A (privk CA))) (recv (enc "cert" (exp (gen) l-0) B (privk CA))) (send (exp (gen) e)) (recv (exp (gen) e-0))) ((recv (hash (exp (gen) (mul l l-0)) (exp (gen) (mul e e-0)))) (send (hash (exp (gen) (mul l l-0)) (exp (gen) (mul e e-0))))) ((recv (cat (exp (gen) (mul l l-0)) (exp (gen) (mul e e-0)))) (send (cat (exp (gen) (mul l l-0)) (exp (gen) (mul e e-0))))) ((recv (enc "cert-req" A (exp (gen) l) (privk A))) (send (enc "cert" (exp (gen) l) A (privk CA)))) ((send (enc "cert-req" A (exp (gen) l) (privk A)))) ((recv (enc "cert-req" B (exp (gen) l-0) (privk B))) (send (enc "cert" (exp (gen) l-0) B (privk CA)))) ((send (enc "cert-req" B (exp (gen) l-0) (privk B))))) (label 91) (parent 90) (unrealized) (comment "1 in cohort - 1 not yet seen")) (defskeleton iadh-um (vars (A B CA name) (e expn) (e-0 expr) (l l-0 expn)) (defstrand init 4 (A A) (B B) (CA CA) (hl (exp (gen) l-0)) (he (exp (gen) e-0)) (l l) (e e)) (deflistener (hash (exp (gen) (mul l l-0)) (exp (gen) (mul e e-0)))) (defstrand ca-gen 2 (P A) (CA CA) (h (exp (gen) l))) (defstrand ltkgen 1 (P A) (l l)) (defstrand ca-gen 2 (P B) (CA CA) (h (exp (gen) l-0))) (defstrand ltkgen 1 (P B) (l l-0)) (precedes ((0 2) (1 0)) ((2 1) (0 0)) ((3 0) (2 0)) ((4 1) (0 1)) ((5 0) (4 0))) (fn-of ("principal-of" (B (exp (gen) l-0)) (A (exp (gen) l)))) (neq ((exp (gen) l-0) (gen)) ((exp (gen) l) (gen)) ((exp (gen) l-0) (exp (gen) l)) ((exp (gen) e-0) (gen))) (non-orig (privk A) (privk B) (privk CA)) (uniq-gen e) (operation generalization deleted (2 0)) (traces ((recv (enc "cert" (exp (gen) l) A (privk CA))) (recv (enc "cert" (exp (gen) l-0) B (privk CA))) (send (exp (gen) e)) (recv (exp (gen) e-0))) ((recv (hash (exp (gen) (mul l l-0)) (exp (gen) (mul e e-0)))) (send (hash (exp (gen) (mul l l-0)) (exp (gen) (mul e e-0))))) ((recv (enc "cert-req" A (exp (gen) l) (privk A))) (send (enc "cert" (exp (gen) l) A (privk CA)))) ((send (enc "cert-req" A (exp (gen) l) (privk A)))) ((recv (enc "cert-req" B (exp (gen) l-0) (privk B))) (send (enc "cert" (exp (gen) l-0) B (privk CA)))) ((send (enc "cert-req" B (exp (gen) l-0) (privk B))))) (label 92) (parent 91) (unrealized) (shape) (maps ((0 1) ((he (exp (gen) e-0)) (hl (exp (gen) l-0)) (e e) (l l) (A A) (B B) (CA CA)))) (origs)) (comment "Nothing left to do")