cpsa-4.4.4: tst/dhnsl_hack_shapes.tst

(comment "CPSA 4.3.1")
(comment "Extracted shapes")

(herald "Diffie-Hellman enhanced Needham-Schroeder-Lowe Protocol"
  (algebra basic))

(comment "CPSA 4.3.1")

(comment "All input read from tst/dhnsl_hack.scm")

(defprotocol dhnsl basic
  (defrole init
    (vars (a b name) (h2 h3 gx akey) (dhkey skey))
    (trace (send (enc gx a (pubk b)))
      (recv (enc h2 (enc "dh" h2 gx dhkey) h3 b (pubk a)))
      (send (enc (enc "dh" h3 gx dhkey) (pubk b))))
    (non-orig dhkey (invk gx))
    (uniq-orig gx)
    (comment "X should be assumed to be freshly chosen per role"))
  (defrole resp
    (vars (b a name) (h1 gy gz akey) (dhkey skey))
    (trace (recv (enc h1 a (pubk b)))
      (send (enc gy (enc "dh" gy h1 dhkey) gz b (pubk a)))
      (recv (enc (enc "dh" gz h1 dhkey) (pubk b))))
    (non-orig dhkey (invk gy) (invk gz))
    (uniq-orig gy gz)
    (comment "Y and Z should be assumed to be freshly chosen per role"))
  (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))))
  (comment
    "Needham-Schroeder-Lowe DH challenge/responses in place of nonces"))

(defskeleton dhnsl
  (vars (dhkey skey) (gx gy gz akey) (a b name))
  (defstrand init 3 (dhkey dhkey) (h2 gy) (h3 gz) (gx gx) (a a) (b b))
  (non-orig dhkey (invk gx) (privk a) (privk b))
  (uniq-orig gx)
  (comment "Initiator point-of-view")
  (traces
    ((send (enc gx a (pubk b)))
      (recv (enc gy (enc "dh" gy gx dhkey) gz b (pubk a)))
      (send (enc (enc "dh" gz gx dhkey) (pubk b)))))
  (label 0)
  (unrealized (0 1))
  (origs (gx (0 0)))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton dhnsl
  (vars (dhkey skey) (gx gy gz akey) (a b name))
  (defstrand init 3 (dhkey dhkey) (h2 gy) (h3 gz) (gx gx) (a a) (b b))
  (defstrand resp 2 (dhkey dhkey) (h1 gx) (gy gy) (gz gz) (b b) (a a))
  (precedes ((0 0) (1 0)) ((1 1) (0 1)))
  (non-orig dhkey (invk gx) (invk gy) (invk gz) (privk a) (privk b))
  (uniq-orig gx gy gz)
  (operation encryption-test (contracted (gz-0 gz))
    (enc "dh" gy gx dhkey) (0 1)
    (enc gy (enc "dh" gy gx dhkey) gz b (pubk a)))
  (traces
    ((send (enc gx a (pubk b)))
      (recv (enc gy (enc "dh" gy gx dhkey) gz b (pubk a)))
      (send (enc (enc "dh" gz gx dhkey) (pubk b))))
    ((recv (enc gx a (pubk b)))
      (send (enc gy (enc "dh" gy gx dhkey) gz b (pubk a)))))
  (label 4)
  (parent 0)
  (realized)
  (shape)
  (maps ((0) ((a a) (b b) (gx gx) (gy gy) (gz gz) (dhkey dhkey))))
  (origs (gy (1 1)) (gz (1 1)) (gx (0 0))))

(comment "Nothing left to do")

(defprotocol dhnsl basic
  (defrole init
    (vars (a b name) (h2 h3 gx akey) (dhkey skey))
    (trace (send (enc gx a (pubk b)))
      (recv (enc h2 (enc "dh" h2 gx dhkey) h3 b (pubk a)))
      (send (enc (enc "dh" h3 gx dhkey) (pubk b))))
    (non-orig dhkey (invk gx))
    (uniq-orig gx)
    (comment "X should be assumed to be freshly chosen per role"))
  (defrole resp
    (vars (b a name) (h1 gy gz akey) (dhkey skey))
    (trace (recv (enc h1 a (pubk b)))
      (send (enc gy (enc "dh" gy h1 dhkey) gz b (pubk a)))
      (recv (enc (enc "dh" gz h1 dhkey) (pubk b))))
    (non-orig dhkey (invk gy) (invk gz))
    (uniq-orig gy gz)
    (comment "Y and Z should be assumed to be freshly chosen per role"))
  (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))))
  (comment
    "Needham-Schroeder-Lowe DH challenge/responses in place of nonces"))

(defskeleton dhnsl
  (vars (dhkey skey) (gx gy gz akey) (a b name))
  (defstrand resp 3 (dhkey dhkey) (h1 gx) (gy gy) (gz gz) (b b) (a a))
  (non-orig dhkey (invk gy) (invk gz) (privk a))
  (uniq-orig gy gz)
  (comment "Responder point-of-view")
  (traces
    ((recv (enc gx a (pubk b)))
      (send (enc gy (enc "dh" gy gx dhkey) gz b (pubk a)))
      (recv (enc (enc "dh" gz gx dhkey) (pubk b)))))
  (label 7)
  (unrealized (0 2))
  (origs (gz (0 1)) (gy (0 1)))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton dhnsl
  (vars (dhkey skey) (gx gy gz akey) (a b name))
  (defstrand resp 3 (dhkey dhkey) (h1 gx) (gy gy) (gz gz) (b b) (a a))
  (defstrand init 3 (dhkey dhkey) (h2 gy) (h3 gz) (gx gx) (a a) (b b))
  (precedes ((0 1) (1 1)) ((1 0) (0 0)) ((1 2) (0 2)))
  (non-orig dhkey (invk gx) (invk gy) (invk gz) (privk a))
  (uniq-orig gx gy gz)
  (operation encryption-test (contracted (a-0 a) (b-0 b))
    (enc "dh" gy gx dhkey) (1 1)
    (enc gy (enc "dh" gy gx dhkey) gz b (pubk a)))
  (traces
    ((recv (enc gx a (pubk b)))
      (send (enc gy (enc "dh" gy gx dhkey) gz b (pubk a)))
      (recv (enc (enc "dh" gz gx dhkey) (pubk b))))
    ((send (enc gx a (pubk b)))
      (recv (enc gy (enc "dh" gy gx dhkey) gz b (pubk a)))
      (send (enc (enc "dh" gz gx dhkey) (pubk b)))))
  (label 13)
  (parent 7)
  (realized)
  (shape)
  (maps ((0) ((a a) (b b) (gx gx) (gy gy) (gz gz) (dhkey dhkey))))
  (origs (gy (0 1)) (gz (0 1)) (gx (1 0))))

(comment "Nothing left to do")