cpsa-4.4.4: tst/pca_shapes.tst

(comment "CPSA 4.3.1")
(comment "Extracted shapes")

(herald "Privacy Certificate Authority" (bound 15)
  (comment "Generation of an Attestation Identity Certificate"))

(comment "CPSA 4.3.1")

(comment "All input read from tst/pca.scm")

(comment "Strand count bounded at 15")

(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)))
  (defgenrule neqRl_indx
    (forall ((x indx)) (implies (fact neq x x) (false))))
  (defgenrule neqRl_strd
    (forall ((x strd)) (implies (fact neq x x) (false))))
  (defgenrule neqRl_mesg
    (forall ((x mesg)) (implies (fact neq x x) (false)))))

(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))
  (origs)
  (comment "1 in cohort - 1 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 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 9)
  (parent 0)
  (realized)
  (shape)
  (maps ((0) ((ki ki) (kp kp) (t t) (a a))))
  (origs (ki (2 0))))

(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 11)
  (parent 0)
  (realized)
  (shape)
  (maps ((0) ((ki ki) (kp kp) (t t) (a a))))
  (origs (ki (3 0)) (ki-0 (2 0))))

(comment "Nothing left to do")