cpsa-4.4.4: tst/dhcr_um3_shapes.tst
(comment "CPSA 4.3.1")
(comment "Extracted shapes")
(herald "DHCR: unified model (UM) three-part" (bound 20) (limit 8000)
(algebra diffie-hellman))
(comment "CPSA 4.3.1")
(comment "All input read from tst/dhcr_um3.scm")
(comment "Step count limited to 8000")
(comment "Strand count bounded at 20")
(defprotocol dhcr-um3 diffie-hellman
(defrole init
(vars (ltxa ltxb x rndx) (y expt) (a b name) (na nb data))
(trace (recv (cat (exp (gen) ltxa) (exp (gen) ltxb)))
(send (cat na a b (exp (gen) x)))
(recv
(cat (exp (gen) y)
(enc na nb a b
(hash (exp (gen) (mul ltxa y)) (exp (gen) (mul ltxb x))
(exp (gen) (mul x y)))))) (send nb))
(uniq-orig na)
(uniq-gen x)
(absent (x ltxa) (x ltxb))
(fn-of ("principal-of" (ltxa a) (ltxb b))
("ltx-of" (a ltxa) (b ltxb)))
(neq ((exp (gen) y) (gen))))
(defrole resp
(vars (ltxa ltxb y rndx) (x expt) (a b name) (na nb data))
(trace (recv (cat (exp (gen) ltxa) (exp (gen) ltxb)))
(recv (cat na a b (exp (gen) x)))
(send
(cat (exp (gen) y)
(enc na nb a b
(hash (exp (gen) (mul ltxa y)) (exp (gen) (mul ltxb x))
(exp (gen) (mul y x)))))) (recv nb))
(uniq-orig nb)
(uniq-gen y)
(absent (y ltxa) (y ltxb) (y x))
(fn-of ("principal-of" (ltxa a) (ltxb b))
("ltx-of" (a ltxa) (b ltxb)))
(neq ((exp (gen) x) (gen))))
(defrole ltx-gen
(vars (self name) (l rndx))
(trace (send (cat self (exp (gen) l))) (recv "end-of-protocol")
(send l))
(uniq-gen l)
(fn-of ("principal-of" (l self)) ("ltx-of" (self l))))
(defgenrule neqRl_indx
(forall ((x indx)) (implies (fact neq x x) (false))))
(defgenrule neqRl_strd
(forall ((x strd)) (implies (fact neq x x) (false))))
(defgenrule neqRl_mesg
(forall ((x mesg)) (implies (fact neq x x) (false)))))
(defskeleton dhcr-um3
(vars (na nb data) (a b self self-0 name) (ltxa ltxb x rndx) (y expt))
(defstrand init 4 (na na) (nb nb) (a a) (b b) (ltxa ltxa) (ltxb ltxb)
(x x) (y y))
(defstrand ltx-gen 1 (self self) (l ltxa))
(defstrand ltx-gen 1 (self self-0) (l ltxb))
(non-orig ltxa ltxb)
(uniq-orig na)
(uniq-gen ltxa ltxb x)
(absent (x ltxa) (x ltxb))
(traces
((recv (cat (exp (gen) ltxa) (exp (gen) ltxb)))
(send (cat na a b (exp (gen) x)))
(recv
(cat (exp (gen) y)
(enc na nb a b
(hash (exp (gen) (mul ltxa y)) (exp (gen) (mul ltxb x))
(exp (gen) (mul x y)))))) (send nb))
((send (cat self (exp (gen) ltxa))))
((send (cat self-0 (exp (gen) ltxb)))))
(label 0)
(unrealized (0 0) (0 2))
(preskeleton)
(origs (na (0 1)))
(comment "Not a skeleton"))
(defskeleton dhcr-um3
(vars (na nb data) (a b self self-0 name) (y x ltxa ltxb rndx))
(defstrand init 4 (na na) (nb nb) (a a) (b b) (ltxa ltxa) (ltxb ltxb)
(x x) (y y))
(defstrand ltx-gen 1 (self self) (l ltxa))
(defstrand ltx-gen 1 (self self-0) (l ltxb))
(defstrand resp 3 (na na) (nb nb) (a a) (b b) (ltxa ltxa) (ltxb ltxb)
(y y) (x x))
(precedes ((0 1) (3 1)) ((1 0) (0 0)) ((1 0) (3 0)) ((2 0) (0 0))
((2 0) (3 0)) ((3 2) (0 2)))
(non-orig ltxa ltxb)
(uniq-orig na nb)
(uniq-gen y x ltxa ltxb)
(absent (y x) (y ltxa) (y ltxb) (x ltxa) (x ltxb))
(operation encryption-test (added-strand resp 3)
(enc na nb a b
(hash (exp (gen) (mul y ltxa)) (exp (gen) (mul x ltxb))
(exp (gen) (mul y x)))) (0 2))
(traces
((recv (cat (exp (gen) ltxa) (exp (gen) ltxb)))
(send (cat na a b (exp (gen) x)))
(recv
(cat (exp (gen) y)
(enc na nb a b
(hash (exp (gen) (mul y ltxa)) (exp (gen) (mul x ltxb))
(exp (gen) (mul y x)))))) (send nb))
((send (cat self (exp (gen) ltxa))))
((send (cat self-0 (exp (gen) ltxb))))
((recv (cat (exp (gen) ltxa) (exp (gen) ltxb)))
(recv (cat na a b (exp (gen) x)))
(send
(cat (exp (gen) y)
(enc na nb a b
(hash (exp (gen) (mul y ltxa)) (exp (gen) (mul x ltxb))
(exp (gen) (mul y x))))))))
(label 3)
(parent 0)
(realized)
(shape)
(maps
((0 1 2)
((ltxa ltxa) (ltxb ltxb) (a a) (b b) (x x) (y y) (na na) (nb nb)
(self self) (self-0 self-0))))
(origs (nb (3 2)) (na (0 1))))
(defskeleton dhcr-um3
(vars (na nb data) (a b self name) (y x ltxb rndx))
(defstrand init 4 (na na) (nb nb) (a a) (b b) (ltxa ltxb) (ltxb ltxb)
(x x) (y y))
(defstrand ltx-gen 1 (self self) (l ltxb))
(defstrand resp 3 (na na) (nb nb) (a a) (b b) (ltxa ltxb) (ltxb ltxb)
(y y) (x x))
(precedes ((0 1) (2 1)) ((1 0) (0 0)) ((1 0) (2 0)) ((2 2) (0 2)))
(non-orig ltxb)
(uniq-orig na nb)
(uniq-gen y x ltxb)
(absent (y x) (y ltxb) (x ltxb))
(operation encryption-test (added-strand resp 3)
(enc na nb a b
(hash (exp (gen) (mul y ltxb)) (exp (gen) (mul x ltxb))
(exp (gen) (mul y x)))) (0 2))
(traces
((recv (cat (exp (gen) ltxb) (exp (gen) ltxb)))
(send (cat na a b (exp (gen) x)))
(recv
(cat (exp (gen) y)
(enc na nb a b
(hash (exp (gen) (mul y ltxb)) (exp (gen) (mul x ltxb))
(exp (gen) (mul y x)))))) (send nb))
((send (cat self (exp (gen) ltxb))))
((recv (cat (exp (gen) ltxb) (exp (gen) ltxb)))
(recv (cat na a b (exp (gen) x)))
(send
(cat (exp (gen) y)
(enc na nb a b
(hash (exp (gen) (mul y ltxb)) (exp (gen) (mul x ltxb))
(exp (gen) (mul y x))))))))
(label 6)
(parent 0)
(realized)
(shape)
(maps
((0 1 1)
((ltxa ltxb) (ltxb ltxb) (a a) (b b) (x x) (y y) (na na) (nb nb)
(self self) (self-0 self))))
(origs (nb (2 2)) (na (0 1))))
(comment "Nothing left to do")
(defprotocol dhcr-um3 diffie-hellman
(defrole init
(vars (ltxa ltxb x rndx) (y expt) (a b name) (na nb data))
(trace (recv (cat (exp (gen) ltxa) (exp (gen) ltxb)))
(send (cat na a b (exp (gen) x)))
(recv
(cat (exp (gen) y)
(enc na nb a b
(hash (exp (gen) (mul ltxa y)) (exp (gen) (mul ltxb x))
(exp (gen) (mul x y)))))) (send nb))
(uniq-orig na)
(uniq-gen x)
(absent (x ltxa) (x ltxb))
(fn-of ("principal-of" (ltxa a) (ltxb b))
("ltx-of" (a ltxa) (b ltxb)))
(neq ((exp (gen) y) (gen))))
(defrole resp
(vars (ltxa ltxb y rndx) (x expt) (a b name) (na nb data))
(trace (recv (cat (exp (gen) ltxa) (exp (gen) ltxb)))
(recv (cat na a b (exp (gen) x)))
(send
(cat (exp (gen) y)
(enc na nb a b
(hash (exp (gen) (mul ltxa y)) (exp (gen) (mul ltxb x))
(exp (gen) (mul y x)))))) (recv nb))
(uniq-orig nb)
(uniq-gen y)
(absent (y ltxa) (y ltxb) (y x))
(fn-of ("principal-of" (ltxa a) (ltxb b))
("ltx-of" (a ltxa) (b ltxb)))
(neq ((exp (gen) x) (gen))))
(defrole ltx-gen
(vars (self name) (l rndx))
(trace (send (cat self (exp (gen) l))) (recv "end-of-protocol")
(send l))
(uniq-gen l)
(fn-of ("principal-of" (l self)) ("ltx-of" (self l))))
(defgenrule neqRl_indx
(forall ((x indx)) (implies (fact neq x x) (false))))
(defgenrule neqRl_strd
(forall ((x strd)) (implies (fact neq x x) (false))))
(defgenrule neqRl_mesg
(forall ((x mesg)) (implies (fact neq x x) (false)))))
(defskeleton dhcr-um3
(vars (na nb data) (a b self name) (ltxa ltxb x rndx) (y expt))
(defstrand init 4 (na na) (nb nb) (a a) (b b) (ltxa ltxa) (ltxb ltxb)
(x x) (y y))
(defstrand ltx-gen 1 (self self) (l ltxb))
(non-orig ltxb)
(uniq-orig na)
(uniq-gen ltxb x)
(absent (x ltxa) (x ltxb))
(traces
((recv (cat (exp (gen) ltxa) (exp (gen) ltxb)))
(send (cat na a b (exp (gen) x)))
(recv
(cat (exp (gen) y)
(enc na nb a b
(hash (exp (gen) (mul ltxa y)) (exp (gen) (mul ltxb x))
(exp (gen) (mul x y)))))) (send nb))
((send (cat self (exp (gen) ltxb)))))
(label 13)
(unrealized (0 0) (0 2))
(preskeleton)
(origs (na (0 1)))
(comment "Not a skeleton"))
(defskeleton dhcr-um3
(vars (na nb data) (a b self name) (y x ltxa ltxb rndx))
(defstrand init 4 (na na) (nb nb) (a a) (b b) (ltxa ltxa) (ltxb ltxb)
(x x) (y y))
(defstrand ltx-gen 1 (self self) (l ltxb))
(defstrand resp 3 (na na) (nb nb) (a a) (b b) (ltxa ltxa) (ltxb ltxb)
(y y) (x x))
(precedes ((0 1) (2 1)) ((1 0) (0 0)) ((1 0) (2 0)) ((2 2) (0 2)))
(non-orig ltxb)
(uniq-orig na nb)
(uniq-gen y x ltxb)
(absent (y x) (y ltxa) (y ltxb) (x ltxa) (x ltxb))
(operation encryption-test (added-strand resp 3)
(enc na nb a b
(hash (exp (gen) (mul y ltxa)) (exp (gen) (mul x ltxb))
(exp (gen) (mul y x)))) (0 2))
(traces
((recv (cat (exp (gen) ltxa) (exp (gen) ltxb)))
(send (cat na a b (exp (gen) x)))
(recv
(cat (exp (gen) y)
(enc na nb a b
(hash (exp (gen) (mul y ltxa)) (exp (gen) (mul x ltxb))
(exp (gen) (mul y x)))))) (send nb))
((send (cat self (exp (gen) ltxb))))
((recv (cat (exp (gen) ltxa) (exp (gen) ltxb)))
(recv (cat na a b (exp (gen) x)))
(send
(cat (exp (gen) y)
(enc na nb a b
(hash (exp (gen) (mul y ltxa)) (exp (gen) (mul x ltxb))
(exp (gen) (mul y x))))))))
(label 15)
(parent 13)
(realized)
(shape)
(maps
((0 1)
((ltxa ltxa) (ltxb ltxb) (a a) (b b) (x x) (y y) (na na) (nb nb)
(self self))))
(origs (nb (2 2)) (na (0 1))))
(defskeleton dhcr-um3
(vars (na nb data) (a b self name) (y x ltxb rndx))
(defstrand init 4 (na na) (nb nb) (a a) (b b) (ltxa ltxb) (ltxb ltxb)
(x x) (y y))
(defstrand ltx-gen 1 (self self) (l ltxb))
(defstrand resp 3 (na na) (nb nb) (a a) (b b) (ltxa ltxb) (ltxb ltxb)
(y y) (x x))
(precedes ((0 1) (2 1)) ((1 0) (0 0)) ((1 0) (2 0)) ((2 2) (0 2)))
(non-orig ltxb)
(uniq-orig na nb)
(uniq-gen y x ltxb)
(absent (y x) (y ltxb) (x ltxb))
(operation nonce-test (displaced 3 0 init 2) (exp (gen) x) (2 1))
(traces
((recv (cat (exp (gen) ltxb) (exp (gen) ltxb)))
(send (cat na a b (exp (gen) x)))
(recv
(cat (exp (gen) y)
(enc na nb a b
(hash (exp (gen) (mul y ltxb)) (exp (gen) (mul x ltxb))
(exp (gen) (mul y x)))))) (send nb))
((send (cat self (exp (gen) ltxb))))
((recv (cat (exp (gen) ltxb) (exp (gen) ltxb)))
(recv (cat na a b (exp (gen) x)))
(send
(cat (exp (gen) y)
(enc na nb a b
(hash (exp (gen) (mul y ltxb)) (exp (gen) (mul x ltxb))
(exp (gen) (mul y x))))))))
(label 18)
(parent 13)
(realized)
(shape)
(maps
((0 1)
((ltxa ltxb) (ltxb ltxb) (a a) (b b) (x x) (y y) (na na) (nb nb)
(self self))))
(origs (na (0 1)) (nb (2 2))))
(comment "Nothing left to do")
(defprotocol dhcr-um3 diffie-hellman
(defrole init
(vars (ltxa ltxb x rndx) (y expt) (a b name) (na nb data))
(trace (recv (cat (exp (gen) ltxa) (exp (gen) ltxb)))
(send (cat na a b (exp (gen) x)))
(recv
(cat (exp (gen) y)
(enc na nb a b
(hash (exp (gen) (mul ltxa y)) (exp (gen) (mul ltxb x))
(exp (gen) (mul x y)))))) (send nb))
(uniq-orig na)
(uniq-gen x)
(absent (x ltxa) (x ltxb))
(fn-of ("principal-of" (ltxa a) (ltxb b))
("ltx-of" (a ltxa) (b ltxb)))
(neq ((exp (gen) y) (gen))))
(defrole resp
(vars (ltxa ltxb y rndx) (x expt) (a b name) (na nb data))
(trace (recv (cat (exp (gen) ltxa) (exp (gen) ltxb)))
(recv (cat na a b (exp (gen) x)))
(send
(cat (exp (gen) y)
(enc na nb a b
(hash (exp (gen) (mul ltxa y)) (exp (gen) (mul ltxb x))
(exp (gen) (mul y x)))))) (recv nb))
(uniq-orig nb)
(uniq-gen y)
(absent (y ltxa) (y ltxb) (y x))
(fn-of ("principal-of" (ltxa a) (ltxb b))
("ltx-of" (a ltxa) (b ltxb)))
(neq ((exp (gen) x) (gen))))
(defrole ltx-gen
(vars (self name) (l rndx))
(trace (send (cat self (exp (gen) l))) (recv "end-of-protocol")
(send l))
(uniq-gen l)
(fn-of ("principal-of" (l self)) ("ltx-of" (self l))))
(defgenrule neqRl_indx
(forall ((x indx)) (implies (fact neq x x) (false))))
(defgenrule neqRl_strd
(forall ((x strd)) (implies (fact neq x x) (false))))
(defgenrule neqRl_mesg
(forall ((x mesg)) (implies (fact neq x x) (false)))))
(defskeleton dhcr-um3
(vars (na nb data) (a b self name) (ltxa ltxb x y rndx))
(defstrand init 4 (na na) (nb nb) (a a) (b b) (ltxa ltxa) (ltxb ltxb)
(x x) (y y))
(defstrand ltx-gen 1 (self self) (l ltxb))
(deflistener (exp (gen) (mul x y)))
(non-orig ltxb)
(uniq-orig na)
(uniq-gen ltxb x)
(absent (x ltxa) (x ltxb))
(traces
((recv (cat (exp (gen) ltxa) (exp (gen) ltxb)))
(send (cat na a b (exp (gen) x)))
(recv
(cat (exp (gen) y)
(enc na nb a b
(hash (exp (gen) (mul ltxa y)) (exp (gen) (mul ltxb x))
(exp (gen) (mul x y)))))) (send nb))
((send (cat self (exp (gen) ltxb))))
((recv (exp (gen) (mul x y))) (send (exp (gen) (mul x y)))))
(label 24)
(unrealized (0 0) (0 2) (2 0))
(preskeleton)
(origs (na (0 1)))
(comment "Not a skeleton"))
(comment "Nothing left to do")
(defprotocol dhcr-um3 diffie-hellman
(defrole init
(vars (ltxa ltxb x rndx) (y expt) (a b name) (na nb data))
(trace (recv (cat (exp (gen) ltxa) (exp (gen) ltxb)))
(send (cat na a b (exp (gen) x)))
(recv
(cat (exp (gen) y)
(enc na nb a b
(hash (exp (gen) (mul ltxa y)) (exp (gen) (mul ltxb x))
(exp (gen) (mul x y)))))) (send nb))
(uniq-orig na)
(uniq-gen x)
(absent (x ltxa) (x ltxb))
(fn-of ("principal-of" (ltxa a) (ltxb b))
("ltx-of" (a ltxa) (b ltxb)))
(neq ((exp (gen) y) (gen))))
(defrole resp
(vars (ltxa ltxb y rndx) (x expt) (a b name) (na nb data))
(trace (recv (cat (exp (gen) ltxa) (exp (gen) ltxb)))
(recv (cat na a b (exp (gen) x)))
(send
(cat (exp (gen) y)
(enc na nb a b
(hash (exp (gen) (mul ltxa y)) (exp (gen) (mul ltxb x))
(exp (gen) (mul y x)))))) (recv nb))
(uniq-orig nb)
(uniq-gen y)
(absent (y ltxa) (y ltxb) (y x))
(fn-of ("principal-of" (ltxa a) (ltxb b))
("ltx-of" (a ltxa) (b ltxb)))
(neq ((exp (gen) x) (gen))))
(defrole ltx-gen
(vars (self name) (l rndx))
(trace (send (cat self (exp (gen) l))) (recv "end-of-protocol")
(send l))
(uniq-gen l)
(fn-of ("principal-of" (l self)) ("ltx-of" (self l))))
(defgenrule neqRl_indx
(forall ((x indx)) (implies (fact neq x x) (false))))
(defgenrule neqRl_strd
(forall ((x strd)) (implies (fact neq x x) (false))))
(defgenrule neqRl_mesg
(forall ((x mesg)) (implies (fact neq x x) (false)))))
(defskeleton dhcr-um3
(vars (na nb data) (a b self self-0 name) (ltxa ltxb y rndx) (x expt))
(defstrand resp 4 (na na) (nb nb) (a a) (b b) (ltxa ltxa) (ltxb ltxb)
(y y) (x x))
(defstrand ltx-gen 1 (self self) (l ltxa))
(defstrand ltx-gen 1 (self self-0) (l ltxb))
(non-orig ltxa ltxb)
(uniq-orig nb)
(uniq-gen ltxa ltxb y)
(absent (y ltxa) (y ltxb) (y x))
(traces
((recv (cat (exp (gen) ltxa) (exp (gen) ltxb)))
(recv (cat na a b (exp (gen) x)))
(send
(cat (exp (gen) y)
(enc na nb a b
(hash (exp (gen) (mul ltxa y)) (exp (gen) (mul ltxb x))
(exp (gen) (mul y x)))))) (recv nb))
((send (cat self (exp (gen) ltxa))))
((send (cat self-0 (exp (gen) ltxb)))))
(label 32)
(unrealized (0 0) (0 3))
(preskeleton)
(origs (nb (0 2)))
(comment "Not a skeleton"))
(defskeleton dhcr-um3
(vars (na nb data) (a b self self-0 name) (y x ltxa ltxb rndx))
(defstrand resp 4 (na na) (nb nb) (a a) (b b) (ltxa ltxa) (ltxb ltxb)
(y y) (x x))
(defstrand ltx-gen 1 (self self) (l ltxa))
(defstrand ltx-gen 1 (self self-0) (l ltxb))
(defstrand init 4 (na na) (nb nb) (a a) (b b) (ltxa ltxa) (ltxb ltxb)
(x x) (y y))
(precedes ((0 2) (3 2)) ((1 0) (0 0)) ((1 0) (3 0)) ((2 0) (0 0))
((2 0) (3 0)) ((3 1) (0 1)) ((3 3) (0 3)))
(non-orig ltxa ltxb)
(uniq-orig na nb)
(uniq-gen y x ltxa ltxb)
(absent (y x) (y ltxa) (y ltxb) (x ltxa) (x ltxb))
(operation nonce-test (added-strand init 4) nb (0 3)
(enc na nb a b
(hash (exp (gen) (mul y ltxa)) (exp (gen) (mul x ltxb))
(exp (gen) (mul y x)))))
(traces
((recv (cat (exp (gen) ltxa) (exp (gen) ltxb)))
(recv (cat na a b (exp (gen) x)))
(send
(cat (exp (gen) y)
(enc na nb a b
(hash (exp (gen) (mul y ltxa)) (exp (gen) (mul x ltxb))
(exp (gen) (mul y x)))))) (recv nb))
((send (cat self (exp (gen) ltxa))))
((send (cat self-0 (exp (gen) ltxb))))
((recv (cat (exp (gen) ltxa) (exp (gen) ltxb)))
(send (cat na a b (exp (gen) x)))
(recv
(cat (exp (gen) y)
(enc na nb a b
(hash (exp (gen) (mul y ltxa)) (exp (gen) (mul x ltxb))
(exp (gen) (mul y x)))))) (send nb)))
(label 35)
(parent 32)
(realized)
(shape)
(maps
((0 1 2)
((ltxa ltxa) (ltxb ltxb) (a a) (b b) (y y) (x x) (na na) (nb nb)
(self self) (self-0 self-0))))
(origs (na (3 1)) (nb (0 2))))
(defskeleton dhcr-um3
(vars (na nb data) (a b self name) (y x ltxb rndx))
(defstrand resp 4 (na na) (nb nb) (a a) (b b) (ltxa ltxb) (ltxb ltxb)
(y y) (x x))
(defstrand ltx-gen 1 (self self) (l ltxb))
(defstrand init 4 (na na) (nb nb) (a a) (b b) (ltxa ltxb) (ltxb ltxb)
(x x) (y y))
(precedes ((0 2) (2 2)) ((1 0) (0 0)) ((1 0) (2 0)) ((2 1) (0 1))
((2 3) (0 3)))
(non-orig ltxb)
(uniq-orig na nb)
(uniq-gen y x ltxb)
(absent (y x) (y ltxb) (x ltxb))
(operation nonce-test (added-strand init 4) nb (0 3)
(enc na nb a b
(hash (exp (gen) (mul y ltxb)) (exp (gen) (mul x ltxb))
(exp (gen) (mul y x)))))
(traces
((recv (cat (exp (gen) ltxb) (exp (gen) ltxb)))
(recv (cat na a b (exp (gen) x)))
(send
(cat (exp (gen) y)
(enc na nb a b
(hash (exp (gen) (mul y ltxb)) (exp (gen) (mul x ltxb))
(exp (gen) (mul y x)))))) (recv nb))
((send (cat self (exp (gen) ltxb))))
((recv (cat (exp (gen) ltxb) (exp (gen) ltxb)))
(send (cat na a b (exp (gen) x)))
(recv
(cat (exp (gen) y)
(enc na nb a b
(hash (exp (gen) (mul y ltxb)) (exp (gen) (mul x ltxb))
(exp (gen) (mul y x)))))) (send nb)))
(label 38)
(parent 32)
(realized)
(shape)
(maps
((0 1 1)
((ltxa ltxb) (ltxb ltxb) (a a) (b b) (y y) (x x) (na na) (nb nb)
(self self) (self-0 self))))
(origs (na (2 1)) (nb (0 2))))
(comment "Nothing left to do")
(defprotocol dhcr-um3 diffie-hellman
(defrole init
(vars (ltxa ltxb x rndx) (y expt) (a b name) (na nb data))
(trace (recv (cat (exp (gen) ltxa) (exp (gen) ltxb)))
(send (cat na a b (exp (gen) x)))
(recv
(cat (exp (gen) y)
(enc na nb a b
(hash (exp (gen) (mul ltxa y)) (exp (gen) (mul ltxb x))
(exp (gen) (mul x y)))))) (send nb))
(uniq-orig na)
(uniq-gen x)
(absent (x ltxa) (x ltxb))
(fn-of ("principal-of" (ltxa a) (ltxb b))
("ltx-of" (a ltxa) (b ltxb)))
(neq ((exp (gen) y) (gen))))
(defrole resp
(vars (ltxa ltxb y rndx) (x expt) (a b name) (na nb data))
(trace (recv (cat (exp (gen) ltxa) (exp (gen) ltxb)))
(recv (cat na a b (exp (gen) x)))
(send
(cat (exp (gen) y)
(enc na nb a b
(hash (exp (gen) (mul ltxa y)) (exp (gen) (mul ltxb x))
(exp (gen) (mul y x)))))) (recv nb))
(uniq-orig nb)
(uniq-gen y)
(absent (y ltxa) (y ltxb) (y x))
(fn-of ("principal-of" (ltxa a) (ltxb b))
("ltx-of" (a ltxa) (b ltxb)))
(neq ((exp (gen) x) (gen))))
(defrole ltx-gen
(vars (self name) (l rndx))
(trace (send (cat self (exp (gen) l))) (recv "end-of-protocol")
(send l))
(uniq-gen l)
(fn-of ("principal-of" (l self)) ("ltx-of" (self l))))
(defgenrule neqRl_indx
(forall ((x indx)) (implies (fact neq x x) (false))))
(defgenrule neqRl_strd
(forall ((x strd)) (implies (fact neq x x) (false))))
(defgenrule neqRl_mesg
(forall ((x mesg)) (implies (fact neq x x) (false)))))
(defskeleton dhcr-um3
(vars (na nb data) (a b self name) (ltxa ltxb y rndx) (x expt))
(defstrand resp 4 (na na) (nb nb) (a a) (b b) (ltxa ltxa) (ltxb ltxb)
(y y) (x x))
(defstrand ltx-gen 1 (self self) (l ltxa))
(non-orig ltxa)
(uniq-orig nb)
(uniq-gen ltxa y)
(absent (y ltxa) (y ltxb) (y x))
(traces
((recv (cat (exp (gen) ltxa) (exp (gen) ltxb)))
(recv (cat na a b (exp (gen) x)))
(send
(cat (exp (gen) y)
(enc na nb a b
(hash (exp (gen) (mul ltxa y)) (exp (gen) (mul ltxb x))
(exp (gen) (mul y x)))))) (recv nb))
((send (cat self (exp (gen) ltxa)))))
(label 45)
(unrealized (0 0) (0 3))
(preskeleton)
(origs (nb (0 2)))
(comment "Not a skeleton"))
(defskeleton dhcr-um3
(vars (na nb data) (a b self name) (y x ltxa ltxb rndx))
(defstrand resp 4 (na na) (nb nb) (a a) (b b) (ltxa ltxa) (ltxb ltxb)
(y y) (x x))
(defstrand ltx-gen 1 (self self) (l ltxa))
(defstrand init 4 (na na) (nb nb) (a a) (b b) (ltxa ltxa) (ltxb ltxb)
(x x) (y y))
(precedes ((0 2) (2 2)) ((1 0) (0 0)) ((1 0) (2 0)) ((2 1) (0 1))
((2 3) (0 3)))
(non-orig ltxa)
(uniq-orig na nb)
(uniq-gen y x ltxa)
(absent (y x) (y ltxa) (y ltxb) (x ltxa) (x ltxb))
(operation nonce-test (added-strand init 4) nb (0 3)
(enc na nb a b
(hash (exp (gen) (mul y ltxa)) (exp (gen) (mul x ltxb))
(exp (gen) (mul y x)))))
(traces
((recv (cat (exp (gen) ltxa) (exp (gen) ltxb)))
(recv (cat na a b (exp (gen) x)))
(send
(cat (exp (gen) y)
(enc na nb a b
(hash (exp (gen) (mul y ltxa)) (exp (gen) (mul x ltxb))
(exp (gen) (mul y x)))))) (recv nb))
((send (cat self (exp (gen) ltxa))))
((recv (cat (exp (gen) ltxa) (exp (gen) ltxb)))
(send (cat na a b (exp (gen) x)))
(recv
(cat (exp (gen) y)
(enc na nb a b
(hash (exp (gen) (mul y ltxa)) (exp (gen) (mul x ltxb))
(exp (gen) (mul y x)))))) (send nb)))
(label 47)
(parent 45)
(realized)
(shape)
(maps
((0 1)
((ltxa ltxa) (ltxb ltxb) (a a) (b b) (y y) (x x) (na na) (nb nb)
(self self))))
(origs (na (2 1)) (nb (0 2))))
(defskeleton dhcr-um3
(vars (na nb data) (a b self name) (y ltxb x rndx))
(defstrand resp 4 (na na) (nb nb) (a a) (b b) (ltxa ltxb) (ltxb ltxb)
(y y) (x x))
(defstrand ltx-gen 1 (self self) (l ltxb))
(defstrand init 4 (na na) (nb nb) (a a) (b b) (ltxa ltxb) (ltxb ltxb)
(x x) (y y))
(precedes ((0 2) (2 2)) ((1 0) (0 0)) ((1 0) (2 0)) ((2 1) (0 1))
((2 3) (0 3)))
(non-orig ltxb)
(uniq-orig na nb)
(uniq-gen y ltxb x)
(absent (y ltxb) (y x) (x ltxb))
(operation nonce-test (displaced 3 0 resp 3) (exp (gen) y) (2 2))
(traces
((recv (cat (exp (gen) ltxb) (exp (gen) ltxb)))
(recv (cat na a b (exp (gen) x)))
(send
(cat (exp (gen) y)
(enc na nb a b
(hash (exp (gen) (mul y ltxb)) (exp (gen) (mul ltxb x))
(exp (gen) (mul y x)))))) (recv nb))
((send (cat self (exp (gen) ltxb))))
((recv (cat (exp (gen) ltxb) (exp (gen) ltxb)))
(send (cat na a b (exp (gen) x)))
(recv
(cat (exp (gen) y)
(enc na nb a b
(hash (exp (gen) (mul y ltxb)) (exp (gen) (mul ltxb x))
(exp (gen) (mul y x)))))) (send nb)))
(label 50)
(parent 45)
(realized)
(shape)
(maps
((0 1)
((ltxa ltxb) (ltxb ltxb) (a a) (b b) (y y) (x x) (na na) (nb nb)
(self self))))
(origs (nb (0 2)) (na (2 1))))
(comment "Nothing left to do")
(defprotocol dhcr-um3 diffie-hellman
(defrole init
(vars (ltxa ltxb x rndx) (y expt) (a b name) (na nb data))
(trace (recv (cat (exp (gen) ltxa) (exp (gen) ltxb)))
(send (cat na a b (exp (gen) x)))
(recv
(cat (exp (gen) y)
(enc na nb a b
(hash (exp (gen) (mul ltxa y)) (exp (gen) (mul ltxb x))
(exp (gen) (mul x y)))))) (send nb))
(uniq-orig na)
(uniq-gen x)
(absent (x ltxa) (x ltxb))
(fn-of ("principal-of" (ltxa a) (ltxb b))
("ltx-of" (a ltxa) (b ltxb)))
(neq ((exp (gen) y) (gen))))
(defrole resp
(vars (ltxa ltxb y rndx) (x expt) (a b name) (na nb data))
(trace (recv (cat (exp (gen) ltxa) (exp (gen) ltxb)))
(recv (cat na a b (exp (gen) x)))
(send
(cat (exp (gen) y)
(enc na nb a b
(hash (exp (gen) (mul ltxa y)) (exp (gen) (mul ltxb x))
(exp (gen) (mul y x)))))) (recv nb))
(uniq-orig nb)
(uniq-gen y)
(absent (y ltxa) (y ltxb) (y x))
(fn-of ("principal-of" (ltxa a) (ltxb b))
("ltx-of" (a ltxa) (b ltxb)))
(neq ((exp (gen) x) (gen))))
(defrole ltx-gen
(vars (self name) (l rndx))
(trace (send (cat self (exp (gen) l))) (recv "end-of-protocol")
(send l))
(uniq-gen l)
(fn-of ("principal-of" (l self)) ("ltx-of" (self l))))
(defgenrule neqRl_indx
(forall ((x indx)) (implies (fact neq x x) (false))))
(defgenrule neqRl_strd
(forall ((x strd)) (implies (fact neq x x) (false))))
(defgenrule neqRl_mesg
(forall ((x mesg)) (implies (fact neq x x) (false)))))
(defskeleton dhcr-um3
(vars (na nb data) (a b self self-0 name) (ltxa ltxb x rndx) (y expt))
(defstrand init 4 (na na) (nb nb) (a a) (b b) (ltxa ltxa) (ltxb ltxb)
(x x) (y y))
(deflistener
(hash (exp (gen) (mul ltxa y)) (exp (gen) (mul ltxb x))
(exp (gen) (mul x y))))
(defstrand ltx-gen 3 (self self) (l ltxa))
(defstrand ltx-gen 3 (self self-0) (l ltxb))
(precedes ((0 3) (2 1)) ((0 3) (3 1)))
(uniq-orig na)
(uniq-gen ltxa ltxb x)
(absent (x ltxa) (x ltxb))
(traces
((recv (cat (exp (gen) ltxa) (exp (gen) ltxb)))
(send (cat na a b (exp (gen) x)))
(recv
(cat (exp (gen) y)
(enc na nb a b
(hash (exp (gen) (mul ltxa y)) (exp (gen) (mul ltxb x))
(exp (gen) (mul x y)))))) (send nb))
((recv
(hash (exp (gen) (mul ltxa y)) (exp (gen) (mul ltxb x))
(exp (gen) (mul x y))))
(send
(hash (exp (gen) (mul ltxa y)) (exp (gen) (mul ltxb x))
(exp (gen) (mul x y)))))
((send (cat self (exp (gen) ltxa))) (recv "end-of-protocol")
(send ltxa))
((send (cat self-0 (exp (gen) ltxb))) (recv "end-of-protocol")
(send ltxb)))
(label 56)
(unrealized (0 0) (0 2) (1 0))
(preskeleton)
(origs (na (0 1)))
(comment "Not a skeleton"))
(comment "Nothing left to do")