cpsa-4.4.4: tst/dh_group_sig_auth_failure_shapes.tst
(comment "CPSA 4.3.1")
(comment "Extracted shapes")
(herald "Signed group DH exchange (version with auth failure)"
(algebra diffie-hellman) (limit 100))
(comment "CPSA 4.3.1")
(comment "All input read from tst/dh_group_sig_auth_failure.scm")
(comment "Step count limited to 100")
(defprotocol dh_sig diffie-hellman
(defrole group-init
(vars (alpha rndx) (group text) (group-dist chan))
(trace (send group-dist (cat "Group id" group (exp (gen) alpha))))
(uniq-gen alpha)
(conf group-dist))
(defrole init
(vars (x rndx) (y expt) (g base) (group text) (a b name)
(group-dist chan))
(trace (recv group-dist (cat "Group id" group g))
(send (enc (exp g x) (privk a)))
(recv (enc (exp g y) (exp g x) (privk b)))
(send (enc "final" (exp g y) (exp g x) (privk a))))
(uniq-gen x)
(auth group-dist))
(defrole resp
(vars (y rndx) (x expt) (g base) (group text) (a b name)
(group-dist chan))
(trace (recv group-dist (cat "Group id" group g))
(recv (enc (exp g x) (privk a)))
(send (enc (exp g y) (exp g x) (privk b)))
(recv (enc "final" (exp g y) (exp g x) (privk a))))
(uniq-gen y)
(absent (y x))
(auth group-dist))
(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 dh_sig
(vars (group text) (a b name) (g base) (group-dist chan) (x rndx)
(y expt))
(defstrand init 4 (group group) (a a) (b b) (g g)
(group-dist group-dist) (x x) (y y))
(non-orig (privk a) (privk b))
(uniq-gen x)
(auth group-dist)
(traces
((recv group-dist (cat "Group id" group g))
(send (enc (exp g x) (privk a)))
(recv (enc (exp g y) (exp g x) (privk b)))
(send (enc "final" (exp g y) (exp g x) (privk a)))))
(label 0)
(unrealized (0 0) (0 2))
(origs)
(comment "1 in cohort - 1 not yet seen"))
(defskeleton dh_sig
(vars (group text) (a b a-0 name) (group-dist chan) (y x alpha rndx))
(defstrand init 4 (group group) (a a) (b b) (g (exp (gen) alpha))
(group-dist group-dist) (x x) (y y))
(defstrand group-init 1 (group group) (group-dist group-dist)
(alpha alpha))
(defstrand resp 3 (group group) (a a-0) (b b) (g (exp (gen) alpha))
(group-dist group-dist) (y y) (x x))
(precedes ((0 1) (2 1)) ((1 0) (0 0)) ((1 0) (2 0)) ((2 2) (0 2)))
(non-orig (privk a) (privk b))
(uniq-gen y x alpha)
(absent (y x))
(conf group-dist)
(auth group-dist)
(operation generalization weakened ((0 1) (2 0)))
(traces
((recv group-dist (cat "Group id" group (exp (gen) alpha)))
(send (enc (exp (gen) (mul x alpha)) (privk a)))
(recv
(enc (exp (gen) (mul y alpha)) (exp (gen) (mul x alpha))
(privk b)))
(send
(enc "final" (exp (gen) (mul y alpha)) (exp (gen) (mul x alpha))
(privk a))))
((send group-dist (cat "Group id" group (exp (gen) alpha))))
((recv group-dist (cat "Group id" group (exp (gen) alpha)))
(recv (enc (exp (gen) (mul x alpha)) (privk a-0)))
(send
(enc (exp (gen) (mul y alpha)) (exp (gen) (mul x alpha))
(privk b)))))
(label 5)
(parent 0)
(realized)
(shape)
(maps
((0)
((a a) (b b) (x x) (y y) (g (exp (gen) alpha)) (group group)
(group-dist group-dist))))
(origs))
(defskeleton dh_sig
(vars (group group-0 text) (a b a-0 name)
(group-dist group-dist-0 chan) (y alpha x alpha-0 rndx))
(defstrand init 4 (group group) (a a) (b b) (g (exp (gen) alpha))
(group-dist group-dist) (x x) (y (mul y (rec alpha) alpha-0)))
(defstrand group-init 1 (group group) (group-dist group-dist)
(alpha alpha))
(defstrand resp 3 (group group-0) (a a-0) (b b)
(g (exp (gen) alpha-0)) (group-dist group-dist-0) (y y)
(x (mul alpha x (rec alpha-0))))
(defstrand group-init 1 (group group-0) (group-dist group-dist-0)
(alpha alpha-0))
(precedes ((0 1) (2 1)) ((1 0) (0 0)) ((2 2) (0 2)) ((3 0) (2 0)))
(non-orig (privk a) (privk b))
(uniq-gen y alpha x alpha-0)
(absent (y (mul alpha x (rec alpha-0))))
(conf group-dist group-dist-0)
(auth group-dist group-dist-0)
(operation generalization weakened ((1 0) (2 0)))
(traces
((recv group-dist (cat "Group id" group (exp (gen) alpha)))
(send (enc (exp (gen) (mul alpha x)) (privk a)))
(recv
(enc (exp (gen) (mul y alpha-0)) (exp (gen) (mul alpha x))
(privk b)))
(send
(enc "final" (exp (gen) (mul y alpha-0))
(exp (gen) (mul alpha x)) (privk a))))
((send group-dist (cat "Group id" group (exp (gen) alpha))))
((recv group-dist-0 (cat "Group id" group-0 (exp (gen) alpha-0)))
(recv (enc (exp (gen) (mul alpha x)) (privk a-0)))
(send
(enc (exp (gen) (mul y alpha-0)) (exp (gen) (mul alpha x))
(privk b))))
((send group-dist-0 (cat "Group id" group-0 (exp (gen) alpha-0)))))
(label 7)
(parent 0)
(realized)
(shape)
(maps
((0)
((a a) (b b) (x x) (y (mul y (rec alpha) alpha-0))
(g (exp (gen) alpha)) (group group) (group-dist group-dist))))
(origs))
(comment "Nothing left to do")
(defprotocol dh_sig diffie-hellman
(defrole group-init
(vars (alpha rndx) (group text) (group-dist chan))
(trace (send group-dist (cat "Group id" group (exp (gen) alpha))))
(uniq-gen alpha)
(conf group-dist))
(defrole init
(vars (x rndx) (y expt) (g base) (group text) (a b name)
(group-dist chan))
(trace (recv group-dist (cat "Group id" group g))
(send (enc (exp g x) (privk a)))
(recv (enc (exp g y) (exp g x) (privk b)))
(send (enc "final" (exp g y) (exp g x) (privk a))))
(uniq-gen x)
(auth group-dist))
(defrole resp
(vars (y rndx) (x expt) (g base) (group text) (a b name)
(group-dist chan))
(trace (recv group-dist (cat "Group id" group g))
(recv (enc (exp g x) (privk a)))
(send (enc (exp g y) (exp g x) (privk b)))
(recv (enc "final" (exp g y) (exp g x) (privk a))))
(uniq-gen y)
(absent (y x))
(auth group-dist))
(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 dh_sig
(vars (group text) (a b name) (g base) (group-dist chan) (y rndx)
(x expt))
(defstrand resp 4 (group group) (a a) (b b) (g g)
(group-dist group-dist) (y y) (x x))
(non-orig (privk a) (privk b))
(uniq-gen y)
(absent (y x))
(auth group-dist)
(traces
((recv group-dist (cat "Group id" group g))
(recv (enc (exp g x) (privk a)))
(send (enc (exp g y) (exp g x) (privk b)))
(recv (enc "final" (exp g y) (exp g x) (privk a)))))
(label 8)
(unrealized (0 0) (0 1) (0 3))
(origs)
(comment "1 in cohort - 1 not yet seen"))
(defskeleton dh_sig
(vars (group text) (a b b-0 name) (group-dist chan) (alpha y x rndx))
(defstrand resp 4 (group group) (a a) (b b) (g (exp (gen) alpha))
(group-dist group-dist) (y y) (x x))
(defstrand group-init 1 (group group) (group-dist group-dist)
(alpha alpha))
(defstrand init 4 (group group) (a a) (b b-0) (g (exp (gen) alpha))
(group-dist group-dist) (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 (privk a) (privk b))
(uniq-gen alpha y x)
(absent (y x))
(conf group-dist)
(auth group-dist)
(operation encryption-test (displaced 2 3 init 4)
(enc "final" (exp (gen) (mul alpha y)) (exp (gen) (mul alpha x-0))
(privk a)) (0 3))
(traces
((recv group-dist (cat "Group id" group (exp (gen) alpha)))
(recv (enc (exp (gen) (mul alpha x)) (privk a)))
(send
(enc (exp (gen) (mul alpha y)) (exp (gen) (mul alpha x))
(privk b)))
(recv
(enc "final" (exp (gen) (mul alpha y)) (exp (gen) (mul alpha x))
(privk a))))
((send group-dist (cat "Group id" group (exp (gen) alpha))))
((recv group-dist (cat "Group id" group (exp (gen) alpha)))
(send (enc (exp (gen) (mul alpha x)) (privk a)))
(recv
(enc (exp (gen) (mul alpha y)) (exp (gen) (mul alpha x))
(privk b-0)))
(send
(enc "final" (exp (gen) (mul alpha y)) (exp (gen) (mul alpha x))
(privk a)))))
(label 13)
(parent 8)
(realized)
(shape)
(maps
((0)
((a a) (b b) (y y) (x x) (g (exp (gen) alpha)) (group group)
(group-dist group-dist))))
(origs))
(defskeleton dh_sig
(vars (group group-0 text) (a b b-0 name)
(group-dist group-dist-0 chan) (y alpha alpha-0 x rndx))
(defstrand resp 4 (group group) (a a) (b b) (g (exp (gen) alpha))
(group-dist group-dist) (y y) (x (mul (rec alpha) alpha-0 x)))
(defstrand group-init 1 (group group) (group-dist group-dist)
(alpha alpha))
(defstrand group-init 1 (group group-0) (group-dist group-dist-0)
(alpha alpha-0))
(defstrand init 4 (group group-0) (a a) (b b-0)
(g (exp (gen) alpha-0)) (group-dist group-dist-0) (x x)
(y (mul y alpha (rec alpha-0))))
(precedes ((0 2) (3 2)) ((1 0) (0 0)) ((2 0) (3 0)) ((3 1) (0 1))
((3 3) (0 3)))
(non-orig (privk a) (privk b))
(uniq-gen y alpha alpha-0 x)
(absent (y (mul (rec alpha) alpha-0 x)))
(conf group-dist group-dist-0)
(auth group-dist group-dist-0)
(operation generalization weakened ((1 0) (3 0)))
(traces
((recv group-dist (cat "Group id" group (exp (gen) alpha)))
(recv (enc (exp (gen) (mul alpha-0 x)) (privk a)))
(send
(enc (exp (gen) (mul y alpha)) (exp (gen) (mul alpha-0 x))
(privk b)))
(recv
(enc "final" (exp (gen) (mul y alpha))
(exp (gen) (mul alpha-0 x)) (privk a))))
((send group-dist (cat "Group id" group (exp (gen) alpha))))
((send group-dist-0 (cat "Group id" group-0 (exp (gen) alpha-0))))
((recv group-dist-0 (cat "Group id" group-0 (exp (gen) alpha-0)))
(send (enc (exp (gen) (mul alpha-0 x)) (privk a)))
(recv
(enc (exp (gen) (mul y alpha)) (exp (gen) (mul alpha-0 x))
(privk b-0)))
(send
(enc "final" (exp (gen) (mul y alpha))
(exp (gen) (mul alpha-0 x)) (privk a)))))
(label 17)
(parent 8)
(realized)
(shape)
(maps
((0)
((a a) (b b) (y y) (x (mul (rec alpha) alpha-0 x))
(g (exp (gen) alpha)) (group group) (group-dist group-dist))))
(origs))
(comment "Nothing left to do")
(defprotocol dh_sig2 diffie-hellman
(defrole group-init
(vars (alpha rndx) (group text) (group-dist chan))
(trace (send group-dist (cat "Group id" group (exp (gen) alpha))))
(uniq-gen alpha)
(conf group-dist))
(defrole init
(vars (x rndx) (y expt) (g base) (n group text) (a b name)
(group-dist chan))
(trace (recv group-dist (cat "Group id" group g))
(send (enc (exp g x) (privk a)))
(recv (enc (exp g y) (exp g x) (privk b)))
(send (enc n (exp g (mul x y)))) (recv n))
(uniq-gen n x)
(auth group-dist))
(defrole resp
(vars (y rndx) (x expt) (g base) (n group text) (a b name)
(group-dist chan))
(trace (recv group-dist (cat "Group id" group g))
(recv (enc (exp g x) (privk a)))
(send (enc (exp g y) (exp g x) (privk b)))
(recv (enc n (exp g (mul y x)))) (send n))
(uniq-gen y)
(absent (y x))
(auth group-dist))
(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 dh_sig2
(vars (n group text) (a b name) (g base) (group-dist chan) (x rndx)
(y expt))
(defstrand init 5 (n n) (group group) (a a) (b b) (g g)
(group-dist group-dist) (x x) (y y))
(non-orig (privk a) (privk b))
(uniq-gen n x)
(auth group-dist)
(traces
((recv group-dist (cat "Group id" group g))
(send (enc (exp g x) (privk a)))
(recv (enc (exp g y) (exp g x) (privk b)))
(send (enc n (exp g (mul x y)))) (recv n)))
(label 18)
(unrealized (0 0) (0 2))
(origs)
(comment "1 in cohort - 1 not yet seen"))
(defskeleton dh_sig2
(vars (n group text) (a a-0 b name) (group-dist chan)
(alpha x y rndx))
(defstrand init 5 (n n) (group group) (a a) (b b)
(g (exp (gen) alpha)) (group-dist group-dist) (x x) (y y))
(defstrand group-init 1 (group group) (group-dist group-dist)
(alpha alpha))
(defstrand resp 5 (n n) (group group) (a a-0) (b b)
(g (exp (gen) alpha)) (group-dist group-dist) (y y) (x x))
(precedes ((0 1) (2 1)) ((0 3) (2 3)) ((1 0) (0 0)) ((1 0) (2 0))
((2 2) (0 2)) ((2 4) (0 4)))
(non-orig (privk a) (privk b))
(uniq-gen n alpha x y)
(absent (y x))
(conf group-dist)
(auth group-dist)
(operation generalization weakened ((0 1) (2 0)))
(traces
((recv group-dist (cat "Group id" group (exp (gen) alpha)))
(send (enc (exp (gen) (mul alpha x)) (privk a)))
(recv
(enc (exp (gen) (mul alpha y)) (exp (gen) (mul alpha x))
(privk b))) (send (enc n (exp (gen) (mul alpha x y))))
(recv n))
((send group-dist (cat "Group id" group (exp (gen) alpha))))
((recv group-dist (cat "Group id" group (exp (gen) alpha)))
(recv (enc (exp (gen) (mul alpha x)) (privk a-0)))
(send
(enc (exp (gen) (mul alpha y)) (exp (gen) (mul alpha x))
(privk b))) (recv (enc n (exp (gen) (mul alpha x y))))
(send n)))
(label 28)
(parent 18)
(realized)
(shape)
(maps
((0)
((a a) (b b) (x x) (y y) (g (exp (gen) alpha)) (n n) (group group)
(group-dist group-dist))))
(origs))
(comment "Nothing left to do")
(defprotocol dh_sig2 diffie-hellman
(defrole group-init
(vars (alpha rndx) (group text) (group-dist chan))
(trace (send group-dist (cat "Group id" group (exp (gen) alpha))))
(uniq-gen alpha)
(conf group-dist))
(defrole init
(vars (x rndx) (y expt) (g base) (n group text) (a b name)
(group-dist chan))
(trace (recv group-dist (cat "Group id" group g))
(send (enc (exp g x) (privk a)))
(recv (enc (exp g y) (exp g x) (privk b)))
(send (enc n (exp g (mul x y)))) (recv n))
(uniq-gen n x)
(auth group-dist))
(defrole resp
(vars (y rndx) (x expt) (g base) (n group text) (a b name)
(group-dist chan))
(trace (recv group-dist (cat "Group id" group g))
(recv (enc (exp g x) (privk a)))
(send (enc (exp g y) (exp g x) (privk b)))
(recv (enc n (exp g (mul y x)))) (send n))
(uniq-gen y)
(absent (y x))
(auth group-dist))
(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 dh_sig2
(vars (n group text) (a b name) (g base) (group-dist chan) (y rndx)
(x expt))
(defstrand resp 5 (n n) (group group) (a a) (b b) (g g)
(group-dist group-dist) (y y) (x x))
(non-orig (privk a) (privk b))
(uniq-gen y)
(absent (y x))
(auth group-dist)
(traces
((recv group-dist (cat "Group id" group g))
(recv (enc (exp g x) (privk a)))
(send (enc (exp g y) (exp g x) (privk b)))
(recv (enc n (exp g (mul y x)))) (send n)))
(label 39)
(unrealized (0 0) (0 1))
(origs)
(comment "1 in cohort - 1 not yet seen"))
(defskeleton dh_sig2
(vars (n group text) (b a b-0 name) (group-dist chan)
(alpha y x rndx))
(defstrand resp 5 (n n) (group group) (a a) (b b)
(g (exp (gen) alpha)) (group-dist group-dist) (y y) (x x))
(defstrand group-init 1 (group group) (group-dist group-dist)
(alpha alpha))
(defstrand init 4 (n n) (group group) (a a) (b b-0)
(g (exp (gen) alpha)) (group-dist group-dist) (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 (privk b) (privk a))
(uniq-gen n alpha y x)
(absent (y x))
(conf group-dist)
(auth group-dist)
(operation encryption-test (displaced 2 3 init 4)
(enc n (exp (gen) (mul y-0 x-0 alpha))) (0 3))
(traces
((recv group-dist (cat "Group id" group (exp (gen) alpha)))
(recv (enc (exp (gen) (mul alpha x)) (privk a)))
(send
(enc (exp (gen) (mul alpha y)) (exp (gen) (mul alpha x))
(privk b))) (recv (enc n (exp (gen) (mul alpha y x))))
(send n))
((send group-dist (cat "Group id" group (exp (gen) alpha))))
((recv group-dist (cat "Group id" group (exp (gen) alpha)))
(send (enc (exp (gen) (mul alpha x)) (privk a)))
(recv
(enc (exp (gen) (mul alpha y)) (exp (gen) (mul alpha x))
(privk b-0))) (send (enc n (exp (gen) (mul alpha y x))))))
(label 44)
(parent 39)
(realized)
(shape)
(maps
((0)
((a a) (b b) (y y) (x x) (g (exp (gen) alpha)) (n n) (group group)
(group-dist group-dist))))
(origs))
(comment "Nothing left to do")