(comment "CPSA 3.4.0")
(comment "All input read from kerb.scm")

Trees: 0 5.

Tree 0.

4 3 2 1 0 
(defprotocol kerb-flawed basic
  (defrole init
    (vars (a b s name) (m n text) (k skey))
    (trace (send (cat a b n))
      (recv (cat (enc k n (ltk a s)) (enc k a b (ltk b s))))
      (send (cat (enc m k) (enc k a b (ltk b s)))))
    (uniq-orig n))
  (defrole resp
    (vars (a b s name) (m text) (k skey))
    (trace (recv (cat (enc m k) (enc k a b (ltk b s))))))
  (defrole keyserv
    (vars (a b s name) (n text) (k skey))
    (trace (recv (cat a b n))
      (send (cat (enc k n (ltk a s)) (enc k a b (ltk b s)))))
    (uniq-orig k)))

Item 0, Child: 1.

m m (cat (enc m k) (enc k a b (ltk b s))) (cat (enc k n (ltk a s)) (enc k a b (ltk b s))) (cat a b n) ((m m) (n n) (a a) (b b) (s s) (k k)) init kerb-flawed 0
(defskeleton kerb-flawed
  (vars (m n text) (a b s name) (k skey))
  (defstrand init 3 (m m) (n n) (a a) (b b) (s s) (k k))
  (deflistener m)
  (non-orig (ltk a s) (ltk b s))
  (uniq-orig m n)
  (label 0)
  (unrealized (0 1) (1 0))
  (preskeleton)
  (comment "Not a skeleton"))

Item 1, Parent: 0, Child: 2.

m m (cat (enc m k) (enc k a b (ltk b s))) (cat (enc k n (ltk a s)) (enc k a b (ltk b s))) (cat a b n) ((m m) (n n) (a a) (b b) (s s) (k k)) init kerb-flawed 1
(defskeleton kerb-flawed
  (vars (m n text) (a b s name) (k skey))
  (defstrand init 3 (m m) (n n) (a a) (b b) (s s) (k k))
  (deflistener m)
  (precedes ((0 2) (1 0)))
  (non-orig (ltk a s) (ltk b s))
  (uniq-orig m n)
  (label 1)
  (parent 0)
  (unrealized (0 1))
  (origs (n (0 0)) (m (0 2)))
  (comment "1 in cohort - 1 not yet seen"))

Item 2, Parent: 1, Child: 3.

(cat (enc k n (ltk a s)) (enc k a b-0 (ltk b-0 s))) (cat a b-0 n) m m (cat (enc m k) (enc k a b (ltk b s))) (cat (enc k n (ltk a s)) (enc k a b (ltk b s))) (cat a b n) ((n n) (a a) (b b-0) (s s) (k k)) keyserv ((m m) (n n) (a a) (b b) (s s) (k k)) init kerb-flawed 2
(defskeleton kerb-flawed
  (vars (m n text) (a b s b-0 name) (k skey))
  (defstrand init 3 (m m) (n n) (a a) (b b) (s s) (k k))
  (deflistener m)
  (defstrand keyserv 2 (n n) (a a) (b b-0) (s s) (k k))
  (precedes ((0 0) (2 0)) ((0 2) (1 0)) ((2 1) (0 1)))
  (non-orig (ltk a s) (ltk b s))
  (uniq-orig m n k)
  (operation encryption-test (added-strand keyserv 2)
    (enc k n (ltk a s)) (0 1))
  (label 2)
  (parent 1)
  (unrealized (0 1))
  (comment "1 in cohort - 1 not yet seen"))

Item 3, Parent: 2, Child: 4.

(cat (enc k n (ltk a s)) (enc k a b (ltk b s))) (cat a b n) m m (cat (enc m k) (enc k a b (ltk b s))) (cat (enc k n (ltk a s)) (enc k a b (ltk b s))) (cat a b n) ((n n) (a a) (b b) (s s) (k k)) keyserv ((m m) (n n) (a a) (b b) (s s) (k k)) init kerb-flawed 3
(defskeleton kerb-flawed
  (vars (m n text) (a s b name) (k skey))
  (defstrand init 3 (m m) (n n) (a a) (b b) (s s) (k k))
  (deflistener m)
  (defstrand keyserv 2 (n n) (a a) (b b) (s s) (k k))
  (precedes ((0 0) (2 0)) ((0 2) (1 0)) ((2 1) (0 1)))
  (non-orig (ltk a s) (ltk b s))
  (uniq-orig m n k)
  (operation encryption-test (displaced 3 2 keyserv 2)
    (enc k a b-0 (ltk b-0 s)) (0 1))
  (label 3)
  (parent 2)
  (unrealized (1 0))
  (comment "1 in cohort - 1 not yet seen"))

Item 4, Parent: 3.

k k (cat (enc k n (ltk a s)) (enc k a b (ltk b s))) (cat a b n) m m (cat (enc m k) (enc k a b (ltk b s))) (cat (enc k n (ltk a s)) (enc k a b (ltk b s))) (cat a b n) ((n n) (a a) (b b) (s s) (k k)) keyserv ((m m) (n n) (a a) (b b) (s s) (k k)) init kerb-flawed 4
(defskeleton kerb-flawed
  (vars (m n text) (a s b name) (k skey))
  (defstrand init 3 (m m) (n n) (a a) (b b) (s s) (k k))
  (deflistener m)
  (defstrand keyserv 2 (n n) (a a) (b b) (s s) (k k))
  (deflistener k)
  (precedes ((0 0) (2 0)) ((0 2) (1 0)) ((2 1) (0 1)) ((2 1) (3 0))
    ((3 1) (1 0)))
  (non-orig (ltk a s) (ltk b s))
  (uniq-orig m n k)
  (operation nonce-test (added-listener k) m (1 0) (enc m k))
  (label 4)
  (parent 3)
  (unrealized (3 0))
  (comment "empty cohort"))

Tree 5.

7 6 5 
(defprotocol kerb-flawed2 basic
  (defrole init
    (vars (a b s name) (ticket mesg) (m n text) (k skey))
    (trace (send (cat a b n)) (recv (cat (enc k n (ltk a s)) ticket))
      (send (cat (enc m k) ticket)))
    (uniq-orig n))
  (defrole resp
    (vars (a b s name) (m text) (k skey))
    (trace (recv (cat (enc m k) (enc k a b (ltk b s))))))
  (defrole keyserv
    (vars (a b s name) (n text) (k skey))
    (trace (recv (cat a b n))
      (send (cat (enc k n (ltk a s)) (enc k a b (ltk b s)))))
    (uniq-orig k)))

Item 5, Child: 6.

m m (cat (enc m k) ticket) (cat (enc k n (ltk a s)) ticket) (cat a b n) ((ticket ticket) (m m) (n n) (a a) (b b) (s s) (k k)) init kerb-flawed2 5
(defskeleton kerb-flawed2
  (vars (ticket mesg) (m n text) (a b s name) (k skey))
  (defstrand init 3 (ticket ticket) (m m) (n n) (a a) (b b) (s s) (k k))
  (deflistener m)
  (non-orig (ltk a s) (ltk b s))
  (uniq-orig m n)
  (label 5)
  (unrealized (0 1) (1 0))
  (preskeleton)
  (comment "Not a skeleton"))

Item 6, Parent: 5, Child: 7.

m m (cat (enc m k) ticket) (cat (enc k n (ltk a s)) ticket) (cat a b n) ((ticket ticket) (m m) (n n) (a a) (b b) (s s) (k k)) init kerb-flawed2 6
(defskeleton kerb-flawed2
  (vars (ticket mesg) (m n text) (a b s name) (k skey))
  (defstrand init 3 (ticket ticket) (m m) (n n) (a a) (b b) (s s) (k k))
  (deflistener m)
  (precedes ((0 2) (1 0)))
  (non-orig (ltk a s) (ltk b s))
  (uniq-orig m n)
  (label 6)
  (parent 5)
  (unrealized (0 1))
  (origs (n (0 0)) (m (0 2)))
  (comment "1 in cohort - 1 not yet seen"))

Item 7, Parent: 6.

(cat (enc k n (ltk a s)) (enc k a b-0 (ltk b-0 s))) (cat a b-0 n) m m (cat (enc m k) ticket) (cat (enc k n (ltk a s)) ticket) (cat a b n) ((n n) (a a) (b b-0) (s s) (k k)) keyserv ((ticket ticket) (m m) (n n) (a a) (b b) (s s) (k k)) init kerb-flawed2 7 (realized) 
(defskeleton kerb-flawed2
  (vars (ticket mesg) (m n text) (a b s b-0 name) (k skey))
  (defstrand init 3 (ticket ticket) (m m) (n n) (a a) (b b) (s s) (k k))
  (deflistener m)
  (defstrand keyserv 2 (n n) (a a) (b b-0) (s s) (k k))
  (precedes ((0 0) (2 0)) ((0 2) (1 0)) ((2 1) (0 1)))
  (non-orig (ltk a s) (ltk b s))
  (uniq-orig m n k)
  (operation encryption-test (added-strand keyserv 2)
    (enc k n (ltk a s)) (0 1))
  (label 7)
  (parent 6)
  (unrealized)
  (shape)
  (maps ((0 1) ((a a) (b b) (s s) (m m) (ticket ticket) (n n) (k k))))
  (origs (k (2 1)) (n (0 0)) (m (0 2))))