cpsa-4.4.4: tst/dhcr_um_expt_shapes.tst
(comment "CPSA 4.3.1")
(comment "Extracted shapes")
(herald "DHCR: unified model (UM) original" (bound 20) (limit 12000)
(algebra diffie-hellman))
(comment "CPSA 4.3.1")
(comment "All input read from tst/dhcr_um_expt.scm")
(comment "Step count limited to 12000")
(comment "Strand count bounded at 20")
(defprotocol dhcr-um diffie-hellman
(defrole init
(vars (la x rndx) (beta upsilon expt) (a b name) (na nb data)
(priv-stor locn))
(trace (load priv-stor (pv a la))
(recv
(sig (body b (exp (gen) beta) (pubk "sig" b)) (privk "sig" b)))
(send (cat na a b (exp (gen) x)))
(recv
(cat (exp (gen) upsilon)
(enc na nb a b
(hash (exp (gen) (mul la beta))
(exp (gen) (mul x upsilon)))))) (send nb))
(uniq-orig na)
(uniq-gen x)
(absent (x la) (x beta))
(facts (neq (exp (gen) upsilon) (gen)))
(gen-st (pv a la))
(fn-of ("principal-of" (ltxa a) (ltxb b))
("ltx-of" (a ltxa) (b ltxb))))
(defrole resp
(vars (lb y rndx) (alpha zeta expt) (a b name) (na nb data)
(priv-stor locn))
(trace (load priv-stor (pv b lb))
(recv
(sig (body a (exp (gen) alpha) (pubk "sig" a)) (privk "sig" a)))
(recv (cat na a b (exp (gen) zeta)))
(send
(cat (exp (gen) y)
(enc na nb a b
(hash (exp (gen) (mul lb alpha))
(exp (gen) (mul y zeta)))))) (recv nb))
(uniq-orig nb)
(uniq-gen y)
(absent (y lb) (y alpha) (y zeta))
(facts (neq (exp (gen) zeta) (gen)))
(gen-st (pv b lb))
(fn-of ("principal-of" (ltxa a) (ltxb b))
("ltx-of" (a ltxa) (b ltxb))))
(defrole ltx-gen
(vars (self name) (l rndx) (priv-stor locn) (ignore mesg))
(trace (load priv-stor ignore) (stor priv-stor (pv self l))
(send
(sig (body self (exp (gen) l) (pubk "sig" self))
(privk "sig" self))))
(uniq-orig l)
(fn-of ("principal-of" (l self)) ("ltx-of" (self l))))
(defrole ltx-disclose
(vars (self name) (l rndx) (priv-stor locn))
(trace (load priv-stor (pv self l)) (stor priv-stor "nil") (send l))
(gen-st (pv self l))
(fn-of ("principal-of" (l self)) ("ltx-of" (self l))))
(defrule undisclosed-not-disclosed
(forall ((z strd) (l rndx))
(implies
(and (fact undisclosed l) (p "ltx-disclose" z 2)
(p "ltx-disclose" "l" z l))
(false))))
(defgenrule neqRl_indx
(forall ((x indx)) (implies (fact neq x x) (false))))
(defgenrule neqRl_strd
(forall ((x strd)) (implies (fact neq x x) (false))))
(defgenrule neqRl_mesg
(forall ((x mesg)) (implies (fact neq x x) (false))))
(defgenrule shearsRule
(forall ((z0 z1 z2 strd) (i0 i1 i2 indx))
(implies
(and (trans z0 i0) (trans z1 i1) (trans z2 i2)
(leads-to z0 i0 z1 i1) (same-locn z0 i0 z2 i2)
(prec z0 i0 z2 i2))
(or (and (= z1 z2) (= i1 i2)) (prec z1 i1 z2 i2)))))
(defgenrule invShearsRule
(forall ((z0 z1 z2 strd) (i0 i1 i2 indx))
(implies
(and (trans z0 i0) (trans z1 i1) (same-locn z0 i0 z1 i1)
(leads-to z1 i1 z2 i2) (prec z0 i0 z2 i2))
(or (and (= z0 z1) (= i0 i1)) (prec z0 i0 z1 i1)))))
(defgenrule fact-init-neq0
(forall ((z strd) (upsilon expt))
(implies (and (p "init" z 4) (p "init" "upsilon" z upsilon))
(fact neq (exp (gen) upsilon) (gen)))))
(defgenrule fact-resp-neq0
(forall ((z strd) (zeta expt))
(implies (and (p "resp" z 3) (p "resp" "zeta" z zeta))
(fact neq (exp (gen) zeta) (gen)))))
(defgenrule trRl_ltx-gen-at-1
(forall ((z strd)) (implies (p "ltx-gen" z 2) (trans z 1))))
(defgenrule trRl_ltx-gen-at-0
(forall ((z strd)) (implies (p "ltx-gen" z 2) (trans z 0))))
(defgenrule trRl_ltx-disclose-at-1
(forall ((z strd)) (implies (p "ltx-disclose" z 2) (trans z 1))))
(defgenrule trRl_ltx-disclose-at-0
(forall ((z strd)) (implies (p "ltx-disclose" z 2) (trans z 0))))
(defgenrule gen-st-init-0
(forall ((z strd) (la rndx) (a name))
(implies
(and (p "init" z 1) (p "init" "la" z la) (p "init" "a" z a))
(gen-st (pv a la)))))
(defgenrule gen-st-resp-0
(forall ((z strd) (lb rndx) (b name))
(implies
(and (p "resp" z 1) (p "resp" "lb" z lb) (p "resp" "b" z b))
(gen-st (pv b lb)))))
(defgenrule gen-st-ltx-disclose-0
(forall ((z strd) (l rndx) (self name))
(implies
(and (p "ltx-disclose" z 1) (p "ltx-disclose" "l" z l)
(p "ltx-disclose" "self" z self)) (gen-st (pv self l)))))
(lang (sig sign) (body (tuple 3)) (pv (tuple 2))))
(defskeleton dhcr-um
(vars (na nb data) (a b name) (pt pval) (priv-stor locn) (la rndx)
(beta expt) (x rndx) (upsilon expt))
(defstrand init 5 (na na) (nb nb) (a a) (b b) (priv-stor priv-stor)
(la la) (x x) (beta beta) (upsilon upsilon))
(non-orig (privk "sig" b))
(uniq-orig na)
(uniq-gen x)
(absent (x la) (x beta))
(facts (neq a b) (undisclosed la) (undisclosed beta))
(traces
((load priv-stor (cat pt (pv a la)))
(recv
(sig (body b (exp (gen) beta) (pubk "sig" b)) (privk "sig" b)))
(send (cat na a b (exp (gen) x)))
(recv
(cat (exp (gen) upsilon)
(enc na nb a b
(hash (exp (gen) (mul la beta))
(exp (gen) (mul x upsilon)))))) (send nb)))
(label 0)
(unrealized (0 1))
(origs (na (0 2)))
(comment "Not closed under rules"))
(defskeleton dhcr-um
(vars (ignore ignore-0 mesg) (na nb data) (b self name)
(pt pt-0 pt-1 pt-2 pval) (priv-stor priv-stor-0 locn)
(lb l x y rndx))
(defstrand init 5 (na na) (nb nb) (a self) (b b)
(priv-stor priv-stor-0) (la l) (x x) (beta lb) (upsilon y))
(defstrand ltx-gen 3 (ignore ignore) (self b) (priv-stor priv-stor)
(l lb))
(defstrand resp 4 (na na) (nb nb) (a self) (b b) (priv-stor priv-stor)
(lb lb) (y y) (alpha l) (zeta x))
(defstrand ltx-gen 3 (ignore ignore-0) (self self)
(priv-stor priv-stor-0) (l l))
(precedes ((0 2) (2 2)) ((1 1) (2 0)) ((1 2) (0 1)) ((2 3) (0 3))
((3 1) (0 0)) ((3 2) (2 1)))
(non-orig (privk "sig" b))
(uniq-orig na nb lb l)
(uniq-gen x y)
(absent (x lb) (x l) (y lb) (y l) (y x))
(gen-st (pv b lb) (pv self l))
(facts (neq (exp (gen) x) (gen)) (trans 1 1) (trans 1 0) (trans 3 1)
(trans 3 0) (neq (exp (gen) y) (gen)) (neq self b) (undisclosed l)
(undisclosed lb))
(operation nonce-test (displaced 4 2 resp 4) (exp (gen) y-0) (0 3))
(traces
((load priv-stor-0 (cat pt-2 (pv self l)))
(recv
(sig (body b (exp (gen) lb) (pubk "sig" b)) (privk "sig" b)))
(send (cat na self b (exp (gen) x)))
(recv
(cat (exp (gen) y)
(enc na nb self b
(hash (exp (gen) (mul lb l)) (exp (gen) (mul x y))))))
(send nb))
((load priv-stor (cat pt ignore))
(stor priv-stor (cat pt-0 (pv b lb)))
(send
(sig (body b (exp (gen) lb) (pubk "sig" b)) (privk "sig" b))))
((load priv-stor (cat pt-0 (pv b lb)))
(recv
(sig (body self (exp (gen) l) (pubk "sig" self))
(privk "sig" self))) (recv (cat na self b (exp (gen) x)))
(send
(cat (exp (gen) y)
(enc na nb self b
(hash (exp (gen) (mul lb l)) (exp (gen) (mul x y)))))))
((load priv-stor-0 (cat pt-1 ignore-0))
(stor priv-stor-0 (cat pt-2 (pv self l)))
(send
(sig (body self (exp (gen) l) (pubk "sig" self))
(privk "sig" self)))))
(label 16)
(parent 0)
(realized)
(shape)
(maps
((0)
((a self) (b b) (la l) (beta lb) (x x) (upsilon y) (na na) (nb nb)
(priv-stor priv-stor-0) (pt pt-2))))
(origs (nb (2 3)) (l (3 1)) (pt-2 (3 1)) (lb (1 1)) (pt-0 (1 1))
(na (0 2))))
(comment "Nothing left to do")
(defprotocol dhcr-um diffie-hellman
(defrole init
(vars (la x rndx) (beta upsilon expt) (a b name) (na nb data)
(priv-stor locn))
(trace (load priv-stor (pv a la))
(recv
(sig (body b (exp (gen) beta) (pubk "sig" b)) (privk "sig" b)))
(send (cat na a b (exp (gen) x)))
(recv
(cat (exp (gen) upsilon)
(enc na nb a b
(hash (exp (gen) (mul la beta))
(exp (gen) (mul x upsilon)))))) (send nb))
(uniq-orig na)
(uniq-gen x)
(absent (x la) (x beta))
(facts (neq (exp (gen) upsilon) (gen)))
(gen-st (pv a la))
(fn-of ("principal-of" (ltxa a) (ltxb b))
("ltx-of" (a ltxa) (b ltxb))))
(defrole resp
(vars (lb y rndx) (alpha zeta expt) (a b name) (na nb data)
(priv-stor locn))
(trace (load priv-stor (pv b lb))
(recv
(sig (body a (exp (gen) alpha) (pubk "sig" a)) (privk "sig" a)))
(recv (cat na a b (exp (gen) zeta)))
(send
(cat (exp (gen) y)
(enc na nb a b
(hash (exp (gen) (mul lb alpha))
(exp (gen) (mul y zeta)))))) (recv nb))
(uniq-orig nb)
(uniq-gen y)
(absent (y lb) (y alpha) (y zeta))
(facts (neq (exp (gen) zeta) (gen)))
(gen-st (pv b lb))
(fn-of ("principal-of" (ltxa a) (ltxb b))
("ltx-of" (a ltxa) (b ltxb))))
(defrole ltx-gen
(vars (self name) (l rndx) (priv-stor locn) (ignore mesg))
(trace (load priv-stor ignore) (stor priv-stor (pv self l))
(send
(sig (body self (exp (gen) l) (pubk "sig" self))
(privk "sig" self))))
(uniq-orig l)
(fn-of ("principal-of" (l self)) ("ltx-of" (self l))))
(defrole ltx-disclose
(vars (self name) (l rndx) (priv-stor locn))
(trace (load priv-stor (pv self l)) (stor priv-stor "nil") (send l))
(gen-st (pv self l))
(fn-of ("principal-of" (l self)) ("ltx-of" (self l))))
(defrule undisclosed-not-disclosed
(forall ((z strd) (l rndx))
(implies
(and (fact undisclosed l) (p "ltx-disclose" z 2)
(p "ltx-disclose" "l" z l))
(false))))
(defgenrule neqRl_indx
(forall ((x indx)) (implies (fact neq x x) (false))))
(defgenrule neqRl_strd
(forall ((x strd)) (implies (fact neq x x) (false))))
(defgenrule neqRl_mesg
(forall ((x mesg)) (implies (fact neq x x) (false))))
(defgenrule shearsRule
(forall ((z0 z1 z2 strd) (i0 i1 i2 indx))
(implies
(and (trans z0 i0) (trans z1 i1) (trans z2 i2)
(leads-to z0 i0 z1 i1) (same-locn z0 i0 z2 i2)
(prec z0 i0 z2 i2))
(or (and (= z1 z2) (= i1 i2)) (prec z1 i1 z2 i2)))))
(defgenrule invShearsRule
(forall ((z0 z1 z2 strd) (i0 i1 i2 indx))
(implies
(and (trans z0 i0) (trans z1 i1) (same-locn z0 i0 z1 i1)
(leads-to z1 i1 z2 i2) (prec z0 i0 z2 i2))
(or (and (= z0 z1) (= i0 i1)) (prec z0 i0 z1 i1)))))
(defgenrule fact-init-neq0
(forall ((z strd) (upsilon expt))
(implies (and (p "init" z 4) (p "init" "upsilon" z upsilon))
(fact neq (exp (gen) upsilon) (gen)))))
(defgenrule fact-resp-neq0
(forall ((z strd) (zeta expt))
(implies (and (p "resp" z 3) (p "resp" "zeta" z zeta))
(fact neq (exp (gen) zeta) (gen)))))
(defgenrule trRl_ltx-gen-at-1
(forall ((z strd)) (implies (p "ltx-gen" z 2) (trans z 1))))
(defgenrule trRl_ltx-gen-at-0
(forall ((z strd)) (implies (p "ltx-gen" z 2) (trans z 0))))
(defgenrule trRl_ltx-disclose-at-1
(forall ((z strd)) (implies (p "ltx-disclose" z 2) (trans z 1))))
(defgenrule trRl_ltx-disclose-at-0
(forall ((z strd)) (implies (p "ltx-disclose" z 2) (trans z 0))))
(defgenrule gen-st-init-0
(forall ((z strd) (la rndx) (a name))
(implies
(and (p "init" z 1) (p "init" "la" z la) (p "init" "a" z a))
(gen-st (pv a la)))))
(defgenrule gen-st-resp-0
(forall ((z strd) (lb rndx) (b name))
(implies
(and (p "resp" z 1) (p "resp" "lb" z lb) (p "resp" "b" z b))
(gen-st (pv b lb)))))
(defgenrule gen-st-ltx-disclose-0
(forall ((z strd) (l rndx) (self name))
(implies
(and (p "ltx-disclose" z 1) (p "ltx-disclose" "l" z l)
(p "ltx-disclose" "self" z self)) (gen-st (pv self l)))))
(lang (sig sign) (body (tuple 3)) (pv (tuple 2))))
(defskeleton dhcr-um
(vars (na nb data) (a b name) (pt pval) (priv-stor locn) (la rndx)
(beta expt) (x rndx) (upsilon expt))
(defstrand init 5 (na na) (nb nb) (a a) (b b) (priv-stor priv-stor)
(la la) (x x) (beta beta) (upsilon upsilon))
(non-orig (privk "sig" b))
(uniq-orig na)
(uniq-gen x)
(absent (x la) (x beta))
(facts (neq a b) (undisclosed beta))
(traces
((load priv-stor (cat pt (pv a la)))
(recv
(sig (body b (exp (gen) beta) (pubk "sig" b)) (privk "sig" b)))
(send (cat na a b (exp (gen) x)))
(recv
(cat (exp (gen) upsilon)
(enc na nb a b
(hash (exp (gen) (mul la beta))
(exp (gen) (mul x upsilon)))))) (send nb)))
(label 38)
(unrealized (0 1))
(origs (na (0 2)))
(comment "Not closed under rules"))
(defskeleton dhcr-um
(vars (ignore ignore-0 mesg) (na nb data) (b self name)
(pt pt-0 pt-1 pt-2 pval) (priv-stor priv-stor-0 locn)
(lb l x y rndx))
(defstrand init 5 (na na) (nb nb) (a self) (b b)
(priv-stor priv-stor-0) (la l) (x x) (beta lb) (upsilon y))
(defstrand ltx-gen 3 (ignore ignore) (self b) (priv-stor priv-stor)
(l lb))
(defstrand resp 4 (na na) (nb nb) (a self) (b b) (priv-stor priv-stor)
(lb lb) (y y) (alpha l) (zeta x))
(defstrand ltx-gen 3 (ignore ignore-0) (self self)
(priv-stor priv-stor-0) (l l))
(precedes ((0 2) (2 2)) ((1 1) (2 0)) ((1 2) (0 1)) ((2 3) (0 3))
((3 1) (0 0)) ((3 2) (2 1)))
(non-orig (privk "sig" b))
(uniq-orig na nb lb l)
(uniq-gen x y)
(absent (x lb) (x l) (y lb) (y l) (y x))
(gen-st (pv b lb) (pv self l))
(facts (neq (exp (gen) x) (gen)) (trans 1 1) (trans 1 0) (trans 3 1)
(trans 3 0) (neq (exp (gen) y) (gen)) (neq self b) (undisclosed lb))
(operation nonce-test (displaced 4 2 resp 4) (exp (gen) y-0) (0 3))
(traces
((load priv-stor-0 (cat pt-2 (pv self l)))
(recv
(sig (body b (exp (gen) lb) (pubk "sig" b)) (privk "sig" b)))
(send (cat na self b (exp (gen) x)))
(recv
(cat (exp (gen) y)
(enc na nb self b
(hash (exp (gen) (mul lb l)) (exp (gen) (mul x y))))))
(send nb))
((load priv-stor (cat pt ignore))
(stor priv-stor (cat pt-0 (pv b lb)))
(send
(sig (body b (exp (gen) lb) (pubk "sig" b)) (privk "sig" b))))
((load priv-stor (cat pt-0 (pv b lb)))
(recv
(sig (body self (exp (gen) l) (pubk "sig" self))
(privk "sig" self))) (recv (cat na self b (exp (gen) x)))
(send
(cat (exp (gen) y)
(enc na nb self b
(hash (exp (gen) (mul lb l)) (exp (gen) (mul x y)))))))
((load priv-stor-0 (cat pt-1 ignore-0))
(stor priv-stor-0 (cat pt-2 (pv self l)))
(send
(sig (body self (exp (gen) l) (pubk "sig" self))
(privk "sig" self)))))
(label 54)
(parent 38)
(realized)
(shape)
(maps
((0)
((a self) (b b) (la l) (beta lb) (x x) (upsilon y) (na na) (nb nb)
(priv-stor priv-stor-0) (pt pt-2))))
(origs (nb (2 3)) (l (3 1)) (pt-2 (3 1)) (lb (1 1)) (pt-0 (1 1))
(na (0 2))))
(defskeleton dhcr-um
(vars (ignore ignore-0 mesg) (na nb data) (a b name)
(pt pt-0 pt-1 pt-2 pt-3 pval) (priv-stor priv-stor-0 locn) (x rndx)
(upsilon expt) (l l-0 rndx))
(defstrand init 5 (na na) (nb nb) (a a) (b b) (priv-stor priv-stor)
(la l) (x x) (beta l-0) (upsilon upsilon))
(defstrand ltx-gen 2 (ignore ignore) (self a) (priv-stor priv-stor)
(l l))
(defstrand ltx-gen 3 (ignore ignore-0) (self b)
(priv-stor priv-stor-0) (l l-0))
(defstrand ltx-disclose 3 (self a) (priv-stor priv-stor) (l l))
(precedes ((1 1) (0 0)) ((1 1) (3 0)) ((2 2) (0 1)) ((3 2) (0 3)))
(non-orig (privk "sig" b))
(uniq-orig na l l-0)
(uniq-gen x)
(absent (x l) (x l-0))
(gen-st (pv a l))
(facts (trans 3 1) (trans 3 0) (trans 2 1) (trans 2 0) (trans 1 1)
(trans 1 0) (neq (exp (gen) upsilon) (gen)) (neq a b)
(undisclosed l-0))
(operation generalization deleted (3 0))
(traces
((load priv-stor (cat pt (pv a l)))
(recv
(sig (body b (exp (gen) l-0) (pubk "sig" b)) (privk "sig" b)))
(send (cat na a b (exp (gen) x)))
(recv
(cat (exp (gen) upsilon)
(enc na nb a b
(hash (exp (gen) (mul l l-0))
(exp (gen) (mul x upsilon)))))) (send nb))
((load priv-stor (cat pt-0 ignore))
(stor priv-stor (cat pt (pv a l))))
((load priv-stor-0 (cat pt-1 ignore-0))
(stor priv-stor-0 (cat pt-2 (pv b l-0)))
(send
(sig (body b (exp (gen) l-0) (pubk "sig" b)) (privk "sig" b))))
((load priv-stor (cat pt (pv a l)))
(stor priv-stor (cat pt-3 "nil")) (send l)))
(label 131)
(parent 38)
(realized)
(shape)
(maps
((0)
((a a) (b b) (la l) (beta l-0) (x x) (upsilon upsilon) (na na)
(nb nb) (priv-stor priv-stor) (pt pt))))
(origs (l-0 (2 1)) (pt-2 (2 1)) (pt-3 (3 1)) (l (1 1)) (pt (1 1))
(na (0 2))))
(defskeleton dhcr-um
(vars (ignore ignore-0 mesg) (na nb data) (a b name)
(pt pt-0 pt-1 pt-2 pt-3 pval) (priv-stor priv-stor-0 locn)
(lb l x y rndx))
(defstrand init 5 (na na) (nb nb) (a a) (b b) (priv-stor priv-stor)
(la l) (x x) (beta lb) (upsilon y))
(defstrand ltx-gen 2 (ignore ignore) (self a) (priv-stor priv-stor)
(l l))
(defstrand ltx-gen 3 (ignore ignore-0) (self b)
(priv-stor priv-stor-0) (l lb))
(defstrand ltx-disclose 3 (self a) (priv-stor priv-stor) (l l))
(precedes ((1 1) (0 0)) ((1 1) (3 0)) ((2 2) (0 1)) ((3 2) (0 3)))
(non-orig (privk "sig" b))
(uniq-orig na lb l)
(uniq-gen x y)
(absent (x lb) (x l) (y lb) (y l) (y x))
(gen-st (pv a l) (pv b lb))
(facts (trans 3 1) (trans 3 0) (neq (exp (gen) x) (gen)) (trans 2 1)
(trans 2 0) (trans 1 1) (trans 1 0) (neq (exp (gen) y) (gen))
(neq a b) (undisclosed lb))
(operation generalization forgot nb)
(traces
((load priv-stor (cat pt (pv a l)))
(recv
(sig (body b (exp (gen) lb) (pubk "sig" b)) (privk "sig" b)))
(send (cat na a b (exp (gen) x)))
(recv
(cat (exp (gen) y)
(enc na nb a b
(hash (exp (gen) (mul lb l)) (exp (gen) (mul x y))))))
(send nb))
((load priv-stor (cat pt-0 ignore))
(stor priv-stor (cat pt (pv a l))))
((load priv-stor-0 (cat pt-1 ignore-0))
(stor priv-stor-0 (cat pt-2 (pv b lb)))
(send
(sig (body b (exp (gen) lb) (pubk "sig" b)) (privk "sig" b))))
((load priv-stor (cat pt (pv a l)))
(stor priv-stor (cat pt-3 "nil")) (send l)))
(label 133)
(parent 38)
(realized)
(shape)
(maps
((0)
((a a) (b b) (la l) (beta lb) (x x) (upsilon y) (na na) (nb nb)
(priv-stor priv-stor) (pt pt))))
(origs (pt-3 (3 1)) (lb (2 1)) (pt-2 (2 1)) (l (1 1)) (pt (1 1))
(na (0 2))))
(defskeleton dhcr-um
(vars (ignore ignore-0 ignore-1 mesg) (na nb data) (a b b-0 name)
(pt pt-0 pt-1 pt-2 pt-3 pt-4 pt-5 pval)
(priv-stor priv-stor-0 priv-stor-1 locn) (l l-0 lb x y rndx))
(defstrand init 5 (na na) (nb nb) (a a) (b b-0) (priv-stor priv-stor)
(la l) (x x) (beta l-0) (upsilon y))
(defstrand ltx-gen 2 (ignore ignore) (self a) (priv-stor priv-stor)
(l l))
(defstrand ltx-gen 3 (ignore ignore-0) (self b-0)
(priv-stor priv-stor-0) (l l-0))
(defstrand ltx-gen 2 (ignore ignore-1) (self b)
(priv-stor priv-stor-1) (l lb))
(defstrand ltx-disclose 3 (self a) (priv-stor priv-stor) (l l))
(precedes ((1 1) (0 0)) ((1 1) (4 0)) ((2 2) (0 1)) ((4 2) (0 3)))
(non-orig (privk "sig" b-0))
(uniq-orig na l l-0 lb)
(uniq-gen x y)
(absent (x l) (x l-0) (y (mul l l-0 (rec lb))) (y lb) (y x))
(gen-st (pv a l) (pv b lb))
(facts (trans 4 1) (trans 4 0) (trans 3 1) (trans 3 0)
(neq (exp (gen) x) (gen)) (trans 2 1) (trans 2 0) (trans 1 1)
(trans 1 0) (neq (exp (gen) y) (gen)) (neq a b-0) (undisclosed l-0))
(operation generalization forgot (privk "sig" b))
(traces
((load priv-stor (cat pt (pv a l)))
(recv
(sig (body b-0 (exp (gen) l-0) (pubk "sig" b-0))
(privk "sig" b-0))) (send (cat na a b-0 (exp (gen) x)))
(recv
(cat (exp (gen) y)
(enc na nb a b-0
(hash (exp (gen) (mul l l-0)) (exp (gen) (mul x y))))))
(send nb))
((load priv-stor (cat pt-0 ignore))
(stor priv-stor (cat pt (pv a l))))
((load priv-stor-0 (cat pt-1 ignore-0))
(stor priv-stor-0 (cat pt-2 (pv b-0 l-0)))
(send
(sig (body b-0 (exp (gen) l-0) (pubk "sig" b-0))
(privk "sig" b-0))))
((load priv-stor-1 (cat pt-4 ignore-1))
(stor priv-stor-1 (cat pt-3 (pv b lb))))
((load priv-stor (cat pt (pv a l)))
(stor priv-stor (cat pt-5 "nil")) (send l)))
(label 200)
(parent 38)
(realized)
(shape)
(maps
((0)
((a a) (b b-0) (la l) (beta l-0) (x x) (upsilon y) (na na) (nb nb)
(priv-stor priv-stor) (pt pt))))
(origs (l-0 (2 1)) (pt-2 (2 1)) (pt-5 (4 1)) (lb (3 1)) (pt-3 (3 1))
(l (1 1)) (pt (1 1)) (na (0 2))))
(defskeleton dhcr-um
(vars (ignore ignore-0 mesg) (na nb data) (a b name)
(pt pt-0 pt-1 pt-2 pt-3 pval) (priv-stor priv-stor-0 locn)
(lb l x rndx) (w expt) (y rndx))
(defstrand init 5 (na na) (nb nb) (a a) (b b) (priv-stor priv-stor)
(la l) (x x) (beta lb) (upsilon (mul w y)))
(defstrand ltx-gen 2 (ignore ignore) (self a) (priv-stor priv-stor)
(l l))
(defstrand ltx-gen 3 (ignore ignore-0) (self b)
(priv-stor priv-stor-0) (l lb))
(defstrand ltx-disclose 3 (self a) (priv-stor priv-stor) (l l))
(deflistener (cat (exp (gen) y) w))
(precedes ((1 1) (0 0)) ((1 1) (3 0)) ((2 2) (0 1)) ((3 2) (0 3)))
(non-orig (privk "sig" b))
(uniq-orig na lb l)
(uniq-gen x y)
(absent (x lb) (x l) (y lb) (y l) (y (mul x w)))
(precur (4 0))
(gen-st (pv a l) (pv b lb))
(facts (trans 3 1) (trans 3 0) (neq (exp (gen) (mul x w)) (gen))
(trans 2 1) (trans 2 0) (trans 1 1) (trans 1 0)
(neq (exp (gen) (mul w y)) (gen)) (neq a b) (undisclosed lb))
(operation generalization forgot nb)
(traces
((load priv-stor (cat pt (pv a l)))
(recv
(sig (body b (exp (gen) lb) (pubk "sig" b)) (privk "sig" b)))
(send (cat na a b (exp (gen) x)))
(recv
(cat (exp (gen) (mul w y))
(enc na nb a b
(hash (exp (gen) (mul lb l)) (exp (gen) (mul x w y))))))
(send nb))
((load priv-stor (cat pt-0 ignore))
(stor priv-stor (cat pt (pv a l))))
((load priv-stor-0 (cat pt-1 ignore-0))
(stor priv-stor-0 (cat pt-2 (pv b lb)))
(send
(sig (body b (exp (gen) lb) (pubk "sig" b)) (privk "sig" b))))
((load priv-stor (cat pt (pv a l)))
(stor priv-stor (cat pt-3 "nil")) (send l))
((recv (cat (exp (gen) y) w))))
(label 202)
(parent 38)
(realized)
(shape)
(maps
((0)
((a a) (b b) (la l) (beta lb) (x x) (upsilon (mul w y)) (na na)
(nb nb) (priv-stor priv-stor) (pt pt))))
(origs (pt-3 (3 1)) (lb (2 1)) (pt-2 (2 1)) (l (1 1)) (pt (1 1))
(na (0 2))))
(defskeleton dhcr-um
(vars (ignore ignore-0 ignore-1 mesg) (na nb data) (a b b-0 name)
(pt pt-0 pt-1 pt-2 pt-3 pt-4 pt-5 pval)
(priv-stor priv-stor-0 priv-stor-1 locn) (l l-0 lb x rndx) (w expt)
(y rndx))
(defstrand init 5 (na na) (nb nb) (a a) (b b-0) (priv-stor priv-stor)
(la l) (x x) (beta l-0) (upsilon (mul w y)))
(defstrand ltx-gen 2 (ignore ignore) (self a) (priv-stor priv-stor)
(l l))
(defstrand ltx-gen 3 (ignore ignore-0) (self b-0)
(priv-stor priv-stor-0) (l l-0))
(defstrand ltx-gen 2 (ignore ignore-1) (self b)
(priv-stor priv-stor-1) (l lb))
(defstrand ltx-disclose 3 (self a) (priv-stor priv-stor) (l l))
(deflistener (cat (exp (gen) y) w))
(precedes ((1 1) (0 0)) ((1 1) (4 0)) ((2 2) (0 1)) ((4 2) (0 3)))
(non-orig (privk "sig" b-0))
(uniq-orig na l l-0 lb)
(uniq-gen x y)
(absent (x l) (x l-0) (y (mul l l-0 (rec lb))) (y lb) (y (mul x w)))
(precur (5 0))
(gen-st (pv a l) (pv b lb))
(facts (trans 4 1) (trans 4 0) (trans 3 1) (trans 3 0)
(neq (exp (gen) (mul x w)) (gen)) (trans 2 1) (trans 2 0)
(trans 1 1) (trans 1 0) (neq (exp (gen) (mul w y)) (gen))
(neq a b-0) (undisclosed l-0))
(operation generalization forgot (privk "sig" b))
(traces
((load priv-stor (cat pt (pv a l)))
(recv
(sig (body b-0 (exp (gen) l-0) (pubk "sig" b-0))
(privk "sig" b-0))) (send (cat na a b-0 (exp (gen) x)))
(recv
(cat (exp (gen) (mul w y))
(enc na nb a b-0
(hash (exp (gen) (mul l l-0)) (exp (gen) (mul x w y))))))
(send nb))
((load priv-stor (cat pt-0 ignore))
(stor priv-stor (cat pt (pv a l))))
((load priv-stor-0 (cat pt-1 ignore-0))
(stor priv-stor-0 (cat pt-2 (pv b-0 l-0)))
(send
(sig (body b-0 (exp (gen) l-0) (pubk "sig" b-0))
(privk "sig" b-0))))
((load priv-stor-1 (cat pt-4 ignore-1))
(stor priv-stor-1 (cat pt-3 (pv b lb))))
((load priv-stor (cat pt (pv a l)))
(stor priv-stor (cat pt-5 "nil")) (send l))
((recv (cat (exp (gen) y) w))))
(label 211)
(parent 38)
(realized)
(shape)
(maps
((0)
((a a) (b b-0) (la l) (beta l-0) (x x) (upsilon (mul w y)) (na na)
(nb nb) (priv-stor priv-stor) (pt pt))))
(origs (l-0 (2 1)) (pt-2 (2 1)) (pt-5 (4 1)) (lb (3 1)) (pt-3 (3 1))
(l (1 1)) (pt (1 1)) (na (0 2))))
(comment "Nothing left to do")
(defprotocol dhcr-um diffie-hellman
(defrole init
(vars (la x rndx) (beta upsilon expt) (a b name) (na nb data)
(priv-stor locn))
(trace (load priv-stor (pv a la))
(recv
(sig (body b (exp (gen) beta) (pubk "sig" b)) (privk "sig" b)))
(send (cat na a b (exp (gen) x)))
(recv
(cat (exp (gen) upsilon)
(enc na nb a b
(hash (exp (gen) (mul la beta))
(exp (gen) (mul x upsilon)))))) (send nb))
(uniq-orig na)
(uniq-gen x)
(absent (x la) (x beta))
(facts (neq (exp (gen) upsilon) (gen)))
(gen-st (pv a la))
(fn-of ("principal-of" (ltxa a) (ltxb b))
("ltx-of" (a ltxa) (b ltxb))))
(defrole resp
(vars (lb y rndx) (alpha zeta expt) (a b name) (na nb data)
(priv-stor locn))
(trace (load priv-stor (pv b lb))
(recv
(sig (body a (exp (gen) alpha) (pubk "sig" a)) (privk "sig" a)))
(recv (cat na a b (exp (gen) zeta)))
(send
(cat (exp (gen) y)
(enc na nb a b
(hash (exp (gen) (mul lb alpha))
(exp (gen) (mul y zeta)))))) (recv nb))
(uniq-orig nb)
(uniq-gen y)
(absent (y lb) (y alpha) (y zeta))
(facts (neq (exp (gen) zeta) (gen)))
(gen-st (pv b lb))
(fn-of ("principal-of" (ltxa a) (ltxb b))
("ltx-of" (a ltxa) (b ltxb))))
(defrole ltx-gen
(vars (self name) (l rndx) (priv-stor locn) (ignore mesg))
(trace (load priv-stor ignore) (stor priv-stor (pv self l))
(send
(sig (body self (exp (gen) l) (pubk "sig" self))
(privk "sig" self))))
(uniq-orig l)
(fn-of ("principal-of" (l self)) ("ltx-of" (self l))))
(defrole ltx-disclose
(vars (self name) (l rndx) (priv-stor locn))
(trace (load priv-stor (pv self l)) (stor priv-stor "nil") (send l))
(gen-st (pv self l))
(fn-of ("principal-of" (l self)) ("ltx-of" (self l))))
(defrule undisclosed-not-disclosed
(forall ((z strd) (l rndx))
(implies
(and (fact undisclosed l) (p "ltx-disclose" z 2)
(p "ltx-disclose" "l" z l))
(false))))
(defgenrule neqRl_indx
(forall ((x indx)) (implies (fact neq x x) (false))))
(defgenrule neqRl_strd
(forall ((x strd)) (implies (fact neq x x) (false))))
(defgenrule neqRl_mesg
(forall ((x mesg)) (implies (fact neq x x) (false))))
(defgenrule shearsRule
(forall ((z0 z1 z2 strd) (i0 i1 i2 indx))
(implies
(and (trans z0 i0) (trans z1 i1) (trans z2 i2)
(leads-to z0 i0 z1 i1) (same-locn z0 i0 z2 i2)
(prec z0 i0 z2 i2))
(or (and (= z1 z2) (= i1 i2)) (prec z1 i1 z2 i2)))))
(defgenrule invShearsRule
(forall ((z0 z1 z2 strd) (i0 i1 i2 indx))
(implies
(and (trans z0 i0) (trans z1 i1) (same-locn z0 i0 z1 i1)
(leads-to z1 i1 z2 i2) (prec z0 i0 z2 i2))
(or (and (= z0 z1) (= i0 i1)) (prec z0 i0 z1 i1)))))
(defgenrule fact-init-neq0
(forall ((z strd) (upsilon expt))
(implies (and (p "init" z 4) (p "init" "upsilon" z upsilon))
(fact neq (exp (gen) upsilon) (gen)))))
(defgenrule fact-resp-neq0
(forall ((z strd) (zeta expt))
(implies (and (p "resp" z 3) (p "resp" "zeta" z zeta))
(fact neq (exp (gen) zeta) (gen)))))
(defgenrule trRl_ltx-gen-at-1
(forall ((z strd)) (implies (p "ltx-gen" z 2) (trans z 1))))
(defgenrule trRl_ltx-gen-at-0
(forall ((z strd)) (implies (p "ltx-gen" z 2) (trans z 0))))
(defgenrule trRl_ltx-disclose-at-1
(forall ((z strd)) (implies (p "ltx-disclose" z 2) (trans z 1))))
(defgenrule trRl_ltx-disclose-at-0
(forall ((z strd)) (implies (p "ltx-disclose" z 2) (trans z 0))))
(defgenrule gen-st-init-0
(forall ((z strd) (la rndx) (a name))
(implies
(and (p "init" z 1) (p "init" "la" z la) (p "init" "a" z a))
(gen-st (pv a la)))))
(defgenrule gen-st-resp-0
(forall ((z strd) (lb rndx) (b name))
(implies
(and (p "resp" z 1) (p "resp" "lb" z lb) (p "resp" "b" z b))
(gen-st (pv b lb)))))
(defgenrule gen-st-ltx-disclose-0
(forall ((z strd) (l rndx) (self name))
(implies
(and (p "ltx-disclose" z 1) (p "ltx-disclose" "l" z l)
(p "ltx-disclose" "self" z self)) (gen-st (pv self l)))))
(lang (sig sign) (body (tuple 3)) (pv (tuple 2))))
(defskeleton dhcr-um
(vars (na nb data) (a b name) (pt pval) (priv-stor locn) (la x rndx)
(beta upsilon expt))
(defstrand init 5 (na na) (nb nb) (a a) (b b) (priv-stor priv-stor)
(la la) (x x) (beta beta) (upsilon upsilon))
(non-orig (privk "sig" b))
(uniq-orig na)
(uniq-gen x)
(absent (x la) (x beta))
(facts (neq a b) (undisclosed la))
(traces
((load priv-stor (cat pt (pv a la)))
(recv
(sig (body b (exp (gen) beta) (pubk "sig" b)) (privk "sig" b)))
(send (cat na a b (exp (gen) x)))
(recv
(cat (exp (gen) upsilon)
(enc na nb a b
(hash (exp (gen) (mul la beta))
(exp (gen) (mul x upsilon)))))) (send nb)))
(label 212)
(unrealized (0 1))
(origs (na (0 2)))
(comment "Not closed under rules"))
(defskeleton dhcr-um
(vars (ignore ignore-0 mesg) (na nb data) (b self name)
(pt pt-0 pt-1 pt-2 pval) (priv-stor priv-stor-0 locn)
(lb l x y rndx))
(defstrand init 5 (na na) (nb nb) (a self) (b b)
(priv-stor priv-stor-0) (la l) (x x) (beta lb) (upsilon y))
(defstrand ltx-gen 3 (ignore ignore) (self b) (priv-stor priv-stor)
(l lb))
(defstrand resp 4 (na na) (nb nb) (a self) (b b) (priv-stor priv-stor)
(lb lb) (y y) (alpha l) (zeta x))
(defstrand ltx-gen 3 (ignore ignore-0) (self self)
(priv-stor priv-stor-0) (l l))
(precedes ((0 2) (2 2)) ((1 1) (2 0)) ((1 2) (0 1)) ((2 3) (0 3))
((3 1) (0 0)) ((3 2) (2 1)))
(non-orig (privk "sig" b))
(uniq-orig na nb lb l)
(uniq-gen x y)
(absent (x lb) (x l) (y lb) (y l) (y x))
(gen-st (pv b lb) (pv self l))
(facts (neq (exp (gen) x) (gen)) (trans 1 1) (trans 1 0) (trans 3 1)
(trans 3 0) (neq (exp (gen) y) (gen)) (neq self b) (undisclosed l))
(operation nonce-test (displaced 4 2 resp 4) (exp (gen) y-0) (0 3))
(traces
((load priv-stor-0 (cat pt-2 (pv self l)))
(recv
(sig (body b (exp (gen) lb) (pubk "sig" b)) (privk "sig" b)))
(send (cat na self b (exp (gen) x)))
(recv
(cat (exp (gen) y)
(enc na nb self b
(hash (exp (gen) (mul lb l)) (exp (gen) (mul x y))))))
(send nb))
((load priv-stor (cat pt ignore))
(stor priv-stor (cat pt-0 (pv b lb)))
(send
(sig (body b (exp (gen) lb) (pubk "sig" b)) (privk "sig" b))))
((load priv-stor (cat pt-0 (pv b lb)))
(recv
(sig (body self (exp (gen) l) (pubk "sig" self))
(privk "sig" self))) (recv (cat na self b (exp (gen) x)))
(send
(cat (exp (gen) y)
(enc na nb self b
(hash (exp (gen) (mul lb l)) (exp (gen) (mul x y)))))))
((load priv-stor-0 (cat pt-1 ignore-0))
(stor priv-stor-0 (cat pt-2 (pv self l)))
(send
(sig (body self (exp (gen) l) (pubk "sig" self))
(privk "sig" self)))))
(label 228)
(parent 212)
(realized)
(shape)
(maps
((0)
((a self) (b b) (la l) (x x) (beta lb) (upsilon y) (na na) (nb nb)
(priv-stor priv-stor-0) (pt pt-2))))
(origs (nb (2 3)) (l (3 1)) (pt-2 (3 1)) (lb (1 1)) (pt-0 (1 1))
(na (0 2))))
(defskeleton dhcr-um
(vars (ignore ignore-0 mesg) (na nb data) (b self name)
(pt pt-0 pt-1 pt-2 pt-3 pval) (priv-stor priv-stor-0 locn) (x rndx)
(upsilon expt) (l l-0 rndx))
(defstrand init 5 (na na) (nb nb) (a self) (b b)
(priv-stor priv-stor-0) (la l-0) (x x) (beta l) (upsilon upsilon))
(defstrand ltx-gen 3 (ignore ignore) (self b) (priv-stor priv-stor)
(l l))
(defstrand ltx-disclose 3 (self b) (priv-stor priv-stor) (l l))
(defstrand ltx-gen 3 (ignore ignore-0) (self self)
(priv-stor priv-stor-0) (l l-0))
(precedes ((1 1) (2 0)) ((1 2) (0 1)) ((2 2) (0 3)) ((3 1) (0 0))
((3 2) (0 3)))
(non-orig (privk "sig" b))
(uniq-orig na l l-0)
(uniq-gen x)
(absent (x l) (x l-0))
(gen-st (pv b l) (pv self l-0))
(facts (trans 2 1) (trans 2 0) (trans 1 1) (trans 1 0) (trans 3 1)
(trans 3 0) (neq (exp (gen) upsilon) (gen)) (neq self b)
(undisclosed l-0))
(operation generalization deleted (2 0))
(traces
((load priv-stor-0 (cat pt-3 (pv self l-0)))
(recv (sig (body b (exp (gen) l) (pubk "sig" b)) (privk "sig" b)))
(send (cat na self b (exp (gen) x)))
(recv
(cat (exp (gen) upsilon)
(enc na nb self b
(hash (exp (gen) (mul l l-0))
(exp (gen) (mul x upsilon)))))) (send nb))
((load priv-stor (cat pt ignore))
(stor priv-stor (cat pt-0 (pv b l)))
(send
(sig (body b (exp (gen) l) (pubk "sig" b)) (privk "sig" b))))
((load priv-stor (cat pt-0 (pv b l)))
(stor priv-stor (cat pt-1 "nil")) (send l))
((load priv-stor-0 (cat pt-2 ignore-0))
(stor priv-stor-0 (cat pt-3 (pv self l-0)))
(send
(sig (body self (exp (gen) l-0) (pubk "sig" self))
(privk "sig" self)))))
(label 298)
(parent 212)
(realized)
(shape)
(maps
((0)
((a self) (b b) (la l-0) (x x) (beta l) (upsilon upsilon) (na na)
(nb nb) (priv-stor priv-stor-0) (pt pt-3))))
(origs (l-0 (3 1)) (pt-3 (3 1)) (pt-1 (2 1)) (l (1 1)) (pt-0 (1 1))
(na (0 2))))
(defskeleton dhcr-um
(vars (ignore ignore-0 ignore-1 mesg) (na nb data) (b self name)
(pt pt-0 pt-1 pt-2 pt-3 pt-4 pt-5 pval)
(priv-stor priv-stor-0 priv-stor-1 locn) (l l-0 lb x y rndx))
(defstrand init 5 (na na) (nb nb) (a self) (b b)
(priv-stor priv-stor-1) (la l-0) (x x) (beta l) (upsilon y))
(defstrand ltx-gen 3 (ignore ignore) (self b) (priv-stor priv-stor)
(l l))
(defstrand ltx-gen 2 (ignore ignore-0) (self b)
(priv-stor priv-stor-0) (l lb))
(defstrand ltx-disclose 3 (self b) (priv-stor priv-stor) (l l))
(defstrand ltx-gen 3 (ignore ignore-1) (self self)
(priv-stor priv-stor-1) (l l-0))
(precedes ((1 1) (3 0)) ((1 2) (0 1)) ((3 2) (0 3)) ((4 1) (0 0))
((4 2) (0 3)))
(non-orig (privk "sig" b))
(uniq-orig na l l-0 lb)
(uniq-gen x y)
(absent (x l) (x l-0) (y (mul l l-0 (rec lb))) (y lb) (y x))
(gen-st (pv b l) (pv b lb) (pv self l-0))
(facts (trans 3 1) (trans 3 0) (trans 2 1) (trans 2 0)
(neq (exp (gen) x) (gen)) (trans 1 1) (trans 1 0) (trans 4 1)
(trans 4 0) (neq (exp (gen) y) (gen)) (neq self b)
(undisclosed l-0))
(operation generalization forgot nb)
(traces
((load priv-stor-1 (cat pt-5 (pv self l-0)))
(recv (sig (body b (exp (gen) l) (pubk "sig" b)) (privk "sig" b)))
(send (cat na self b (exp (gen) x)))
(recv
(cat (exp (gen) y)
(enc na nb self b
(hash (exp (gen) (mul l l-0)) (exp (gen) (mul x y))))))
(send nb))
((load priv-stor (cat pt ignore))
(stor priv-stor (cat pt-0 (pv b l)))
(send
(sig (body b (exp (gen) l) (pubk "sig" b)) (privk "sig" b))))
((load priv-stor-0 (cat pt-2 ignore-0))
(stor priv-stor-0 (cat pt-1 (pv b lb))))
((load priv-stor (cat pt-0 (pv b l)))
(stor priv-stor (cat pt-3 "nil")) (send l))
((load priv-stor-1 (cat pt-4 ignore-1))
(stor priv-stor-1 (cat pt-5 (pv self l-0)))
(send
(sig (body self (exp (gen) l-0) (pubk "sig" self))
(privk "sig" self)))))
(label 353)
(parent 212)
(realized)
(shape)
(maps
((0)
((a self) (b b) (la l-0) (x x) (beta l) (upsilon y) (na na)
(nb nb) (priv-stor priv-stor-1) (pt pt-5))))
(origs (l-0 (4 1)) (pt-5 (4 1)) (pt-3 (3 1)) (lb (2 1)) (pt-1 (2 1))
(l (1 1)) (pt-0 (1 1)) (na (0 2))))
(defskeleton dhcr-um
(vars (ignore ignore-0 ignore-1 mesg) (na nb data) (b self name)
(pt pt-0 pt-1 pt-2 pt-3 pt-4 pt-5 pval)
(priv-stor priv-stor-0 priv-stor-1 locn) (l l-0 lb x rndx) (w expt)
(y rndx))
(defstrand init 5 (na na) (nb nb) (a self) (b b)
(priv-stor priv-stor-1) (la l-0) (x x) (beta l) (upsilon (mul w y)))
(defstrand ltx-gen 3 (ignore ignore) (self b) (priv-stor priv-stor)
(l l))
(defstrand ltx-gen 2 (ignore ignore-0) (self b)
(priv-stor priv-stor-0) (l lb))
(defstrand ltx-disclose 3 (self b) (priv-stor priv-stor) (l l))
(defstrand ltx-gen 3 (ignore ignore-1) (self self)
(priv-stor priv-stor-1) (l l-0))
(deflistener (cat (exp (gen) y) w))
(precedes ((1 1) (3 0)) ((1 2) (0 1)) ((3 2) (0 3)) ((4 1) (0 0))
((4 2) (0 3)))
(non-orig (privk "sig" b))
(uniq-orig na l l-0 lb)
(uniq-gen x y)
(absent (x l) (x l-0) (y (mul l l-0 (rec lb))) (y lb) (y (mul x w)))
(precur (5 0))
(gen-st (pv b l) (pv b lb) (pv self l-0))
(facts (trans 3 1) (trans 3 0) (trans 2 1) (trans 2 0)
(neq (exp (gen) (mul x w)) (gen)) (trans 1 1) (trans 1 0)
(trans 4 1) (trans 4 0) (neq (exp (gen) (mul w y)) (gen))
(neq self b) (undisclosed l-0))
(operation generalization forgot nb)
(traces
((load priv-stor-1 (cat pt-5 (pv self l-0)))
(recv (sig (body b (exp (gen) l) (pubk "sig" b)) (privk "sig" b)))
(send (cat na self b (exp (gen) x)))
(recv
(cat (exp (gen) (mul w y))
(enc na nb self b
(hash (exp (gen) (mul l l-0)) (exp (gen) (mul x w y))))))
(send nb))
((load priv-stor (cat pt ignore))
(stor priv-stor (cat pt-0 (pv b l)))
(send
(sig (body b (exp (gen) l) (pubk "sig" b)) (privk "sig" b))))
((load priv-stor-0 (cat pt-2 ignore-0))
(stor priv-stor-0 (cat pt-1 (pv b lb))))
((load priv-stor (cat pt-0 (pv b l)))
(stor priv-stor (cat pt-3 "nil")) (send l))
((load priv-stor-1 (cat pt-4 ignore-1))
(stor priv-stor-1 (cat pt-5 (pv self l-0)))
(send
(sig (body self (exp (gen) l-0) (pubk "sig" self))
(privk "sig" self)))) ((recv (cat (exp (gen) y) w))))
(label 365)
(parent 212)
(realized)
(shape)
(maps
((0)
((a self) (b b) (la l-0) (x x) (beta l) (upsilon (mul w y))
(na na) (nb nb) (priv-stor priv-stor-1) (pt pt-5))))
(origs (l-0 (4 1)) (pt-5 (4 1)) (pt-3 (3 1)) (lb (2 1)) (pt-1 (2 1))
(l (1 1)) (pt-0 (1 1)) (na (0 2))))
(comment "Nothing left to do")
(defprotocol dhcr-um diffie-hellman
(defrole init
(vars (la x rndx) (beta upsilon expt) (a b name) (na nb data)
(priv-stor locn))
(trace (load priv-stor (pv a la))
(recv
(sig (body b (exp (gen) beta) (pubk "sig" b)) (privk "sig" b)))
(send (cat na a b (exp (gen) x)))
(recv
(cat (exp (gen) upsilon)
(enc na nb a b
(hash (exp (gen) (mul la beta))
(exp (gen) (mul x upsilon)))))) (send nb))
(uniq-orig na)
(uniq-gen x)
(absent (x la) (x beta))
(facts (neq (exp (gen) upsilon) (gen)))
(gen-st (pv a la))
(fn-of ("principal-of" (ltxa a) (ltxb b))
("ltx-of" (a ltxa) (b ltxb))))
(defrole resp
(vars (lb y rndx) (alpha zeta expt) (a b name) (na nb data)
(priv-stor locn))
(trace (load priv-stor (pv b lb))
(recv
(sig (body a (exp (gen) alpha) (pubk "sig" a)) (privk "sig" a)))
(recv (cat na a b (exp (gen) zeta)))
(send
(cat (exp (gen) y)
(enc na nb a b
(hash (exp (gen) (mul lb alpha))
(exp (gen) (mul y zeta)))))) (recv nb))
(uniq-orig nb)
(uniq-gen y)
(absent (y lb) (y alpha) (y zeta))
(facts (neq (exp (gen) zeta) (gen)))
(gen-st (pv b lb))
(fn-of ("principal-of" (ltxa a) (ltxb b))
("ltx-of" (a ltxa) (b ltxb))))
(defrole ltx-gen
(vars (self name) (l rndx) (priv-stor locn) (ignore mesg))
(trace (load priv-stor ignore) (stor priv-stor (pv self l))
(send
(sig (body self (exp (gen) l) (pubk "sig" self))
(privk "sig" self))))
(uniq-orig l)
(fn-of ("principal-of" (l self)) ("ltx-of" (self l))))
(defrole ltx-disclose
(vars (self name) (l rndx) (priv-stor locn))
(trace (load priv-stor (pv self l)) (stor priv-stor "nil") (send l))
(gen-st (pv self l))
(fn-of ("principal-of" (l self)) ("ltx-of" (self l))))
(defrule undisclosed-not-disclosed
(forall ((z strd) (l rndx))
(implies
(and (fact undisclosed l) (p "ltx-disclose" z 2)
(p "ltx-disclose" "l" z l))
(false))))
(defgenrule neqRl_indx
(forall ((x indx)) (implies (fact neq x x) (false))))
(defgenrule neqRl_strd
(forall ((x strd)) (implies (fact neq x x) (false))))
(defgenrule neqRl_mesg
(forall ((x mesg)) (implies (fact neq x x) (false))))
(defgenrule shearsRule
(forall ((z0 z1 z2 strd) (i0 i1 i2 indx))
(implies
(and (trans z0 i0) (trans z1 i1) (trans z2 i2)
(leads-to z0 i0 z1 i1) (same-locn z0 i0 z2 i2)
(prec z0 i0 z2 i2))
(or (and (= z1 z2) (= i1 i2)) (prec z1 i1 z2 i2)))))
(defgenrule invShearsRule
(forall ((z0 z1 z2 strd) (i0 i1 i2 indx))
(implies
(and (trans z0 i0) (trans z1 i1) (same-locn z0 i0 z1 i1)
(leads-to z1 i1 z2 i2) (prec z0 i0 z2 i2))
(or (and (= z0 z1) (= i0 i1)) (prec z0 i0 z1 i1)))))
(defgenrule fact-init-neq0
(forall ((z strd) (upsilon expt))
(implies (and (p "init" z 4) (p "init" "upsilon" z upsilon))
(fact neq (exp (gen) upsilon) (gen)))))
(defgenrule fact-resp-neq0
(forall ((z strd) (zeta expt))
(implies (and (p "resp" z 3) (p "resp" "zeta" z zeta))
(fact neq (exp (gen) zeta) (gen)))))
(defgenrule trRl_ltx-gen-at-1
(forall ((z strd)) (implies (p "ltx-gen" z 2) (trans z 1))))
(defgenrule trRl_ltx-gen-at-0
(forall ((z strd)) (implies (p "ltx-gen" z 2) (trans z 0))))
(defgenrule trRl_ltx-disclose-at-1
(forall ((z strd)) (implies (p "ltx-disclose" z 2) (trans z 1))))
(defgenrule trRl_ltx-disclose-at-0
(forall ((z strd)) (implies (p "ltx-disclose" z 2) (trans z 0))))
(defgenrule gen-st-init-0
(forall ((z strd) (la rndx) (a name))
(implies
(and (p "init" z 1) (p "init" "la" z la) (p "init" "a" z a))
(gen-st (pv a la)))))
(defgenrule gen-st-resp-0
(forall ((z strd) (lb rndx) (b name))
(implies
(and (p "resp" z 1) (p "resp" "lb" z lb) (p "resp" "b" z b))
(gen-st (pv b lb)))))
(defgenrule gen-st-ltx-disclose-0
(forall ((z strd) (l rndx) (self name))
(implies
(and (p "ltx-disclose" z 1) (p "ltx-disclose" "l" z l)
(p "ltx-disclose" "self" z self)) (gen-st (pv self l)))))
(lang (sig sign) (body (tuple 3)) (pv (tuple 2))))
(defskeleton dhcr-um
(vars (na nb data) (a b name) (pt pval) (priv-stor locn) (la x rndx)
(beta upsilon expt))
(defstrand init 5 (na na) (nb nb) (a a) (b b) (priv-stor priv-stor)
(la la) (x x) (beta beta) (upsilon upsilon))
(non-orig (privk "sig" b))
(uniq-orig na)
(uniq-gen x)
(absent (x la) (x beta))
(facts (neq a b))
(traces
((load priv-stor (cat pt (pv a la)))
(recv
(sig (body b (exp (gen) beta) (pubk "sig" b)) (privk "sig" b)))
(send (cat na a b (exp (gen) x)))
(recv
(cat (exp (gen) upsilon)
(enc na nb a b
(hash (exp (gen) (mul la beta))
(exp (gen) (mul x upsilon)))))) (send nb)))
(label 366)
(unrealized (0 1))
(origs (na (0 2)))
(comment "Not closed under rules"))
(defskeleton dhcr-um
(vars (ignore ignore-0 mesg) (na nb data) (b self name)
(pt pt-0 pt-1 pt-2 pval) (priv-stor priv-stor-0 locn)
(lb l x y rndx))
(defstrand init 5 (na na) (nb nb) (a self) (b b)
(priv-stor priv-stor-0) (la l) (x x) (beta lb) (upsilon y))
(defstrand ltx-gen 3 (ignore ignore) (self b) (priv-stor priv-stor)
(l lb))
(defstrand resp 4 (na na) (nb nb) (a self) (b b) (priv-stor priv-stor)
(lb lb) (y y) (alpha l) (zeta x))
(defstrand ltx-gen 3 (ignore ignore-0) (self self)
(priv-stor priv-stor-0) (l l))
(precedes ((0 2) (2 2)) ((1 1) (2 0)) ((1 2) (0 1)) ((2 3) (0 3))
((3 1) (0 0)) ((3 2) (2 1)))
(non-orig (privk "sig" b))
(uniq-orig na nb lb l)
(uniq-gen x y)
(absent (x lb) (x l) (y lb) (y l) (y x))
(gen-st (pv b lb) (pv self l))
(facts (neq (exp (gen) x) (gen)) (trans 1 1) (trans 1 0) (trans 3 1)
(trans 3 0) (neq (exp (gen) y) (gen)) (neq self b))
(operation nonce-test (displaced 4 2 resp 4) (exp (gen) y-0) (0 3))
(traces
((load priv-stor-0 (cat pt-2 (pv self l)))
(recv
(sig (body b (exp (gen) lb) (pubk "sig" b)) (privk "sig" b)))
(send (cat na self b (exp (gen) x)))
(recv
(cat (exp (gen) y)
(enc na nb self b
(hash (exp (gen) (mul lb l)) (exp (gen) (mul x y))))))
(send nb))
((load priv-stor (cat pt ignore))
(stor priv-stor (cat pt-0 (pv b lb)))
(send
(sig (body b (exp (gen) lb) (pubk "sig" b)) (privk "sig" b))))
((load priv-stor (cat pt-0 (pv b lb)))
(recv
(sig (body self (exp (gen) l) (pubk "sig" self))
(privk "sig" self))) (recv (cat na self b (exp (gen) x)))
(send
(cat (exp (gen) y)
(enc na nb self b
(hash (exp (gen) (mul lb l)) (exp (gen) (mul x y)))))))
((load priv-stor-0 (cat pt-1 ignore-0))
(stor priv-stor-0 (cat pt-2 (pv self l)))
(send
(sig (body self (exp (gen) l) (pubk "sig" self))
(privk "sig" self)))))
(label 382)
(parent 366)
(realized)
(shape)
(maps
((0)
((a self) (b b) (la l) (x x) (beta lb) (upsilon y) (na na) (nb nb)
(priv-stor priv-stor-0) (pt pt-2))))
(origs (nb (2 3)) (l (3 1)) (pt-2 (3 1)) (lb (1 1)) (pt-0 (1 1))
(na (0 2))))
(defskeleton dhcr-um
(vars (ignore ignore-0 mesg) (na nb data) (b self name)
(pt pt-0 pt-1 pt-2 pt-3 pval) (priv-stor priv-stor-0 locn) (x rndx)
(upsilon expt) (l l-0 rndx))
(defstrand init 5 (na na) (nb nb) (a self) (b b)
(priv-stor priv-stor-0) (la l-0) (x x) (beta l) (upsilon upsilon))
(defstrand ltx-gen 3 (ignore ignore) (self b) (priv-stor priv-stor)
(l l))
(defstrand ltx-disclose 3 (self b) (priv-stor priv-stor) (l l))
(defstrand ltx-gen 3 (ignore ignore-0) (self self)
(priv-stor priv-stor-0) (l l-0))
(precedes ((1 1) (2 0)) ((1 2) (0 1)) ((2 2) (0 3)) ((3 1) (0 0))
((3 2) (0 3)))
(non-orig (privk "sig" b))
(uniq-orig na l l-0)
(uniq-gen x)
(absent (x l) (x l-0))
(gen-st (pv b l) (pv self l-0))
(facts (trans 2 1) (trans 2 0) (trans 1 1) (trans 1 0) (trans 3 1)
(trans 3 0) (neq (exp (gen) upsilon) (gen)) (neq self b))
(operation generalization deleted (2 0))
(traces
((load priv-stor-0 (cat pt-3 (pv self l-0)))
(recv (sig (body b (exp (gen) l) (pubk "sig" b)) (privk "sig" b)))
(send (cat na self b (exp (gen) x)))
(recv
(cat (exp (gen) upsilon)
(enc na nb self b
(hash (exp (gen) (mul l l-0))
(exp (gen) (mul x upsilon)))))) (send nb))
((load priv-stor (cat pt ignore))
(stor priv-stor (cat pt-0 (pv b l)))
(send
(sig (body b (exp (gen) l) (pubk "sig" b)) (privk "sig" b))))
((load priv-stor (cat pt-0 (pv b l)))
(stor priv-stor (cat pt-1 "nil")) (send l))
((load priv-stor-0 (cat pt-2 ignore-0))
(stor priv-stor-0 (cat pt-3 (pv self l-0)))
(send
(sig (body self (exp (gen) l-0) (pubk "sig" self))
(privk "sig" self)))))
(label 529)
(parent 366)
(realized)
(shape)
(maps
((0)
((a self) (b b) (la l-0) (x x) (beta l) (upsilon upsilon) (na na)
(nb nb) (priv-stor priv-stor-0) (pt pt-3))))
(origs (l-0 (3 1)) (pt-3 (3 1)) (pt-1 (2 1)) (l (1 1)) (pt-0 (1 1))
(na (0 2))))
(defskeleton dhcr-um
(vars (ignore ignore-0 mesg) (na nb data) (a b name)
(pt pt-0 pt-1 pt-2 pt-3 pval) (priv-stor priv-stor-0 locn) (x rndx)
(upsilon expt) (l l-0 rndx))
(defstrand init 5 (na na) (nb nb) (a a) (b b) (priv-stor priv-stor)
(la l) (x x) (beta l-0) (upsilon upsilon))
(defstrand ltx-gen 2 (ignore ignore) (self a) (priv-stor priv-stor)
(l l))
(defstrand ltx-gen 3 (ignore ignore-0) (self b)
(priv-stor priv-stor-0) (l l-0))
(defstrand ltx-disclose 3 (self a) (priv-stor priv-stor) (l l))
(precedes ((1 1) (0 0)) ((1 1) (3 0)) ((2 2) (0 1)) ((3 2) (0 3)))
(non-orig (privk "sig" b))
(uniq-orig na l l-0)
(uniq-gen x)
(absent (x l) (x l-0))
(gen-st (pv a l))
(facts (trans 3 1) (trans 3 0) (trans 2 1) (trans 2 0) (trans 1 1)
(trans 1 0) (neq (exp (gen) upsilon) (gen)) (neq a b))
(operation generalization deleted (3 0))
(traces
((load priv-stor (cat pt (pv a l)))
(recv
(sig (body b (exp (gen) l-0) (pubk "sig" b)) (privk "sig" b)))
(send (cat na a b (exp (gen) x)))
(recv
(cat (exp (gen) upsilon)
(enc na nb a b
(hash (exp (gen) (mul l l-0))
(exp (gen) (mul x upsilon)))))) (send nb))
((load priv-stor (cat pt-0 ignore))
(stor priv-stor (cat pt (pv a l))))
((load priv-stor-0 (cat pt-1 ignore-0))
(stor priv-stor-0 (cat pt-2 (pv b l-0)))
(send
(sig (body b (exp (gen) l-0) (pubk "sig" b)) (privk "sig" b))))
((load priv-stor (cat pt (pv a l)))
(stor priv-stor (cat pt-3 "nil")) (send l)))
(label 532)
(parent 366)
(realized)
(shape)
(maps
((0)
((a a) (b b) (la l) (x x) (beta l-0) (upsilon upsilon) (na na)
(nb nb) (priv-stor priv-stor) (pt pt))))
(origs (l-0 (2 1)) (pt-2 (2 1)) (pt-3 (3 1)) (l (1 1)) (pt (1 1))
(na (0 2))))
(defskeleton dhcr-um
(vars (ignore ignore-0 mesg) (na nb data) (a b name)
(pt pt-0 pt-1 pt-2 pt-3 pval) (priv-stor priv-stor-0 locn)
(lb l x y rndx))
(defstrand init 5 (na na) (nb nb) (a a) (b b) (priv-stor priv-stor)
(la l) (x x) (beta lb) (upsilon y))
(defstrand ltx-gen 2 (ignore ignore) (self a) (priv-stor priv-stor)
(l l))
(defstrand ltx-gen 3 (ignore ignore-0) (self b)
(priv-stor priv-stor-0) (l lb))
(defstrand ltx-disclose 3 (self a) (priv-stor priv-stor) (l l))
(precedes ((1 1) (0 0)) ((1 1) (3 0)) ((2 2) (0 1)) ((3 2) (0 3)))
(non-orig (privk "sig" b))
(uniq-orig na lb l)
(uniq-gen x y)
(absent (x lb) (x l) (y lb) (y l) (y x))
(gen-st (pv a l) (pv b lb))
(facts (trans 3 1) (trans 3 0) (neq (exp (gen) x) (gen)) (trans 2 1)
(trans 2 0) (trans 1 1) (trans 1 0) (neq (exp (gen) y) (gen))
(neq a b))
(operation generalization forgot nb)
(traces
((load priv-stor (cat pt (pv a l)))
(recv
(sig (body b (exp (gen) lb) (pubk "sig" b)) (privk "sig" b)))
(send (cat na a b (exp (gen) x)))
(recv
(cat (exp (gen) y)
(enc na nb a b
(hash (exp (gen) (mul lb l)) (exp (gen) (mul x y))))))
(send nb))
((load priv-stor (cat pt-0 ignore))
(stor priv-stor (cat pt (pv a l))))
((load priv-stor-0 (cat pt-1 ignore-0))
(stor priv-stor-0 (cat pt-2 (pv b lb)))
(send
(sig (body b (exp (gen) lb) (pubk "sig" b)) (privk "sig" b))))
((load priv-stor (cat pt (pv a l)))
(stor priv-stor (cat pt-3 "nil")) (send l)))
(label 535)
(parent 366)
(realized)
(shape)
(maps
((0)
((a a) (b b) (la l) (x x) (beta lb) (upsilon y) (na na) (nb nb)
(priv-stor priv-stor) (pt pt))))
(origs (pt-3 (3 1)) (lb (2 1)) (pt-2 (2 1)) (l (1 1)) (pt (1 1))
(na (0 2))))
(defskeleton dhcr-um
(vars (ignore ignore-0 mesg) (na nb data) (a b name)
(pt pt-0 pt-1 pt-2 pt-3 pval) (priv-stor priv-stor-0 locn) (x rndx)
(upsilon expt) (l l-0 rndx))
(defstrand init 5 (na na) (nb nb) (a a) (b b) (priv-stor priv-stor)
(la l-0) (x x) (beta l) (upsilon upsilon))
(defstrand ltx-gen 2 (ignore ignore) (self a) (priv-stor priv-stor)
(l l-0))
(defstrand ltx-gen 3 (ignore ignore-0) (self b)
(priv-stor priv-stor-0) (l l))
(defstrand ltx-disclose 3 (self a) (priv-stor priv-stor) (l l-0))
(precedes ((1 1) (0 0)) ((1 1) (3 0)) ((2 2) (0 1)) ((3 2) (0 3)))
(non-orig (privk "sig" b))
(uniq-orig na l l-0)
(uniq-gen x)
(absent (x l) (x l-0))
(gen-st (pv a l-0) (pv b l))
(facts (trans 3 1) (trans 3 0) (trans 2 1) (trans 2 0) (trans 1 1)
(trans 1 0) (neq (exp (gen) upsilon) (gen)) (neq a b))
(operation generalization deleted (3 0))
(traces
((load priv-stor (cat pt (pv a l-0)))
(recv (sig (body b (exp (gen) l) (pubk "sig" b)) (privk "sig" b)))
(send (cat na a b (exp (gen) x)))
(recv
(cat (exp (gen) upsilon)
(enc na nb a b
(hash (exp (gen) (mul l l-0))
(exp (gen) (mul x upsilon)))))) (send nb))
((load priv-stor (cat pt-0 ignore))
(stor priv-stor (cat pt (pv a l-0))))
((load priv-stor-0 (cat pt-1 ignore-0))
(stor priv-stor-0 (cat pt-2 (pv b l)))
(send
(sig (body b (exp (gen) l) (pubk "sig" b)) (privk "sig" b))))
((load priv-stor (cat pt (pv a l-0)))
(stor priv-stor (cat pt-3 "nil")) (send l-0)))
(label 710)
(parent 366)
(realized)
(shape)
(maps
((0)
((a a) (b b) (la l-0) (x x) (beta l) (upsilon upsilon) (na na)
(nb nb) (priv-stor priv-stor) (pt pt))))
(origs (pt-3 (3 1)) (l (2 1)) (pt-2 (2 1)) (l-0 (1 1)) (pt (1 1))
(na (0 2))))
(defskeleton dhcr-um
(vars (ignore ignore-0 ignore-1 mesg) (na nb data) (b self name)
(pt pt-0 pt-1 pt-2 pt-3 pt-4 pt-5 pval)
(priv-stor priv-stor-0 priv-stor-1 locn) (l l-0 lb x y rndx))
(defstrand init 5 (na na) (nb nb) (a self) (b b)
(priv-stor priv-stor-1) (la l-0) (x x) (beta l) (upsilon y))
(defstrand ltx-gen 3 (ignore ignore) (self b) (priv-stor priv-stor)
(l l))
(defstrand ltx-gen 2 (ignore ignore-0) (self b)
(priv-stor priv-stor-0) (l lb))
(defstrand ltx-disclose 3 (self b) (priv-stor priv-stor) (l l))
(defstrand ltx-gen 3 (ignore ignore-1) (self self)
(priv-stor priv-stor-1) (l l-0))
(precedes ((1 1) (3 0)) ((1 2) (0 1)) ((3 2) (0 3)) ((4 1) (0 0))
((4 2) (0 3)))
(non-orig (privk "sig" b))
(uniq-orig na l l-0 lb)
(uniq-gen x y)
(absent (x l) (x l-0) (y (mul l l-0 (rec lb))) (y lb) (y x))
(gen-st (pv b l) (pv b lb) (pv self l-0))
(facts (trans 3 1) (trans 3 0) (trans 2 1) (trans 2 0)
(neq (exp (gen) x) (gen)) (trans 1 1) (trans 1 0) (trans 4 1)
(trans 4 0) (neq (exp (gen) y) (gen)) (neq self b))
(operation generalization forgot nb)
(traces
((load priv-stor-1 (cat pt-5 (pv self l-0)))
(recv (sig (body b (exp (gen) l) (pubk "sig" b)) (privk "sig" b)))
(send (cat na self b (exp (gen) x)))
(recv
(cat (exp (gen) y)
(enc na nb self b
(hash (exp (gen) (mul l l-0)) (exp (gen) (mul x y))))))
(send nb))
((load priv-stor (cat pt ignore))
(stor priv-stor (cat pt-0 (pv b l)))
(send
(sig (body b (exp (gen) l) (pubk "sig" b)) (privk "sig" b))))
((load priv-stor-0 (cat pt-2 ignore-0))
(stor priv-stor-0 (cat pt-1 (pv b lb))))
((load priv-stor (cat pt-0 (pv b l)))
(stor priv-stor (cat pt-3 "nil")) (send l))
((load priv-stor-1 (cat pt-4 ignore-1))
(stor priv-stor-1 (cat pt-5 (pv self l-0)))
(send
(sig (body self (exp (gen) l-0) (pubk "sig" self))
(privk "sig" self)))))
(label 739)
(parent 366)
(realized)
(shape)
(maps
((0)
((a self) (b b) (la l-0) (x x) (beta l) (upsilon y) (na na)
(nb nb) (priv-stor priv-stor-1) (pt pt-5))))
(origs (l-0 (4 1)) (pt-5 (4 1)) (pt-3 (3 1)) (lb (2 1)) (pt-1 (2 1))
(l (1 1)) (pt-0 (1 1)) (na (0 2))))
(defskeleton dhcr-um
(vars (ignore ignore-0 ignore-1 mesg) (na nb data) (a b b-0 name)
(pt pt-0 pt-1 pt-2 pt-3 pt-4 pt-5 pval)
(priv-stor priv-stor-0 priv-stor-1 locn) (l l-0 lb x y rndx))
(defstrand init 5 (na na) (nb nb) (a a) (b b-0) (priv-stor priv-stor)
(la l) (x x) (beta l-0) (upsilon y))
(defstrand ltx-gen 2 (ignore ignore) (self a) (priv-stor priv-stor)
(l l))
(defstrand ltx-gen 3 (ignore ignore-0) (self b-0)
(priv-stor priv-stor-0) (l l-0))
(defstrand ltx-gen 2 (ignore ignore-1) (self b)
(priv-stor priv-stor-1) (l lb))
(defstrand ltx-disclose 3 (self a) (priv-stor priv-stor) (l l))
(precedes ((1 1) (0 0)) ((1 1) (4 0)) ((2 2) (0 1)) ((4 2) (0 3)))
(non-orig (privk "sig" b-0))
(uniq-orig na l l-0 lb)
(uniq-gen x y)
(absent (x l) (x l-0) (y (mul l l-0 (rec lb))) (y lb) (y x))
(gen-st (pv a l) (pv b lb))
(facts (trans 4 1) (trans 4 0) (trans 3 1) (trans 3 0)
(neq (exp (gen) x) (gen)) (trans 2 1) (trans 2 0) (trans 1 1)
(trans 1 0) (neq (exp (gen) y) (gen)) (neq a b-0))
(operation generalization forgot (privk "sig" b))
(traces
((load priv-stor (cat pt (pv a l)))
(recv
(sig (body b-0 (exp (gen) l-0) (pubk "sig" b-0))
(privk "sig" b-0))) (send (cat na a b-0 (exp (gen) x)))
(recv
(cat (exp (gen) y)
(enc na nb a b-0
(hash (exp (gen) (mul l l-0)) (exp (gen) (mul x y))))))
(send nb))
((load priv-stor (cat pt-0 ignore))
(stor priv-stor (cat pt (pv a l))))
((load priv-stor-0 (cat pt-1 ignore-0))
(stor priv-stor-0 (cat pt-2 (pv b-0 l-0)))
(send
(sig (body b-0 (exp (gen) l-0) (pubk "sig" b-0))
(privk "sig" b-0))))
((load priv-stor-1 (cat pt-4 ignore-1))
(stor priv-stor-1 (cat pt-3 (pv b lb))))
((load priv-stor (cat pt (pv a l)))
(stor priv-stor (cat pt-5 "nil")) (send l)))
(label 779)
(parent 366)
(realized)
(shape)
(maps
((0)
((a a) (b b-0) (la l) (x x) (beta l-0) (upsilon y) (na na) (nb nb)
(priv-stor priv-stor) (pt pt))))
(origs (l-0 (2 1)) (pt-2 (2 1)) (pt-5 (4 1)) (lb (3 1)) (pt-3 (3 1))
(l (1 1)) (pt (1 1)) (na (0 2))))
(defskeleton dhcr-um
(vars (ignore ignore-0 mesg) (na nb data) (a b name)
(pt pt-0 pt-1 pt-2 pt-3 pval) (priv-stor priv-stor-0 locn)
(lb l x rndx) (w expt) (y rndx))
(defstrand init 5 (na na) (nb nb) (a a) (b b) (priv-stor priv-stor)
(la l) (x x) (beta lb) (upsilon (mul w y)))
(defstrand ltx-gen 2 (ignore ignore) (self a) (priv-stor priv-stor)
(l l))
(defstrand ltx-gen 3 (ignore ignore-0) (self b)
(priv-stor priv-stor-0) (l lb))
(defstrand ltx-disclose 3 (self a) (priv-stor priv-stor) (l l))
(deflistener (cat (exp (gen) y) w))
(precedes ((1 1) (0 0)) ((1 1) (3 0)) ((2 2) (0 1)) ((3 2) (0 3)))
(non-orig (privk "sig" b))
(uniq-orig na lb l)
(uniq-gen x y)
(absent (x lb) (x l) (y lb) (y l) (y (mul x w)))
(precur (4 0))
(gen-st (pv a l) (pv b lb))
(facts (trans 3 1) (trans 3 0) (neq (exp (gen) (mul x w)) (gen))
(trans 2 1) (trans 2 0) (trans 1 1) (trans 1 0)
(neq (exp (gen) (mul w y)) (gen)) (neq a b))
(operation generalization forgot nb)
(traces
((load priv-stor (cat pt (pv a l)))
(recv
(sig (body b (exp (gen) lb) (pubk "sig" b)) (privk "sig" b)))
(send (cat na a b (exp (gen) x)))
(recv
(cat (exp (gen) (mul w y))
(enc na nb a b
(hash (exp (gen) (mul lb l)) (exp (gen) (mul x w y))))))
(send nb))
((load priv-stor (cat pt-0 ignore))
(stor priv-stor (cat pt (pv a l))))
((load priv-stor-0 (cat pt-1 ignore-0))
(stor priv-stor-0 (cat pt-2 (pv b lb)))
(send
(sig (body b (exp (gen) lb) (pubk "sig" b)) (privk "sig" b))))
((load priv-stor (cat pt (pv a l)))
(stor priv-stor (cat pt-3 "nil")) (send l))
((recv (cat (exp (gen) y) w))))
(label 786)
(parent 366)
(realized)
(shape)
(maps
((0)
((a a) (b b) (la l) (x x) (beta lb) (upsilon (mul w y)) (na na)
(nb nb) (priv-stor priv-stor) (pt pt))))
(origs (pt-3 (3 1)) (lb (2 1)) (pt-2 (2 1)) (l (1 1)) (pt (1 1))
(na (0 2))))
(defskeleton dhcr-um
(vars (ignore ignore-0 ignore-1 mesg) (na nb data) (a b name)
(pt pt-0 pt-1 pt-2 pt-3 pt-4 pt-5 pval)
(priv-stor priv-stor-0 priv-stor-1 locn) (l l-0 lb x y rndx))
(defstrand init 5 (na na) (nb nb) (a a) (b b) (priv-stor priv-stor)
(la l-0) (x x) (beta l) (upsilon y))
(defstrand ltx-gen 2 (ignore ignore) (self a) (priv-stor priv-stor)
(l l-0))
(defstrand ltx-gen 3 (ignore ignore-0) (self b)
(priv-stor priv-stor-0) (l l))
(defstrand ltx-gen 2 (ignore ignore-1) (self b)
(priv-stor priv-stor-1) (l lb))
(defstrand ltx-disclose 3 (self a) (priv-stor priv-stor) (l l-0))
(precedes ((1 1) (0 0)) ((1 1) (4 0)) ((2 2) (0 1)) ((4 2) (0 3)))
(non-orig (privk "sig" b))
(uniq-orig na l l-0 lb)
(uniq-gen x y)
(absent (x l) (x l-0) (y (mul l l-0 (rec lb))) (y lb) (y x))
(gen-st (pv a l-0) (pv b l) (pv b lb))
(facts (trans 4 1) (trans 4 0) (trans 3 1) (trans 3 0)
(neq (exp (gen) x) (gen)) (trans 2 1) (trans 2 0) (trans 1 1)
(trans 1 0) (neq (exp (gen) y) (gen)) (neq a b))
(operation generalization forgot nb)
(traces
((load priv-stor (cat pt (pv a l-0)))
(recv (sig (body b (exp (gen) l) (pubk "sig" b)) (privk "sig" b)))
(send (cat na a b (exp (gen) x)))
(recv
(cat (exp (gen) y)
(enc na nb a b
(hash (exp (gen) (mul l l-0)) (exp (gen) (mul x y))))))
(send nb))
((load priv-stor (cat pt-0 ignore))
(stor priv-stor (cat pt (pv a l-0))))
((load priv-stor-0 (cat pt-1 ignore-0))
(stor priv-stor-0 (cat pt-2 (pv b l)))
(send
(sig (body b (exp (gen) l) (pubk "sig" b)) (privk "sig" b))))
((load priv-stor-1 (cat pt-4 ignore-1))
(stor priv-stor-1 (cat pt-3 (pv b lb))))
((load priv-stor (cat pt (pv a l-0)))
(stor priv-stor (cat pt-5 "nil")) (send l-0)))
(label 795)
(parent 366)
(realized)
(shape)
(maps
((0)
((a a) (b b) (la l-0) (x x) (beta l) (upsilon y) (na na) (nb nb)
(priv-stor priv-stor) (pt pt))))
(origs (pt-5 (4 1)) (lb (3 1)) (pt-3 (3 1)) (l (2 1)) (pt-2 (2 1))
(l-0 (1 1)) (pt (1 1)) (na (0 2))))
(defskeleton dhcr-um
(vars (ignore ignore-0 ignore-1 mesg) (na nb data) (b self name)
(pt pt-0 pt-1 pt-2 pt-3 pt-4 pt-5 pval)
(priv-stor priv-stor-0 priv-stor-1 locn) (l l-0 lb x rndx) (w expt)
(y rndx))
(defstrand init 5 (na na) (nb nb) (a self) (b b)
(priv-stor priv-stor-1) (la l-0) (x x) (beta l) (upsilon (mul w y)))
(defstrand ltx-gen 3 (ignore ignore) (self b) (priv-stor priv-stor)
(l l))
(defstrand ltx-gen 2 (ignore ignore-0) (self b)
(priv-stor priv-stor-0) (l lb))
(defstrand ltx-disclose 3 (self b) (priv-stor priv-stor) (l l))
(defstrand ltx-gen 3 (ignore ignore-1) (self self)
(priv-stor priv-stor-1) (l l-0))
(deflistener (cat (exp (gen) y) w))
(precedes ((1 1) (3 0)) ((1 2) (0 1)) ((3 2) (0 3)) ((4 1) (0 0))
((4 2) (0 3)))
(non-orig (privk "sig" b))
(uniq-orig na l l-0 lb)
(uniq-gen x y)
(absent (x l) (x l-0) (y (mul l l-0 (rec lb))) (y lb) (y (mul x w)))
(precur (5 0))
(gen-st (pv b l) (pv b lb) (pv self l-0))
(facts (trans 3 1) (trans 3 0) (trans 2 1) (trans 2 0)
(neq (exp (gen) (mul x w)) (gen)) (trans 1 1) (trans 1 0)
(trans 4 1) (trans 4 0) (neq (exp (gen) (mul w y)) (gen))
(neq self b))
(operation generalization forgot nb)
(traces
((load priv-stor-1 (cat pt-5 (pv self l-0)))
(recv (sig (body b (exp (gen) l) (pubk "sig" b)) (privk "sig" b)))
(send (cat na self b (exp (gen) x)))
(recv
(cat (exp (gen) (mul w y))
(enc na nb self b
(hash (exp (gen) (mul l l-0)) (exp (gen) (mul x w y))))))
(send nb))
((load priv-stor (cat pt ignore))
(stor priv-stor (cat pt-0 (pv b l)))
(send
(sig (body b (exp (gen) l) (pubk "sig" b)) (privk "sig" b))))
((load priv-stor-0 (cat pt-2 ignore-0))
(stor priv-stor-0 (cat pt-1 (pv b lb))))
((load priv-stor (cat pt-0 (pv b l)))
(stor priv-stor (cat pt-3 "nil")) (send l))
((load priv-stor-1 (cat pt-4 ignore-1))
(stor priv-stor-1 (cat pt-5 (pv self l-0)))
(send
(sig (body self (exp (gen) l-0) (pubk "sig" self))
(privk "sig" self)))) ((recv (cat (exp (gen) y) w))))
(label 814)
(parent 366)
(realized)
(shape)
(maps
((0)
((a self) (b b) (la l-0) (x x) (beta l) (upsilon (mul w y))
(na na) (nb nb) (priv-stor priv-stor-1) (pt pt-5))))
(origs (l-0 (4 1)) (pt-5 (4 1)) (pt-3 (3 1)) (lb (2 1)) (pt-1 (2 1))
(l (1 1)) (pt-0 (1 1)) (na (0 2))))
(defskeleton dhcr-um
(vars (ignore ignore-0 ignore-1 mesg) (na nb data) (a b b-0 name)
(pt pt-0 pt-1 pt-2 pt-3 pt-4 pt-5 pval)
(priv-stor priv-stor-0 priv-stor-1 locn) (l l-0 lb x rndx) (w expt)
(y rndx))
(defstrand init 5 (na na) (nb nb) (a a) (b b-0) (priv-stor priv-stor)
(la l) (x x) (beta l-0) (upsilon (mul w y)))
(defstrand ltx-gen 2 (ignore ignore) (self a) (priv-stor priv-stor)
(l l))
(defstrand ltx-gen 3 (ignore ignore-0) (self b-0)
(priv-stor priv-stor-0) (l l-0))
(defstrand ltx-gen 2 (ignore ignore-1) (self b)
(priv-stor priv-stor-1) (l lb))
(defstrand ltx-disclose 3 (self a) (priv-stor priv-stor) (l l))
(deflistener (cat (exp (gen) y) w))
(precedes ((1 1) (0 0)) ((1 1) (4 0)) ((2 2) (0 1)) ((4 2) (0 3)))
(non-orig (privk "sig" b-0))
(uniq-orig na l l-0 lb)
(uniq-gen x y)
(absent (x l) (x l-0) (y (mul l l-0 (rec lb))) (y lb) (y (mul x w)))
(precur (5 0))
(gen-st (pv a l) (pv b lb))
(facts (trans 4 1) (trans 4 0) (trans 3 1) (trans 3 0)
(neq (exp (gen) (mul x w)) (gen)) (trans 2 1) (trans 2 0)
(trans 1 1) (trans 1 0) (neq (exp (gen) (mul w y)) (gen))
(neq a b-0))
(operation generalization forgot (privk "sig" b))
(traces
((load priv-stor (cat pt (pv a l)))
(recv
(sig (body b-0 (exp (gen) l-0) (pubk "sig" b-0))
(privk "sig" b-0))) (send (cat na a b-0 (exp (gen) x)))
(recv
(cat (exp (gen) (mul w y))
(enc na nb a b-0
(hash (exp (gen) (mul l l-0)) (exp (gen) (mul x w y))))))
(send nb))
((load priv-stor (cat pt-0 ignore))
(stor priv-stor (cat pt (pv a l))))
((load priv-stor-0 (cat pt-1 ignore-0))
(stor priv-stor-0 (cat pt-2 (pv b-0 l-0)))
(send
(sig (body b-0 (exp (gen) l-0) (pubk "sig" b-0))
(privk "sig" b-0))))
((load priv-stor-1 (cat pt-4 ignore-1))
(stor priv-stor-1 (cat pt-3 (pv b lb))))
((load priv-stor (cat pt (pv a l)))
(stor priv-stor (cat pt-5 "nil")) (send l))
((recv (cat (exp (gen) y) w))))
(label 818)
(parent 366)
(realized)
(shape)
(maps
((0)
((a a) (b b-0) (la l) (x x) (beta l-0) (upsilon (mul w y)) (na na)
(nb nb) (priv-stor priv-stor) (pt pt))))
(origs (l-0 (2 1)) (pt-2 (2 1)) (pt-5 (4 1)) (lb (3 1)) (pt-3 (3 1))
(l (1 1)) (pt (1 1)) (na (0 2))))
(defskeleton dhcr-um
(vars (ignore ignore-0 ignore-1 mesg) (na nb data) (a b name)
(pt pt-0 pt-1 pt-2 pt-3 pt-4 pt-5 pval)
(priv-stor priv-stor-0 priv-stor-1 locn) (l l-0 lb x rndx) (w expt)
(y rndx))
(defstrand init 5 (na na) (nb nb) (a a) (b b) (priv-stor priv-stor)
(la l-0) (x x) (beta l) (upsilon (mul w y)))
(defstrand ltx-gen 2 (ignore ignore) (self a) (priv-stor priv-stor)
(l l-0))
(defstrand ltx-gen 3 (ignore ignore-0) (self b)
(priv-stor priv-stor-0) (l l))
(defstrand ltx-gen 2 (ignore ignore-1) (self b)
(priv-stor priv-stor-1) (l lb))
(defstrand ltx-disclose 3 (self a) (priv-stor priv-stor) (l l-0))
(deflistener (cat (exp (gen) y) w))
(precedes ((1 1) (0 0)) ((1 1) (4 0)) ((2 2) (0 1)) ((4 2) (0 3)))
(non-orig (privk "sig" b))
(uniq-orig na l l-0 lb)
(uniq-gen x y)
(absent (x l) (x l-0) (y (mul l l-0 (rec lb))) (y lb) (y (mul x w)))
(precur (5 0))
(gen-st (pv a l-0) (pv b l) (pv b lb))
(facts (trans 4 1) (trans 4 0) (trans 3 1) (trans 3 0)
(neq (exp (gen) (mul x w)) (gen)) (trans 2 1) (trans 2 0)
(trans 1 1) (trans 1 0) (neq (exp (gen) (mul w y)) (gen)) (neq a b))
(operation generalization forgot nb)
(traces
((load priv-stor (cat pt (pv a l-0)))
(recv (sig (body b (exp (gen) l) (pubk "sig" b)) (privk "sig" b)))
(send (cat na a b (exp (gen) x)))
(recv
(cat (exp (gen) (mul w y))
(enc na nb a b
(hash (exp (gen) (mul l l-0)) (exp (gen) (mul x w y))))))
(send nb))
((load priv-stor (cat pt-0 ignore))
(stor priv-stor (cat pt (pv a l-0))))
((load priv-stor-0 (cat pt-1 ignore-0))
(stor priv-stor-0 (cat pt-2 (pv b l)))
(send
(sig (body b (exp (gen) l) (pubk "sig" b)) (privk "sig" b))))
((load priv-stor-1 (cat pt-4 ignore-1))
(stor priv-stor-1 (cat pt-3 (pv b lb))))
((load priv-stor (cat pt (pv a l-0)))
(stor priv-stor (cat pt-5 "nil")) (send l-0))
((recv (cat (exp (gen) y) w))))
(label 820)
(parent 366)
(realized)
(shape)
(maps
((0)
((a a) (b b) (la l-0) (x x) (beta l) (upsilon (mul w y)) (na na)
(nb nb) (priv-stor priv-stor) (pt pt))))
(origs (pt-5 (4 1)) (lb (3 1)) (pt-3 (3 1)) (l (2 1)) (pt-2 (2 1))
(l-0 (1 1)) (pt (1 1)) (na (0 2))))
(comment "Nothing left to do")
(defprotocol dhcr-um diffie-hellman
(defrole init
(vars (la x rndx) (beta upsilon expt) (a b name) (na nb data)
(priv-stor locn))
(trace (load priv-stor (pv a la))
(recv
(sig (body b (exp (gen) beta) (pubk "sig" b)) (privk "sig" b)))
(send (cat na a b (exp (gen) x)))
(recv
(cat (exp (gen) upsilon)
(enc na nb a b
(hash (exp (gen) (mul la beta))
(exp (gen) (mul x upsilon)))))) (send nb))
(uniq-orig na)
(uniq-gen x)
(absent (x la) (x beta))
(facts (neq (exp (gen) upsilon) (gen)))
(gen-st (pv a la))
(fn-of ("principal-of" (ltxa a) (ltxb b))
("ltx-of" (a ltxa) (b ltxb))))
(defrole resp
(vars (lb y rndx) (alpha zeta expt) (a b name) (na nb data)
(priv-stor locn))
(trace (load priv-stor (pv b lb))
(recv
(sig (body a (exp (gen) alpha) (pubk "sig" a)) (privk "sig" a)))
(recv (cat na a b (exp (gen) zeta)))
(send
(cat (exp (gen) y)
(enc na nb a b
(hash (exp (gen) (mul lb alpha))
(exp (gen) (mul y zeta)))))) (recv nb))
(uniq-orig nb)
(uniq-gen y)
(absent (y lb) (y alpha) (y zeta))
(facts (neq (exp (gen) zeta) (gen)))
(gen-st (pv b lb))
(fn-of ("principal-of" (ltxa a) (ltxb b))
("ltx-of" (a ltxa) (b ltxb))))
(defrole ltx-gen
(vars (self name) (l rndx) (priv-stor locn) (ignore mesg))
(trace (load priv-stor ignore) (stor priv-stor (pv self l))
(send
(sig (body self (exp (gen) l) (pubk "sig" self))
(privk "sig" self))))
(uniq-orig l)
(fn-of ("principal-of" (l self)) ("ltx-of" (self l))))
(defrole ltx-disclose
(vars (self name) (l rndx) (priv-stor locn))
(trace (load priv-stor (pv self l)) (stor priv-stor "nil") (send l))
(gen-st (pv self l))
(fn-of ("principal-of" (l self)) ("ltx-of" (self l))))
(defrule undisclosed-not-disclosed
(forall ((z strd) (l rndx))
(implies
(and (fact undisclosed l) (p "ltx-disclose" z 2)
(p "ltx-disclose" "l" z l))
(false))))
(defgenrule neqRl_indx
(forall ((x indx)) (implies (fact neq x x) (false))))
(defgenrule neqRl_strd
(forall ((x strd)) (implies (fact neq x x) (false))))
(defgenrule neqRl_mesg
(forall ((x mesg)) (implies (fact neq x x) (false))))
(defgenrule shearsRule
(forall ((z0 z1 z2 strd) (i0 i1 i2 indx))
(implies
(and (trans z0 i0) (trans z1 i1) (trans z2 i2)
(leads-to z0 i0 z1 i1) (same-locn z0 i0 z2 i2)
(prec z0 i0 z2 i2))
(or (and (= z1 z2) (= i1 i2)) (prec z1 i1 z2 i2)))))
(defgenrule invShearsRule
(forall ((z0 z1 z2 strd) (i0 i1 i2 indx))
(implies
(and (trans z0 i0) (trans z1 i1) (same-locn z0 i0 z1 i1)
(leads-to z1 i1 z2 i2) (prec z0 i0 z2 i2))
(or (and (= z0 z1) (= i0 i1)) (prec z0 i0 z1 i1)))))
(defgenrule fact-init-neq0
(forall ((z strd) (upsilon expt))
(implies (and (p "init" z 4) (p "init" "upsilon" z upsilon))
(fact neq (exp (gen) upsilon) (gen)))))
(defgenrule fact-resp-neq0
(forall ((z strd) (zeta expt))
(implies (and (p "resp" z 3) (p "resp" "zeta" z zeta))
(fact neq (exp (gen) zeta) (gen)))))
(defgenrule trRl_ltx-gen-at-1
(forall ((z strd)) (implies (p "ltx-gen" z 2) (trans z 1))))
(defgenrule trRl_ltx-gen-at-0
(forall ((z strd)) (implies (p "ltx-gen" z 2) (trans z 0))))
(defgenrule trRl_ltx-disclose-at-1
(forall ((z strd)) (implies (p "ltx-disclose" z 2) (trans z 1))))
(defgenrule trRl_ltx-disclose-at-0
(forall ((z strd)) (implies (p "ltx-disclose" z 2) (trans z 0))))
(defgenrule gen-st-init-0
(forall ((z strd) (la rndx) (a name))
(implies
(and (p "init" z 1) (p "init" "la" z la) (p "init" "a" z a))
(gen-st (pv a la)))))
(defgenrule gen-st-resp-0
(forall ((z strd) (lb rndx) (b name))
(implies
(and (p "resp" z 1) (p "resp" "lb" z lb) (p "resp" "b" z b))
(gen-st (pv b lb)))))
(defgenrule gen-st-ltx-disclose-0
(forall ((z strd) (l rndx) (self name))
(implies
(and (p "ltx-disclose" z 1) (p "ltx-disclose" "l" z l)
(p "ltx-disclose" "self" z self)) (gen-st (pv self l)))))
(lang (sig sign) (body (tuple 3)) (pv (tuple 2))))
(defskeleton dhcr-um
(vars (na nb data) (a b name) (pt pval) (priv-stor locn) (lb rndx)
(alpha expt) (y rndx) (zeta expt))
(defstrand resp 5 (na na) (nb nb) (a a) (b b) (priv-stor priv-stor)
(lb lb) (y y) (alpha alpha) (zeta zeta))
(non-orig (privk "sig" a))
(uniq-orig nb)
(uniq-gen y)
(absent (y lb) (y alpha) (y zeta))
(facts (neq a b) (undisclosed lb) (undisclosed alpha))
(traces
((load priv-stor (cat pt (pv b lb)))
(recv
(sig (body a (exp (gen) alpha) (pubk "sig" a)) (privk "sig" a)))
(recv (cat na a b (exp (gen) zeta)))
(send
(cat (exp (gen) y)
(enc na nb a b
(hash (exp (gen) (mul lb alpha))
(exp (gen) (mul y zeta)))))) (recv nb)))
(label 821)
(unrealized (0 1))
(origs (nb (0 3)))
(comment "Not closed under rules"))
(comment "Nothing left to do")
(defprotocol dhcr-um diffie-hellman
(defrole init
(vars (la x rndx) (beta upsilon expt) (a b name) (na nb data)
(priv-stor locn))
(trace (load priv-stor (pv a la))
(recv
(sig (body b (exp (gen) beta) (pubk "sig" b)) (privk "sig" b)))
(send (cat na a b (exp (gen) x)))
(recv
(cat (exp (gen) upsilon)
(enc na nb a b
(hash (exp (gen) (mul la beta))
(exp (gen) (mul x upsilon)))))) (send nb))
(uniq-orig na)
(uniq-gen x)
(absent (x la) (x beta))
(facts (neq (exp (gen) upsilon) (gen)))
(gen-st (pv a la))
(fn-of ("principal-of" (ltxa a) (ltxb b))
("ltx-of" (a ltxa) (b ltxb))))
(defrole resp
(vars (lb y rndx) (alpha zeta expt) (a b name) (na nb data)
(priv-stor locn))
(trace (load priv-stor (pv b lb))
(recv
(sig (body a (exp (gen) alpha) (pubk "sig" a)) (privk "sig" a)))
(recv (cat na a b (exp (gen) zeta)))
(send
(cat (exp (gen) y)
(enc na nb a b
(hash (exp (gen) (mul lb alpha))
(exp (gen) (mul y zeta)))))) (recv nb))
(uniq-orig nb)
(uniq-gen y)
(absent (y lb) (y alpha) (y zeta))
(facts (neq (exp (gen) zeta) (gen)))
(gen-st (pv b lb))
(fn-of ("principal-of" (ltxa a) (ltxb b))
("ltx-of" (a ltxa) (b ltxb))))
(defrole ltx-gen
(vars (self name) (l rndx) (priv-stor locn) (ignore mesg))
(trace (load priv-stor ignore) (stor priv-stor (pv self l))
(send
(sig (body self (exp (gen) l) (pubk "sig" self))
(privk "sig" self))))
(uniq-orig l)
(fn-of ("principal-of" (l self)) ("ltx-of" (self l))))
(defrole ltx-disclose
(vars (self name) (l rndx) (priv-stor locn))
(trace (load priv-stor (pv self l)) (stor priv-stor "nil") (send l))
(gen-st (pv self l))
(fn-of ("principal-of" (l self)) ("ltx-of" (self l))))
(defrule undisclosed-not-disclosed
(forall ((z strd) (l rndx))
(implies
(and (fact undisclosed l) (p "ltx-disclose" z 2)
(p "ltx-disclose" "l" z l))
(false))))
(defgenrule neqRl_indx
(forall ((x indx)) (implies (fact neq x x) (false))))
(defgenrule neqRl_strd
(forall ((x strd)) (implies (fact neq x x) (false))))
(defgenrule neqRl_mesg
(forall ((x mesg)) (implies (fact neq x x) (false))))
(defgenrule shearsRule
(forall ((z0 z1 z2 strd) (i0 i1 i2 indx))
(implies
(and (trans z0 i0) (trans z1 i1) (trans z2 i2)
(leads-to z0 i0 z1 i1) (same-locn z0 i0 z2 i2)
(prec z0 i0 z2 i2))
(or (and (= z1 z2) (= i1 i2)) (prec z1 i1 z2 i2)))))
(defgenrule invShearsRule
(forall ((z0 z1 z2 strd) (i0 i1 i2 indx))
(implies
(and (trans z0 i0) (trans z1 i1) (same-locn z0 i0 z1 i1)
(leads-to z1 i1 z2 i2) (prec z0 i0 z2 i2))
(or (and (= z0 z1) (= i0 i1)) (prec z0 i0 z1 i1)))))
(defgenrule fact-init-neq0
(forall ((z strd) (upsilon expt))
(implies (and (p "init" z 4) (p "init" "upsilon" z upsilon))
(fact neq (exp (gen) upsilon) (gen)))))
(defgenrule fact-resp-neq0
(forall ((z strd) (zeta expt))
(implies (and (p "resp" z 3) (p "resp" "zeta" z zeta))
(fact neq (exp (gen) zeta) (gen)))))
(defgenrule trRl_ltx-gen-at-1
(forall ((z strd)) (implies (p "ltx-gen" z 2) (trans z 1))))
(defgenrule trRl_ltx-gen-at-0
(forall ((z strd)) (implies (p "ltx-gen" z 2) (trans z 0))))
(defgenrule trRl_ltx-disclose-at-1
(forall ((z strd)) (implies (p "ltx-disclose" z 2) (trans z 1))))
(defgenrule trRl_ltx-disclose-at-0
(forall ((z strd)) (implies (p "ltx-disclose" z 2) (trans z 0))))
(defgenrule gen-st-init-0
(forall ((z strd) (la rndx) (a name))
(implies
(and (p "init" z 1) (p "init" "la" z la) (p "init" "a" z a))
(gen-st (pv a la)))))
(defgenrule gen-st-resp-0
(forall ((z strd) (lb rndx) (b name))
(implies
(and (p "resp" z 1) (p "resp" "lb" z lb) (p "resp" "b" z b))
(gen-st (pv b lb)))))
(defgenrule gen-st-ltx-disclose-0
(forall ((z strd) (l rndx) (self name))
(implies
(and (p "ltx-disclose" z 1) (p "ltx-disclose" "l" z l)
(p "ltx-disclose" "self" z self)) (gen-st (pv self l)))))
(lang (sig sign) (body (tuple 3)) (pv (tuple 2))))
(defskeleton dhcr-um
(vars (na nb data) (a b name) (pt pval) (priv-stor locn) (lb rndx)
(alpha expt) (y rndx) (zeta expt))
(defstrand resp 5 (na na) (nb nb) (a a) (b b) (priv-stor priv-stor)
(lb lb) (y y) (alpha alpha) (zeta zeta))
(non-orig (privk "sig" a))
(uniq-orig nb)
(uniq-gen y)
(absent (y lb) (y alpha) (y zeta))
(facts (neq a b) (undisclosed alpha))
(traces
((load priv-stor (cat pt (pv b lb)))
(recv
(sig (body a (exp (gen) alpha) (pubk "sig" a)) (privk "sig" a)))
(recv (cat na a b (exp (gen) zeta)))
(send
(cat (exp (gen) y)
(enc na nb a b
(hash (exp (gen) (mul lb alpha))
(exp (gen) (mul y zeta)))))) (recv nb)))
(label 829)
(unrealized (0 1))
(origs (nb (0 3)))
(comment "Not closed under rules"))
(defskeleton dhcr-um
(vars (ignore ignore-0 mesg) (na nb data) (a b name)
(pt pt-0 pt-1 pt-2 pt-3 pval) (priv-stor priv-stor-0 locn) (y rndx)
(zeta expt) (l l-0 rndx))
(defstrand resp 5 (na na) (nb nb) (a a) (b b) (priv-stor priv-stor)
(lb l) (y y) (alpha l-0) (zeta zeta))
(defstrand ltx-gen 2 (ignore ignore) (self b) (priv-stor priv-stor)
(l l))
(defstrand ltx-gen 3 (ignore ignore-0) (self a)
(priv-stor priv-stor-0) (l l-0))
(defstrand ltx-disclose 3 (self b) (priv-stor priv-stor) (l l))
(precedes ((1 1) (0 0)) ((1 1) (3 0)) ((2 2) (0 1)) ((3 2) (0 4)))
(non-orig (privk "sig" a))
(uniq-orig nb l l-0)
(uniq-gen y)
(absent (y zeta) (y l) (y l-0))
(gen-st (pv b l))
(facts (trans 3 1) (trans 3 0) (trans 2 1) (trans 2 0) (trans 1 1)
(trans 1 0) (neq (exp (gen) zeta) (gen)) (neq a b)
(undisclosed l-0))
(operation generalization deleted (3 0))
(traces
((load priv-stor (cat pt (pv b l)))
(recv
(sig (body a (exp (gen) l-0) (pubk "sig" a)) (privk "sig" a)))
(recv (cat na a b (exp (gen) zeta)))
(send
(cat (exp (gen) y)
(enc na nb a b
(hash (exp (gen) (mul l l-0)) (exp (gen) (mul y zeta))))))
(recv nb))
((load priv-stor (cat pt-0 ignore))
(stor priv-stor (cat pt (pv b l))))
((load priv-stor-0 (cat pt-1 ignore-0))
(stor priv-stor-0 (cat pt-2 (pv a l-0)))
(send
(sig (body a (exp (gen) l-0) (pubk "sig" a)) (privk "sig" a))))
((load priv-stor (cat pt (pv b l)))
(stor priv-stor (cat pt-3 "nil")) (send l)))
(label 856)
(parent 829)
(realized)
(shape)
(maps
((0)
((a a) (b b) (lb l) (alpha l-0) (y y) (zeta zeta) (na na) (nb nb)
(priv-stor priv-stor) (pt pt))))
(origs (l-0 (2 1)) (pt-2 (2 1)) (pt-3 (3 1)) (l (1 1)) (pt (1 1))
(nb (0 3))))
(comment "Nothing left to do")
(defprotocol dhcr-um diffie-hellman
(defrole init
(vars (la x rndx) (beta upsilon expt) (a b name) (na nb data)
(priv-stor locn))
(trace (load priv-stor (pv a la))
(recv
(sig (body b (exp (gen) beta) (pubk "sig" b)) (privk "sig" b)))
(send (cat na a b (exp (gen) x)))
(recv
(cat (exp (gen) upsilon)
(enc na nb a b
(hash (exp (gen) (mul la beta))
(exp (gen) (mul x upsilon)))))) (send nb))
(uniq-orig na)
(uniq-gen x)
(absent (x la) (x beta))
(facts (neq (exp (gen) upsilon) (gen)))
(gen-st (pv a la))
(fn-of ("principal-of" (ltxa a) (ltxb b))
("ltx-of" (a ltxa) (b ltxb))))
(defrole resp
(vars (lb y rndx) (alpha zeta expt) (a b name) (na nb data)
(priv-stor locn))
(trace (load priv-stor (pv b lb))
(recv
(sig (body a (exp (gen) alpha) (pubk "sig" a)) (privk "sig" a)))
(recv (cat na a b (exp (gen) zeta)))
(send
(cat (exp (gen) y)
(enc na nb a b
(hash (exp (gen) (mul lb alpha))
(exp (gen) (mul y zeta)))))) (recv nb))
(uniq-orig nb)
(uniq-gen y)
(absent (y lb) (y alpha) (y zeta))
(facts (neq (exp (gen) zeta) (gen)))
(gen-st (pv b lb))
(fn-of ("principal-of" (ltxa a) (ltxb b))
("ltx-of" (a ltxa) (b ltxb))))
(defrole ltx-gen
(vars (self name) (l rndx) (priv-stor locn) (ignore mesg))
(trace (load priv-stor ignore) (stor priv-stor (pv self l))
(send
(sig (body self (exp (gen) l) (pubk "sig" self))
(privk "sig" self))))
(uniq-orig l)
(fn-of ("principal-of" (l self)) ("ltx-of" (self l))))
(defrole ltx-disclose
(vars (self name) (l rndx) (priv-stor locn))
(trace (load priv-stor (pv self l)) (stor priv-stor "nil") (send l))
(gen-st (pv self l))
(fn-of ("principal-of" (l self)) ("ltx-of" (self l))))
(defrule undisclosed-not-disclosed
(forall ((z strd) (l rndx))
(implies
(and (fact undisclosed l) (p "ltx-disclose" z 2)
(p "ltx-disclose" "l" z l))
(false))))
(defgenrule neqRl_indx
(forall ((x indx)) (implies (fact neq x x) (false))))
(defgenrule neqRl_strd
(forall ((x strd)) (implies (fact neq x x) (false))))
(defgenrule neqRl_mesg
(forall ((x mesg)) (implies (fact neq x x) (false))))
(defgenrule shearsRule
(forall ((z0 z1 z2 strd) (i0 i1 i2 indx))
(implies
(and (trans z0 i0) (trans z1 i1) (trans z2 i2)
(leads-to z0 i0 z1 i1) (same-locn z0 i0 z2 i2)
(prec z0 i0 z2 i2))
(or (and (= z1 z2) (= i1 i2)) (prec z1 i1 z2 i2)))))
(defgenrule invShearsRule
(forall ((z0 z1 z2 strd) (i0 i1 i2 indx))
(implies
(and (trans z0 i0) (trans z1 i1) (same-locn z0 i0 z1 i1)
(leads-to z1 i1 z2 i2) (prec z0 i0 z2 i2))
(or (and (= z0 z1) (= i0 i1)) (prec z0 i0 z1 i1)))))
(defgenrule fact-init-neq0
(forall ((z strd) (upsilon expt))
(implies (and (p "init" z 4) (p "init" "upsilon" z upsilon))
(fact neq (exp (gen) upsilon) (gen)))))
(defgenrule fact-resp-neq0
(forall ((z strd) (zeta expt))
(implies (and (p "resp" z 3) (p "resp" "zeta" z zeta))
(fact neq (exp (gen) zeta) (gen)))))
(defgenrule trRl_ltx-gen-at-1
(forall ((z strd)) (implies (p "ltx-gen" z 2) (trans z 1))))
(defgenrule trRl_ltx-gen-at-0
(forall ((z strd)) (implies (p "ltx-gen" z 2) (trans z 0))))
(defgenrule trRl_ltx-disclose-at-1
(forall ((z strd)) (implies (p "ltx-disclose" z 2) (trans z 1))))
(defgenrule trRl_ltx-disclose-at-0
(forall ((z strd)) (implies (p "ltx-disclose" z 2) (trans z 0))))
(defgenrule gen-st-init-0
(forall ((z strd) (la rndx) (a name))
(implies
(and (p "init" z 1) (p "init" "la" z la) (p "init" "a" z a))
(gen-st (pv a la)))))
(defgenrule gen-st-resp-0
(forall ((z strd) (lb rndx) (b name))
(implies
(and (p "resp" z 1) (p "resp" "lb" z lb) (p "resp" "b" z b))
(gen-st (pv b lb)))))
(defgenrule gen-st-ltx-disclose-0
(forall ((z strd) (l rndx) (self name))
(implies
(and (p "ltx-disclose" z 1) (p "ltx-disclose" "l" z l)
(p "ltx-disclose" "self" z self)) (gen-st (pv self l)))))
(lang (sig sign) (body (tuple 3)) (pv (tuple 2))))
(defskeleton dhcr-um
(vars (na nb data) (a b name) (pt pval) (priv-stor locn) (lb y rndx)
(alpha zeta expt))
(defstrand resp 5 (na na) (nb nb) (a a) (b b) (priv-stor priv-stor)
(lb lb) (y y) (alpha alpha) (zeta zeta))
(non-orig (privk "sig" a))
(uniq-orig nb)
(uniq-gen y)
(absent (y lb) (y alpha) (y zeta))
(facts (neq a b) (undisclosed lb))
(traces
((load priv-stor (cat pt (pv b lb)))
(recv
(sig (body a (exp (gen) alpha) (pubk "sig" a)) (privk "sig" a)))
(recv (cat na a b (exp (gen) zeta)))
(send
(cat (exp (gen) y)
(enc na nb a b
(hash (exp (gen) (mul lb alpha))
(exp (gen) (mul y zeta)))))) (recv nb)))
(label 859)
(unrealized (0 1))
(origs (nb (0 3)))
(comment "Not closed under rules"))
(defskeleton dhcr-um
(vars (ignore ignore-0 mesg) (na nb data) (a self name)
(pt pt-0 pt-1 pt-2 pt-3 pval) (priv-stor priv-stor-0 locn) (y rndx)
(zeta expt) (l l-0 rndx))
(defstrand resp 5 (na na) (nb nb) (a a) (b self)
(priv-stor priv-stor-0) (lb l-0) (y y) (alpha l) (zeta zeta))
(defstrand ltx-gen 3 (ignore ignore) (self a) (priv-stor priv-stor)
(l l))
(defstrand ltx-disclose 3 (self a) (priv-stor priv-stor) (l l))
(defstrand ltx-gen 3 (ignore ignore-0) (self self)
(priv-stor priv-stor-0) (l l-0))
(precedes ((1 1) (2 0)) ((1 2) (0 1)) ((2 2) (0 4)) ((3 1) (0 0))
((3 2) (0 4)))
(non-orig (privk "sig" a))
(uniq-orig nb l l-0)
(uniq-gen y)
(absent (y zeta) (y l) (y l-0))
(gen-st (pv a l) (pv self l-0))
(facts (trans 2 1) (trans 2 0) (trans 1 1) (trans 1 0) (trans 3 1)
(trans 3 0) (neq (exp (gen) zeta) (gen)) (neq a self)
(undisclosed l-0))
(operation generalization deleted (2 0))
(traces
((load priv-stor-0 (cat pt-3 (pv self l-0)))
(recv (sig (body a (exp (gen) l) (pubk "sig" a)) (privk "sig" a)))
(recv (cat na a self (exp (gen) zeta)))
(send
(cat (exp (gen) y)
(enc na nb a self
(hash (exp (gen) (mul l l-0)) (exp (gen) (mul y zeta))))))
(recv nb))
((load priv-stor (cat pt ignore))
(stor priv-stor (cat pt-0 (pv a l)))
(send
(sig (body a (exp (gen) l) (pubk "sig" a)) (privk "sig" a))))
((load priv-stor (cat pt-0 (pv a l)))
(stor priv-stor (cat pt-1 "nil")) (send l))
((load priv-stor-0 (cat pt-2 ignore-0))
(stor priv-stor-0 (cat pt-3 (pv self l-0)))
(send
(sig (body self (exp (gen) l-0) (pubk "sig" self))
(privk "sig" self)))))
(label 886)
(parent 859)
(realized)
(shape)
(maps
((0)
((a a) (b self) (lb l-0) (y y) (alpha l) (zeta zeta) (na na)
(nb nb) (priv-stor priv-stor-0) (pt pt-3))))
(origs (l-0 (3 1)) (pt-3 (3 1)) (pt-1 (2 1)) (l (1 1)) (pt-0 (1 1))
(nb (0 3))))
(comment "Nothing left to do")
(defprotocol dhcr-um diffie-hellman
(defrole init
(vars (la x rndx) (beta upsilon expt) (a b name) (na nb data)
(priv-stor locn))
(trace (load priv-stor (pv a la))
(recv
(sig (body b (exp (gen) beta) (pubk "sig" b)) (privk "sig" b)))
(send (cat na a b (exp (gen) x)))
(recv
(cat (exp (gen) upsilon)
(enc na nb a b
(hash (exp (gen) (mul la beta))
(exp (gen) (mul x upsilon)))))) (send nb))
(uniq-orig na)
(uniq-gen x)
(absent (x la) (x beta))
(facts (neq (exp (gen) upsilon) (gen)))
(gen-st (pv a la))
(fn-of ("principal-of" (ltxa a) (ltxb b))
("ltx-of" (a ltxa) (b ltxb))))
(defrole resp
(vars (lb y rndx) (alpha zeta expt) (a b name) (na nb data)
(priv-stor locn))
(trace (load priv-stor (pv b lb))
(recv
(sig (body a (exp (gen) alpha) (pubk "sig" a)) (privk "sig" a)))
(recv (cat na a b (exp (gen) zeta)))
(send
(cat (exp (gen) y)
(enc na nb a b
(hash (exp (gen) (mul lb alpha))
(exp (gen) (mul y zeta)))))) (recv nb))
(uniq-orig nb)
(uniq-gen y)
(absent (y lb) (y alpha) (y zeta))
(facts (neq (exp (gen) zeta) (gen)))
(gen-st (pv b lb))
(fn-of ("principal-of" (ltxa a) (ltxb b))
("ltx-of" (a ltxa) (b ltxb))))
(defrole ltx-gen
(vars (self name) (l rndx) (priv-stor locn) (ignore mesg))
(trace (load priv-stor ignore) (stor priv-stor (pv self l))
(send
(sig (body self (exp (gen) l) (pubk "sig" self))
(privk "sig" self))))
(uniq-orig l)
(fn-of ("principal-of" (l self)) ("ltx-of" (self l))))
(defrole ltx-disclose
(vars (self name) (l rndx) (priv-stor locn))
(trace (load priv-stor (pv self l)) (stor priv-stor "nil") (send l))
(gen-st (pv self l))
(fn-of ("principal-of" (l self)) ("ltx-of" (self l))))
(defrule undisclosed-not-disclosed
(forall ((z strd) (l rndx))
(implies
(and (fact undisclosed l) (p "ltx-disclose" z 2)
(p "ltx-disclose" "l" z l))
(false))))
(defgenrule neqRl_indx
(forall ((x indx)) (implies (fact neq x x) (false))))
(defgenrule neqRl_strd
(forall ((x strd)) (implies (fact neq x x) (false))))
(defgenrule neqRl_mesg
(forall ((x mesg)) (implies (fact neq x x) (false))))
(defgenrule shearsRule
(forall ((z0 z1 z2 strd) (i0 i1 i2 indx))
(implies
(and (trans z0 i0) (trans z1 i1) (trans z2 i2)
(leads-to z0 i0 z1 i1) (same-locn z0 i0 z2 i2)
(prec z0 i0 z2 i2))
(or (and (= z1 z2) (= i1 i2)) (prec z1 i1 z2 i2)))))
(defgenrule invShearsRule
(forall ((z0 z1 z2 strd) (i0 i1 i2 indx))
(implies
(and (trans z0 i0) (trans z1 i1) (same-locn z0 i0 z1 i1)
(leads-to z1 i1 z2 i2) (prec z0 i0 z2 i2))
(or (and (= z0 z1) (= i0 i1)) (prec z0 i0 z1 i1)))))
(defgenrule fact-init-neq0
(forall ((z strd) (upsilon expt))
(implies (and (p "init" z 4) (p "init" "upsilon" z upsilon))
(fact neq (exp (gen) upsilon) (gen)))))
(defgenrule fact-resp-neq0
(forall ((z strd) (zeta expt))
(implies (and (p "resp" z 3) (p "resp" "zeta" z zeta))
(fact neq (exp (gen) zeta) (gen)))))
(defgenrule trRl_ltx-gen-at-1
(forall ((z strd)) (implies (p "ltx-gen" z 2) (trans z 1))))
(defgenrule trRl_ltx-gen-at-0
(forall ((z strd)) (implies (p "ltx-gen" z 2) (trans z 0))))
(defgenrule trRl_ltx-disclose-at-1
(forall ((z strd)) (implies (p "ltx-disclose" z 2) (trans z 1))))
(defgenrule trRl_ltx-disclose-at-0
(forall ((z strd)) (implies (p "ltx-disclose" z 2) (trans z 0))))
(defgenrule gen-st-init-0
(forall ((z strd) (la rndx) (a name))
(implies
(and (p "init" z 1) (p "init" "la" z la) (p "init" "a" z a))
(gen-st (pv a la)))))
(defgenrule gen-st-resp-0
(forall ((z strd) (lb rndx) (b name))
(implies
(and (p "resp" z 1) (p "resp" "lb" z lb) (p "resp" "b" z b))
(gen-st (pv b lb)))))
(defgenrule gen-st-ltx-disclose-0
(forall ((z strd) (l rndx) (self name))
(implies
(and (p "ltx-disclose" z 1) (p "ltx-disclose" "l" z l)
(p "ltx-disclose" "self" z self)) (gen-st (pv self l)))))
(lang (sig sign) (body (tuple 3)) (pv (tuple 2))))
(defskeleton dhcr-um
(vars (na nb data) (a b name) (pt pval) (priv-stor locn) (lb y rndx)
(alpha zeta expt))
(defstrand resp 5 (na na) (nb nb) (a a) (b b) (priv-stor priv-stor)
(lb lb) (y y) (alpha alpha) (zeta zeta))
(non-orig (privk "sig" a))
(uniq-orig nb)
(uniq-gen y)
(absent (y lb) (y alpha) (y zeta))
(facts (neq a b))
(traces
((load priv-stor (cat pt (pv b lb)))
(recv
(sig (body a (exp (gen) alpha) (pubk "sig" a)) (privk "sig" a)))
(recv (cat na a b (exp (gen) zeta)))
(send
(cat (exp (gen) y)
(enc na nb a b
(hash (exp (gen) (mul lb alpha))
(exp (gen) (mul y zeta)))))) (recv nb)))
(label 889)
(unrealized (0 1))
(origs (nb (0 3)))
(comment "Not closed under rules"))
(defskeleton dhcr-um
(vars (ignore ignore-0 mesg) (na nb data) (a self name)
(pt pt-0 pt-1 pt-2 pt-3 pval) (priv-stor priv-stor-0 locn) (y rndx)
(zeta expt) (l l-0 rndx))
(defstrand resp 5 (na na) (nb nb) (a a) (b self)
(priv-stor priv-stor-0) (lb l-0) (y y) (alpha l) (zeta zeta))
(defstrand ltx-gen 3 (ignore ignore) (self a) (priv-stor priv-stor)
(l l))
(defstrand ltx-disclose 3 (self a) (priv-stor priv-stor) (l l))
(defstrand ltx-gen 3 (ignore ignore-0) (self self)
(priv-stor priv-stor-0) (l l-0))
(precedes ((1 1) (2 0)) ((1 2) (0 1)) ((2 2) (0 4)) ((3 1) (0 0))
((3 2) (0 4)))
(non-orig (privk "sig" a))
(uniq-orig nb l l-0)
(uniq-gen y)
(absent (y zeta) (y l) (y l-0))
(gen-st (pv a l) (pv self l-0))
(facts (trans 2 1) (trans 2 0) (trans 1 1) (trans 1 0) (trans 3 1)
(trans 3 0) (neq (exp (gen) zeta) (gen)) (neq a self))
(operation generalization deleted (2 0))
(traces
((load priv-stor-0 (cat pt-3 (pv self l-0)))
(recv (sig (body a (exp (gen) l) (pubk "sig" a)) (privk "sig" a)))
(recv (cat na a self (exp (gen) zeta)))
(send
(cat (exp (gen) y)
(enc na nb a self
(hash (exp (gen) (mul l l-0)) (exp (gen) (mul y zeta))))))
(recv nb))
((load priv-stor (cat pt ignore))
(stor priv-stor (cat pt-0 (pv a l)))
(send
(sig (body a (exp (gen) l) (pubk "sig" a)) (privk "sig" a))))
((load priv-stor (cat pt-0 (pv a l)))
(stor priv-stor (cat pt-1 "nil")) (send l))
((load priv-stor-0 (cat pt-2 ignore-0))
(stor priv-stor-0 (cat pt-3 (pv self l-0)))
(send
(sig (body self (exp (gen) l-0) (pubk "sig" self))
(privk "sig" self)))))
(label 937)
(parent 889)
(realized)
(shape)
(maps
((0)
((a a) (b self) (lb l-0) (y y) (alpha l) (zeta zeta) (na na)
(nb nb) (priv-stor priv-stor-0) (pt pt-3))))
(origs (l-0 (3 1)) (pt-3 (3 1)) (pt-1 (2 1)) (l (1 1)) (pt-0 (1 1))
(nb (0 3))))
(defskeleton dhcr-um
(vars (ignore ignore-0 mesg) (na nb data) (a b name)
(pt pt-0 pt-1 pt-2 pt-3 pval) (priv-stor priv-stor-0 locn) (y rndx)
(zeta expt) (l l-0 rndx))
(defstrand resp 5 (na na) (nb nb) (a a) (b b) (priv-stor priv-stor)
(lb l) (y y) (alpha l-0) (zeta zeta))
(defstrand ltx-gen 2 (ignore ignore) (self b) (priv-stor priv-stor)
(l l))
(defstrand ltx-gen 3 (ignore ignore-0) (self a)
(priv-stor priv-stor-0) (l l-0))
(defstrand ltx-disclose 3 (self b) (priv-stor priv-stor) (l l))
(precedes ((1 1) (0 0)) ((1 1) (3 0)) ((2 2) (0 1)) ((3 2) (0 4)))
(non-orig (privk "sig" a))
(uniq-orig nb l l-0)
(uniq-gen y)
(absent (y zeta) (y l) (y l-0))
(gen-st (pv b l))
(facts (trans 3 1) (trans 3 0) (trans 2 1) (trans 2 0) (trans 1 1)
(trans 1 0) (neq (exp (gen) zeta) (gen)) (neq a b))
(operation generalization deleted (3 0))
(traces
((load priv-stor (cat pt (pv b l)))
(recv
(sig (body a (exp (gen) l-0) (pubk "sig" a)) (privk "sig" a)))
(recv (cat na a b (exp (gen) zeta)))
(send
(cat (exp (gen) y)
(enc na nb a b
(hash (exp (gen) (mul l l-0)) (exp (gen) (mul y zeta))))))
(recv nb))
((load priv-stor (cat pt-0 ignore))
(stor priv-stor (cat pt (pv b l))))
((load priv-stor-0 (cat pt-1 ignore-0))
(stor priv-stor-0 (cat pt-2 (pv a l-0)))
(send
(sig (body a (exp (gen) l-0) (pubk "sig" a)) (privk "sig" a))))
((load priv-stor (cat pt (pv b l)))
(stor priv-stor (cat pt-3 "nil")) (send l)))
(label 940)
(parent 889)
(realized)
(shape)
(maps
((0)
((a a) (b b) (lb l) (y y) (alpha l-0) (zeta zeta) (na na) (nb nb)
(priv-stor priv-stor) (pt pt))))
(origs (l-0 (2 1)) (pt-2 (2 1)) (pt-3 (3 1)) (l (1 1)) (pt (1 1))
(nb (0 3))))
(defskeleton dhcr-um
(vars (ignore ignore-0 mesg) (na nb data) (a b name)
(pt pt-0 pt-1 pt-2 pt-3 pval) (priv-stor priv-stor-0 locn) (y rndx)
(zeta expt) (l l-0 rndx))
(defstrand resp 5 (na na) (nb nb) (a a) (b b) (priv-stor priv-stor)
(lb l-0) (y y) (alpha l) (zeta zeta))
(defstrand ltx-gen 2 (ignore ignore) (self b) (priv-stor priv-stor)
(l l-0))
(defstrand ltx-gen 3 (ignore ignore-0) (self a)
(priv-stor priv-stor-0) (l l))
(defstrand ltx-disclose 3 (self b) (priv-stor priv-stor) (l l-0))
(precedes ((1 1) (0 0)) ((1 1) (3 0)) ((2 2) (0 1)) ((3 2) (0 4)))
(non-orig (privk "sig" a))
(uniq-orig nb l l-0)
(uniq-gen y)
(absent (y zeta) (y l) (y l-0))
(gen-st (pv a l) (pv b l-0))
(facts (trans 3 1) (trans 3 0) (trans 2 1) (trans 2 0) (trans 1 1)
(trans 1 0) (neq (exp (gen) zeta) (gen)) (neq a b))
(operation generalization deleted (3 0))
(traces
((load priv-stor (cat pt (pv b l-0)))
(recv (sig (body a (exp (gen) l) (pubk "sig" a)) (privk "sig" a)))
(recv (cat na a b (exp (gen) zeta)))
(send
(cat (exp (gen) y)
(enc na nb a b
(hash (exp (gen) (mul l l-0)) (exp (gen) (mul y zeta))))))
(recv nb))
((load priv-stor (cat pt-0 ignore))
(stor priv-stor (cat pt (pv b l-0))))
((load priv-stor-0 (cat pt-1 ignore-0))
(stor priv-stor-0 (cat pt-2 (pv a l)))
(send
(sig (body a (exp (gen) l) (pubk "sig" a)) (privk "sig" a))))
((load priv-stor (cat pt (pv b l-0)))
(stor priv-stor (cat pt-3 "nil")) (send l-0)))
(label 951)
(parent 889)
(realized)
(shape)
(maps
((0)
((a a) (b b) (lb l-0) (y y) (alpha l) (zeta zeta) (na na) (nb nb)
(priv-stor priv-stor) (pt pt))))
(origs (pt-3 (3 1)) (l (2 1)) (pt-2 (2 1)) (l-0 (1 1)) (pt (1 1))
(nb (0 3))))
(comment "Nothing left to do")