cpsa-4.4.1: tst/dh_group_sig.scm

(herald "Signed group DH exchange (improved version)" (algebra diffie-hellman)
	(limit 100)
	;(limit 20000) (bound 25)
	)

;;; This is not a very convincing protocol in my mind.  -- JDG

(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 a  (exp g y) (exp g x) (privk b)))
     (send (enc "final" b (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 a (exp g y) (exp g x) (privk b)))
     (recv (enc "final" b (exp g y) (exp g x) (privk a))))
    (uniq-gen y)
    (auth group-dist))
)

(defskeleton dh_sig
  (vars (a b name))
  (defstrand init 4 (a a) (b b))
  (non-orig (privk b) (privk a))
)

(defskeleton dh_sig
  (vars (a b name))
  (defstrand resp 4 (a a) (b b))
  (non-orig (privk a) (privk b))
)

(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 a (exp g y) (exp g x) (privk b)))
     (send (enc n b (exp g (mul x y))))
     (recv n))
    (uniq-gen x n)
    (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 a (exp g y) (exp g x) (privk b)))
     (recv (enc n b (exp g (mul x y))))
     (send n))
    (uniq-gen y)
    (auth group-dist))
)

(defskeleton dh_sig2
  (vars (a b name))
  (defstrand init 5 (a a) (b b))
  (non-orig (privk b) (privk a))
)

(defskeleton dh_sig2
  (vars (a b name))
  (defstrand resp 5 (a a) (b b))
  (non-orig (privk a) (privk b))
)