(herald "Yahalom Protocol Without Forwarding" (bound 15))

(comment "CPSA 4.4.6")
(comment "All input read from tst/tmp-yahalom.scm")
(comment "Strand count bounded at 15")

(defprotocol yahalom basic
  (defrole init
    (vars (a b c name) (n-a n-b text) (k skey))
    (trace (send (cat a n-a)) (recv (enc b k n-a n-b (ltk a c)))
      (send (enc n-b k))))
  (defrole resp
    (vars (b a c 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 c))))
      (recv (enc a k (ltk b c))) (recv (enc n-b k))))
  (defrole serv
    (vars (c a b name) (n-a n-b text) (k skey))
    (trace (recv (cat b (enc a n-a n-b (ltk b c))))
      (send (enc b k n-a n-b (ltk a c))) (send (enc a k (ltk b c))))
    (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)))))

(defskeleton yahalom
  (vars (k skey) (n-a n-b text) (c a b name))
  (defstrand serv 3 (k k) (n-a n-a) (n-b n-b) (c c) (a a) (b b))
  (non-orig (ltk a c) (ltk b c))
  (uniq-orig k)
  (traces
    ((recv (cat b (enc a n-a n-b (ltk b c))))
      (send (enc b k n-a n-b (ltk a c))) (send (enc a k (ltk b c)))))
  (label 0)
  (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) (c a b name))
  (defstrand serv 3 (k k) (n-a n-a) (n-b n-b) (c c) (a a) (b b))
  (defstrand resp 2 (n-a n-a) (n-b n-b) (b b) (a a) (c c))
  (precedes ((1 1) (0 0)))
  (non-orig (ltk a c) (ltk b c))
  (uniq-orig k)
  (operation encryption-test (added-strand resp 2)
    (enc a n-a n-b (ltk b c)) (0 0))
  (strand-map 0)
  (traces
    ((recv (cat b (enc a n-a n-b (ltk b c))))
      (send (enc b k n-a n-b (ltk a c))) (send (enc a k (ltk b c))))
    ((recv (cat a n-a)) (send (cat b (enc a n-a n-b (ltk b c))))))
  (label 1)
  (parent 0)
  (realized)
  (shape)
  (maps ((0) ((c c) (a a) (b b) (k k) (n-a n-a) (n-b n-b))))
  (origs (k (0 1))))

(comment "Nothing left to do")

(defprotocol yahalom basic
  (defrole init
    (vars (a b c name) (n-a n-b text) (k skey))
    (trace (send (cat a n-a)) (recv (enc b k n-a n-b (ltk a c)))
      (send (enc n-b k))))
  (defrole resp
    (vars (b a c 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 c))))
      (recv (enc a k (ltk b c))) (recv (enc n-b k))))
  (defrole serv
    (vars (c a b name) (n-a n-b text) (k skey))
    (trace (recv (cat b (enc a n-a n-b (ltk b c))))
      (send (enc b k n-a n-b (ltk a c))) (send (enc a k (ltk b c))))
    (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)))))

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

(defskeleton yahalom
  (vars (k skey) (n-a n-b n-a-0 n-b-0 text) (b a c name))
  (defstrand resp 4 (k k) (n-a n-a) (n-b n-b) (b b) (a a) (c c))
  (deflistener k)
  (defstrand serv 3 (k k) (n-a n-a-0) (n-b n-b-0) (c c) (a a) (b b))
  (precedes ((2 1) (1 0)) ((2 2) (0 2)))
  (non-orig (ltk b c) (ltk a c))
  (uniq-orig k)
  (operation encryption-test (added-strand serv 3) (enc a k (ltk b c))
    (0 2))
  (strand-map 0 1)
  (traces
    ((recv (cat a n-a)) (send (cat b (enc a n-a n-b (ltk b c))))
      (recv (enc a k (ltk b c))) (recv (enc n-b k))) ((recv k) (send k))
    ((recv (cat b (enc a n-a-0 n-b-0 (ltk b c))))
      (send (enc b k n-a-0 n-b-0 (ltk a c)))
      (send (enc a k (ltk b c)))))
  (label 3)
  (parent 2)
  (unrealized (0 3) (1 0) (2 0))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton yahalom
  (vars (k skey) (n-a n-b text) (b a c name))
  (defstrand resp 4 (k k) (n-a n-a) (n-b n-b) (b b) (a a) (c c))
  (deflistener k)
  (defstrand serv 3 (k k) (n-a n-a) (n-b n-b) (c c) (a a) (b b))
  (precedes ((0 1) (2 0)) ((2 1) (1 0)) ((2 2) (0 2)))
  (non-orig (ltk b c) (ltk a c))
  (uniq-orig k)
  (operation encryption-test (displaced 3 0 resp 2)
    (enc a n-a-0 n-b-0 (ltk b c)) (2 0))
  (strand-map 0 1 2)
  (traces
    ((recv (cat a n-a)) (send (cat b (enc a n-a n-b (ltk b c))))
      (recv (enc a k (ltk b c))) (recv (enc n-b k))) ((recv k) (send k))
    ((recv (cat b (enc a n-a n-b (ltk b c))))
      (send (enc b k n-a n-b (ltk a c))) (send (enc a k (ltk b c)))))
  (label 4)
  (parent 3)
  (unrealized (0 3) (1 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton yahalom
  (vars (k skey) (n-a n-b n-a-0 n-b-0 text) (b a c name))
  (defstrand resp 4 (k k) (n-a n-a) (n-b n-b) (b b) (a a) (c c))
  (deflistener k)
  (defstrand serv 3 (k k) (n-a n-a-0) (n-b n-b-0) (c c) (a a) (b b))
  (defstrand resp 2 (n-a n-a-0) (n-b n-b-0) (b b) (a a) (c c))
  (precedes ((2 1) (1 0)) ((2 2) (0 2)) ((3 1) (2 0)))
  (non-orig (ltk b c) (ltk a c))
  (uniq-orig k)
  (operation encryption-test (added-strand resp 2)
    (enc a n-a-0 n-b-0 (ltk b c)) (2 0))
  (strand-map 0 1 2)
  (traces
    ((recv (cat a n-a)) (send (cat b (enc a n-a n-b (ltk b c))))
      (recv (enc a k (ltk b c))) (recv (enc n-b k))) ((recv k) (send k))
    ((recv (cat b (enc a n-a-0 n-b-0 (ltk b c))))
      (send (enc b k n-a-0 n-b-0 (ltk a c))) (send (enc a k (ltk b c))))
    ((recv (cat a n-a-0)) (send (cat b (enc a n-a-0 n-b-0 (ltk b c))))))
  (label 5)
  (parent 3)
  (unrealized (0 3) (1 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton yahalom
  (vars (k skey) (n-a n-b text) (b a c name))
  (defstrand resp 4 (k k) (n-a n-a) (n-b n-b) (b b) (a a) (c c))
  (deflistener k)
  (defstrand serv 3 (k k) (n-a n-a) (n-b n-b) (c c) (a a) (b b))
  (precedes ((0 1) (2 0)) ((2 2) (0 2)) ((2 2) (1 0)))
  (non-orig (ltk b c) (ltk a c))
  (uniq-orig k)
  (operation nonce-test (displaced 3 2 serv 3) k (1 0)
    (enc b k n-a n-b (ltk a c)))
  (strand-map 0 1 2)
  (traces
    ((recv (cat a n-a)) (send (cat b (enc a n-a n-b (ltk b c))))
      (recv (enc a k (ltk b c))) (recv (enc n-b k))) ((recv k) (send k))
    ((recv (cat b (enc a n-a n-b (ltk b c))))
      (send (enc b k n-a n-b (ltk a c))) (send (enc a k (ltk b c)))))
  (label 6)
  (parent 4)
  (unrealized (0 3) (1 0))
  (dead)
  (comment "empty cohort"))

(defskeleton yahalom
  (vars (k skey) (n-a n-b n-a-0 n-b-0 text) (b a c name))
  (defstrand resp 4 (k k) (n-a n-a) (n-b n-b) (b b) (a a) (c c))
  (deflistener k)
  (defstrand serv 3 (k k) (n-a n-a-0) (n-b n-b-0) (c c) (a a) (b b))
  (defstrand resp 2 (n-a n-a-0) (n-b n-b-0) (b b) (a a) (c c))
  (precedes ((2 2) (0 2)) ((2 2) (1 0)) ((3 1) (2 0)))
  (non-orig (ltk b c) (ltk a c))
  (uniq-orig k)
  (operation nonce-test (displaced 4 2 serv 3) k (1 0)
    (enc b k n-a-0 n-b-0 (ltk a c)))
  (strand-map 0 1 2 3)
  (traces
    ((recv (cat a n-a)) (send (cat b (enc a n-a n-b (ltk b c))))
      (recv (enc a k (ltk b c))) (recv (enc n-b k))) ((recv k) (send k))
    ((recv (cat b (enc a n-a-0 n-b-0 (ltk b c))))
      (send (enc b k n-a-0 n-b-0 (ltk a c))) (send (enc a k (ltk b c))))
    ((recv (cat a n-a-0)) (send (cat b (enc a n-a-0 n-b-0 (ltk b c))))))
  (label 7)
  (parent 5)
  (unrealized (0 3) (1 0))
  (dead)
  (comment "empty cohort"))

(comment "Nothing left to do")

(defprotocol yahalom basic
  (defrole init
    (vars (a b c name) (n-a n-b text) (k skey))
    (trace (send (cat a n-a)) (recv (enc b k n-a n-b (ltk a c)))
      (send (enc n-b k))))
  (defrole resp
    (vars (b a c 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 c))))
      (recv (enc a k (ltk b c))) (recv (enc n-b k))))
  (defrole serv
    (vars (c a b name) (n-a n-b text) (k skey))
    (trace (recv (cat b (enc a n-a n-b (ltk b c))))
      (send (enc b k n-a n-b (ltk a c))) (send (enc a k (ltk b c))))
    (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)))))

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

(defskeleton yahalom
  (vars (k skey) (n-a n-b n-a-0 n-b-0 text) (b a c name))
  (defstrand resp 4 (k k) (n-a n-a) (n-b n-b) (b b) (a a) (c c))
  (deflistener k)
  (defstrand serv 3 (k k) (n-a n-a-0) (n-b n-b-0) (c c) (a a) (b b))
  (precedes ((2 1) (1 0)) ((2 2) (0 2)))
  (non-orig (ltk b c) (ltk a c))
  (uniq-orig k)
  (operation encryption-test (added-strand serv 3) (enc a k (ltk b c))
    (0 2))
  (strand-map 0 1)
  (traces
    ((recv (cat a n-a)) (send (cat b (enc a n-a n-b (ltk b c))))
      (recv (enc a k (ltk b c))) (recv (enc n-b k))) ((recv k) (send k))
    ((recv (cat b (enc a n-a-0 n-b-0 (ltk b c))))
      (send (enc b k n-a-0 n-b-0 (ltk a c)))
      (send (enc a k (ltk b c)))))
  (label 9)
  (parent 8)
  (unrealized (0 3) (1 0) (2 0))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton yahalom
  (vars (k skey) (n-a n-b text) (b a c name))
  (defstrand resp 4 (k k) (n-a n-a) (n-b n-b) (b b) (a a) (c c))
  (deflistener k)
  (defstrand serv 3 (k k) (n-a n-a) (n-b n-b) (c c) (a a) (b b))
  (precedes ((0 1) (2 0)) ((2 1) (1 0)) ((2 2) (0 2)))
  (non-orig (ltk b c) (ltk a c))
  (uniq-orig k)
  (operation encryption-test (displaced 3 0 resp 2)
    (enc a n-a-0 n-b-0 (ltk b c)) (2 0))
  (strand-map 0 1 2)
  (traces
    ((recv (cat a n-a)) (send (cat b (enc a n-a n-b (ltk b c))))
      (recv (enc a k (ltk b c))) (recv (enc n-b k))) ((recv k) (send k))
    ((recv (cat b (enc a n-a n-b (ltk b c))))
      (send (enc b k n-a n-b (ltk a c))) (send (enc a k (ltk b c)))))
  (label 10)
  (parent 9)
  (unrealized (0 3) (1 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton yahalom
  (vars (k skey) (n-a n-b n-a-0 n-b-0 text) (b a c name))
  (defstrand resp 4 (k k) (n-a n-a) (n-b n-b) (b b) (a a) (c c))
  (deflistener k)
  (defstrand serv 3 (k k) (n-a n-a-0) (n-b n-b-0) (c c) (a a) (b b))
  (defstrand resp 2 (n-a n-a-0) (n-b n-b-0) (b b) (a a) (c c))
  (precedes ((2 1) (1 0)) ((2 2) (0 2)) ((3 1) (2 0)))
  (non-orig (ltk b c) (ltk a c))
  (uniq-orig k)
  (operation encryption-test (added-strand resp 2)
    (enc a n-a-0 n-b-0 (ltk b c)) (2 0))
  (strand-map 0 1 2)
  (traces
    ((recv (cat a n-a)) (send (cat b (enc a n-a n-b (ltk b c))))
      (recv (enc a k (ltk b c))) (recv (enc n-b k))) ((recv k) (send k))
    ((recv (cat b (enc a n-a-0 n-b-0 (ltk b c))))
      (send (enc b k n-a-0 n-b-0 (ltk a c))) (send (enc a k (ltk b c))))
    ((recv (cat a n-a-0)) (send (cat b (enc a n-a-0 n-b-0 (ltk b c))))))
  (label 11)
  (parent 9)
  (unrealized (0 3) (1 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton yahalom
  (vars (k skey) (n-a n-b text) (b a c name))
  (defstrand resp 4 (k k) (n-a n-a) (n-b n-b) (b b) (a a) (c c))
  (deflistener k)
  (defstrand serv 3 (k k) (n-a n-a) (n-b n-b) (c c) (a a) (b b))
  (precedes ((0 1) (2 0)) ((2 2) (0 2)) ((2 2) (1 0)))
  (non-orig (ltk b c) (ltk a c))
  (uniq-orig k)
  (operation nonce-test (displaced 3 2 serv 3) k (1 0)
    (enc b k n-a n-b (ltk a c)))
  (strand-map 0 1 2)
  (traces
    ((recv (cat a n-a)) (send (cat b (enc a n-a n-b (ltk b c))))
      (recv (enc a k (ltk b c))) (recv (enc n-b k))) ((recv k) (send k))
    ((recv (cat b (enc a n-a n-b (ltk b c))))
      (send (enc b k n-a n-b (ltk a c))) (send (enc a k (ltk b c)))))
  (label 12)
  (parent 10)
  (unrealized (0 3) (1 0))
  (dead)
  (comment "empty cohort"))

(defskeleton yahalom
  (vars (k skey) (n-a n-b n-a-0 n-b-0 text) (b a c name))
  (defstrand resp 4 (k k) (n-a n-a) (n-b n-b) (b b) (a a) (c c))
  (deflistener k)
  (defstrand serv 3 (k k) (n-a n-a-0) (n-b n-b-0) (c c) (a a) (b b))
  (defstrand resp 2 (n-a n-a-0) (n-b n-b-0) (b b) (a a) (c c))
  (precedes ((2 2) (0 2)) ((2 2) (1 0)) ((3 1) (2 0)))
  (non-orig (ltk b c) (ltk a c))
  (uniq-orig k)
  (operation nonce-test (displaced 4 2 serv 3) k (1 0)
    (enc b k n-a-0 n-b-0 (ltk a c)))
  (strand-map 0 1 2 3)
  (traces
    ((recv (cat a n-a)) (send (cat b (enc a n-a n-b (ltk b c))))
      (recv (enc a k (ltk b c))) (recv (enc n-b k))) ((recv k) (send k))
    ((recv (cat b (enc a n-a-0 n-b-0 (ltk b c))))
      (send (enc b k n-a-0 n-b-0 (ltk a c))) (send (enc a k (ltk b c))))
    ((recv (cat a n-a-0)) (send (cat b (enc a n-a-0 n-b-0 (ltk b c))))))
  (label 13)
  (parent 11)
  (unrealized (0 3) (1 0))
  (dead)
  (comment "empty cohort"))

(comment "Nothing left to do")