(herald "Kerberos PKINIT")
(comment "CPSA 3.4.0")
(comment "All input read from pkinit.scm")

Trees: 0 2 8 13 16 23.

Tree 0.

1 0 
(defprotocol pkinit-flawed basic
  (defrole client
    (vars (c t as name) (n2 n1 text) (tc tk tgt data) (k ak skey))
    (trace (send (cat (enc tc n2 (privk c)) c t n1))
      (recv
        (cat (enc (enc k n2 (privk as)) (pubk c)) c tgt
          (enc ak n1 tk t k))))
    (uniq-orig n2 n1))
  (defrole auth
    (vars (c t as name) (n2 n1 text) (tc tk tgt data) (k ak skey))
    (trace (recv (cat (enc tc n2 (privk c)) c t n1))
      (send
        (cat (enc (enc k n2 (privk as)) (pubk c)) c tgt
          (enc ak n1 tk t k))))
    (uniq-orig k ak)))

Item 0, Child: 1.

(cat (enc (enc k n2 (privk as)) (pubk c)) c tgt (enc ak n1 tk t k)) (cat (enc tc n2 (privk c)) c t n1) ((n2 n2) (n1 n1) (tc tc) (tk tk) (tgt tgt) (c c) (t t) (as as) (k k) (ak ak)) client pkinit-flawed 0
(defskeleton pkinit-flawed
  (vars (n2 n1 text) (tc tk tgt data) (c as t name) (k ak skey))
  (defstrand client 2 (n2 n2) (n1 n1) (tc tc) (tk tk) (tgt tgt) (c c)
    (t t) (as as) (k k) (ak ak))
  (non-orig (privk c) (privk as))
  (uniq-orig n2 n1)
  (goals
    (forall ((c as name) (k skey) (z node))
      (implies
        (and (p "client" 1 z) (p "client" "c" z c)
          (p "client" "as" z as) (p "client" "k" z k) (non (privk as))
          (non (privk c)))
        (exists ((z-0 node))
          (and (p "auth" 1 z-0) (p "auth" "as" z-0 as)
            (p "auth" "k" z-0 k) (p "auth" "c" z-0 c))))))
  (label 0)
  (unrealized (0 1))
  (origs (n1 (0 0)) (n2 (0 0)))
  (comment "1 in cohort - 1 not yet seen"))

Item 1, Parent: 0.

(cat (enc (enc k n2 (privk as)) (pubk c-0)) c-0 tgt-0 (enc ak-0 n1-0 tk-0 t-0 k)) (cat (enc tc-0 n2 (privk c-0)) c-0 t-0 n1-0) (cat (enc (enc k n2 (privk as)) (pubk c)) c tgt (enc ak n1 tk t k)) (cat (enc tc n2 (privk c)) c t n1) ((n2 n2) (n1 n1-0) (tc tc-0) (tk tk-0) (tgt tgt-0) (c c-0) (t t-0) (as as) (k k) (ak ak-0)) auth ((n2 n2) (n1 n1) (tc tc) (tk tk) (tgt tgt) (c c) (t t) (as as) (k k) (ak ak)) client pkinit-flawed 1 (realized) 
(defskeleton pkinit-flawed
  (vars (n2 n1 n1-0 text) (tc tk tgt tc-0 tk-0 tgt-0 data)
    (c as t c-0 t-0 name) (k ak ak-0 skey))
  (defstrand client 2 (n2 n2) (n1 n1) (tc tc) (tk tk) (tgt tgt) (c c)
    (t t) (as as) (k k) (ak ak))
  (defstrand auth 2 (n2 n2) (n1 n1-0) (tc tc-0) (tk tk-0) (tgt tgt-0)
    (c c-0) (t t-0) (as as) (k k) (ak ak-0))
  (precedes ((0 0) (1 0)) ((1 1) (0 1)))
  (non-orig (privk c) (privk as))
  (uniq-orig n2 n1 k ak-0)
  (operation encryption-test (added-strand auth 2) (enc k n2 (privk as))
    (0 1))
  (label 1)
  (parent 0)
  (unrealized)
  (shape)
  (satisfies (no (c c) (as as) (k k) (z (0 1))))
  (maps
    ((0)
      ((c c) (as as) (k k) (t t) (n2 n2) (n1 n1) (tc tc) (tk tk)
        (tgt tgt) (ak ak))))
  (origs (k (1 1)) (ak-0 (1 1)) (n1 (0 0)) (n2 (0 0))))

Tree 2.

7 6 5 4 3 2 
(defprotocol pkinit-fix1 basic
  (defrole client
    (vars (c t as name) (n2 n1 text) (tc tk tgt data) (k ak skey))
    (trace (send (cat (enc tc n2 (privk c)) c t n1))
      (recv
        (cat (enc (enc k n2 c (privk as)) (pubk c)) c tgt
          (enc ak n1 tk t k))))
    (uniq-orig n2 n1))
  (defrole auth
    (vars (c t as name) (n2 n1 text) (tc tk tgt data) (k ak skey))
    (trace (recv (cat (enc tc n2 (privk c)) c t n1))
      (send
        (cat (enc (enc k n2 c (privk as)) (pubk c)) c tgt
          (enc ak n1 tk t k))))
    (uniq-orig k ak)))

Item 2, Child: 3.

(cat (enc (enc k n2 c (privk as)) (pubk c)) c tgt (enc ak n1 tk t k)) (cat (enc tc n2 (privk c)) c t n1) ((n2 n2) (n1 n1) (tc tc) (tk tk) (tgt tgt) (c c) (t t) (as as) (k k) (ak ak)) client pkinit-fix1 2
(defskeleton pkinit-fix1
  (vars (n2 n1 text) (tc tk tgt data) (c as t name) (k ak skey))
  (defstrand client 2 (n2 n2) (n1 n1) (tc tc) (tk tk) (tgt tgt) (c c)
    (t t) (as as) (k k) (ak ak))
  (non-orig (privk c) (privk as))
  (uniq-orig n2 n1)
  (goals
    (forall ((c as name) (k skey) (z node))
      (implies
        (and (p "client" 1 z) (p "client" "c" z c)
          (p "client" "as" z as) (p "client" "k" z k) (non (privk as))
          (non (privk c)))
        (exists ((z-0 node))
          (and (p "auth" 1 z-0) (p "auth" "as" z-0 as)
            (p "auth" "k" z-0 k) (p "auth" "c" z-0 c))))))
  (label 2)
  (unrealized (0 1))
  (origs (n1 (0 0)) (n2 (0 0)))
  (comment "1 in cohort - 1 not yet seen"))

Item 3, Parent: 2, Child: 4.

(cat (enc (enc k n2 c (privk as)) (pubk c)) c tgt-0 (enc ak-0 n1-0 tk-0 t-0 k)) (cat (enc tc-0 n2 (privk c)) c t-0 n1-0) (cat (enc (enc k n2 c (privk as)) (pubk c)) c tgt (enc ak n1 tk t k)) (cat (enc tc n2 (privk c)) c t n1) ((n2 n2) (n1 n1-0) (tc tc-0) (tk tk-0) (tgt tgt-0) (c c) (t t-0) (as as) (k k) (ak ak-0)) auth ((n2 n2) (n1 n1) (tc tc) (tk tk) (tgt tgt) (c c) (t t) (as as) (k k) (ak ak)) client pkinit-fix1 3
(defskeleton pkinit-fix1
  (vars (n2 n1 n1-0 text) (tc tk tgt tc-0 tk-0 tgt-0 data)
    (c as t t-0 name) (k ak ak-0 skey))
  (defstrand client 2 (n2 n2) (n1 n1) (tc tc) (tk tk) (tgt tgt) (c c)
    (t t) (as as) (k k) (ak ak))
  (defstrand auth 2 (n2 n2) (n1 n1-0) (tc tc-0) (tk tk-0) (tgt tgt-0)
    (c c) (t t-0) (as as) (k k) (ak ak-0))
  (precedes ((0 0) (1 0)) ((1 1) (0 1)))
  (non-orig (privk c) (privk as))
  (uniq-orig n2 n1 k ak-0)
  (operation encryption-test (added-strand auth 2)
    (enc k n2 c (privk as)) (0 1))
  (label 3)
  (parent 2)
  (unrealized (0 1) (1 0))
  (comment "1 in cohort - 1 not yet seen"))

Item 4, Parent: 3, Children: 5 6.

(cat (enc (enc k n2 c (privk as)) (pubk c)) c tgt-0 (enc ak-0 n1-0 tk-0 t-0 k)) (cat (enc tc n2 (privk c)) c t-0 n1-0) (cat (enc (enc k n2 c (privk as)) (pubk c)) c tgt (enc ak n1 tk t k)) (cat (enc tc n2 (privk c)) c t n1) ((n2 n2) (n1 n1-0) (tc tc) (tk tk-0) (tgt tgt-0) (c c) (t t-0) (as as) (k k) (ak ak-0)) auth ((n2 n2) (n1 n1) (tc tc) (tk tk) (tgt tgt) (c c) (t t) (as as) (k k) (ak ak)) client pkinit-fix1 4
(defskeleton pkinit-fix1
  (vars (n2 n1 n1-0 text) (tc tk tgt tk-0 tgt-0 data) (c as t t-0 name)
    (k ak ak-0 skey))
  (defstrand client 2 (n2 n2) (n1 n1) (tc tc) (tk tk) (tgt tgt) (c c)
    (t t) (as as) (k k) (ak ak))
  (defstrand auth 2 (n2 n2) (n1 n1-0) (tc tc) (tk tk-0) (tgt tgt-0)
    (c c) (t t-0) (as as) (k k) (ak ak-0))
  (precedes ((0 0) (1 0)) ((1 1) (0 1)))
  (non-orig (privk c) (privk as))
  (uniq-orig n2 n1 k ak-0)
  (operation encryption-test (displaced 2 0 client 1)
    (enc tc-0 n2 (privk c)) (1 0))
  (label 4)
  (parent 3)
  (unrealized (0 1))
  (comment "2 in cohort - 2 not yet seen"))

Item 5, Parent: 4.

(cat (enc (enc k n2 c (privk as)) (pubk c)) c tgt-0 (enc ak n1 tk t k)) (cat (enc tc n2 (privk c)) c t n1) (cat (enc (enc k n2 c (privk as)) (pubk c)) c tgt (enc ak n1 tk t k)) (cat (enc tc n2 (privk c)) c t n1) ((n2 n2) (n1 n1) (tc tc) (tk tk) (tgt tgt-0) (c c) (t t) (as as) (k k) (ak ak)) auth ((n2 n2) (n1 n1) (tc tc) (tk tk) (tgt tgt) (c c) (t t) (as as) (k k) (ak ak)) client pkinit-fix1 5 (realized) 
(defskeleton pkinit-fix1
  (vars (n2 n1 text) (tc tgt tk tgt-0 data) (c as t name) (k ak skey))
  (defstrand client 2 (n2 n2) (n1 n1) (tc tc) (tk tk) (tgt tgt) (c c)
    (t t) (as as) (k k) (ak ak))
  (defstrand auth 2 (n2 n2) (n1 n1) (tc tc) (tk tk) (tgt tgt-0) (c c)
    (t t) (as as) (k k) (ak ak))
  (precedes ((0 0) (1 0)) ((1 1) (0 1)))
  (non-orig (privk c) (privk as))
  (uniq-orig n2 n1 k ak)
  (operation encryption-test (displaced 2 1 auth 2)
    (enc ak-0 n1-0 tk-0 t-0 k) (0 1))
  (label 5)
  (parent 4)
  (unrealized)
  (shape)
  (satisfies yes)
  (maps
    ((0)
      ((c c) (as as) (k k) (t t) (n2 n2) (n1 n1) (tc tc) (tk tk)
        (tgt tgt) (ak ak))))
  (origs (k (1 1)) (ak (1 1)) (n1 (0 0)) (n2 (0 0))))

Item 6, Parent: 4, Child: 7.

k k (cat (enc (enc k n2 c (privk as)) (pubk c)) c tgt-0 (enc ak-0 n1-0 tk-0 t-0 k)) (cat (enc tc n2 (privk c)) c t-0 n1-0) (cat (enc (enc k n2 c (privk as)) (pubk c)) c tgt (enc ak n1 tk t k)) (cat (enc tc n2 (privk c)) c t n1) ((n2 n2) (n1 n1-0) (tc tc) (tk tk-0) (tgt tgt-0) (c c) (t t-0) (as as) (k k) (ak ak-0)) auth ((n2 n2) (n1 n1) (tc tc) (tk tk) (tgt tgt) (c c) (t t) (as as) (k k) (ak ak)) client pkinit-fix1 6
(defskeleton pkinit-fix1
  (vars (n2 n1 n1-0 text) (tc tk tgt tk-0 tgt-0 data) (c as t t-0 name)
    (k ak ak-0 skey))
  (defstrand client 2 (n2 n2) (n1 n1) (tc tc) (tk tk) (tgt tgt) (c c)
    (t t) (as as) (k k) (ak ak))
  (defstrand auth 2 (n2 n2) (n1 n1-0) (tc tc) (tk tk-0) (tgt tgt-0)
    (c c) (t t-0) (as as) (k k) (ak ak-0))
  (deflistener k)
  (precedes ((0 0) (1 0)) ((1 1) (2 0)) ((2 1) (0 1)))
  (non-orig (privk c) (privk as))
  (uniq-orig n2 n1 k ak-0)
  (operation encryption-test (added-listener k) (enc ak n1 tk t k)
    (0 1))
  (label 6)
  (parent 4)
  (unrealized (2 0))
  (comment "1 in cohort - 1 not yet seen"))

Item 7, Parent: 6.

ak-0 ak-0 (cat (enc (enc ak-0 n2 c (privk as)) (pubk c)) c tgt-0 (enc ak-0 n1-0 tk-0 t-0 ak-0)) (cat (enc tc n2 (privk c)) c t-0 n1-0) (cat (enc (enc ak-0 n2 c (privk as)) (pubk c)) c tgt (enc ak n1 tk t ak-0)) (cat (enc tc n2 (privk c)) c t n1) ((n2 n2) (n1 n1-0) (tc tc) (tk tk-0) (tgt tgt-0) (c c) (t t-0) (as as) (k ak-0) (ak ak-0)) auth ((n2 n2) (n1 n1) (tc tc) (tk tk) (tgt tgt) (c c) (t t) (as as) (k ak-0) (ak ak)) client pkinit-fix1 7
(defskeleton pkinit-fix1
  (vars (n2 n1 n1-0 text) (tc tk tgt tk-0 tgt-0 data) (c as t t-0 name)
    (ak ak-0 skey))
  (defstrand client 2 (n2 n2) (n1 n1) (tc tc) (tk tk) (tgt tgt) (c c)
    (t t) (as as) (k ak-0) (ak ak))
  (defstrand auth 2 (n2 n2) (n1 n1-0) (tc tc) (tk tk-0) (tgt tgt-0)
    (c c) (t t-0) (as as) (k ak-0) (ak ak-0))
  (deflistener ak-0)
  (precedes ((0 0) (1 0)) ((1 1) (2 0)) ((2 1) (0 1)))
  (non-orig (privk c) (privk as))
  (uniq-orig n2 n1 ak-0)
  (operation nonce-test (displaced 3 1 auth 2) k (2 0)
    (enc (enc k n2 c (privk as)) (pubk c)))
  (label 7)
  (parent 6)
  (unrealized (2 0))
  (comment "empty cohort"))

Tree 8.

12 11 10 9 8 
(defprotocol pkinit-fix2 basic
  (defrole client
    (vars (c t as name) (n2 n1 text) (tc tk tgt data) (k ak skey))
    (trace (send (cat (enc tc n2 (privk c)) c t n1))
      (recv
        (cat
          (enc (enc k (hash (enc tc n2 (privk c)) c t n1) (privk as))
            (pubk c)) c tgt (enc ak n1 tk t k))))
    (uniq-orig n2 n1))
  (defrole auth
    (vars (c t as name) (n2 n1 text) (tc tk tgt data) (k ak skey))
    (trace (recv (cat (enc tc n2 (privk c)) c t n1))
      (send
        (cat
          (enc (enc k (hash (enc tc n2 (privk c)) c t n1) (privk as))
            (pubk c)) c tgt (enc ak n1 tk t k))))
    (uniq-orig k ak)))

Item 8, Child: 9.

(cat (enc (enc k (hash (enc tc n2 (privk c)) c t n1) (privk as)) (pubk c)) c tgt (enc ak n1 tk t k)) (cat (enc tc n2 (privk c)) c t n1) ((n2 n2) (n1 n1) (tc tc) (tk tk) (tgt tgt) (c c) (t t) (as as) (k k) (ak ak)) client pkinit-fix2 8
(defskeleton pkinit-fix2
  (vars (n2 n1 text) (tc tk tgt data) (c as t name) (k ak skey))
  (defstrand client 2 (n2 n2) (n1 n1) (tc tc) (tk tk) (tgt tgt) (c c)
    (t t) (as as) (k k) (ak ak))
  (non-orig (privk c) (privk as))
  (uniq-orig n2 n1)
  (goals
    (forall ((c as name) (k skey) (z node))
      (implies
        (and (p "client" 1 z) (p "client" "c" z c)
          (p "client" "as" z as) (p "client" "k" z k) (non (privk as))
          (non (privk c)))
        (exists ((z-0 node))
          (and (p "auth" 1 z-0) (p "auth" "as" z-0 as)
            (p "auth" "k" z-0 k) (p "auth" "c" z-0 c))))))
  (label 8)
  (unrealized (0 1))
  (origs (n1 (0 0)) (n2 (0 0)))
  (comment "1 in cohort - 1 not yet seen"))

Item 9, Parent: 8, Children: 10 11.

(cat (enc (enc k (hash (enc tc n2 (privk c)) c t n1) (privk as)) (pubk c)) c tgt-0 (enc ak-0 n1 tk-0 t k)) (cat (enc tc n2 (privk c)) c t n1) (cat (enc (enc k (hash (enc tc n2 (privk c)) c t n1) (privk as)) (pubk c)) c tgt (enc ak n1 tk t k)) (cat (enc tc n2 (privk c)) c t n1) ((n2 n2) (n1 n1) (tc tc) (tk tk-0) (tgt tgt-0) (c c) (t t) (as as) (k k) (ak ak-0)) auth ((n2 n2) (n1 n1) (tc tc) (tk tk) (tgt tgt) (c c) (t t) (as as) (k k) (ak ak)) client pkinit-fix2 9
(defskeleton pkinit-fix2
  (vars (n2 n1 text) (tc tk tgt tk-0 tgt-0 data) (c as t name)
    (k ak ak-0 skey))
  (defstrand client 2 (n2 n2) (n1 n1) (tc tc) (tk tk) (tgt tgt) (c c)
    (t t) (as as) (k k) (ak ak))
  (defstrand auth 2 (n2 n2) (n1 n1) (tc tc) (tk tk-0) (tgt tgt-0) (c c)
    (t t) (as as) (k k) (ak ak-0))
  (precedes ((0 0) (1 0)) ((1 1) (0 1)))
  (non-orig (privk c) (privk as))
  (uniq-orig n2 n1 k ak-0)
  (operation encryption-test (added-strand auth 2)
    (enc k (hash (enc tc n2 (privk c)) c t n1) (privk as)) (0 1))
  (label 9)
  (parent 8)
  (unrealized (0 1))
  (comment "2 in cohort - 2 not yet seen"))

Item 10, Parent: 9.

(cat (enc (enc k (hash (enc tc n2 (privk c)) c t n1) (privk as)) (pubk c)) c tgt-0 (enc ak n1 tk t k)) (cat (enc tc n2 (privk c)) c t n1) (cat (enc (enc k (hash (enc tc n2 (privk c)) c t n1) (privk as)) (pubk c)) c tgt (enc ak n1 tk t k)) (cat (enc tc n2 (privk c)) c t n1) ((n2 n2) (n1 n1) (tc tc) (tk tk) (tgt tgt-0) (c c) (t t) (as as) (k k) (ak ak)) auth ((n2 n2) (n1 n1) (tc tc) (tk tk) (tgt tgt) (c c) (t t) (as as) (k k) (ak ak)) client pkinit-fix2 10 (realized) 
(defskeleton pkinit-fix2
  (vars (n2 n1 text) (tc tgt tk tgt-0 data) (c as t name) (k ak skey))
  (defstrand client 2 (n2 n2) (n1 n1) (tc tc) (tk tk) (tgt tgt) (c c)
    (t t) (as as) (k k) (ak ak))
  (defstrand auth 2 (n2 n2) (n1 n1) (tc tc) (tk tk) (tgt tgt-0) (c c)
    (t t) (as as) (k k) (ak ak))
  (precedes ((0 0) (1 0)) ((1 1) (0 1)))
  (non-orig (privk c) (privk as))
  (uniq-orig n2 n1 k ak)
  (operation encryption-test (displaced 2 1 auth 2)
    (enc ak-0 n1 tk-0 t k) (0 1))
  (label 10)
  (parent 9)
  (unrealized)
  (shape)
  (satisfies yes)
  (maps
    ((0)
      ((c c) (as as) (k k) (t t) (n2 n2) (n1 n1) (tc tc) (tk tk)
        (tgt tgt) (ak ak))))
  (origs (k (1 1)) (ak (1 1)) (n1 (0 0)) (n2 (0 0))))

Item 11, Parent: 9, Child: 12.

k k (cat (enc (enc k (hash (enc tc n2 (privk c)) c t n1) (privk as)) (pubk c)) c tgt-0 (enc ak-0 n1 tk-0 t k)) (cat (enc tc n2 (privk c)) c t n1) (cat (enc (enc k (hash (enc tc n2 (privk c)) c t n1) (privk as)) (pubk c)) c tgt (enc ak n1 tk t k)) (cat (enc tc n2 (privk c)) c t n1) ((n2 n2) (n1 n1) (tc tc) (tk tk-0) (tgt tgt-0) (c c) (t t) (as as) (k k) (ak ak-0)) auth ((n2 n2) (n1 n1) (tc tc) (tk tk) (tgt tgt) (c c) (t t) (as as) (k k) (ak ak)) client pkinit-fix2 11
(defskeleton pkinit-fix2
  (vars (n2 n1 text) (tc tk tgt tk-0 tgt-0 data) (c as t name)
    (k ak ak-0 skey))
  (defstrand client 2 (n2 n2) (n1 n1) (tc tc) (tk tk) (tgt tgt) (c c)
    (t t) (as as) (k k) (ak ak))
  (defstrand auth 2 (n2 n2) (n1 n1) (tc tc) (tk tk-0) (tgt tgt-0) (c c)
    (t t) (as as) (k k) (ak ak-0))
  (deflistener k)
  (precedes ((0 0) (1 0)) ((1 1) (2 0)) ((2 1) (0 1)))
  (non-orig (privk c) (privk as))
  (uniq-orig n2 n1 k ak-0)
  (operation encryption-test (added-listener k) (enc ak n1 tk t k)
    (0 1))
  (label 11)
  (parent 9)
  (unrealized (2 0))
  (comment "1 in cohort - 1 not yet seen"))

Item 12, Parent: 11.

ak-0 ak-0 (cat (enc (enc ak-0 (hash (enc tc n2 (privk c)) c t n1) (privk as)) (pubk c)) c tgt-0 (enc ak-0 n1 tk-0 t ak-0)) (cat (enc tc n2 (privk c)) c t n1) (cat (enc (enc ak-0 (hash (enc tc n2 (privk c)) c t n1) (privk as)) (pubk c)) c tgt (enc ak n1 tk t ak-0)) (cat (enc tc n2 (privk c)) c t n1) ((n2 n2) (n1 n1) (tc tc) (tk tk-0) (tgt tgt-0) (c c) (t t) (as as) (k ak-0) (ak ak-0)) auth ((n2 n2) (n1 n1) (tc tc) (tk tk) (tgt tgt) (c c) (t t) (as as) (k ak-0) (ak ak)) client pkinit-fix2 12
(defskeleton pkinit-fix2
  (vars (n2 n1 text) (tc tk tgt tk-0 tgt-0 data) (c as t name)
    (ak ak-0 skey))
  (defstrand client 2 (n2 n2) (n1 n1) (tc tc) (tk tk) (tgt tgt) (c c)
    (t t) (as as) (k ak-0) (ak ak))
  (defstrand auth 2 (n2 n2) (n1 n1) (tc tc) (tk tk-0) (tgt tgt-0) (c c)
    (t t) (as as) (k ak-0) (ak ak-0))
  (deflistener ak-0)
  (precedes ((0 0) (1 0)) ((1 1) (2 0)) ((2 1) (0 1)))
  (non-orig (privk c) (privk as))
  (uniq-orig n2 n1 ak-0)
  (operation nonce-test (displaced 3 1 auth 2) k (2 0)
    (enc (enc k (hash (enc tc n2 (privk c)) c t n1) (privk as))
      (pubk c)))
  (label 12)
  (parent 11)
  (unrealized (2 0))
  (comment "empty cohort"))

Tree 13.

15 14 13 
(defprotocol pkinit-flawed basic
  (defrole client
    (vars (c t as name) (n2 n1 text) (tc tk tgt data) (k ak skey))
    (trace (send (cat (enc tc n2 (privk c)) c t n1))
      (recv
        (cat (enc (enc k n2 (privk as)) (pubk c)) c tgt
          (enc ak n1 tk t k))))
    (uniq-orig n2 n1))
  (defrole auth
    (vars (c t as name) (n2 n1 text) (tc tk tgt data) (k ak skey))
    (trace (recv (cat (enc tc n2 (privk c)) c t n1))
      (send
        (cat (enc (enc k n2 (privk as)) (pubk c)) c tgt
          (enc ak n1 tk t k))))
    (uniq-orig k ak)))

Item 13, Child: 14.

(cat (enc (enc k n2-0 (privk as)) (pubk c)) c tgt-0 (enc ak-0 n1-0 tk-0 t-0 k)) (cat (enc tc-0 n2-0 (privk c)) c t-0 n1-0) (cat (enc (enc k n2 (privk as-0)) (pubk c-0)) c-0 tgt (enc ak n1 tk t k)) (cat (enc tc n2 (privk c-0)) c-0 t n1) ((n2 n2-0) (n1 n1-0) (tc tc-0) (tk tk-0) (tgt tgt-0) (c c) (t t-0) (as as) (k k) (ak ak-0)) client ((n2 n2) (n1 n1) (tc tc) (tk tk) (tgt tgt) (c c-0) (t t) (as as-0) (k k) (ak ak)) auth pkinit-flawed 13
(defskeleton pkinit-flawed
  (vars (n2 n1 n2-0 n1-0 text) (tc tk tgt tc-0 tk-0 tgt-0 data)
    (c c-0 as t as-0 t-0 name) (k ak ak-0 skey))
  (defstrand auth 2 (n2 n2) (n1 n1) (tc tc) (tk tk) (tgt tgt) (c c-0)
    (t t) (as as-0) (k k) (ak ak))
  (defstrand client 2 (n2 n2-0) (n1 n1-0) (tc tc-0) (tk tk-0)
    (tgt tgt-0) (c c) (t t-0) (as as) (k k) (ak ak-0))
  (non-orig (privk c) (privk as))
  (uniq-orig n2-0 n1-0 k ak)
  (goals
    (forall ((c c-0 as name) (k skey) (z z-0 node))
      (implies
        (and (p "client" 1 z) (p "client" "c" z c)
          (p "client" "as" z as) (p "client" "k" z k) (p "auth" 1 z-0)
          (p "auth" "k" z-0 k) (p "auth" "c" z-0 c-0) (non (privk as))
          (non (privk c))) (= c c-0))))
  (label 13)
  (unrealized (1 1))
  (preskeleton)
  (comment "Not a skeleton"))

Item 14, Parent: 13, Child: 15.

(cat (enc (enc k n2-0 (privk as)) (pubk c)) c tgt-0 (enc ak-0 n1-0 tk-0 t-0 k)) (cat (enc tc-0 n2-0 (privk c)) c t-0 n1-0) (cat (enc (enc k n2 (privk as-0)) (pubk c-0)) c-0 tgt (enc ak n1 tk t k)) (cat (enc tc n2 (privk c-0)) c-0 t n1) ((n2 n2-0) (n1 n1-0) (tc tc-0) (tk tk-0) (tgt tgt-0) (c c) (t t-0) (as as) (k k) (ak ak-0)) client ((n2 n2) (n1 n1) (tc tc) (tk tk) (tgt tgt) (c c-0) (t t) (as as-0) (k k) (ak ak)) auth pkinit-flawed 14
(defskeleton pkinit-flawed
  (vars (n2 n1 n2-0 n1-0 text) (tc tk tgt tc-0 tk-0 tgt-0 data)
    (c c-0 as t as-0 t-0 name) (k ak ak-0 skey))
  (defstrand auth 2 (n2 n2) (n1 n1) (tc tc) (tk tk) (tgt tgt) (c c-0)
    (t t) (as as-0) (k k) (ak ak))
  (defstrand client 2 (n2 n2-0) (n1 n1-0) (tc tc-0) (tk tk-0)
    (tgt tgt-0) (c c) (t t-0) (as as) (k k) (ak ak-0))
  (precedes ((0 1) (1 1)))
  (non-orig (privk c) (privk as))
  (uniq-orig n2-0 n1-0 k ak)
  (goals
    (forall ((c c-0 as name) (k skey) (z z-0 node))
      (implies
        (and (p "client" 1 z) (p "client" "c" z c)
          (p "client" "as" z as) (p "client" "k" z k) (p "auth" 1 z-0)
          (p "auth" "k" z-0 k) (p "auth" "c" z-0 c-0) (non (privk as))
          (non (privk c))) (= c c-0))))
  (label 14)
  (parent 13)
  (unrealized (1 1))
  (origs (n1-0 (1 0)) (n2-0 (1 0)) (k (0 1)) (ak (0 1)))
  (comment "1 in cohort - 1 not yet seen"))

Item 15, Parent: 14.

(cat (enc (enc k n2 (privk as)) (pubk c)) c tgt-0 (enc ak-0 n1-0 tk-0 t-0 k)) (cat (enc tc-0 n2 (privk c)) c t-0 n1-0) (cat (enc (enc k n2 (privk as)) (pubk c-0)) c-0 tgt (enc ak n1 tk t k)) (cat (enc tc n2 (privk c-0)) c-0 t n1) ((n2 n2) (n1 n1-0) (tc tc-0) (tk tk-0) (tgt tgt-0) (c c) (t t-0) (as as) (k k) (ak ak-0)) client ((n2 n2) (n1 n1) (tc tc) (tk tk) (tgt tgt) (c c-0) (t t) (as as) (k k) (ak ak)) auth pkinit-flawed 15 (realized) 
(defskeleton pkinit-flawed
  (vars (n2 n1 n1-0 text) (tc tk tgt tc-0 tk-0 tgt-0 data)
    (c c-0 t as t-0 name) (k ak ak-0 skey))
  (defstrand auth 2 (n2 n2) (n1 n1) (tc tc) (tk tk) (tgt tgt) (c c-0)
    (t t) (as as) (k k) (ak ak))
  (defstrand client 2 (n2 n2) (n1 n1-0) (tc tc-0) (tk tk-0) (tgt tgt-0)
    (c c) (t t-0) (as as) (k k) (ak ak-0))
  (precedes ((0 1) (1 1)) ((1 0) (0 0)))
  (non-orig (privk c) (privk as))
  (uniq-orig n2 n1-0 k ak)
  (operation encryption-test (displaced 2 0 auth 2)
    (enc k n2-0 (privk as-0)) (1 1))
  (label 15)
  (parent 14)
  (unrealized)
  (shape)
  (satisfies (no (c c) (c-0 c-0) (as as) (k k) (z (1 1)) (z-0 (0 1))))
  (maps
    ((0 1)
      ((c c) (c-0 c-0) (as as) (k k) (t t) (as-0 as) (n2 n2) (n1 n1)
        (tc tc) (tk tk) (tgt tgt) (ak ak) (t-0 t-0) (n2-0 n2)
        (n1-0 n1-0) (tc-0 tc-0) (tk-0 tk-0) (tgt-0 tgt-0) (ak-0 ak-0))))
  (origs (k (0 1)) (ak (0 1)) (n1-0 (1 0)) (n2 (1 0))))

Tree 16.

22 20 21 19 18 17 16 
(defprotocol pkinit-fix1 basic
  (defrole client
    (vars (c t as name) (n2 n1 text) (tc tk tgt data) (k ak skey))
    (trace (send (cat (enc tc n2 (privk c)) c t n1))
      (recv
        (cat (enc (enc k n2 c (privk as)) (pubk c)) c tgt
          (enc ak n1 tk t k))))
    (uniq-orig n2 n1))
  (defrole auth
    (vars (c t as name) (n2 n1 text) (tc tk tgt data) (k ak skey))
    (trace (recv (cat (enc tc n2 (privk c)) c t n1))
      (send
        (cat (enc (enc k n2 c (privk as)) (pubk c)) c tgt
          (enc ak n1 tk t k))))
    (uniq-orig k ak)))

Item 16, Child: 17.

(cat (enc (enc k n2-0 c (privk as)) (pubk c)) c tgt-0 (enc ak-0 n1-0 tk-0 t-0 k)) (cat (enc tc-0 n2-0 (privk c)) c t-0 n1-0) (cat (enc (enc k n2 c-0 (privk as-0)) (pubk c-0)) c-0 tgt (enc ak n1 tk t k)) (cat (enc tc n2 (privk c-0)) c-0 t n1) ((n2 n2-0) (n1 n1-0) (tc tc-0) (tk tk-0) (tgt tgt-0) (c c) (t t-0) (as as) (k k) (ak ak-0)) client ((n2 n2) (n1 n1) (tc tc) (tk tk) (tgt tgt) (c c-0) (t t) (as as-0) (k k) (ak ak)) auth pkinit-fix1 16
(defskeleton pkinit-fix1
  (vars (n2 n1 n2-0 n1-0 text) (tc tk tgt tc-0 tk-0 tgt-0 data)
    (c c-0 as t as-0 t-0 name) (k ak ak-0 skey))
  (defstrand auth 2 (n2 n2) (n1 n1) (tc tc) (tk tk) (tgt tgt) (c c-0)
    (t t) (as as-0) (k k) (ak ak))
  (defstrand client 2 (n2 n2-0) (n1 n1-0) (tc tc-0) (tk tk-0)
    (tgt tgt-0) (c c) (t t-0) (as as) (k k) (ak ak-0))
  (non-orig (privk c) (privk as))
  (uniq-orig n2-0 n1-0 k ak)
  (goals
    (forall ((c c-0 as name) (k skey) (z z-0 node))
      (implies
        (and (p "client" 1 z) (p "client" "c" z c)
          (p "client" "as" z as) (p "client" "k" z k) (p "auth" 1 z-0)
          (p "auth" "k" z-0 k) (p "auth" "c" z-0 c-0) (non (privk as))
          (non (privk c))) (exists ((z-1 node)) (p "client" 1 z-1)))))
  (label 16)
  (unrealized (1 1))
  (preskeleton)
  (comment "Not a skeleton"))

Item 17, Parent: 16, Child: 18.

(cat (enc (enc k n2-0 c (privk as)) (pubk c)) c tgt-0 (enc ak-0 n1-0 tk-0 t-0 k)) (cat (enc tc-0 n2-0 (privk c)) c t-0 n1-0) (cat (enc (enc k n2 c-0 (privk as-0)) (pubk c-0)) c-0 tgt (enc ak n1 tk t k)) (cat (enc tc n2 (privk c-0)) c-0 t n1) ((n2 n2-0) (n1 n1-0) (tc tc-0) (tk tk-0) (tgt tgt-0) (c c) (t t-0) (as as) (k k) (ak ak-0)) client ((n2 n2) (n1 n1) (tc tc) (tk tk) (tgt tgt) (c c-0) (t t) (as as-0) (k k) (ak ak)) auth pkinit-fix1 17
(defskeleton pkinit-fix1
  (vars (n2 n1 n2-0 n1-0 text) (tc tk tgt tc-0 tk-0 tgt-0 data)
    (c c-0 as t as-0 t-0 name) (k ak ak-0 skey))
  (defstrand auth 2 (n2 n2) (n1 n1) (tc tc) (tk tk) (tgt tgt) (c c-0)
    (t t) (as as-0) (k k) (ak ak))
  (defstrand client 2 (n2 n2-0) (n1 n1-0) (tc tc-0) (tk tk-0)
    (tgt tgt-0) (c c) (t t-0) (as as) (k k) (ak ak-0))
  (precedes ((0 1) (1 1)))
  (non-orig (privk c) (privk as))
  (uniq-orig n2-0 n1-0 k ak)
  (goals
    (forall ((c c-0 as name) (k skey) (z z-0 node))
      (implies
        (and (p "client" 1 z) (p "client" "c" z c)
          (p "client" "as" z as) (p "client" "k" z k) (p "auth" 1 z-0)
          (p "auth" "k" z-0 k) (p "auth" "c" z-0 c-0) (non (privk as))
          (non (privk c))) (exists ((z-1 node)) (p "client" 1 z-1)))))
  (label 17)
  (parent 16)
  (unrealized (1 1))
  (origs (n1-0 (1 0)) (n2-0 (1 0)) (k (0 1)) (ak (0 1)))
  (comment "1 in cohort - 1 not yet seen"))

Item 18, Parent: 17, Children: 19 20.

(cat (enc (enc k n2 c (privk as)) (pubk c)) c tgt-0 (enc ak-0 n1-0 tk-0 t-0 k)) (cat (enc tc-0 n2 (privk c)) c t-0 n1-0) (cat (enc (enc k n2 c (privk as)) (pubk c)) c tgt (enc ak n1 tk t k)) (cat (enc tc n2 (privk c)) c t n1) ((n2 n2) (n1 n1-0) (tc tc-0) (tk tk-0) (tgt tgt-0) (c c) (t t-0) (as as) (k k) (ak ak-0)) client ((n2 n2) (n1 n1) (tc tc) (tk tk) (tgt tgt) (c c) (t t) (as as) (k k) (ak ak)) auth pkinit-fix1 18
(defskeleton pkinit-fix1
  (vars (n2 n1 n1-0 text) (tc tk tgt tc-0 tk-0 tgt-0 data)
    (c t as t-0 name) (k ak ak-0 skey))
  (defstrand auth 2 (n2 n2) (n1 n1) (tc tc) (tk tk) (tgt tgt) (c c)
    (t t) (as as) (k k) (ak ak))
  (defstrand client 2 (n2 n2) (n1 n1-0) (tc tc-0) (tk tk-0) (tgt tgt-0)
    (c c) (t t-0) (as as) (k k) (ak ak-0))
  (precedes ((0 1) (1 1)) ((1 0) (0 0)))
  (non-orig (privk c) (privk as))
  (uniq-orig n2 n1-0 k ak)
  (operation encryption-test (displaced 2 0 auth 2)
    (enc k n2-0 c-0 (privk as-0)) (1 1))
  (label 18)
  (parent 17)
  (unrealized (0 0) (1 1))
  (origs (k (0 1)) (ak (0 1)) (n1-0 (1 0)) (n2 (1 0)))
  (comment "2 in cohort - 2 not yet seen"))

Item 19, Parent: 18, Child: 21.

(cat (enc (enc k n2 c (privk as)) (pubk c)) c tgt-0 (enc ak n1 tk t k)) (cat (enc tc-0 n2 (privk c)) c t n1) (cat (enc (enc k n2 c (privk as)) (pubk c)) c tgt (enc ak n1 tk t k)) (cat (enc tc n2 (privk c)) c t n1) ((n2 n2) (n1 n1) (tc tc-0) (tk tk) (tgt tgt-0) (c c) (t t) (as as) (k k) (ak ak)) client ((n2 n2) (n1 n1) (tc tc) (tk tk) (tgt tgt) (c c) (t t) (as as) (k k) (ak ak)) auth pkinit-fix1 19
(defskeleton pkinit-fix1
  (vars (n2 n1 text) (tc tk tgt tc-0 tgt-0 data) (c t as name)
    (k ak skey))
  (defstrand auth 2 (n2 n2) (n1 n1) (tc tc) (tk tk) (tgt tgt) (c c)
    (t t) (as as) (k k) (ak ak))
  (defstrand client 2 (n2 n2) (n1 n1) (tc tc-0) (tk tk) (tgt tgt-0)
    (c c) (t t) (as as) (k k) (ak ak))
  (precedes ((0 1) (1 1)) ((1 0) (0 0)))
  (non-orig (privk c) (privk as))
  (uniq-orig n2 n1 k ak)
  (operation encryption-test (displaced 2 0 auth 2)
    (enc ak-0 n1-0 tk-0 t-0 k) (1 1))
  (label 19)
  (parent 18)
  (unrealized (0 0))
  (origs (k (0 1)) (ak (0 1)) (n1 (1 0)) (n2 (1 0)))
  (comment "1 in cohort - 1 not yet seen"))

Item 20, Parent: 18, Child: 22.

k k (cat (enc (enc k n2 c (privk as)) (pubk c)) c tgt-0 (enc ak-0 n1-0 tk-0 t-0 k)) (cat (enc tc-0 n2 (privk c)) c t-0 n1-0) (cat (enc (enc k n2 c (privk as)) (pubk c)) c tgt (enc ak n1 tk t k)) (cat (enc tc n2 (privk c)) c t n1) ((n2 n2) (n1 n1-0) (tc tc-0) (tk tk-0) (tgt tgt-0) (c c) (t t-0) (as as) (k k) (ak ak-0)) client ((n2 n2) (n1 n1) (tc tc) (tk tk) (tgt tgt) (c c) (t t) (as as) (k k) (ak ak)) auth pkinit-fix1 20
(defskeleton pkinit-fix1
  (vars (n2 n1 n1-0 text) (tc tk tgt tc-0 tk-0 tgt-0 data)
    (c t as t-0 name) (k ak ak-0 skey))
  (defstrand auth 2 (n2 n2) (n1 n1) (tc tc) (tk tk) (tgt tgt) (c c)
    (t t) (as as) (k k) (ak ak))
  (defstrand client 2 (n2 n2) (n1 n1-0) (tc tc-0) (tk tk-0) (tgt tgt-0)
    (c c) (t t-0) (as as) (k k) (ak ak-0))
  (deflistener k)
  (precedes ((0 1) (2 0)) ((1 0) (0 0)) ((2 1) (1 1)))
  (non-orig (privk c) (privk as))
  (uniq-orig n2 n1-0 k ak)
  (operation encryption-test (added-listener k)
    (enc ak-0 n1-0 tk-0 t-0 k) (1 1))
  (label 20)
  (parent 18)
  (unrealized (0 0) (2 0))
  (comment "1 in cohort - 1 not yet seen"))

Item 21, Parent: 19.

(cat (enc (enc k n2 c (privk as)) (pubk c)) c tgt-0 (enc ak n1 tk t k)) (cat (enc tc n2 (privk c)) c t n1) (cat (enc (enc k n2 c (privk as)) (pubk c)) c tgt (enc ak n1 tk t k)) (cat (enc tc n2 (privk c)) c t n1) ((n2 n2) (n1 n1) (tc tc) (tk tk) (tgt tgt-0) (c c) (t t) (as as) (k k) (ak ak)) client ((n2 n2) (n1 n1) (tc tc) (tk tk) (tgt tgt) (c c) (t t) (as as) (k k) (ak ak)) auth pkinit-fix1 21 (realized) 
(defskeleton pkinit-fix1
  (vars (n2 n1 text) (tk tgt tc tgt-0 data) (c t as name) (k ak skey))
  (defstrand auth 2 (n2 n2) (n1 n1) (tc tc) (tk tk) (tgt tgt) (c c)
    (t t) (as as) (k k) (ak ak))
  (defstrand client 2 (n2 n2) (n1 n1) (tc tc) (tk tk) (tgt tgt-0) (c c)
    (t t) (as as) (k k) (ak ak))
  (precedes ((0 1) (1 1)) ((1 0) (0 0)))
  (non-orig (privk c) (privk as))
  (uniq-orig n2 n1 k ak)
  (operation encryption-test (displaced 2 1 client 1)
    (enc tc-0 n2 (privk c)) (0 0))
  (label 21)
  (parent 19)
  (unrealized)
  (shape)
  (satisfies yes)
  (maps
    ((0 1)
      ((c c) (c-0 c) (as as) (k k) (t t) (as-0 as) (n2 n2) (n1 n1)
        (tc tc) (tk tk) (tgt tgt) (ak ak) (t-0 t) (n2-0 n2) (n1-0 n1)
        (tc-0 tc) (tk-0 tk) (tgt-0 tgt-0) (ak-0 ak))))
  (origs (n1 (1 0)) (n2 (1 0)) (k (0 1)) (ak (0 1))))

Item 22, Parent: 20.

ak ak (cat (enc (enc ak n2 c (privk as)) (pubk c)) c tgt-0 (enc ak-0 n1-0 tk-0 t-0 ak)) (cat (enc tc-0 n2 (privk c)) c t-0 n1-0) (cat (enc (enc ak n2 c (privk as)) (pubk c)) c tgt (enc ak n1 tk t ak)) (cat (enc tc n2 (privk c)) c t n1) ((n2 n2) (n1 n1-0) (tc tc-0) (tk tk-0) (tgt tgt-0) (c c) (t t-0) (as as) (k ak) (ak ak-0)) client ((n2 n2) (n1 n1) (tc tc) (tk tk) (tgt tgt) (c c) (t t) (as as) (k ak) (ak ak)) auth pkinit-fix1 22
(defskeleton pkinit-fix1
  (vars (n2 n1 n1-0 text) (tc tk tgt tc-0 tk-0 tgt-0 data)
    (c t as t-0 name) (ak ak-0 skey))
  (defstrand auth 2 (n2 n2) (n1 n1) (tc tc) (tk tk) (tgt tgt) (c c)
    (t t) (as as) (k ak) (ak ak))
  (defstrand client 2 (n2 n2) (n1 n1-0) (tc tc-0) (tk tk-0) (tgt tgt-0)
    (c c) (t t-0) (as as) (k ak) (ak ak-0))
  (deflistener ak)
  (precedes ((0 1) (2 0)) ((1 0) (0 0)) ((2 1) (1 1)))
  (non-orig (privk c) (privk as))
  (uniq-orig n2 n1-0 ak)
  (operation nonce-test (displaced 3 0 auth 2) k (2 0)
    (enc (enc k n2 c (privk as)) (pubk c)))
  (label 22)
  (parent 20)
  (unrealized (0 0) (2 0))
  (comment "empty cohort"))

Tree 23.

28 27 26 25 24 23 
(defprotocol pkinit-fix2 basic
  (defrole client
    (vars (c t as name) (n2 n1 text) (tc tk tgt data) (k ak skey))
    (trace (send (cat (enc tc n2 (privk c)) c t n1))
      (recv
        (cat
          (enc (enc k (hash (enc tc n2 (privk c)) c t n1) (privk as))
            (pubk c)) c tgt (enc ak n1 tk t k))))
    (uniq-orig n2 n1))
  (defrole auth
    (vars (c t as name) (n2 n1 text) (tc tk tgt data) (k ak skey))
    (trace (recv (cat (enc tc n2 (privk c)) c t n1))
      (send
        (cat
          (enc (enc k (hash (enc tc n2 (privk c)) c t n1) (privk as))
            (pubk c)) c tgt (enc ak n1 tk t k))))
    (uniq-orig k ak)))

Item 23, Child: 24.

(cat (enc (enc k (hash (enc tc-0 n2-0 (privk c)) c t-0 n1-0) (privk as)) (pubk c)) c tgt-0 (enc ak-0 n1-0 tk-0 t-0 k)) (cat (enc tc-0 n2-0 (privk c)) c t-0 n1-0) (cat (enc (enc k (hash (enc tc n2 (privk c-0)) c-0 t n1) (privk as-0)) (pubk c-0)) c-0 tgt (enc ak n1 tk t k)) (cat (enc tc n2 (privk c-0)) c-0 t n1) ((n2 n2-0) (n1 n1-0) (tc tc-0) (tk tk-0) (tgt tgt-0) (c c) (t t-0) (as as) (k k) (ak ak-0)) client ((n2 n2) (n1 n1) (tc tc) (tk tk) (tgt tgt) (c c-0) (t t) (as as-0) (k k) (ak ak)) auth pkinit-fix2 23
(defskeleton pkinit-fix2
  (vars (n2 n1 n2-0 n1-0 text) (tc tk tgt tc-0 tk-0 tgt-0 data)
    (c c-0 as t as-0 t-0 name) (k ak ak-0 skey))
  (defstrand auth 2 (n2 n2) (n1 n1) (tc tc) (tk tk) (tgt tgt) (c c-0)
    (t t) (as as-0) (k k) (ak ak))
  (defstrand client 2 (n2 n2-0) (n1 n1-0) (tc tc-0) (tk tk-0)
    (tgt tgt-0) (c c) (t t-0) (as as) (k k) (ak ak-0))
  (non-orig (privk c) (privk as))
  (uniq-orig n2-0 n1-0 k ak)
  (goals
    (forall ((c c-0 as name) (k skey) (z z-0 node))
      (implies
        (and (p "client" 1 z) (p "client" "c" z c)
          (p "client" "as" z as) (p "client" "k" z k) (p "auth" 1 z-0)
          (p "auth" "k" z-0 k) (p "auth" "c" z-0 c-0) (non (privk as))
          (non (privk c))) (exists ((z-1 node)) (p "client" 1 z-1)))))
  (label 23)
  (unrealized (1 1))
  (preskeleton)
  (comment "Not a skeleton"))

Item 24, Parent: 23, Child: 25.

(cat (enc (enc k (hash (enc tc-0 n2-0 (privk c)) c t-0 n1-0) (privk as)) (pubk c)) c tgt-0 (enc ak-0 n1-0 tk-0 t-0 k)) (cat (enc tc-0 n2-0 (privk c)) c t-0 n1-0) (cat (enc (enc k (hash (enc tc n2 (privk c-0)) c-0 t n1) (privk as-0)) (pubk c-0)) c-0 tgt (enc ak n1 tk t k)) (cat (enc tc n2 (privk c-0)) c-0 t n1) ((n2 n2-0) (n1 n1-0) (tc tc-0) (tk tk-0) (tgt tgt-0) (c c) (t t-0) (as as) (k k) (ak ak-0)) client ((n2 n2) (n1 n1) (tc tc) (tk tk) (tgt tgt) (c c-0) (t t) (as as-0) (k k) (ak ak)) auth pkinit-fix2 24
(defskeleton pkinit-fix2
  (vars (n2 n1 n2-0 n1-0 text) (tc tk tgt tc-0 tk-0 tgt-0 data)
    (c c-0 as t as-0 t-0 name) (k ak ak-0 skey))
  (defstrand auth 2 (n2 n2) (n1 n1) (tc tc) (tk tk) (tgt tgt) (c c-0)
    (t t) (as as-0) (k k) (ak ak))
  (defstrand client 2 (n2 n2-0) (n1 n1-0) (tc tc-0) (tk tk-0)
    (tgt tgt-0) (c c) (t t-0) (as as) (k k) (ak ak-0))
  (precedes ((0 1) (1 1)))
  (non-orig (privk c) (privk as))
  (uniq-orig n2-0 n1-0 k ak)
  (goals
    (forall ((c c-0 as name) (k skey) (z z-0 node))
      (implies
        (and (p "client" 1 z) (p "client" "c" z c)
          (p "client" "as" z as) (p "client" "k" z k) (p "auth" 1 z-0)
          (p "auth" "k" z-0 k) (p "auth" "c" z-0 c-0) (non (privk as))
          (non (privk c))) (exists ((z-1 node)) (p "client" 1 z-1)))))
  (label 24)
  (parent 23)
  (unrealized (1 1))
  (origs (n1-0 (1 0)) (n2-0 (1 0)) (k (0 1)) (ak (0 1)))
  (comment "1 in cohort - 1 not yet seen"))

Item 25, Parent: 24, Children: 26 27.

(cat (enc (enc k (hash (enc tc n2 (privk c)) c t n1) (privk as)) (pubk c)) c tgt-0 (enc ak-0 n1 tk-0 t k)) (cat (enc tc n2 (privk c)) c t n1) (cat (enc (enc k (hash (enc tc n2 (privk c)) c t n1) (privk as)) (pubk c)) c tgt (enc ak n1 tk t k)) (cat (enc tc n2 (privk c)) c t n1) ((n2 n2) (n1 n1) (tc tc) (tk tk-0) (tgt tgt-0) (c c) (t t) (as as) (k k) (ak ak-0)) client ((n2 n2) (n1 n1) (tc tc) (tk tk) (tgt tgt) (c c) (t t) (as as) (k k) (ak ak)) auth pkinit-fix2 25
(defskeleton pkinit-fix2
  (vars (n2 n1 text) (tc tk tgt tk-0 tgt-0 data) (c t as name)
    (k ak ak-0 skey))
  (defstrand auth 2 (n2 n2) (n1 n1) (tc tc) (tk tk) (tgt tgt) (c c)
    (t t) (as as) (k k) (ak ak))
  (defstrand client 2 (n2 n2) (n1 n1) (tc tc) (tk tk-0) (tgt tgt-0)
    (c c) (t t) (as as) (k k) (ak ak-0))
  (precedes ((0 1) (1 1)) ((1 0) (0 0)))
  (non-orig (privk c) (privk as))
  (uniq-orig n2 n1 k ak)
  (operation encryption-test (displaced 2 0 auth 2)
    (enc k (hash (enc tc-0 n2-0 (privk c-0)) c-0 t-0 n1-0) (privk as-0))
    (1 1))
  (label 25)
  (parent 24)
  (unrealized (1 1))
  (origs (k (0 1)) (ak (0 1)) (n1 (1 0)) (n2 (1 0)))
  (comment "2 in cohort - 2 not yet seen"))

Item 26, Parent: 25.

(cat (enc (enc k (hash (enc tc n2 (privk c)) c t n1) (privk as)) (pubk c)) c tgt-0 (enc ak n1 tk t k)) (cat (enc tc n2 (privk c)) c t n1) (cat (enc (enc k (hash (enc tc n2 (privk c)) c t n1) (privk as)) (pubk c)) c tgt (enc ak n1 tk t k)) (cat (enc tc n2 (privk c)) c t n1) ((n2 n2) (n1 n1) (tc tc) (tk tk) (tgt tgt-0) (c c) (t t) (as as) (k k) (ak ak)) client ((n2 n2) (n1 n1) (tc tc) (tk tk) (tgt tgt) (c c) (t t) (as as) (k k) (ak ak)) auth pkinit-fix2 26 (realized) 
(defskeleton pkinit-fix2
  (vars (n2 n1 text) (tc tk tgt tgt-0 data) (c t as name) (k ak skey))
  (defstrand auth 2 (n2 n2) (n1 n1) (tc tc) (tk tk) (tgt tgt) (c c)
    (t t) (as as) (k k) (ak ak))
  (defstrand client 2 (n2 n2) (n1 n1) (tc tc) (tk tk) (tgt tgt-0) (c c)
    (t t) (as as) (k k) (ak ak))
  (precedes ((0 1) (1 1)) ((1 0) (0 0)))
  (non-orig (privk c) (privk as))
  (uniq-orig n2 n1 k ak)
  (operation encryption-test (displaced 2 0 auth 2)
    (enc ak-0 n1 tk-0 t k) (1 1))
  (label 26)
  (parent 25)
  (unrealized)
  (shape)
  (satisfies yes)
  (maps
    ((0 1)
      ((c c) (c-0 c) (as as) (k k) (t t) (as-0 as) (n2 n2) (n1 n1)
        (tc tc) (tk tk) (tgt tgt) (ak ak) (t-0 t) (n2-0 n2) (n1-0 n1)
        (tc-0 tc) (tk-0 tk) (tgt-0 tgt-0) (ak-0 ak))))
  (origs (k (0 1)) (ak (0 1)) (n1 (1 0)) (n2 (1 0))))

Item 27, Parent: 25, Child: 28.

k k (cat (enc (enc k (hash (enc tc n2 (privk c)) c t n1) (privk as)) (pubk c)) c tgt-0 (enc ak-0 n1 tk-0 t k)) (cat (enc tc n2 (privk c)) c t n1) (cat (enc (enc k (hash (enc tc n2 (privk c)) c t n1) (privk as)) (pubk c)) c tgt (enc ak n1 tk t k)) (cat (enc tc n2 (privk c)) c t n1) ((n2 n2) (n1 n1) (tc tc) (tk tk-0) (tgt tgt-0) (c c) (t t) (as as) (k k) (ak ak-0)) client ((n2 n2) (n1 n1) (tc tc) (tk tk) (tgt tgt) (c c) (t t) (as as) (k k) (ak ak)) auth pkinit-fix2 27
(defskeleton pkinit-fix2
  (vars (n2 n1 text) (tc tk tgt tk-0 tgt-0 data) (c t as name)
    (k ak ak-0 skey))
  (defstrand auth 2 (n2 n2) (n1 n1) (tc tc) (tk tk) (tgt tgt) (c c)
    (t t) (as as) (k k) (ak ak))
  (defstrand client 2 (n2 n2) (n1 n1) (tc tc) (tk tk-0) (tgt tgt-0)
    (c c) (t t) (as as) (k k) (ak ak-0))
  (deflistener k)
  (precedes ((0 1) (2 0)) ((1 0) (0 0)) ((2 1) (1 1)))
  (non-orig (privk c) (privk as))
  (uniq-orig n2 n1 k ak)
  (operation encryption-test (added-listener k) (enc ak-0 n1 tk-0 t k)
    (1 1))
  (label 27)
  (parent 25)
  (unrealized (2 0))
  (comment "1 in cohort - 1 not yet seen"))

Item 28, Parent: 27.

ak ak (cat (enc (enc ak (hash (enc tc n2 (privk c)) c t n1) (privk as)) (pubk c)) c tgt-0 (enc ak-0 n1 tk-0 t ak)) (cat (enc tc n2 (privk c)) c t n1) (cat (enc (enc ak (hash (enc tc n2 (privk c)) c t n1) (privk as)) (pubk c)) c tgt (enc ak n1 tk t ak)) (cat (enc tc n2 (privk c)) c t n1) ((n2 n2) (n1 n1) (tc tc) (tk tk-0) (tgt tgt-0) (c c) (t t) (as as) (k ak) (ak ak-0)) client ((n2 n2) (n1 n1) (tc tc) (tk tk) (tgt tgt) (c c) (t t) (as as) (k ak) (ak ak)) auth pkinit-fix2 28
(defskeleton pkinit-fix2
  (vars (n2 n1 text) (tc tk tgt tk-0 tgt-0 data) (c t as name)
    (ak ak-0 skey))
  (defstrand auth 2 (n2 n2) (n1 n1) (tc tc) (tk tk) (tgt tgt) (c c)
    (t t) (as as) (k ak) (ak ak))
  (defstrand client 2 (n2 n2) (n1 n1) (tc tc) (tk tk-0) (tgt tgt-0)
    (c c) (t t) (as as) (k ak) (ak ak-0))
  (deflistener ak)
  (precedes ((0 1) (2 0)) ((1 0) (0 0)) ((2 1) (1 1)))
  (non-orig (privk c) (privk as))
  (uniq-orig n2 n1 ak)
  (operation nonce-test (displaced 3 0 auth 2) k (2 0)
    (enc (enc k (hash (enc tc n2 (privk c)) c t n1) (privk as))
      (pubk c)))
  (label 28)
  (parent 27)
  (unrealized (2 0))
  (comment "empty cohort"))