cpsa-4.4.4: tst/yahalom-6.3.6_shapes.tst

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

(herald "Yahalom Protocol"
  (comment "A Survey of Authentication Protocol Literature:"
    "Version 1.0, John Clark and Jeremy Jacob,"
    "Yahalom Protocol, Section 6.3.6, Page 49")
  (url "http://www.eecs.umich.edu/acal/swerve/docs/49-1.pdf")
  (bound 15))

(comment "CPSA 4.3.1")

(comment "All input read from tst/yahalom-6.3.6.scm")

(comment "Strand count bounded at 15")

(defprotocol yahalom basic
  (defrole init
    (vars (a b s name) (n-a n-b text) (k skey) (blob mesg))
    (trace (send (cat a n-a))
      (recv (cat (enc b k n-a n-b (ltk a s)) blob))
      (send (cat blob (enc n-b k)))))
  (defrole resp
    (vars (a b s name) (n-a n-b text) (k skey))
    (trace (recv (cat a n-a)) (send (cat b (enc a n-a n-b (ltk b s))))
      (recv (cat (enc a k (ltk b s)) (enc n-b k)))))
  (defrole serv
    (vars (a b s name) (n-a n-b text) (k skey))
    (trace (recv (cat b (enc a n-a n-b (ltk b s))))
      (send (cat (enc b k n-a n-b (ltk a s)) (enc a k (ltk b s)))))
    (uniq-orig k))
  (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 "Yahalom protocol, Section 6.3.6, Page 49")
  (url "http://www.eecs.umich.edu/acal/swerve/docs/49-1.pdf"))

(defskeleton yahalom
  (vars (blob mesg) (k skey) (n-a n-b text) (a b s name))
  (defstrand init 3 (blob blob) (k k) (n-a n-a) (n-b n-b) (a a) (b b)
    (s s))
  (non-orig (ltk a s) (ltk b s))
  (uniq-orig n-a n-b)
  (traces
    ((send (cat a n-a)) (recv (cat (enc b k n-a n-b (ltk a s)) blob))
      (send (cat blob (enc n-b k)))))
  (label 0)
  (unrealized (0 1))
  (origs (n-a (0 0)))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton yahalom
  (vars (blob mesg) (k skey) (n-a n-b text) (a b s name))
  (defstrand init 3 (blob blob) (k k) (n-a n-a) (n-b n-b) (a a) (b b)
    (s s))
  (defstrand serv 2 (k k) (n-a n-a) (n-b n-b) (a a) (b b) (s s))
  (defstrand resp 2 (n-a n-a) (n-b n-b) (a a) (b b) (s s))
  (precedes ((0 0) (2 0)) ((1 1) (0 1)) ((2 1) (1 0)))
  (non-orig (ltk a s) (ltk b s))
  (uniq-orig k n-a n-b)
  (operation encryption-test (added-strand resp 2)
    (enc a n-a n-b (ltk b s)) (1 0))
  (traces
    ((send (cat a n-a)) (recv (cat (enc b k n-a n-b (ltk a s)) blob))
      (send (cat blob (enc n-b k))))
    ((recv (cat b (enc a n-a n-b (ltk b s))))
      (send (cat (enc b k n-a n-b (ltk a s)) (enc a k (ltk b s)))))
    ((recv (cat a n-a)) (send (cat b (enc a n-a n-b (ltk b s))))))
  (label 2)
  (parent 0)
  (realized)
  (shape)
  (maps ((0) ((a a) (b b) (s s) (n-a n-a) (n-b n-b) (k k) (blob blob))))
  (origs (k (1 1)) (n-a (0 0)) (n-b (2 1))))

(comment "Nothing left to do")

(defprotocol yahalom basic
  (defrole init
    (vars (a b s name) (n-a n-b text) (k skey) (blob mesg))
    (trace (send (cat a n-a))
      (recv (cat (enc b k n-a n-b (ltk a s)) blob))
      (send (cat blob (enc n-b k)))))
  (defrole resp
    (vars (a b s name) (n-a n-b text) (k skey))
    (trace (recv (cat a n-a)) (send (cat b (enc a n-a n-b (ltk b s))))
      (recv (cat (enc a k (ltk b s)) (enc n-b k)))))
  (defrole serv
    (vars (a b s name) (n-a n-b text) (k skey))
    (trace (recv (cat b (enc a n-a n-b (ltk b s))))
      (send (cat (enc b k n-a n-b (ltk a s)) (enc a k (ltk b s)))))
    (uniq-orig k))
  (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 "Yahalom protocol, Section 6.3.6, Page 49")
  (url "http://www.eecs.umich.edu/acal/swerve/docs/49-1.pdf"))

(defskeleton yahalom
  (vars (k skey) (n-a n-b text) (a b s name))
  (defstrand resp 3 (k k) (n-a n-a) (n-b n-b) (a a) (b b) (s s))
  (deflistener k)
  (non-orig (ltk a s) (ltk b s))
  (uniq-orig n-a n-b)
  (traces
    ((recv (cat a n-a)) (send (cat b (enc a n-a n-b (ltk b s))))
      (recv (cat (enc a k (ltk b s)) (enc n-b k)))) ((recv k) (send k)))
  (label 3)
  (unrealized (0 2))
  (origs (n-b (0 1)))
  (comment "1 in cohort - 1 not yet seen"))

(comment "Nothing left to do")

(defprotocol yahalom basic
  (defrole init
    (vars (a b s name) (n-a n-b text) (k skey) (blob mesg))
    (trace (send (cat a n-a))
      (recv (cat (enc b k n-a n-b (ltk a s)) blob))
      (send (cat blob (enc n-b k)))))
  (defrole resp
    (vars (a b s name) (n-a n-b text) (k skey))
    (trace (recv (cat a n-a)) (send (cat b (enc a n-a n-b (ltk b s))))
      (recv (cat (enc a k (ltk b s)) (enc n-b k)))))
  (defrole serv
    (vars (a b s name) (n-a n-b text) (k skey))
    (trace (recv (cat b (enc a n-a n-b (ltk b s))))
      (send (cat (enc b k n-a n-b (ltk a s)) (enc a k (ltk b s)))))
    (uniq-orig k))
  (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 "Yahalom protocol, Section 6.3.6, Page 49")
  (url "http://www.eecs.umich.edu/acal/swerve/docs/49-1.pdf"))

(defskeleton yahalom
  (vars (k skey) (n-a n-b text) (a b s name))
  (defstrand resp 3 (k k) (n-a n-a) (n-b n-b) (a a) (b b) (s s))
  (non-orig (ltk a s) (ltk b s))
  (uniq-orig n-a n-b)
  (traces
    ((recv (cat a n-a)) (send (cat b (enc a n-a n-b (ltk b s))))
      (recv (cat (enc a k (ltk b s)) (enc n-b k)))))
  (label 7)
  (unrealized (0 2))
  (origs (n-b (0 1)))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton yahalom
  (vars (blob mesg) (k skey) (n-a n-b text) (a b s name))
  (defstrand resp 3 (k k) (n-a n-a) (n-b n-b) (a a) (b b) (s s))
  (defstrand serv 2 (k k) (n-a n-a) (n-b n-b) (a a) (b b) (s s))
  (defstrand init 3 (blob blob) (k k) (n-a n-a) (n-b n-b) (a a) (b b)
    (s s))
  (precedes ((0 1) (1 0)) ((1 1) (2 1)) ((2 0) (0 0)) ((2 2) (0 2)))
  (non-orig (ltk a s) (ltk b s))
  (uniq-orig k n-a n-b)
  (operation nonce-test (contracted (a-0 a) (b-0 b) (s-0 s) (n-a-0 n-a))
    n-b (2 1) (enc a n-a n-b (ltk b s)) (enc b k n-a n-b (ltk a s)))
  (traces
    ((recv (cat a n-a)) (send (cat b (enc a n-a n-b (ltk b s))))
      (recv (cat (enc a k (ltk b s)) (enc n-b k))))
    ((recv (cat b (enc a n-a n-b (ltk b s))))
      (send (cat (enc b k n-a n-b (ltk a s)) (enc a k (ltk b s)))))
    ((send (cat a n-a)) (recv (cat (enc b k n-a n-b (ltk a s)) blob))
      (send (cat blob (enc n-b k)))))
  (label 15)
  (parent 7)
  (realized)
  (shape)
  (maps ((0) ((a a) (b b) (s s) (n-a n-a) (n-b n-b) (k k))))
  (origs (k (1 1)) (n-a (2 0)) (n-b (0 1))))

(comment "Nothing left to do")

(defprotocol yahalom basic
  (defrole init
    (vars (a b s name) (n-a n-b text) (k skey) (blob mesg))
    (trace (send (cat a n-a))
      (recv (cat (enc b k n-a n-b (ltk a s)) blob))
      (send (cat blob (enc n-b k)))))
  (defrole resp
    (vars (a b s name) (n-a n-b text) (k skey))
    (trace (recv (cat a n-a)) (send (cat b (enc a n-a n-b (ltk b s))))
      (recv (cat (enc a k (ltk b s)) (enc n-b k)))))
  (defrole serv
    (vars (a b s name) (n-a n-b text) (k skey))
    (trace (recv (cat b (enc a n-a n-b (ltk b s))))
      (send (cat (enc b k n-a n-b (ltk a s)) (enc a k (ltk b s)))))
    (uniq-orig k))
  (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 "Yahalom protocol, Section 6.3.6, Page 49")
  (url "http://www.eecs.umich.edu/acal/swerve/docs/49-1.pdf"))

(defskeleton yahalom
  (vars (k skey) (n-a n-b text) (a b s name))
  (defstrand serv 2 (k k) (n-a n-a) (n-b n-b) (a a) (b b) (s s))
  (non-orig (ltk a s) (ltk b s))
  (uniq-orig k n-a n-b)
  (traces
    ((recv (cat b (enc a n-a n-b (ltk b s))))
      (send (cat (enc b k n-a n-b (ltk a s)) (enc a k (ltk b s))))))
  (label 31)
  (unrealized (0 0))
  (origs (k (0 1)))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton yahalom
  (vars (k skey) (n-a n-b text) (a b s name))
  (defstrand serv 2 (k k) (n-a n-a) (n-b n-b) (a a) (b b) (s s))
  (defstrand resp 2 (n-a n-a) (n-b n-b) (a a) (b b) (s s))
  (precedes ((1 1) (0 0)))
  (non-orig (ltk a s) (ltk b s))
  (uniq-orig k n-a n-b)
  (operation encryption-test (added-strand resp 2)
    (enc a n-a n-b (ltk b s)) (0 0))
  (traces
    ((recv (cat b (enc a n-a n-b (ltk b s))))
      (send (cat (enc b k n-a n-b (ltk a s)) (enc a k (ltk b s)))))
    ((recv (cat a n-a)) (send (cat b (enc a n-a n-b (ltk b s))))))
  (label 32)
  (parent 31)
  (realized)
  (shape)
  (maps ((0) ((a a) (b b) (s s) (n-a n-a) (n-b n-b) (k k))))
  (origs (k (0 1)) (n-b (1 1))))

(comment "Nothing left to do")