(comment "CPSA 2.0.4")
(comment "All input read")

(defprotocol completeness-test basic
  (defrole init
    (vars (a b name) (n text) (s skey))
    (trace (send (enc a n (pubk b))) (recv (enc n (pubk a)))
      (send (enc "ok" s))))
  (defrole resp
    (vars (a b name) (n text))
    (trace (recv (enc a n (pubk b))) (send (enc n (pubk a)))))
  (defrole probe (vars (s skey)) (trace (recv (enc "ok" s)))))

(defskeleton completeness-test
  (vars (n text) (b a name) (s s-0 skey))
  (defstrand init 3 (n n) (a a) (b b) (s s-0))
  (defstrand probe 1 (s s))
  (non-orig s (privk b))
  (uniq-orig n)
  (traces
    ((send (enc a n (pubk b))) (recv (enc n (pubk a)))
      (send (enc "ok" s-0))) ((recv (enc "ok" s))))
  (label 0)
  (unrealized (0 1) (1 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton completeness-test
  (vars (n n-0 text) (b a a-0 b-0 name) (s s-0 skey))
  (defstrand init 3 (n n) (a a) (b b) (s s-0))
  (defstrand probe 1 (s s))
  (defstrand init 3 (n n-0) (a a-0) (b b-0) (s s))
  (precedes ((2 2) (1 0)))
  (non-orig s (privk b))
  (uniq-orig n)
  (operation encryption-test (added-strand init 3) (enc "ok" s) (1 0))
  (traces
    ((send (enc a n (pubk b))) (recv (enc n (pubk a)))
      (send (enc "ok" s-0))) ((recv (enc "ok" s)))
    ((send (enc a-0 n-0 (pubk b-0))) (recv (enc n-0 (pubk a-0)))
      (send (enc "ok" s))))
  (label 1)
  (parent 0)
  (unrealized (0 1))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton completeness-test
  (vars (n n-0 text) (b a a-0 b-0 name) (s s-0 skey))
  (defstrand init 3 (n n) (a a) (b b) (s s-0))
  (defstrand probe 1 (s s))
  (defstrand init 3 (n n-0) (a a-0) (b b-0) (s s))
  (defstrand resp 2 (n n) (a a) (b b))
  (precedes ((0 0) (3 0)) ((2 2) (1 0)) ((3 1) (0 1)))
  (non-orig s (privk b))
  (uniq-orig n)
  (operation nonce-test (added-strand resp 2) n (0 1)
    (enc a n (pubk b)))
  (traces
    ((send (enc a n (pubk b))) (recv (enc n (pubk a)))
      (send (enc "ok" s-0))) ((recv (enc "ok" s)))
    ((send (enc a-0 n-0 (pubk b-0))) (recv (enc n-0 (pubk a-0)))
      (send (enc "ok" s)))
    ((recv (enc a n (pubk b))) (send (enc n (pubk a)))))
  (label 2)
  (parent 1)
  (unrealized)
  (shape)
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton completeness-test
  (vars (n text) (b a name) (s skey))
  (defstrand init 3 (n n) (a a) (b b) (s s))
  (defstrand probe 1 (s s))
  (defstrand resp 2 (n n) (a a) (b b))
  (precedes ((0 0) (2 0)) ((0 2) (1 0)) ((2 1) (0 1)))
  (non-orig s (privk b))
  (uniq-orig n)
  (operation collapsed 2 0)
  (traces
    ((send (enc a n (pubk b))) (recv (enc n (pubk a)))
      (send (enc "ok" s))) ((recv (enc "ok" s)))
    ((recv (enc a n (pubk b))) (send (enc n (pubk a)))))
  (label 3)
  (parent 2)
  (unrealized)
  (shape))

(comment "Nothing left to do")

(defprotocol completeness-test basic
  (defrole init
    (vars (a b name) (n text) (s skey))
    (trace (send (enc a n (pubk b))) (recv (enc n (pubk a)))
      (send (enc "ok" s))))
  (defrole resp
    (vars (a b name) (n text))
    (trace (recv (enc a n (pubk b))) (send (enc n (pubk a)))))
  (defrole probe (vars (s skey)) (trace (recv (enc "ok" s)))))

(defskeleton completeness-test
  (vars (n text) (b a name) (s s-0 skey))
  (defstrand probe 1 (s s))
  (defstrand init 3 (n n) (a a) (b b) (s s-0))
  (non-orig s (privk b))
  (uniq-orig n)
  (traces ((recv (enc "ok" s)))
    ((send (enc a n (pubk b))) (recv (enc n (pubk a)))
      (send (enc "ok" s-0))))
  (label 4)
  (unrealized (0 0) (1 1))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton completeness-test
  (vars (n text) (b a name) (s s-0 skey))
  (defstrand probe 1 (s s))
  (defstrand init 3 (n n) (a a) (b b) (s s-0))
  (defstrand resp 2 (n n) (a a) (b b))
  (precedes ((1 0) (2 0)) ((2 1) (1 1)))
  (non-orig s (privk b))
  (uniq-orig n)
  (operation nonce-test (added-strand resp 2) n (1 1)
    (enc a n (pubk b)))
  (traces ((recv (enc "ok" s)))
    ((send (enc a n (pubk b))) (recv (enc n (pubk a)))
      (send (enc "ok" s-0)))
    ((recv (enc a n (pubk b))) (send (enc n (pubk a)))))
  (label 5)
  (parent 4)
  (unrealized (0 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton completeness-test
  (vars (n n-0 text) (b a a-0 b-0 name) (s s-0 skey))
  (defstrand probe 1 (s s))
  (defstrand init 3 (n n) (a a) (b b) (s s-0))
  (defstrand resp 2 (n n) (a a) (b b))
  (defstrand init 3 (n n-0) (a a-0) (b b-0) (s s))
  (precedes ((1 0) (2 0)) ((2 1) (1 1)) ((3 2) (0 0)))
  (non-orig s (privk b))
  (uniq-orig n)
  (operation encryption-test (added-strand init 3) (enc "ok" s) (0 0))
  (traces ((recv (enc "ok" s)))
    ((send (enc a n (pubk b))) (recv (enc n (pubk a)))
      (send (enc "ok" s-0)))
    ((recv (enc a n (pubk b))) (send (enc n (pubk a))))
    ((send (enc a-0 n-0 (pubk b-0))) (recv (enc n-0 (pubk a-0)))
      (send (enc "ok" s))))
  (label 6)
  (parent 5)
  (unrealized)
  (shape)
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton completeness-test
  (vars (n text) (b a name) (s skey))
  (defstrand probe 1 (s s))
  (defstrand init 3 (n n) (a a) (b b) (s s))
  (defstrand resp 2 (n n) (a a) (b b))
  (precedes ((1 0) (2 0)) ((1 2) (0 0)) ((2 1) (1 1)))
  (non-orig s (privk b))
  (uniq-orig n)
  (operation collapsed 3 1)
  (traces ((recv (enc "ok" s)))
    ((send (enc a n (pubk b))) (recv (enc n (pubk a)))
      (send (enc "ok" s)))
    ((recv (enc a n (pubk b))) (send (enc n (pubk a)))))
  (label 7)
  (parent 6)
  (unrealized)
  (shape))

(comment "Nothing left to do")

(defprotocol completeness-test basic
  (defrole init
    (vars (a b name) (n text) (s skey))
    (trace (send (enc a n (pubk b))) (recv (enc n (pubk a)))
      (send (enc "ok" s))))
  (defrole resp
    (vars (a b name) (n text))
    (trace (recv (enc a n (pubk b))) (send (enc n (pubk a)))))
  (defrole probe (vars (s skey)) (trace (recv (enc "ok" s)))))

(defskeleton completeness-test
  (vars (n text) (b a name) (s skey))
  (defstrand init 2 (n n) (a a) (b b))
  (defstrand probe 1 (s s))
  (non-orig s (privk b))
  (uniq-orig n)
  (traces ((send (enc a n (pubk b))) (recv (enc n (pubk a))))
    ((recv (enc "ok" s))))
  (label 8)
  (unrealized (0 1) (1 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton completeness-test
  (vars (n n-0 text) (b a a-0 b-0 name) (s skey))
  (defstrand init 2 (n n) (a a) (b b))
  (defstrand probe 1 (s s))
  (defstrand init 3 (n n-0) (a a-0) (b b-0) (s s))
  (precedes ((2 2) (1 0)))
  (non-orig s (privk b))
  (uniq-orig n)
  (operation encryption-test (added-strand init 3) (enc "ok" s) (1 0))
  (traces ((send (enc a n (pubk b))) (recv (enc n (pubk a))))
    ((recv (enc "ok" s)))
    ((send (enc a-0 n-0 (pubk b-0))) (recv (enc n-0 (pubk a-0)))
      (send (enc "ok" s))))
  (label 9)
  (parent 8)
  (unrealized (0 1))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton completeness-test
  (vars (n n-0 text) (b a a-0 b-0 name) (s skey))
  (defstrand init 2 (n n) (a a) (b b))
  (defstrand probe 1 (s s))
  (defstrand init 3 (n n-0) (a a-0) (b b-0) (s s))
  (defstrand resp 2 (n n) (a a) (b b))
  (precedes ((0 0) (3 0)) ((2 2) (1 0)) ((3 1) (0 1)))
  (non-orig s (privk b))
  (uniq-orig n)
  (operation nonce-test (added-strand resp 2) n (0 1)
    (enc a n (pubk b)))
  (traces ((send (enc a n (pubk b))) (recv (enc n (pubk a))))
    ((recv (enc "ok" s)))
    ((send (enc a-0 n-0 (pubk b-0))) (recv (enc n-0 (pubk a-0)))
      (send (enc "ok" s)))
    ((recv (enc a n (pubk b))) (send (enc n (pubk a)))))
  (label 10)
  (parent 9)
  (unrealized)
  (shape)
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton completeness-test
  (vars (n text) (a b name) (s skey))
  (defstrand probe 1 (s s))
  (defstrand init 3 (n n) (a a) (b b) (s s))
  (defstrand resp 2 (n n) (a a) (b b))
  (precedes ((1 0) (2 0)) ((1 2) (0 0)) ((2 1) (1 1)))
  (non-orig s (privk b))
  (uniq-orig n)
  (operation collapsed 0 2)
  (traces ((recv (enc "ok" s)))
    ((send (enc a n (pubk b))) (recv (enc n (pubk a)))
      (send (enc "ok" s)))
    ((recv (enc a n (pubk b))) (send (enc n (pubk a)))))
  (label 11)
  (parent 10)
  (unrealized)
  (shape))

(comment "Nothing left to do")

(defprotocol completeness-test basic
  (defrole init
    (vars (a b name) (n text) (s skey))
    (trace (send (enc a n (pubk b))) (recv (enc n (pubk a)))
      (send (enc "ok" s))))
  (defrole resp
    (vars (a b name) (n text))
    (trace (recv (enc a n (pubk b))) (send (enc n (pubk a)))))
  (defrole probe (vars (s skey)) (trace (recv (enc "ok" s)))))

(defskeleton completeness-test
  (vars (n text) (b a name) (s skey))
  (defstrand probe 1 (s s))
  (defstrand init 2 (n n) (a a) (b b))
  (non-orig s (privk b))
  (uniq-orig n)
  (traces ((recv (enc "ok" s)))
    ((send (enc a n (pubk b))) (recv (enc n (pubk a)))))
  (label 12)
  (unrealized (0 0) (1 1))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton completeness-test
  (vars (n text) (b a name) (s skey))
  (defstrand probe 1 (s s))
  (defstrand init 2 (n n) (a a) (b b))
  (defstrand resp 2 (n n) (a a) (b b))
  (precedes ((1 0) (2 0)) ((2 1) (1 1)))
  (non-orig s (privk b))
  (uniq-orig n)
  (operation nonce-test (added-strand resp 2) n (1 1)
    (enc a n (pubk b)))
  (traces ((recv (enc "ok" s)))
    ((send (enc a n (pubk b))) (recv (enc n (pubk a))))
    ((recv (enc a n (pubk b))) (send (enc n (pubk a)))))
  (label 13)
  (parent 12)
  (unrealized (0 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton completeness-test
  (vars (n n-0 text) (b a a-0 b-0 name) (s skey))
  (defstrand probe 1 (s s))
  (defstrand init 2 (n n) (a a) (b b))
  (defstrand resp 2 (n n) (a a) (b b))
  (defstrand init 3 (n n-0) (a a-0) (b b-0) (s s))
  (precedes ((1 0) (2 0)) ((2 1) (1 1)) ((3 2) (0 0)))
  (non-orig s (privk b))
  (uniq-orig n)
  (operation encryption-test (added-strand init 3) (enc "ok" s) (0 0))
  (traces ((recv (enc "ok" s)))
    ((send (enc a n (pubk b))) (recv (enc n (pubk a))))
    ((recv (enc a n (pubk b))) (send (enc n (pubk a))))
    ((send (enc a-0 n-0 (pubk b-0))) (recv (enc n-0 (pubk a-0)))
      (send (enc "ok" s))))
  (label 14)
  (parent 13)
  (unrealized)
  (shape)
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton completeness-test
  (vars (n text) (a b name) (s skey))
  (defstrand probe 1 (s s))
  (defstrand resp 2 (n n) (a a) (b b))
  (defstrand init 3 (n n) (a a) (b b) (s s))
  (precedes ((1 1) (2 1)) ((2 0) (1 0)) ((2 2) (0 0)))
  (non-orig s (privk b))
  (uniq-orig n)
  (operation collapsed 1 3)
  (traces ((recv (enc "ok" s)))
    ((recv (enc a n (pubk b))) (send (enc n (pubk a))))
    ((send (enc a n (pubk b))) (recv (enc n (pubk a)))
      (send (enc "ok" s))))
  (label 15)
  (parent 14)
  (unrealized)
  (shape))

(comment "Nothing left to do")