cpsa-4.4.4: tst/aik_shapes.tst

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

(herald "Anonymous identity protocol from TCG")

(comment "CPSA 4.3.1")

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

(defprotocol aikprot basic
  (defrole ca
    (vars (mf name) (ek akey))
    (trace (send (enc "ekc" mf ek (privk mf))))
    (non-orig (invk ek)))
  (defrole tpm
    (vars (i x mf pc name) (ek k akey) (srk skey))
    (trace (recv (cat x i (enc "ekc" mf ek (privk mf))))
      (send (cat i k x (enc "ekc" mf ek (privk mf))))
      (recv (enc (enc "aic" i k x (privk pc)) ek))
      (send (cat (enc "aic" i k x (privk pc)) (enc k (invk k) srk))))
    (non-orig srk (invk ek))
    (uniq-orig k (invk k)))
  (defrole pca
    (vars (i x mf pc name) (ek k akey))
    (trace (recv (cat i k x (enc "ekc" mf ek (privk mf))))
      (send (enc (enc "aic" i k x (privk pc)) ek)))
    (non-orig (privk mf)))
  (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 aikprot
  (vars (srk skey) (ek k akey) (mf pc i x name))
  (defstrand tpm 4 (srk srk) (ek ek) (k k) (i i) (x x) (mf mf) (pc pc))
  (non-orig srk (invk ek) (privk pc))
  (uniq-orig k (invk k))
  (traces
    ((recv (cat x i (enc "ekc" mf ek (privk mf))))
      (send (cat i k x (enc "ekc" mf ek (privk mf))))
      (recv (enc (enc "aic" i k x (privk pc)) ek))
      (send (cat (enc "aic" i k x (privk pc)) (enc k (invk k) srk)))))
  (label 0)
  (unrealized (0 2))
  (origs ((invk k) (0 3)) (k (0 1)))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton aikprot
  (vars (srk skey) (k ek akey) (mf pc i x mf-0 name))
  (defstrand tpm 4 (srk srk) (ek ek) (k k) (i i) (x x) (mf mf) (pc pc))
  (defstrand pca 2 (ek ek) (k k) (i i) (x x) (mf mf-0) (pc pc))
  (defstrand ca 1 (ek ek) (mf mf-0))
  (precedes ((0 1) (1 0)) ((1 1) (0 2)) ((2 0) (1 0)))
  (non-orig srk (invk ek) (privk pc) (privk mf-0))
  (uniq-orig k (invk k))
  (operation encryption-test (contracted (ek-0 ek))
    (enc "aic" i k x (privk pc)) (0 2)
    (enc (enc "aic" i k x (privk pc)) ek))
  (traces
    ((recv (cat x i (enc "ekc" mf ek (privk mf))))
      (send (cat i k x (enc "ekc" mf ek (privk mf))))
      (recv (enc (enc "aic" i k x (privk pc)) ek))
      (send (cat (enc "aic" i k x (privk pc)) (enc k (invk k) srk))))
    ((recv (cat i k x (enc "ekc" mf-0 ek (privk mf-0))))
      (send (enc (enc "aic" i k x (privk pc)) ek)))
    ((send (enc "ekc" mf-0 ek (privk mf-0)))))
  (label 3)
  (parent 0)
  (realized)
  (shape)
  (maps ((0) ((mf mf) (pc pc) (i i) (x x) (ek ek) (k k) (srk srk))))
  (origs ((invk k) (0 3)) (k (0 1))))

(comment "Nothing left to do")

(defprotocol aikprot basic
  (defrole ca
    (vars (mf name) (ek akey))
    (trace (send (enc "ekc" mf ek (privk mf))))
    (non-orig (invk ek)))
  (defrole tpm
    (vars (i x mf pc name) (ek k akey) (srk skey))
    (trace (recv (cat x i (enc "ekc" mf ek (privk mf))))
      (send (cat i k x (enc "ekc" mf ek (privk mf))))
      (recv (enc (enc "aic" i k x (privk pc)) ek))
      (send (cat (enc "aic" i k x (privk pc)) (enc k (invk k) srk))))
    (non-orig srk (invk ek))
    (uniq-orig k (invk k)))
  (defrole pca
    (vars (i x mf pc name) (ek k akey))
    (trace (recv (cat i k x (enc "ekc" mf ek (privk mf))))
      (send (enc (enc "aic" i k x (privk pc)) ek)))
    (non-orig (privk mf)))
  (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 aikprot
  (vars (k akey) (i x pc name))
  (deflistener (enc "aic" i k x (privk pc)))
  (non-orig (privk pc))
  (traces
    ((recv (enc "aic" i k x (privk pc)))
      (send (enc "aic" i k x (privk pc)))))
  (label 5)
  (unrealized (0 0))
  (origs)
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton aikprot
  (vars (srk skey) (k ek akey) (i x pc mf mf-0 name))
  (deflistener (enc "aic" i k x (privk pc)))
  (defstrand pca 2 (ek ek) (k k) (i i) (x x) (mf mf) (pc pc))
  (defstrand ca 1 (ek ek) (mf mf))
  (defstrand tpm 4 (srk srk) (ek ek) (k k) (i i) (x x) (mf mf-0)
    (pc pc))
  (precedes ((1 1) (3 2)) ((2 0) (1 0)) ((3 1) (1 0)) ((3 3) (0 0)))
  (non-orig srk (invk ek) (privk pc) (privk mf))
  (uniq-orig k (invk k))
  (operation encryption-test (displaced 4 1 pca 2)
    (enc "aic" i k x (privk pc)) (3 2))
  (traces
    ((recv (enc "aic" i k x (privk pc)))
      (send (enc "aic" i k x (privk pc))))
    ((recv (cat i k x (enc "ekc" mf ek (privk mf))))
      (send (enc (enc "aic" i k x (privk pc)) ek)))
    ((send (enc "ekc" mf ek (privk mf))))
    ((recv (cat x i (enc "ekc" mf-0 ek (privk mf-0))))
      (send (cat i k x (enc "ekc" mf-0 ek (privk mf-0))))
      (recv (enc (enc "aic" i k x (privk pc)) ek))
      (send (cat (enc "aic" i k x (privk pc)) (enc k (invk k) srk)))))
  (label 10)
  (parent 5)
  (realized)
  (shape)
  (maps ((0) ((i i) (x x) (pc pc) (k k))))
  (origs (k (3 1)) ((invk k) (3 3))))

(comment "Nothing left to do")