cpsa-2.1.2: tst/pca.tst

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

(defprotocol pca basic
  (defrole tpm
    (vars (ke ki km kp akey) (t a text))
    (trace (send (cat (enc ki a (invk ki)) (enc t ke (invk km))))
      (recv (enc (enc ki a t (invk kp)) ke))
      (send (enc ki a t (invk kp))))
    (non-orig (invk ke) (invk ki) (invk km) (invk kp))
    (uniq-orig ki))
  (defrole pca
    (vars (ke ki km kp akey) (t a text))
    (trace (recv (cat (enc ki a (invk ki)) (enc t ke (invk km))))
      (send (enc (enc ki a t (invk kp)) ke)))
    (non-orig (invk ke) (invk ki) (invk km) (invk kp)))
  (defrole appr
    (vars (ki kp akey) (t a text))
    (trace (recv (enc ki a t (invk kp))))
    (non-orig (invk ki) (invk kp))))

(defskeleton pca
  (vars (t a text) (ki kp akey))
  (defstrand appr 1 (t t) (a a) (ki ki) (kp kp))
  (non-orig (invk ki) (invk kp))
  (traces ((recv (enc ki a t (invk kp)))))
  (label 0)
  (unrealized (0 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton pca
  (vars (t a text) (ki kp ke km akey))
  (defstrand appr 1 (t t) (a a) (ki ki) (kp kp))
  (defstrand pca 2 (t t) (a a) (ke ke) (ki ki) (km km) (kp kp))
  (precedes ((1 1) (0 0)))
  (non-orig (invk ki) (invk kp) (invk ke) (invk km))
  (operation encryption-test (added-strand pca 2) (enc ki a t (invk kp))
    (0 0))
  (traces ((recv (enc ki a t (invk kp))))
    ((recv (cat (enc ki a (invk ki)) (enc t ke (invk km))))
      (send (enc (enc ki a t (invk kp)) ke))))
  (label 1)
  (parent 0)
  (unrealized (0 0) (1 0))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton pca
  (vars (t a t-0 text) (ki kp ke km ke-0 km-0 akey))
  (defstrand appr 1 (t t) (a a) (ki ki) (kp kp))
  (defstrand pca 2 (t t) (a a) (ke ke) (ki ki) (km km) (kp kp))
  (defstrand tpm 1 (t t-0) (a a) (ke ke-0) (ki ki) (km km-0))
  (precedes ((1 1) (0 0)) ((2 0) (1 0)))
  (non-orig (invk ki) (invk kp) (invk ke) (invk km) (invk ke-0)
    (invk km-0))
  (uniq-orig ki)
  (operation encryption-test (added-strand tpm 1) (enc ki a (invk ki))
    (1 0))
  (traces ((recv (enc ki a t (invk kp))))
    ((recv (cat (enc ki a (invk ki)) (enc t ke (invk km))))
      (send (enc (enc ki a t (invk kp)) ke)))
    ((send (cat (enc ki a (invk ki)) (enc t-0 ke-0 (invk km-0))))))
  (label 2)
  (parent 1)
  (unrealized (0 0) (1 0))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton pca
  (vars (t a t-0 a-0 text) (ki kp ke km ke-0 km-0 ki-0 akey))
  (defstrand appr 1 (t t) (a a) (ki ki) (kp kp))
  (defstrand pca 2 (t t) (a a) (ke ke) (ki ki) (km km) (kp kp))
  (defstrand tpm 1 (t t-0) (a a) (ke ke-0) (ki ki) (km km-0))
  (defstrand tpm 1 (t t) (a a-0) (ke ke) (ki ki-0) (km km))
  (precedes ((1 1) (0 0)) ((2 0) (1 0)) ((3 0) (1 0)))
  (non-orig (invk ki) (invk kp) (invk ke) (invk km) (invk ke-0)
    (invk km-0) (invk ki-0))
  (uniq-orig ki ki-0)
  (operation encryption-test (added-strand tpm 1) (enc t ke (invk km))
    (1 0))
  (traces ((recv (enc ki a t (invk kp))))
    ((recv (cat (enc ki a (invk ki)) (enc t ke (invk km))))
      (send (enc (enc ki a t (invk kp)) ke)))
    ((send (cat (enc ki a (invk ki)) (enc t-0 ke-0 (invk km-0)))))
    ((send (cat (enc ki-0 a-0 (invk ki-0)) (enc t ke (invk km))))))
  (label 3)
  (parent 2)
  (seen 5)
  (unrealized (0 0))
  (comment "3 in cohort - 2 not yet seen"))

(defskeleton pca
  (vars (a t text) (ki kp ke km akey))
  (defstrand appr 1 (t t) (a a) (ki ki) (kp kp))
  (defstrand pca 2 (t t) (a a) (ke ke) (ki ki) (km km) (kp kp))
  (defstrand tpm 1 (t t) (a a) (ke ke) (ki ki) (km km))
  (precedes ((1 1) (0 0)) ((2 0) (1 0)))
  (non-orig (invk ki) (invk kp) (invk ke) (invk km))
  (uniq-orig ki)
  (operation encryption-test (displaced 3 2 tpm 1)
    (enc t-0 ke-0 (invk km-0)) (1 0))
  (traces ((recv (enc ki a t (invk kp))))
    ((recv (cat (enc ki a (invk ki)) (enc t ke (invk km))))
      (send (enc (enc ki a t (invk kp)) ke)))
    ((send (cat (enc ki a (invk ki)) (enc t ke (invk km))))))
  (label 4)
  (parent 2)
  (seen 6)
  (unrealized (0 0))
  (comment "2 in cohort - 0 not yet seen"))

(defskeleton pca
  (vars (t a a-0 text) (ki kp ke km ki-0 km-0 akey))
  (defstrand appr 1 (t t) (a a) (ki ki) (kp kp))
  (defstrand pca 2 (t t) (a a) (ke ke) (ki ki) (km km) (kp kp))
  (defstrand tpm 1 (t t) (a a-0) (ke ke) (ki ki-0) (km km))
  (defstrand tpm 3 (t t) (a a) (ke ke) (ki ki) (km km-0) (kp kp))
  (precedes ((1 1) (0 0)) ((2 0) (1 0)) ((3 0) (1 0)) ((3 2) (0 0)))
  (non-orig (invk ki) (invk kp) (invk ke) (invk km) (invk ki-0)
    (invk km-0))
  (uniq-orig ki ki-0)
  (operation encryption-test (added-strand tpm 3) (enc ki a t (invk kp))
    (0 0) (enc (enc ki a t (invk kp)) ke))
  (traces ((recv (enc ki a t (invk kp))))
    ((recv (cat (enc ki a (invk ki)) (enc t ke (invk km))))
      (send (enc (enc ki a t (invk kp)) ke)))
    ((send (cat (enc ki-0 a-0 (invk ki-0)) (enc t ke (invk km)))))
    ((send (cat (enc ki a (invk ki)) (enc t ke (invk km-0))))
      (recv (enc (enc ki a t (invk kp)) ke))
      (send (enc ki a t (invk kp)))))
  (label 5)
  (parent 3)
  (unrealized (3 1))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton pca
  (vars (t a text) (ki kp ke km akey))
  (defstrand appr 1 (t t) (a a) (ki ki) (kp kp))
  (defstrand pca 2 (t t) (a a) (ke ke) (ki ki) (km km) (kp kp))
  (defstrand tpm 3 (t t) (a a) (ke ke) (ki ki) (km km) (kp kp))
  (precedes ((1 1) (0 0)) ((2 0) (1 0)) ((2 2) (0 0)))
  (non-orig (invk ki) (invk kp) (invk ke) (invk km))
  (uniq-orig ki)
  (operation encryption-test (displaced 3 4 tpm 3)
    (enc ki a t (invk kp)) (0 0) (enc (enc ki a t (invk kp)) ke))
  (traces ((recv (enc ki a t (invk kp))))
    ((recv (cat (enc ki a (invk ki)) (enc t ke (invk km))))
      (send (enc (enc ki a t (invk kp)) ke)))
    ((send (cat (enc ki a (invk ki)) (enc t ke (invk km))))
      (recv (enc (enc ki a t (invk kp)) ke))
      (send (enc ki a t (invk kp)))))
  (label 6)
  (parent 3)
  (unrealized (2 1))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton pca
  (vars (t a a-0 text) (ki kp ke km ki-0 km-0 ke-0 km-1 akey))
  (defstrand appr 1 (t t) (a a) (ki ki) (kp kp))
  (defstrand pca 2 (t t) (a a) (ke ke) (ki ki) (km km) (kp kp))
  (defstrand tpm 1 (t t) (a a-0) (ke ke) (ki ki-0) (km km))
  (defstrand tpm 3 (t t) (a a) (ke ke) (ki ki) (km km-0) (kp kp))
  (defstrand pca 2 (t t) (a a) (ke ke-0) (ki ki) (km km-1) (kp kp))
  (precedes ((1 1) (0 0)) ((2 0) (1 0)) ((3 0) (1 0)) ((3 0) (4 0))
    ((3 2) (0 0)) ((4 1) (3 1)))
  (non-orig (invk ki) (invk kp) (invk ke) (invk km) (invk ki-0)
    (invk km-0) (invk ke-0) (invk km-1))
  (uniq-orig ki ki-0)
  (operation encryption-test (added-strand pca 2) (enc ki a t (invk kp))
    (3 1))
  (traces ((recv (enc ki a t (invk kp))))
    ((recv (cat (enc ki a (invk ki)) (enc t ke (invk km))))
      (send (enc (enc ki a t (invk kp)) ke)))
    ((send (cat (enc ki-0 a-0 (invk ki-0)) (enc t ke (invk km)))))
    ((send (cat (enc ki a (invk ki)) (enc t ke (invk km-0))))
      (recv (enc (enc ki a t (invk kp)) ke))
      (send (enc ki a t (invk kp))))
    ((recv (cat (enc ki a (invk ki)) (enc t ke-0 (invk km-1))))
      (send (enc (enc ki a t (invk kp)) ke-0))))
  (label 7)
  (parent 5)
  (unrealized (3 1) (4 0))
  (comment "3 in cohort - 3 not yet seen"))

(defskeleton pca
  (vars (t a a-0 text) (ki kp ke km ki-0 km-0 akey))
  (defstrand appr 1 (t t) (a a) (ki ki) (kp kp))
  (defstrand pca 2 (t t) (a a) (ke ke) (ki ki) (km km) (kp kp))
  (defstrand tpm 1 (t t) (a a-0) (ke ke) (ki ki-0) (km km))
  (defstrand tpm 3 (t t) (a a) (ke ke) (ki ki) (km km-0) (kp kp))
  (precedes ((1 1) (3 1)) ((2 0) (1 0)) ((3 0) (1 0)) ((3 2) (0 0)))
  (non-orig (invk ki) (invk kp) (invk ke) (invk km) (invk ki-0)
    (invk km-0))
  (uniq-orig ki ki-0)
  (operation encryption-test (displaced 4 1 pca 2)
    (enc ki a t (invk kp)) (3 1))
  (traces ((recv (enc ki a t (invk kp))))
    ((recv (cat (enc ki a (invk ki)) (enc t ke (invk km))))
      (send (enc (enc ki a t (invk kp)) ke)))
    ((send (cat (enc ki-0 a-0 (invk ki-0)) (enc t ke (invk km)))))
    ((send (cat (enc ki a (invk ki)) (enc t ke (invk km-0))))
      (recv (enc (enc ki a t (invk kp)) ke))
      (send (enc ki a t (invk kp)))))
  (label 8)
  (parent 5)
  (seen 10)
  (unrealized)
  (shape)
  (comment "1 in cohort - 0 not yet seen"))

(defskeleton pca
  (vars (t a text) (ki kp ke km ke-0 km-0 akey))
  (defstrand appr 1 (t t) (a a) (ki ki) (kp kp))
  (defstrand pca 2 (t t) (a a) (ke ke) (ki ki) (km km) (kp kp))
  (defstrand tpm 3 (t t) (a a) (ke ke) (ki ki) (km km) (kp kp))
  (defstrand pca 2 (t t) (a a) (ke ke-0) (ki ki) (km km-0) (kp kp))
  (precedes ((1 1) (0 0)) ((2 0) (1 0)) ((2 0) (3 0)) ((2 2) (0 0))
    ((3 1) (2 1)))
  (non-orig (invk ki) (invk kp) (invk ke) (invk km) (invk ke-0)
    (invk km-0))
  (uniq-orig ki)
  (operation encryption-test (added-strand pca 2) (enc ki a t (invk kp))
    (2 1))
  (traces ((recv (enc ki a t (invk kp))))
    ((recv (cat (enc ki a (invk ki)) (enc t ke (invk km))))
      (send (enc (enc ki a t (invk kp)) ke)))
    ((send (cat (enc ki a (invk ki)) (enc t ke (invk km))))
      (recv (enc (enc ki a t (invk kp)) ke))
      (send (enc ki a t (invk kp))))
    ((recv (cat (enc ki a (invk ki)) (enc t ke-0 (invk km-0))))
      (send (enc (enc ki a t (invk kp)) ke-0))))
  (label 9)
  (parent 6)
  (unrealized (2 1) (3 0))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton pca
  (vars (t a text) (ki kp ke km akey))
  (defstrand appr 1 (t t) (a a) (ki ki) (kp kp))
  (defstrand pca 2 (t t) (a a) (ke ke) (ki ki) (km km) (kp kp))
  (defstrand tpm 3 (t t) (a a) (ke ke) (ki ki) (km km) (kp kp))
  (precedes ((1 1) (2 1)) ((2 0) (1 0)) ((2 2) (0 0)))
  (non-orig (invk ki) (invk kp) (invk ke) (invk km))
  (uniq-orig ki)
  (operation encryption-test (displaced 3 1 pca 2)
    (enc ki a t (invk kp)) (2 1))
  (traces ((recv (enc ki a t (invk kp))))
    ((recv (cat (enc ki a (invk ki)) (enc t ke (invk km))))
      (send (enc (enc ki a t (invk kp)) ke)))
    ((send (cat (enc ki a (invk ki)) (enc t ke (invk km))))
      (recv (enc (enc ki a t (invk kp)) ke))
      (send (enc ki a t (invk kp)))))
  (label 10)
  (parent 6)
  (unrealized)
  (shape))

(defskeleton pca
  (vars (t a a-0 a-1 text) (ki kp ke km ki-0 km-0 ke-0 km-1 ki-1 akey))
  (defstrand appr 1 (t t) (a a) (ki ki) (kp kp))
  (defstrand pca 2 (t t) (a a) (ke ke) (ki ki) (km km) (kp kp))
  (defstrand tpm 1 (t t) (a a-0) (ke ke) (ki ki-0) (km km))
  (defstrand tpm 3 (t t) (a a) (ke ke) (ki ki) (km km-0) (kp kp))
  (defstrand pca 2 (t t) (a a) (ke ke-0) (ki ki) (km km-1) (kp kp))
  (defstrand tpm 1 (t t) (a a-1) (ke ke-0) (ki ki-1) (km km-1))
  (precedes ((1 1) (0 0)) ((2 0) (1 0)) ((3 0) (1 0)) ((3 0) (4 0))
    ((3 2) (0 0)) ((4 1) (3 1)) ((5 0) (4 0)))
  (non-orig (invk ki) (invk kp) (invk ke) (invk km) (invk ki-0)
    (invk km-0) (invk ke-0) (invk km-1) (invk ki-1))
  (uniq-orig ki ki-0 ki-1)
  (operation encryption-test (added-strand tpm 1)
    (enc t ke-0 (invk km-1)) (4 0))
  (traces ((recv (enc ki a t (invk kp))))
    ((recv (cat (enc ki a (invk ki)) (enc t ke (invk km))))
      (send (enc (enc ki a t (invk kp)) ke)))
    ((send (cat (enc ki-0 a-0 (invk ki-0)) (enc t ke (invk km)))))
    ((send (cat (enc ki a (invk ki)) (enc t ke (invk km-0))))
      (recv (enc (enc ki a t (invk kp)) ke))
      (send (enc ki a t (invk kp))))
    ((recv (cat (enc ki a (invk ki)) (enc t ke-0 (invk km-1))))
      (send (enc (enc ki a t (invk kp)) ke-0)))
    ((send (cat (enc ki-1 a-1 (invk ki-1)) (enc t ke-0 (invk km-1))))))
  (label 11)
  (parent 7)
  (unrealized (3 1))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton pca
  (vars (t a a-0 text) (ki kp ke km ki-0 km-0 akey))
  (defstrand appr 1 (t t) (a a) (ki ki) (kp kp))
  (defstrand pca 2 (t t) (a a) (ke ke) (ki ki) (km km) (kp kp))
  (defstrand tpm 1 (t t) (a a-0) (ke ke) (ki ki-0) (km km))
  (defstrand tpm 3 (t t) (a a) (ke ke) (ki ki) (km km-0) (kp kp))
  (defstrand pca 2 (t t) (a a) (ke ke) (ki ki) (km km) (kp kp))
  (precedes ((1 1) (0 0)) ((2 0) (1 0)) ((2 0) (4 0)) ((3 0) (1 0))
    ((3 0) (4 0)) ((3 2) (0 0)) ((4 1) (3 1)))
  (non-orig (invk ki) (invk kp) (invk ke) (invk km) (invk ki-0)
    (invk km-0))
  (uniq-orig ki ki-0)
  (operation encryption-test (displaced 5 2 tpm 1)
    (enc t ke-0 (invk km-1)) (4 0))
  (traces ((recv (enc ki a t (invk kp))))
    ((recv (cat (enc ki a (invk ki)) (enc t ke (invk km))))
      (send (enc (enc ki a t (invk kp)) ke)))
    ((send (cat (enc ki-0 a-0 (invk ki-0)) (enc t ke (invk km)))))
    ((send (cat (enc ki a (invk ki)) (enc t ke (invk km-0))))
      (recv (enc (enc ki a t (invk kp)) ke))
      (send (enc ki a t (invk kp))))
    ((recv (cat (enc ki a (invk ki)) (enc t ke (invk km))))
      (send (enc (enc ki a t (invk kp)) ke))))
  (label 12)
  (parent 7)
  (seen 8)
  (unrealized)
  (comment "1 in cohort - 0 not yet seen"))

(defskeleton pca
  (vars (t a a-0 text) (ki kp ke km ki-0 km-0 akey))
  (defstrand appr 1 (t t) (a a) (ki ki) (kp kp))
  (defstrand pca 2 (t t) (a a) (ke ke) (ki ki) (km km) (kp kp))
  (defstrand tpm 1 (t t) (a a-0) (ke ke) (ki ki-0) (km km))
  (defstrand tpm 3 (t t) (a a) (ke ke) (ki ki) (km km-0) (kp kp))
  (defstrand pca 2 (t t) (a a) (ke ke) (ki ki) (km km-0) (kp kp))
  (precedes ((1 1) (0 0)) ((2 0) (1 0)) ((3 0) (1 0)) ((3 0) (4 0))
    ((3 2) (0 0)) ((4 1) (3 1)))
  (non-orig (invk ki) (invk kp) (invk ke) (invk km) (invk ki-0)
    (invk km-0))
  (uniq-orig ki ki-0)
  (operation encryption-test (displaced 5 3 tpm 1)
    (enc t ke-0 (invk km-1)) (4 0))
  (traces ((recv (enc ki a t (invk kp))))
    ((recv (cat (enc ki a (invk ki)) (enc t ke (invk km))))
      (send (enc (enc ki a t (invk kp)) ke)))
    ((send (cat (enc ki-0 a-0 (invk ki-0)) (enc t ke (invk km)))))
    ((send (cat (enc ki a (invk ki)) (enc t ke (invk km-0))))
      (recv (enc (enc ki a t (invk kp)) ke))
      (send (enc ki a t (invk kp))))
    ((recv (cat (enc ki a (invk ki)) (enc t ke (invk km-0))))
      (send (enc (enc ki a t (invk kp)) ke))))
  (label 13)
  (parent 7)
  (unrealized)
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton pca
  (vars (t a a-0 text) (ki kp ke km ke-0 km-0 ki-0 akey))
  (defstrand appr 1 (t t) (a a) (ki ki) (kp kp))
  (defstrand pca 2 (t t) (a a) (ke ke) (ki ki) (km km) (kp kp))
  (defstrand tpm 3 (t t) (a a) (ke ke) (ki ki) (km km) (kp kp))
  (defstrand pca 2 (t t) (a a) (ke ke-0) (ki ki) (km km-0) (kp kp))
  (defstrand tpm 1 (t t) (a a-0) (ke ke-0) (ki ki-0) (km km-0))
  (precedes ((1 1) (0 0)) ((2 0) (1 0)) ((2 0) (3 0)) ((2 2) (0 0))
    ((3 1) (2 1)) ((4 0) (3 0)))
  (non-orig (invk ki) (invk kp) (invk ke) (invk km) (invk ke-0)
    (invk km-0) (invk ki-0))
  (uniq-orig ki ki-0)
  (operation encryption-test (added-strand tpm 1)
    (enc t ke-0 (invk km-0)) (3 0))
  (traces ((recv (enc ki a t (invk kp))))
    ((recv (cat (enc ki a (invk ki)) (enc t ke (invk km))))
      (send (enc (enc ki a t (invk kp)) ke)))
    ((send (cat (enc ki a (invk ki)) (enc t ke (invk km))))
      (recv (enc (enc ki a t (invk kp)) ke))
      (send (enc ki a t (invk kp))))
    ((recv (cat (enc ki a (invk ki)) (enc t ke-0 (invk km-0))))
      (send (enc (enc ki a t (invk kp)) ke-0)))
    ((send (cat (enc ki-0 a-0 (invk ki-0)) (enc t ke-0 (invk km-0))))))
  (label 14)
  (parent 9)
  (unrealized (2 1))
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton pca
  (vars (t a text) (ki kp ke km akey))
  (defstrand appr 1 (t t) (a a) (ki ki) (kp kp))
  (defstrand pca 2 (t t) (a a) (ke ke) (ki ki) (km km) (kp kp))
  (defstrand tpm 3 (t t) (a a) (ke ke) (ki ki) (km km) (kp kp))
  (defstrand pca 2 (t t) (a a) (ke ke) (ki ki) (km km) (kp kp))
  (precedes ((1 1) (0 0)) ((2 0) (1 0)) ((2 0) (3 0)) ((2 2) (0 0))
    ((3 1) (2 1)))
  (non-orig (invk ki) (invk kp) (invk ke) (invk km))
  (uniq-orig ki)
  (operation encryption-test (displaced 4 2 tpm 1)
    (enc t ke-0 (invk km-0)) (3 0))
  (traces ((recv (enc ki a t (invk kp))))
    ((recv (cat (enc ki a (invk ki)) (enc t ke (invk km))))
      (send (enc (enc ki a t (invk kp)) ke)))
    ((send (cat (enc ki a (invk ki)) (enc t ke (invk km))))
      (recv (enc (enc ki a t (invk kp)) ke))
      (send (enc ki a t (invk kp))))
    ((recv (cat (enc ki a (invk ki)) (enc t ke (invk km))))
      (send (enc (enc ki a t (invk kp)) ke))))
  (label 15)
  (parent 9)
  (seen 10)
  (unrealized)
  (comment "1 in cohort - 0 not yet seen"))

(defskeleton pca
  (vars (t a a-0 a-1 text) (ki kp km ki-0 km-0 ke km-1 ki-1 akey))
  (defstrand appr 1 (t t) (a a) (ki ki) (kp kp))
  (defstrand pca 2 (t t) (a a) (ke ke) (ki ki) (km km) (kp kp))
  (defstrand tpm 1 (t t) (a a-0) (ke ke) (ki ki-0) (km km))
  (defstrand tpm 3 (t t) (a a) (ke ke) (ki ki) (km km-0) (kp kp))
  (defstrand pca 2 (t t) (a a) (ke ke) (ki ki) (km km-1) (kp kp))
  (defstrand tpm 1 (t t) (a a-1) (ke ke) (ki ki-1) (km km-1))
  (precedes ((1 1) (0 0)) ((2 0) (1 0)) ((3 0) (1 0)) ((3 0) (4 0))
    ((3 2) (0 0)) ((4 1) (3 1)) ((5 0) (4 0)))
  (non-orig (invk ki) (invk kp) (invk km) (invk ki-0) (invk km-0)
    (invk ke) (invk km-1) (invk ki-1))
  (uniq-orig ki ki-0 ki-1)
  (operation encryption-test (contracted (ke-0 ke))
    (enc ki a t (invk kp)) (3 1) (enc (enc ki a t (invk kp)) ke))
  (traces ((recv (enc ki a t (invk kp))))
    ((recv (cat (enc ki a (invk ki)) (enc t ke (invk km))))
      (send (enc (enc ki a t (invk kp)) ke)))
    ((send (cat (enc ki-0 a-0 (invk ki-0)) (enc t ke (invk km)))))
    ((send (cat (enc ki a (invk ki)) (enc t ke (invk km-0))))
      (recv (enc (enc ki a t (invk kp)) ke))
      (send (enc ki a t (invk kp))))
    ((recv (cat (enc ki a (invk ki)) (enc t ke (invk km-1))))
      (send (enc (enc ki a t (invk kp)) ke)))
    ((send (cat (enc ki-1 a-1 (invk ki-1)) (enc t ke (invk km-1))))))
  (label 16)
  (parent 11)
  (unrealized)
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton pca
  (vars (t a a-0 a-1 text) (ki kp ke km ki-0 km-0 ke-0 km-1 ki-1 akey))
  (defstrand appr 1 (t t) (a a) (ki ki) (kp kp))
  (defstrand pca 2 (t t) (a a) (ke ke) (ki ki) (km km) (kp kp))
  (defstrand tpm 1 (t t) (a a-0) (ke ke) (ki ki-0) (km km))
  (defstrand tpm 3 (t t) (a a) (ke ke) (ki ki) (km km-0) (kp kp))
  (defstrand pca 2 (t t) (a a) (ke ke-0) (ki ki) (km km-1) (kp kp))
  (defstrand tpm 1 (t t) (a a-1) (ke ke-0) (ki ki-1) (km km-1))
  (precedes ((1 1) (3 1)) ((2 0) (1 0)) ((3 0) (1 0)) ((3 0) (4 0))
    ((3 2) (0 0)) ((4 1) (3 1)) ((5 0) (4 0)))
  (non-orig (invk ki) (invk kp) (invk ke) (invk km) (invk ki-0)
    (invk km-0) (invk ke-0) (invk km-1) (invk ki-1))
  (uniq-orig ki ki-0 ki-1)
  (operation encryption-test (displaced 6 1 pca 2)
    (enc ki a t (invk kp)) (3 1) (enc (enc ki a t (invk kp)) ke-0))
  (traces ((recv (enc ki a t (invk kp))))
    ((recv (cat (enc ki a (invk ki)) (enc t ke (invk km))))
      (send (enc (enc ki a t (invk kp)) ke)))
    ((send (cat (enc ki-0 a-0 (invk ki-0)) (enc t ke (invk km)))))
    ((send (cat (enc ki a (invk ki)) (enc t ke (invk km-0))))
      (recv (enc (enc ki a t (invk kp)) ke))
      (send (enc ki a t (invk kp))))
    ((recv (cat (enc ki a (invk ki)) (enc t ke-0 (invk km-1))))
      (send (enc (enc ki a t (invk kp)) ke-0)))
    ((send (cat (enc ki-1 a-1 (invk ki-1)) (enc t ke-0 (invk km-1))))))
  (label 17)
  (parent 11)
  (unrealized)
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton pca
  (vars (t a a-0 text) (ki kp ke km ki-0 km-0 akey))
  (defstrand appr 1 (t t) (a a) (ki ki) (kp kp))
  (defstrand tpm 1 (t t) (a a-0) (ke ke) (ki ki-0) (km km))
  (defstrand tpm 3 (t t) (a a) (ke ke) (ki ki) (km km-0) (kp kp))
  (defstrand pca 2 (t t) (a a) (ke ke) (ki ki) (km km-0) (kp kp))
  (precedes ((1 0) (0 0)) ((2 0) (3 0)) ((2 2) (0 0)) ((3 1) (2 1)))
  (non-orig (invk ki) (invk kp) (invk ke) (invk km) (invk ki-0)
    (invk km-0))
  (uniq-orig ki ki-0)
  (operation generalization deleted (1 0))
  (traces ((recv (enc ki a t (invk kp))))
    ((send (cat (enc ki-0 a-0 (invk ki-0)) (enc t ke (invk km)))))
    ((send (cat (enc ki a (invk ki)) (enc t ke (invk km-0))))
      (recv (enc (enc ki a t (invk kp)) ke))
      (send (enc ki a t (invk kp))))
    ((recv (cat (enc ki a (invk ki)) (enc t ke (invk km-0))))
      (send (enc (enc ki a t (invk kp)) ke))))
  (label 18)
  (parent 13)
  (seen 10)
  (unrealized)
  (comment "1 in cohort - 0 not yet seen"))

(defskeleton pca
  (vars (t a a-0 text) (ki kp km ke km-0 ki-0 akey))
  (defstrand appr 1 (t t) (a a) (ki ki) (kp kp))
  (defstrand pca 2 (t t) (a a) (ke ke) (ki ki) (km km) (kp kp))
  (defstrand tpm 3 (t t) (a a) (ke ke) (ki ki) (km km) (kp kp))
  (defstrand pca 2 (t t) (a a) (ke ke) (ki ki) (km km-0) (kp kp))
  (defstrand tpm 1 (t t) (a a-0) (ke ke) (ki ki-0) (km km-0))
  (precedes ((1 1) (0 0)) ((2 0) (1 0)) ((2 0) (3 0)) ((2 2) (0 0))
    ((3 1) (2 1)) ((4 0) (3 0)))
  (non-orig (invk ki) (invk kp) (invk km) (invk ke) (invk km-0)
    (invk ki-0))
  (uniq-orig ki ki-0)
  (operation encryption-test (contracted (ke-0 ke))
    (enc ki a t (invk kp)) (2 1) (enc (enc ki a t (invk kp)) ke))
  (traces ((recv (enc ki a t (invk kp))))
    ((recv (cat (enc ki a (invk ki)) (enc t ke (invk km))))
      (send (enc (enc ki a t (invk kp)) ke)))
    ((send (cat (enc ki a (invk ki)) (enc t ke (invk km))))
      (recv (enc (enc ki a t (invk kp)) ke))
      (send (enc ki a t (invk kp))))
    ((recv (cat (enc ki a (invk ki)) (enc t ke (invk km-0))))
      (send (enc (enc ki a t (invk kp)) ke)))
    ((send (cat (enc ki-0 a-0 (invk ki-0)) (enc t ke (invk km-0))))))
  (label 19)
  (parent 14)
  (seen 8)
  (unrealized)
  (comment "1 in cohort - 0 not yet seen"))

(defskeleton pca
  (vars (t a a-0 text) (ki kp ke km ke-0 km-0 ki-0 akey))
  (defstrand appr 1 (t t) (a a) (ki ki) (kp kp))
  (defstrand pca 2 (t t) (a a) (ke ke) (ki ki) (km km) (kp kp))
  (defstrand tpm 3 (t t) (a a) (ke ke) (ki ki) (km km) (kp kp))
  (defstrand pca 2 (t t) (a a) (ke ke-0) (ki ki) (km km-0) (kp kp))
  (defstrand tpm 1 (t t) (a a-0) (ke ke-0) (ki ki-0) (km km-0))
  (precedes ((1 1) (2 1)) ((2 0) (1 0)) ((2 0) (3 0)) ((2 2) (0 0))
    ((3 1) (2 1)) ((4 0) (3 0)))
  (non-orig (invk ki) (invk kp) (invk ke) (invk km) (invk ke-0)
    (invk km-0) (invk ki-0))
  (uniq-orig ki ki-0)
  (operation encryption-test (displaced 5 1 pca 2)
    (enc ki a t (invk kp)) (2 1) (enc (enc ki a t (invk kp)) ke-0))
  (traces ((recv (enc ki a t (invk kp))))
    ((recv (cat (enc ki a (invk ki)) (enc t ke (invk km))))
      (send (enc (enc ki a t (invk kp)) ke)))
    ((send (cat (enc ki a (invk ki)) (enc t ke (invk km))))
      (recv (enc (enc ki a t (invk kp)) ke))
      (send (enc ki a t (invk kp))))
    ((recv (cat (enc ki a (invk ki)) (enc t ke-0 (invk km-0))))
      (send (enc (enc ki a t (invk kp)) ke-0)))
    ((send (cat (enc ki-0 a-0 (invk ki-0)) (enc t ke-0 (invk km-0))))))
  (label 20)
  (parent 14)
  (unrealized)
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton pca
  (vars (t a a-0 a-1 text) (ki kp km ki-0 km-0 ke km-1 ki-1 akey))
  (defstrand appr 1 (t t) (a a) (ki ki) (kp kp))
  (defstrand tpm 1 (t t) (a a-0) (ke ke) (ki ki-0) (km km))
  (defstrand tpm 3 (t t) (a a) (ke ke) (ki ki) (km km-0) (kp kp))
  (defstrand pca 2 (t t) (a a) (ke ke) (ki ki) (km km-1) (kp kp))
  (defstrand tpm 1 (t t) (a a-1) (ke ke) (ki ki-1) (km km-1))
  (precedes ((1 0) (0 0)) ((2 0) (3 0)) ((2 2) (0 0)) ((3 1) (2 1))
    ((4 0) (3 0)))
  (non-orig (invk ki) (invk kp) (invk km) (invk ki-0) (invk km-0)
    (invk ke) (invk km-1) (invk ki-1))
  (uniq-orig ki ki-0 ki-1)
  (operation generalization deleted (1 0))
  (traces ((recv (enc ki a t (invk kp))))
    ((send (cat (enc ki-0 a-0 (invk ki-0)) (enc t ke (invk km)))))
    ((send (cat (enc ki a (invk ki)) (enc t ke (invk km-0))))
      (recv (enc (enc ki a t (invk kp)) ke))
      (send (enc ki a t (invk kp))))
    ((recv (cat (enc ki a (invk ki)) (enc t ke (invk km-1))))
      (send (enc (enc ki a t (invk kp)) ke)))
    ((send (cat (enc ki-1 a-1 (invk ki-1)) (enc t ke (invk km-1))))))
  (label 21)
  (parent 16)
  (seen 8)
  (unrealized)
  (comment "1 in cohort - 0 not yet seen"))

(defskeleton pca
  (vars (t a a-0 a-1 text) (ki kp ke km ki-0 km-0 ke-0 km-1 ki-1 akey))
  (defstrand appr 1 (t t) (a a) (ki ki) (kp kp))
  (defstrand pca 2 (t t) (a a) (ke ke) (ki ki) (km km) (kp kp))
  (defstrand tpm 1 (t t) (a a-0) (ke ke) (ki ki-0) (km km))
  (defstrand tpm 3 (t t) (a a) (ke ke) (ki ki) (km km-0) (kp kp))
  (defstrand tpm 1 (t t) (a a-1) (ke ke-0) (ki ki-1) (km km-1))
  (precedes ((1 1) (3 1)) ((2 0) (1 0)) ((3 0) (1 0)) ((3 2) (0 0))
    ((4 0) (3 1)))
  (non-orig (invk ki) (invk kp) (invk ke) (invk km) (invk ki-0)
    (invk km-0) (invk ke-0) (invk km-1) (invk ki-1))
  (uniq-orig ki ki-0 ki-1)
  (operation generalization deleted (4 0))
  (traces ((recv (enc ki a t (invk kp))))
    ((recv (cat (enc ki a (invk ki)) (enc t ke (invk km))))
      (send (enc (enc ki a t (invk kp)) ke)))
    ((send (cat (enc ki-0 a-0 (invk ki-0)) (enc t ke (invk km)))))
    ((send (cat (enc ki a (invk ki)) (enc t ke (invk km-0))))
      (recv (enc (enc ki a t (invk kp)) ke))
      (send (enc ki a t (invk kp))))
    ((send (cat (enc ki-1 a-1 (invk ki-1)) (enc t ke-0 (invk km-1))))))
  (label 22)
  (parent 17)
  (seen 8)
  (unrealized)
  (comment "1 in cohort - 0 not yet seen"))

(defskeleton pca
  (vars (t a a-0 text) (ki kp ke km ke-0 km-0 ki-0 akey))
  (defstrand appr 1 (t t) (a a) (ki ki) (kp kp))
  (defstrand pca 2 (t t) (a a) (ke ke) (ki ki) (km km) (kp kp))
  (defstrand tpm 3 (t t) (a a) (ke ke) (ki ki) (km km) (kp kp))
  (defstrand tpm 1 (t t) (a a-0) (ke ke-0) (ki ki-0) (km km-0))
  (precedes ((1 1) (2 1)) ((2 0) (1 0)) ((2 2) (0 0)) ((3 0) (2 1)))
  (non-orig (invk ki) (invk kp) (invk ke) (invk km) (invk ke-0)
    (invk km-0) (invk ki-0))
  (uniq-orig ki ki-0)
  (operation generalization deleted (3 0))
  (traces ((recv (enc ki a t (invk kp))))
    ((recv (cat (enc ki a (invk ki)) (enc t ke (invk km))))
      (send (enc (enc ki a t (invk kp)) ke)))
    ((send (cat (enc ki a (invk ki)) (enc t ke (invk km))))
      (recv (enc (enc ki a t (invk kp)) ke))
      (send (enc ki a t (invk kp))))
    ((send (cat (enc ki-0 a-0 (invk ki-0)) (enc t ke-0 (invk km-0))))))
  (label 23)
  (parent 20)
  (seen 10)
  (unrealized)
  (comment "1 in cohort - 0 not yet seen"))

(comment "Nothing left to do")