(comment "CPSA 2.2.8")
(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))
  (origs (n (0 0)))
  (comment "2 in cohort - 2 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 text) (b a name) (s skey))
  (defstrand init 3 (n n) (a a) (b b) (s s))
  (defstrand probe 1 (s s))
  (precedes ((0 2) (1 0)))
  (non-orig s (privk b))
  (uniq-orig n)
  (operation encryption-test (displaced 2 0 init 3) (enc "ok" s-0)
    (1 0))
  (traces
    ((send (enc a n (pubk b))) (recv (enc n (pubk a)))
      (send (enc "ok" s))) ((recv (enc "ok" s))))
  (label 2)
  (parent 0)
  (unrealized (0 1))
  (origs (n (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 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 3)
  (parent 1)
  (seen 4)
  (unrealized)
  (shape)
  (maps ((0 1) ((b b) (n n) (s s) (a a) (s-0 s-0))))
  (origs (n (0 0)))
  (comment "1 in cohort - 0 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 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))) ((recv (enc "ok" s)))
    ((recv (enc a n (pubk b))) (send (enc n (pubk a)))))
  (label 4)
  (parent 2)
  (unrealized)
  (shape)
  (maps ((0 1) ((b b) (n n) (s s) (a a) (s-0 s))))
  (origs (n (0 0))))

(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 5)
  (unrealized (0 0) (1 1))
  (origs (n (1 0)))
  (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 6)
  (parent 5)
  (unrealized (0 0))
  (comment "2 in cohort - 2 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 7)
  (parent 6)
  (seen 8)
  (unrealized)
  (shape)
  (maps ((0 1) ((b b) (n n) (s s) (a a) (s-0 s-0))))
  (origs (n (1 0)))
  (comment "1 in cohort - 0 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 encryption-test (displaced 3 1 init 3) (enc "ok" s-0)
    (0 0))
  (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 8)
  (parent 6)
  (unrealized)
  (shape)
  (maps ((0 1) ((b b) (n n) (s s) (a a) (s-0 s))))
  (origs (n (1 0))))

(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 9)
  (unrealized (0 1) (1 0))
  (origs (n (0 0)))
  (comment "2 in cohort - 2 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 10)
  (parent 9)
  (unrealized (0 1))
  (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))
  (precedes ((1 2) (0 0)))
  (non-orig s (privk b))
  (uniq-orig n)
  (operation encryption-test (displaced 0 2 init 3) (enc "ok" s) (1 0))
  (traces ((recv (enc "ok" s)))
    ((send (enc a n (pubk b))) (recv (enc n (pubk a)))
      (send (enc "ok" s))))
  (label 11)
  (parent 9)
  (unrealized (1 1))
  (origs (n (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))
  (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 12)
  (parent 10)
  (seen 13)
  (unrealized)
  (shape)
  (maps ((0 1) ((b b) (n n) (s s) (a a))))
  (origs (n (0 0)))
  (comment "1 in cohort - 0 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 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)))
    ((recv (enc a n (pubk b))) (send (enc n (pubk a)))))
  (label 13)
  (parent 11)
  (unrealized)
  (shape)
  (maps ((1 0) ((b b) (n n) (s s) (a a))))
  (origs (n (1 0))))

(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 14)
  (unrealized (0 0) (1 1))
  (origs (n (1 0)))
  (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 15)
  (parent 14)
  (unrealized (0 0))
  (comment "2 in cohort - 2 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 16)
  (parent 15)
  (seen 17)
  (unrealized)
  (shape)
  (maps ((0 1) ((b b) (n n) (s s) (a a))))
  (origs (n (1 0)))
  (comment "1 in cohort - 0 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 encryption-test (displaced 1 3 init 3) (enc "ok" s) (0 0))
  (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 17)
  (parent 15)
  (unrealized)
  (shape)
  (maps ((0 2) ((b b) (n n) (s s) (a a))))
  (origs (n (2 0))))

(comment "Nothing left to do")