cpsa-4.4.4: tst/dhcr_umx_shapes.tst
(comment "CPSA 4.3.1")
(comment "Extracted shapes")
(herald "DHCR: unified model (UM) criss-cross" (bound 20) (limit 8000)
(algebra diffie-hellman))
(comment "CPSA 4.3.1")
(comment "All input read from tst/dhcr_umx.scm")
(comment "Step count limited to 8000")
(comment "Strand count bounded at 20")
(defprotocol dhcr-umx 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))))))
(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))))))
(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-umx
(vars (na nb data) (a b 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 b) (l ltxb))
(precedes ((1 0) (0 0)))
(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))))))
(send nb)) ((send (cat b (exp (gen) ltxb)))))
(label 0)
(unrealized (0 2))
(origs (na (0 1)))
(comment "2 in cohort - 2 not yet seen"))
(defskeleton dhcr-umx
(vars (na nb data) (a b name) (ltxa ltxa-0 y ltxb l rndx))
(defstrand init 4 (na na) (nb nb) (a a) (b b) (ltxa ltxa) (ltxb l)
(x ltxb) (y (mul (rec ltxa) ltxa-0 y)))
(defstrand ltx-gen 1 (self b) (l l))
(defstrand resp 3 (na na) (nb nb) (a a) (b b) (ltxa ltxa-0)
(ltxb ltxb) (y y) (x l))
(precedes ((0 1) (2 0)) ((1 0) (0 0)) ((2 2) (0 2)))
(non-orig l)
(uniq-orig na nb)
(uniq-gen y ltxb l)
(absent (y ltxa-0) (y ltxb) (y l) (ltxb ltxa) (ltxb l))
(operation nonce-test (displaced 3 1 ltx-gen 1) (exp (gen) l) (2 1))
(traces
((recv (cat (exp (gen) ltxa) (exp (gen) l)))
(send (cat na a b (exp (gen) ltxb)))
(recv
(cat (exp (gen) (mul (rec ltxa) ltxa-0 y))
(enc na nb a b
(hash (exp (gen) (mul ltxa-0 y))
(exp (gen) (mul ltxb l)))))) (send nb))
((send (cat b (exp (gen) l))))
((recv (cat (exp (gen) ltxa-0) (exp (gen) ltxb)))
(recv (cat na a b (exp (gen) l)))
(send
(cat (exp (gen) y)
(enc na nb a b
(hash (exp (gen) (mul ltxa-0 y))
(exp (gen) (mul ltxb l))))))))
(label 3)
(parent 0)
(realized)
(shape)
(maps
((0 1)
((ltxa ltxa) (ltxb l) (a a) (b b) (x ltxb)
(y (mul (rec ltxa) ltxa-0 y)) (na na) (nb nb))))
(origs (nb (2 2)) (na (0 1))))
(defskeleton dhcr-umx
(vars (na nb data) (a b name) (ltxa y x ltxa-0 ltxb rndx))
(defstrand init 4 (na na) (nb nb) (a a) (b b) (ltxa ltxa-0)
(ltxb ltxb) (x x) (y (mul ltxa y (rec ltxa-0))))
(defstrand ltx-gen 1 (self b) (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 ltxa) (y x) (y ltxb) (x ltxa-0) (x ltxb))
(operation nonce-test (displaced 3 0 init 2) (exp (gen) x) (2 1))
(traces
((recv (cat (exp (gen) ltxa-0) (exp (gen) ltxb)))
(send (cat na a b (exp (gen) x)))
(recv
(cat (exp (gen) (mul ltxa y (rec ltxa-0)))
(enc na nb a b
(hash (exp (gen) (mul ltxa y)) (exp (gen) (mul x ltxb))))))
(send nb)) ((send (cat b (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 ltxa y))
(exp (gen) (mul x ltxb))))))))
(label 4)
(parent 0)
(realized)
(shape)
(maps
((0 1)
((ltxa ltxa-0) (ltxb ltxb) (a a) (b b) (x x)
(y (mul ltxa y (rec ltxa-0))) (na na) (nb nb))))
(origs (na (0 1)) (nb (2 2))))
(comment "Nothing left to do")
(defprotocol dhcr-umx 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))))))
(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))))))
(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-umx
(vars (na nb data) (a b 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 b) (l ltxb))
(precedes ((1 0) (0 0)))
(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))))))
(send nb)) ((send (cat b (exp (gen) ltxb)))))
(label 10)
(unrealized (0 2))
(origs (na (0 1)))
(comment "2 in cohort - 2 not yet seen"))
(defskeleton dhcr-umx
(vars (na nb data) (a b name) (ltxa ltxa-0 y ltxb l rndx))
(defstrand init 4 (na na) (nb nb) (a a) (b b) (ltxa ltxa) (ltxb l)
(x ltxb) (y (mul (rec ltxa) ltxa-0 y)))
(defstrand ltx-gen 1 (self b) (l l))
(defstrand resp 3 (na na) (nb nb) (a a) (b b) (ltxa ltxa-0)
(ltxb ltxb) (y y) (x l))
(precedes ((0 1) (2 0)) ((1 0) (0 0)) ((2 2) (0 2)))
(non-orig l)
(uniq-orig na nb)
(uniq-gen y ltxb l)
(absent (y ltxa-0) (y ltxb) (y l) (ltxb ltxa) (ltxb l))
(operation nonce-test (displaced 3 1 ltx-gen 1) (exp (gen) l) (2 1))
(traces
((recv (cat (exp (gen) ltxa) (exp (gen) l)))
(send (cat na a b (exp (gen) ltxb)))
(recv
(cat (exp (gen) (mul (rec ltxa) ltxa-0 y))
(enc na nb a b
(hash (exp (gen) (mul ltxa-0 y))
(exp (gen) (mul ltxb l)))))) (send nb))
((send (cat b (exp (gen) l))))
((recv (cat (exp (gen) ltxa-0) (exp (gen) ltxb)))
(recv (cat na a b (exp (gen) l)))
(send
(cat (exp (gen) y)
(enc na nb a b
(hash (exp (gen) (mul ltxa-0 y))
(exp (gen) (mul ltxb l))))))))
(label 13)
(parent 10)
(realized)
(shape)
(maps
((0 1)
((ltxa ltxa) (ltxb l) (a a) (b b) (x ltxb)
(y (mul (rec ltxa) ltxa-0 y)) (na na) (nb nb))))
(origs (nb (2 2)) (na (0 1))))
(defskeleton dhcr-umx
(vars (na nb data) (a b name) (ltxa y x ltxa-0 ltxb rndx))
(defstrand init 4 (na na) (nb nb) (a a) (b b) (ltxa ltxa-0)
(ltxb ltxb) (x x) (y (mul ltxa y (rec ltxa-0))))
(defstrand ltx-gen 1 (self b) (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 ltxa) (y x) (y ltxb) (x ltxa-0) (x ltxb))
(operation nonce-test (displaced 3 0 init 2) (exp (gen) x) (2 1))
(traces
((recv (cat (exp (gen) ltxa-0) (exp (gen) ltxb)))
(send (cat na a b (exp (gen) x)))
(recv
(cat (exp (gen) (mul ltxa y (rec ltxa-0)))
(enc na nb a b
(hash (exp (gen) (mul ltxa y)) (exp (gen) (mul x ltxb))))))
(send nb)) ((send (cat b (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 ltxa y))
(exp (gen) (mul x ltxb))))))))
(label 14)
(parent 10)
(realized)
(shape)
(maps
((0 1)
((ltxa ltxa-0) (ltxb ltxb) (a a) (b b) (x x)
(y (mul ltxa y (rec ltxa-0))) (na na) (nb nb))))
(origs (na (0 1)) (nb (2 2))))
(comment "Nothing left to do")
(defprotocol dhcr-umx 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))))))
(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))))))
(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-umx
(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))))))
(send nb)) ((send (cat self (exp (gen) ltxa))))
((send (cat self-0 (exp (gen) ltxb)))))
(label 20)
(unrealized (0 0) (0 2))
(preskeleton)
(origs (na (0 1)))
(comment "Not a skeleton"))
(defskeleton dhcr-umx
(vars (na nb data) (a b self self-0 name) (y ltxa ltxb l rndx))
(defstrand init 4 (na na) (nb nb) (a a) (b b) (ltxa ltxa) (ltxb l)
(x ltxb) (y y))
(defstrand ltx-gen 1 (self self) (l ltxa))
(defstrand ltx-gen 1 (self self-0) (l l))
(defstrand resp 3 (na na) (nb nb) (a a) (b b) (ltxa ltxa) (ltxb ltxb)
(y y) (x l))
(precedes ((0 1) (3 0)) ((1 0) (0 0)) ((2 0) (0 0)) ((3 2) (0 2)))
(non-orig ltxa l)
(uniq-orig na nb)
(uniq-gen y ltxa ltxb l)
(absent (y ltxa) (y ltxb) (y l) (ltxb ltxa) (ltxb l))
(operation nonce-test (displaced 4 3 resp 3) (exp (gen) y) (0 2))
(traces
((recv (cat (exp (gen) ltxa) (exp (gen) l)))
(send (cat na a b (exp (gen) ltxb)))
(recv
(cat (exp (gen) y)
(enc na nb a b
(hash (exp (gen) (mul y ltxa)) (exp (gen) (mul ltxb l))))))
(send nb)) ((send (cat self (exp (gen) ltxa))))
((send (cat self-0 (exp (gen) l))))
((recv (cat (exp (gen) ltxa) (exp (gen) ltxb)))
(recv (cat na a b (exp (gen) l)))
(send
(cat (exp (gen) y)
(enc na nb a b
(hash (exp (gen) (mul y ltxa))
(exp (gen) (mul ltxb l))))))))
(label 37)
(parent 20)
(realized)
(shape)
(maps
((0 1 2)
((ltxa ltxa) (ltxb l) (a a) (b b) (x ltxb) (y y) (na na) (nb nb)
(self self) (self-0 self-0))))
(origs (nb (3 2)) (na (0 1))))
(defskeleton dhcr-umx
(vars (na nb data) (a b self self-0 name) (y ltxa ltxb x 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 ltxa ltxb x)
(absent (y ltxa) (y ltxb) (y x) (x ltxa) (x ltxb))
(operation nonce-test (displaced 4 3 resp 3) (exp (gen) y) (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 ltxb 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 ltxb x))))))))
(label 40)
(parent 20)
(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-umx
(vars (na nb data) (a b self name) (y ltxb l rndx))
(defstrand init 4 (na na) (nb nb) (a a) (b b) (ltxa l) (ltxb l)
(x ltxb) (y y))
(defstrand ltx-gen 1 (self self) (l l))
(defstrand resp 3 (na na) (nb nb) (a a) (b b) (ltxa l) (ltxb ltxb)
(y y) (x l))
(precedes ((0 1) (2 0)) ((1 0) (0 0)) ((2 2) (0 2)))
(non-orig l)
(uniq-orig na nb)
(uniq-gen y ltxb l)
(absent (y ltxb) (y l) (ltxb l))
(operation nonce-test (displaced 3 2 resp 3) (exp (gen) y) (0 2))
(traces
((recv (cat (exp (gen) l) (exp (gen) l)))
(send (cat na a b (exp (gen) ltxb)))
(recv
(cat (exp (gen) y)
(enc na nb a b
(hash (exp (gen) (mul y l)) (exp (gen) (mul ltxb l))))))
(send nb)) ((send (cat self (exp (gen) l))))
((recv (cat (exp (gen) l) (exp (gen) ltxb)))
(recv (cat na a b (exp (gen) l)))
(send
(cat (exp (gen) y)
(enc na nb a b
(hash (exp (gen) (mul y l)) (exp (gen) (mul ltxb l))))))))
(label 45)
(parent 20)
(realized)
(shape)
(maps
((0 1 1)
((ltxa l) (ltxb l) (a a) (b b) (x ltxb) (y y) (na na) (nb nb)
(self self) (self-0 self))))
(origs (nb (2 2)) (na (0 1))))
(defskeleton dhcr-umx
(vars (na nb data) (a b self name) (y ltxb x 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 ltxb x)
(absent (y ltxb) (y x) (x ltxb))
(operation nonce-test (displaced 3 2 resp 3) (exp (gen) y) (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 ltxb 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 ltxb x))))))))
(label 48)
(parent 20)
(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-umx 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))))))
(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))))))
(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-umx
(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))))))
(recv nb)) ((send (cat self (exp (gen) ltxa))))
((send (cat self-0 (exp (gen) ltxb)))))
(label 57)
(unrealized (0 0) (0 3))
(preskeleton)
(origs (nb (0 2)))
(comment "Not a skeleton"))
(defskeleton dhcr-umx
(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 (displaced 4 3 init 2) (exp (gen) x) (0 1))
(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))))))
(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))))))
(send nb)))
(label 72)
(parent 57)
(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-umx
(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 (displaced 3 2 init 2) (exp (gen) x) (0 1))
(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))))))
(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))))))
(send nb)))
(label 77)
(parent 57)
(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-umx 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))))))
(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))))))
(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-umx
(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))))))
(recv nb)) ((send (cat self (exp (gen) ltxa)))))
(label 84)
(unrealized (0 0) (0 3))
(preskeleton)
(origs (nb (0 2)))
(comment "Not a skeleton"))
(defskeleton dhcr-umx
(vars (na nb data) (a b self name) (y ltxa ltxb x ltxb-0 rndx))
(defstrand resp 4 (na na) (nb nb) (a a) (b b) (ltxa ltxa)
(ltxb ltxb-0) (y y) (x (mul ltxb x (rec ltxb-0))))
(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 ltxa x)
(absent (y ltxa) (y (mul ltxb x (rec ltxb-0))) (y ltxb-0) (x ltxa)
(x ltxb))
(operation nonce-test (displaced 3 0 resp 3) (exp (gen) y) (2 2))
(traces
((recv (cat (exp (gen) ltxa) (exp (gen) ltxb-0)))
(recv (cat na a b (exp (gen) (mul ltxb x (rec ltxb-0)))))
(send
(cat (exp (gen) y)
(enc na nb a b
(hash (exp (gen) (mul y ltxa)) (exp (gen) (mul ltxb 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 ltxb x))))))
(send nb)))
(label 88)
(parent 84)
(realized)
(shape)
(maps
((0 1)
((ltxa ltxa) (ltxb ltxb-0) (a a) (b b) (y y)
(x (mul ltxb x (rec ltxb-0))) (na na) (nb nb) (self self))))
(origs (nb (0 2)) (na (2 1))))
(comment "Nothing left to do")
(defprotocol dhcr-umx 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))))))
(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))))))
(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-umx
(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))))))
(recv nb)) ((send (cat self (exp (gen) ltxa)))))
(label 94)
(unrealized (0 0) (0 3))
(preskeleton)
(origs (nb (0 2)))
(comment "Not a skeleton"))
(defskeleton dhcr-umx
(vars (na nb data) (a b self name) (y ltxa ltxb x ltxb-0 rndx))
(defstrand resp 4 (na na) (nb nb) (a a) (b b) (ltxa ltxa)
(ltxb ltxb-0) (y y) (x (mul ltxb x (rec ltxb-0))))
(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 ltxa x)
(absent (y ltxa) (y (mul ltxb x (rec ltxb-0))) (y ltxb-0) (x ltxa)
(x ltxb))
(operation nonce-test (displaced 3 0 resp 3) (exp (gen) y) (2 2))
(traces
((recv (cat (exp (gen) ltxa) (exp (gen) ltxb-0)))
(recv (cat na a b (exp (gen) (mul ltxb x (rec ltxb-0)))))
(send
(cat (exp (gen) y)
(enc na nb a b
(hash (exp (gen) (mul y ltxa)) (exp (gen) (mul ltxb 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 ltxb x))))))
(send nb)))
(label 98)
(parent 94)
(realized)
(shape)
(maps
((0 1)
((ltxa ltxa) (ltxb ltxb-0) (a a) (b b) (y y)
(x (mul ltxb x (rec ltxb-0))) (na na) (nb nb) (self self))))
(origs (nb (0 2)) (na (2 1))))
(comment "Nothing left to do")
(defprotocol dhcr-umx 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))))))
(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))))))
(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-umx
(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))))
(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))))))
(send nb))
((recv (hash (exp (gen) (mul ltxa y)) (exp (gen) (mul ltxb x))))
(send (hash (exp (gen) (mul ltxa y)) (exp (gen) (mul ltxb x)))))
((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 104)
(unrealized (0 0) (0 2) (1 0))
(preskeleton)
(origs (na (0 1)))
(comment "Not a skeleton"))
(defskeleton dhcr-umx
(vars (na nb data) (a b self name) (y ltxb l rndx))
(defstrand init 4 (na na) (nb nb) (a a) (b b) (ltxa l) (ltxb l)
(x ltxb) (y y))
(deflistener (hash (exp (gen) (mul y l)) (exp (gen) (mul ltxb l))))
(defstrand ltx-gen 3 (self self) (l l))
(defstrand resp 3 (na na) (nb nb) (a a) (b b) (ltxa l) (ltxb ltxb)
(y y) (x l))
(precedes ((0 1) (3 0)) ((0 3) (2 1)) ((2 0) (0 0)) ((2 2) (1 0))
((3 2) (0 2)))
(uniq-orig na nb)
(uniq-gen y ltxb l)
(absent (y ltxb) (y l) (ltxb l))
(operation generalization deleted (3 0))
(traces
((recv (cat (exp (gen) l) (exp (gen) l)))
(send (cat na a b (exp (gen) ltxb)))
(recv
(cat (exp (gen) y)
(enc na nb a b
(hash (exp (gen) (mul y l)) (exp (gen) (mul ltxb l))))))
(send nb))
((recv (hash (exp (gen) (mul y l)) (exp (gen) (mul ltxb l))))
(send (hash (exp (gen) (mul y l)) (exp (gen) (mul ltxb l)))))
((send (cat self (exp (gen) l))) (recv "end-of-protocol") (send l))
((recv (cat (exp (gen) l) (exp (gen) ltxb)))
(recv (cat na a b (exp (gen) l)))
(send
(cat (exp (gen) y)
(enc na nb a b
(hash (exp (gen) (mul y l)) (exp (gen) (mul ltxb l))))))))
(label 171)
(parent 104)
(realized)
(shape)
(maps
((0 1 2 2)
((ltxa l) (ltxb l) (x ltxb) (y y) (a a) (b b) (na na) (nb nb)
(self self) (self-0 self))))
(origs (nb (3 2)) (na (0 1))))
(defskeleton dhcr-umx
(vars (na nb data) (a b self name) (y l x rndx))
(defstrand init 4 (na na) (nb nb) (a a) (b b) (ltxa l) (ltxb l) (x x)
(y y))
(deflistener (hash (exp (gen) (mul y l)) (exp (gen) (mul l x))))
(defstrand ltx-gen 3 (self self) (l l))
(defstrand resp 3 (na na) (nb nb) (a a) (b b) (ltxa l) (ltxb l) (y y)
(x x))
(precedes ((0 1) (3 1)) ((0 3) (2 1)) ((2 0) (0 0)) ((2 0) (3 0))
((2 2) (1 0)) ((3 2) (0 2)))
(uniq-orig na nb)
(uniq-gen y l x)
(absent (y l) (y x) (x l))
(operation generalization deleted (3 0))
(traces
((recv (cat (exp (gen) l) (exp (gen) l)))
(send (cat na a b (exp (gen) x)))
(recv
(cat (exp (gen) y)
(enc na nb a b
(hash (exp (gen) (mul y l)) (exp (gen) (mul l x))))))
(send nb))
((recv (hash (exp (gen) (mul y l)) (exp (gen) (mul l x))))
(send (hash (exp (gen) (mul y l)) (exp (gen) (mul l x)))))
((send (cat self (exp (gen) l))) (recv "end-of-protocol") (send l))
((recv (cat (exp (gen) l) (exp (gen) l)))
(recv (cat na a b (exp (gen) x)))
(send
(cat (exp (gen) y)
(enc na nb a b
(hash (exp (gen) (mul y l)) (exp (gen) (mul l x))))))))
(label 172)
(parent 104)
(realized)
(shape)
(maps
((0 1 2 2)
((ltxa l) (ltxb l) (x x) (y y) (a a) (b b) (na na) (nb nb)
(self self) (self-0 self))))
(origs (nb (3 2)) (na (0 1))))
(defskeleton dhcr-umx
(vars (na nb data) (a b self self-0 name) (y ltxb l l-0 rndx))
(defstrand init 4 (na na) (nb nb) (a a) (b b) (ltxa l-0) (ltxb l)
(x ltxb) (y y))
(deflistener (hash (exp (gen) (mul y l-0)) (exp (gen) (mul ltxb l))))
(defstrand ltx-gen 3 (self self) (l l-0))
(defstrand ltx-gen 3 (self self-0) (l l))
(defstrand resp 3 (na na) (nb nb) (a a) (b b) (ltxa l-0) (ltxb ltxb)
(y y) (x l))
(precedes ((0 1) (4 0)) ((0 3) (2 1)) ((0 3) (3 1)) ((2 0) (0 0))
((2 2) (1 0)) ((3 0) (0 0)) ((3 2) (1 0)) ((4 2) (0 2)))
(uniq-orig na nb)
(uniq-gen y ltxb l l-0)
(absent (y ltxb) (y l) (y l-0) (ltxb l) (ltxb l-0))
(operation generalization deleted (5 0))
(traces
((recv (cat (exp (gen) l-0) (exp (gen) l)))
(send (cat na a b (exp (gen) ltxb)))
(recv
(cat (exp (gen) y)
(enc na nb a b
(hash (exp (gen) (mul y l-0)) (exp (gen) (mul ltxb l))))))
(send nb))
((recv (hash (exp (gen) (mul y l-0)) (exp (gen) (mul ltxb l))))
(send (hash (exp (gen) (mul y l-0)) (exp (gen) (mul ltxb l)))))
((send (cat self (exp (gen) l-0))) (recv "end-of-protocol")
(send l-0))
((send (cat self-0 (exp (gen) l))) (recv "end-of-protocol")
(send l))
((recv (cat (exp (gen) l-0) (exp (gen) ltxb)))
(recv (cat na a b (exp (gen) l)))
(send
(cat (exp (gen) y)
(enc na nb a b
(hash (exp (gen) (mul y l-0)) (exp (gen) (mul ltxb l))))))))
(label 177)
(parent 104)
(realized)
(shape)
(maps
((0 1 2 3)
((ltxa l-0) (ltxb l) (x ltxb) (y y) (a a) (b b) (na na) (nb nb)
(self self) (self-0 self-0))))
(origs (nb (4 2)) (na (0 1))))
(defskeleton dhcr-umx
(vars (na nb data) (a b self self-0 name) (y ltxb x l rndx))
(defstrand init 4 (na na) (nb nb) (a a) (b b) (ltxa l) (ltxb ltxb)
(x x) (y y))
(deflistener (hash (exp (gen) (mul y l)) (exp (gen) (mul ltxb x))))
(defstrand ltx-gen 3 (self self) (l l))
(defstrand ltx-gen 3 (self self-0) (l ltxb))
(defstrand resp 3 (na na) (nb nb) (a a) (b b) (ltxa l) (ltxb ltxb)
(y y) (x x))
(precedes ((0 1) (4 1)) ((0 3) (2 1)) ((0 3) (3 1)) ((2 0) (0 0))
((2 0) (4 0)) ((2 2) (1 0)) ((3 0) (0 0)) ((3 0) (4 0))
((3 2) (1 0)) ((4 2) (0 2)))
(uniq-orig na nb)
(uniq-gen y ltxb x l)
(absent (y ltxb) (y x) (y l) (x ltxb) (x l))
(operation generalization deleted (5 0))
(traces
((recv (cat (exp (gen) l) (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 l)) (exp (gen) (mul ltxb x))))))
(send nb))
((recv (hash (exp (gen) (mul y l)) (exp (gen) (mul ltxb x))))
(send (hash (exp (gen) (mul y l)) (exp (gen) (mul ltxb x)))))
((send (cat self (exp (gen) l))) (recv "end-of-protocol") (send l))
((send (cat self-0 (exp (gen) ltxb))) (recv "end-of-protocol")
(send ltxb))
((recv (cat (exp (gen) l) (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 l)) (exp (gen) (mul ltxb x))))))))
(label 178)
(parent 104)
(realized)
(shape)
(maps
((0 1 2 3)
((ltxa l) (ltxb ltxb) (x x) (y y) (a a) (b b) (na na) (nb nb)
(self self) (self-0 self-0))))
(origs (nb (4 2)) (na (0 1))))
(comment "Nothing left to do")