cpsa-4.4.4: tst/dhcr_um_implicit_auth.scm

;;; Unified Model  This version used in the paper, tooldev/dh/conf_dh/dh_ebn.tex

;;; This file models the "Unified Model" method of determining a fresh
;;; key from long-term and ephemeral Diffie-Hellman exponents.  We use
;;; self-signed certificates to link names to long-term public values.

;;; This file contains the standard version, in which the two
;;; ephemeral are mixed, as are the two static exponents.

;;; A role is provided to expose the long term exponent.  The latter
;;; step is used to test the notion of forward security, assuming that
;;; it happens *after* the session which agrees the key in question.  

;;; This file considers a single goal statement.  It asserts the
;;; implicit authentication claim, namely that if *anyone* shares a
;;; key with me, then that party and I agree on each others'
;;; identities and long term values.  This assumes that the values
;;; remain undisclosed.

;;; CPSA4 revisions:
;;;
;;; 1.  Self certify my public value in ltx-gen,
;;;     and assume signing keys non.
;;; 2.  Deposit private value in state and retrieve
;;;	it at the beginning of each init or resp run.
;;; 3.  Discard the private value from state before
;;;	disclosing it, when testing forward secrecy.

(herald "DHCR: unified model (UM) original"
	(bound 30)
	(limit 4000)
	(goals-sat)
	(algebra diffie-hellman))

(defmacro (kcfa l gb x gy)
  (hash (exp gb l) (exp gy x)))

(defmacro (kcfb l ga y gx)
  (hash (exp ga l) (exp gx y)))

(defprotocol dhcr-um diffie-hellman
  (defrole init
    (vars (l x rndx) (beta eta expt) (a b name) (na nb data) (priv-stor locn))
    (trace
     (load priv-stor (pv a l))
     (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) eta)
		(enc na nb a b
		     (kcfa l (exp (gen) beta)
			   x (exp (gen) eta)))))
     (send nb)
     )
    (uniq-gen x)
    (uniq-orig na)
    (facts (neq a b))
    ;; (facts (neq (exp (gen) eta) (gen)))
    (gen-st (pv a l)))

  (defrole resp
    (vars (l y rndx) (alpha chi expt) (a b name) (na nb data) (priv-stor locn))
    (trace
     (load priv-stor (pv b l))
     (recv (sig (body a (exp (gen) alpha) (pubk "sig" a))
		(privk "sig" a)))
     (recv (cat na a b (exp (gen) chi)))
     (send (cat (exp (gen) y)
		(enc na nb a b
		     (kcfb l (exp (gen) alpha)
			   y (exp (gen) chi)))))
     (recv nb)
     (send "done")
     )
    (uniq-gen y)
    (uniq-orig nb)
    (facts (neq a b))
    ;;    (facts (neq (exp (gen) chi) (gen)))
    (gen-st (pv b l)))

  (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))

  (defrole ltx-disclose
    (vars (self name) (l rndx)
	  (priv-stor locn) (ignore mesg))
    (trace
     (load priv-stor (pv self l))
     (stor priv-stor "nil")
     (send l))
    (gen-st (pv 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))))

  (defrule eq-means-=
    (forall
     ((v1 v2 mesg))
     (implies
      (fact eq v1 v2)
      (= v1 v2))))

  (lang (sig sign)
	(body (tuple 3))
	(pv (tuple 2))))

;; Implicit authentication

(defgoal dhcr-um
  (forall
   ((zi zr strd) (ltxa ltxb x y rndx) (eta chi beta alpha expt)
    (a b a-0 b-0 name))
   (implies
    (and
     (p "init" zi 4)
     (p "init" "l" zi ltxa)
     (p "init" "beta" zi beta)
     (p "init" "x" zi x)
     (p "init" "eta" zi eta)
     (p "init" "a" zi a)
     (p "init" "b" zi b-0)
     
     (p "resp" zr 4)
     (p "resp" "l" zr ltxb)
     (p "resp" "alpha" zr alpha)
     (p "resp" "y" zr y)
     (p "resp" "chi" zr chi)     
     (p "resp" "a" zr a-0)
     (p "resp" "b" zr b)
     (fact eq
	   (kcfa ltxa (exp (gen) beta)
		 x (exp (gen) eta))
	   (kcfb ltxb (exp (gen) alpha)
		 y (exp (gen) chi)))
     (non (privk "sig" b))
     (non (privk "sig" a))
     (fact neq ltxa ltxb)
     (fact undisclosed ltxa)
     (fact undisclosed beta)
     (fact undisclosed ltxb)
     (fact undisclosed alpha))
    (and
     (= a-0 a)
     (= b-0 b)
     (= beta ltxb)
     (= alpha ltxa)))))