cpsa-4.4.4: tst/kerberos_shapes.tst

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

(comment "CPSA 4.3.1")

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

(defprotocol kerberos basic
  (defrole init
    (vars (a b ks name) (t t-prime l text) (k skey))
    (trace (send (cat a b))
      (recv (cat (enc t l k b (ltk a ks)) (enc t l k a (ltk b ks))))
      (send (cat (enc a t k) (enc t l k a (ltk b ks))))
      (recv (enc t-prime k))))
  (defrole resp
    (vars (a b ks name) (t t-prime l text) (k skey))
    (trace (recv (cat (enc a t k) (enc t l k a (ltk b ks))))
      (send (enc t-prime k))))
  (defrole keyserver
    (vars (a b ks name) (t l text) (k skey))
    (trace (recv (cat a b))
      (send (cat (enc t l k b (ltk a ks)) (enc t l k a (ltk b ks)))))
    (uniq-orig k))
  (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 kerberos
  (vars (k skey) (t t-prime l text) (a b ks name))
  (defstrand init 4 (k k) (t t) (t-prime t-prime) (l l) (a a) (b b)
    (ks ks))
  (non-orig (ltk a ks) (ltk b ks))
  (traces
    ((send (cat a b))
      (recv (cat (enc t l k b (ltk a ks)) (enc t l k a (ltk b ks))))
      (send (cat (enc a t k) (enc t l k a (ltk b ks))))
      (recv (enc t-prime k))))
  (label 0)
  (unrealized (0 1))
  (origs)
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton kerberos
  (vars (k skey) (t t-prime l text) (a b ks name))
  (defstrand init 4 (k k) (t t) (t-prime t-prime) (l l) (a a) (b b)
    (ks ks))
  (defstrand keyserver 2 (k k) (t t) (l l) (a a) (b b) (ks ks))
  (defstrand resp 2 (k k) (t t) (t-prime t-prime) (l l) (a a) (b b)
    (ks ks))
  (precedes ((0 2) (2 0)) ((1 1) (0 1)) ((2 1) (0 3)))
  (non-orig (ltk a ks) (ltk b ks))
  (uniq-orig k)
  (operation nonce-test (contracted (b-0 b) (ks-0 ks) (l-0 l)) k (2 0)
    (enc t l k a (ltk b ks)) (enc t l k b (ltk a ks)))
  (traces
    ((send (cat a b))
      (recv (cat (enc t l k b (ltk a ks)) (enc t l k a (ltk b ks))))
      (send (cat (enc a t k) (enc t l k a (ltk b ks))))
      (recv (enc t-prime k)))
    ((recv (cat a b))
      (send (cat (enc t l k b (ltk a ks)) (enc t l k a (ltk b ks)))))
    ((recv (cat (enc a t k) (enc t l k a (ltk b ks))))
      (send (enc t-prime k))))
  (label 13)
  (parent 0)
  (realized)
  (shape)
  (maps ((0) ((a a) (b b) (ks ks) (t t) (t-prime t-prime) (l l) (k k))))
  (origs (k (1 1))))

(defskeleton kerberos
  (vars (k skey) (t t-prime l text) (a b ks name))
  (defstrand init 4 (k k) (t t) (t-prime t-prime) (l l) (a a) (b b)
    (ks ks))
  (defstrand keyserver 2 (k k) (t t) (l l) (a b) (b a) (ks ks))
  (defstrand resp 2 (k k) (t t) (t-prime t-prime) (l l) (a a) (b b)
    (ks ks))
  (precedes ((0 2) (2 0)) ((1 1) (0 1)) ((2 1) (0 3)))
  (non-orig (ltk a ks) (ltk b ks))
  (uniq-orig k)
  (operation nonce-test (contracted (b-0 b) (ks-0 ks) (l-0 l)) k (2 0)
    (enc t l k a (ltk b ks)) (enc t l k b (ltk a ks)))
  (traces
    ((send (cat a b))
      (recv (cat (enc t l k b (ltk a ks)) (enc t l k a (ltk b ks))))
      (send (cat (enc a t k) (enc t l k a (ltk b ks))))
      (recv (enc t-prime k)))
    ((recv (cat b a))
      (send (cat (enc t l k a (ltk b ks)) (enc t l k b (ltk a ks)))))
    ((recv (cat (enc a t k) (enc t l k a (ltk b ks))))
      (send (enc t-prime k))))
  (label 16)
  (parent 0)
  (realized)
  (shape)
  (maps ((0) ((a a) (b b) (ks ks) (t t) (t-prime t-prime) (l l) (k k))))
  (origs (k (1 1))))

(defskeleton kerberos
  (vars (k skey) (t t-prime l text) (a b ks name))
  (defstrand init 4 (k k) (t t) (t-prime t-prime) (l l) (a a) (b b)
    (ks ks))
  (defstrand keyserver 2 (k k) (t t) (l l) (a a) (b b) (ks ks))
  (defstrand resp 2 (k k) (t t) (t-prime t-prime) (l l) (a a) (b b)
    (ks ks))
  (defstrand init 3 (k k) (t t) (l l) (a a) (b b) (ks ks))
  (precedes ((1 1) (0 1)) ((1 1) (3 1)) ((2 1) (0 3)) ((3 2) (2 0)))
  (non-orig (ltk a ks) (ltk b ks))
  (uniq-orig k)
  (operation nonce-test (contracted (b-0 b) (ks-0 ks) (l-0 l)) k (2 0)
    (enc t l k a (ltk b ks)) (enc t l k b (ltk a ks)))
  (traces
    ((send (cat a b))
      (recv (cat (enc t l k b (ltk a ks)) (enc t l k a (ltk b ks))))
      (send (cat (enc a t k) (enc t l k a (ltk b ks))))
      (recv (enc t-prime k)))
    ((recv (cat a b))
      (send (cat (enc t l k b (ltk a ks)) (enc t l k a (ltk b ks)))))
    ((recv (cat (enc a t k) (enc t l k a (ltk b ks))))
      (send (enc t-prime k)))
    ((send (cat a b))
      (recv (cat (enc t l k b (ltk a ks)) (enc t l k a (ltk b ks))))
      (send (cat (enc a t k) (enc t l k a (ltk b ks))))))
  (label 19)
  (parent 0)
  (realized)
  (shape)
  (maps ((0) ((a a) (b b) (ks ks) (t t) (t-prime t-prime) (l l) (k k))))
  (origs (k (1 1))))

(defskeleton kerberos
  (vars (k skey) (t t-prime l text) (a b ks name))
  (defstrand init 4 (k k) (t t) (t-prime t-prime) (l l) (a a) (b b)
    (ks ks))
  (defstrand keyserver 2 (k k) (t t) (l l) (a a) (b b) (ks ks))
  (defstrand resp 2 (k k) (t t) (t-prime t-prime) (l l) (a b) (b a)
    (ks ks))
  (defstrand init 3 (k k) (t t) (l l) (a b) (b a) (ks ks))
  (precedes ((1 1) (0 1)) ((1 1) (3 1)) ((2 1) (0 3)) ((3 2) (2 0)))
  (non-orig (ltk a ks) (ltk b ks))
  (uniq-orig k)
  (operation nonce-test (contracted (b-0 a) (ks-0 ks) (l-0 l)) k (2 0)
    (enc t l k a (ltk b ks)) (enc t l k b (ltk a ks)))
  (traces
    ((send (cat a b))
      (recv (cat (enc t l k b (ltk a ks)) (enc t l k a (ltk b ks))))
      (send (cat (enc a t k) (enc t l k a (ltk b ks))))
      (recv (enc t-prime k)))
    ((recv (cat a b))
      (send (cat (enc t l k b (ltk a ks)) (enc t l k a (ltk b ks)))))
    ((recv (cat (enc b t k) (enc t l k b (ltk a ks))))
      (send (enc t-prime k)))
    ((send (cat b a))
      (recv (cat (enc t l k a (ltk b ks)) (enc t l k b (ltk a ks))))
      (send (cat (enc b t k) (enc t l k b (ltk a ks))))))
  (label 20)
  (parent 0)
  (realized)
  (shape)
  (maps ((0) ((a a) (b b) (ks ks) (t t) (t-prime t-prime) (l l) (k k))))
  (origs (k (1 1))))

(defskeleton kerberos
  (vars (k skey) (t t-prime l text) (a b ks name))
  (defstrand init 4 (k k) (t t) (t-prime t-prime) (l l) (a a) (b b)
    (ks ks))
  (defstrand keyserver 2 (k k) (t t) (l l) (a b) (b a) (ks ks))
  (defstrand resp 2 (k k) (t t) (t-prime t-prime) (l l) (a a) (b b)
    (ks ks))
  (defstrand init 3 (k k) (t t) (l l) (a a) (b b) (ks ks))
  (precedes ((1 1) (0 1)) ((1 1) (3 1)) ((2 1) (0 3)) ((3 2) (2 0)))
  (non-orig (ltk a ks) (ltk b ks))
  (uniq-orig k)
  (operation nonce-test (contracted (b-0 b) (ks-0 ks) (l-0 l)) k (2 0)
    (enc t l k a (ltk b ks)) (enc t l k b (ltk a ks)))
  (traces
    ((send (cat a b))
      (recv (cat (enc t l k b (ltk a ks)) (enc t l k a (ltk b ks))))
      (send (cat (enc a t k) (enc t l k a (ltk b ks))))
      (recv (enc t-prime k)))
    ((recv (cat b a))
      (send (cat (enc t l k a (ltk b ks)) (enc t l k b (ltk a ks)))))
    ((recv (cat (enc a t k) (enc t l k a (ltk b ks))))
      (send (enc t-prime k)))
    ((send (cat a b))
      (recv (cat (enc t l k b (ltk a ks)) (enc t l k a (ltk b ks))))
      (send (cat (enc a t k) (enc t l k a (ltk b ks))))))
  (label 21)
  (parent 0)
  (realized)
  (shape)
  (maps ((0) ((a a) (b b) (ks ks) (t t) (t-prime t-prime) (l l) (k k))))
  (origs (k (1 1))))

(defskeleton kerberos
  (vars (k skey) (t t-prime l text) (a b ks name))
  (defstrand init 4 (k k) (t t) (t-prime t-prime) (l l) (a a) (b b)
    (ks ks))
  (defstrand keyserver 2 (k k) (t t) (l l) (a b) (b a) (ks ks))
  (defstrand resp 2 (k k) (t t) (t-prime t-prime) (l l) (a b) (b a)
    (ks ks))
  (defstrand init 3 (k k) (t t) (l l) (a b) (b a) (ks ks))
  (precedes ((1 1) (0 1)) ((1 1) (3 1)) ((2 1) (0 3)) ((3 2) (2 0)))
  (non-orig (ltk a ks) (ltk b ks))
  (uniq-orig k)
  (operation nonce-test (contracted (b-0 a) (ks-0 ks) (l-0 l)) k (2 0)
    (enc t l k a (ltk b ks)) (enc t l k b (ltk a ks)))
  (traces
    ((send (cat a b))
      (recv (cat (enc t l k b (ltk a ks)) (enc t l k a (ltk b ks))))
      (send (cat (enc a t k) (enc t l k a (ltk b ks))))
      (recv (enc t-prime k)))
    ((recv (cat b a))
      (send (cat (enc t l k a (ltk b ks)) (enc t l k b (ltk a ks)))))
    ((recv (cat (enc b t k) (enc t l k b (ltk a ks))))
      (send (enc t-prime k)))
    ((send (cat b a))
      (recv (cat (enc t l k a (ltk b ks)) (enc t l k b (ltk a ks))))
      (send (cat (enc b t k) (enc t l k b (ltk a ks))))))
  (label 22)
  (parent 0)
  (realized)
  (shape)
  (maps ((0) ((a a) (b b) (ks ks) (t t) (t-prime t-prime) (l l) (k k))))
  (origs (k (1 1))))

(comment "Nothing left to do")

(defprotocol kerberos basic
  (defrole init
    (vars (a b ks name) (t t-prime l text) (k skey))
    (trace (send (cat a b))
      (recv (cat (enc t l k b (ltk a ks)) (enc t l k a (ltk b ks))))
      (send (cat (enc a t k) (enc t l k a (ltk b ks))))
      (recv (enc t-prime k))))
  (defrole resp
    (vars (a b ks name) (t t-prime l text) (k skey))
    (trace (recv (cat (enc a t k) (enc t l k a (ltk b ks))))
      (send (enc t-prime k))))
  (defrole keyserver
    (vars (a b ks name) (t l text) (k skey))
    (trace (recv (cat a b))
      (send (cat (enc t l k b (ltk a ks)) (enc t l k a (ltk b ks)))))
    (uniq-orig k))
  (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 kerberos
  (vars (k skey) (t t-prime l text) (a b ks name))
  (defstrand resp 2 (k k) (t t) (t-prime t-prime) (l l) (a a) (b b)
    (ks ks))
  (non-orig (ltk a ks) (ltk b ks))
  (traces
    ((recv (cat (enc a t k) (enc t l k a (ltk b ks))))
      (send (enc t-prime k))))
  (label 23)
  (unrealized (0 0))
  (origs)
  (comment "2 in cohort - 2 not yet seen"))

(defskeleton kerberos
  (vars (k skey) (t t-prime l text) (a b ks name))
  (defstrand resp 2 (k k) (t t) (t-prime t-prime) (l l) (a a) (b b)
    (ks ks))
  (defstrand keyserver 2 (k k) (t t) (l l) (a b) (b a) (ks ks))
  (defstrand init 3 (k k) (t t) (l l) (a a) (b b) (ks ks))
  (precedes ((1 1) (2 1)) ((2 2) (0 0)))
  (non-orig (ltk a ks) (ltk b ks))
  (uniq-orig k)
  (operation nonce-test (contracted (b-0 b) (ks-0 ks) (l-0 l)) k (2 1)
    (enc t l k a (ltk b ks)) (enc t l k b (ltk a ks)))
  (traces
    ((recv (cat (enc a t k) (enc t l k a (ltk b ks))))
      (send (enc t-prime k)))
    ((recv (cat b a))
      (send (cat (enc t l k a (ltk b ks)) (enc t l k b (ltk a ks)))))
    ((send (cat a b))
      (recv (cat (enc t l k b (ltk a ks)) (enc t l k a (ltk b ks))))
      (send (cat (enc a t k) (enc t l k a (ltk b ks))))))
  (label 30)
  (parent 23)
  (realized)
  (shape)
  (maps ((0) ((a a) (b b) (ks ks) (t t) (t-prime t-prime) (l l) (k k))))
  (origs (k (1 1))))

(defskeleton kerberos
  (vars (k skey) (t t-prime l text) (a b ks name))
  (defstrand resp 2 (k k) (t t) (t-prime t-prime) (l l) (a a) (b b)
    (ks ks))
  (defstrand keyserver 2 (k k) (t t) (l l) (a a) (b b) (ks ks))
  (defstrand init 3 (k k) (t t) (l l) (a a) (b b) (ks ks))
  (precedes ((1 1) (2 1)) ((2 2) (0 0)))
  (non-orig (ltk a ks) (ltk b ks))
  (uniq-orig k)
  (operation nonce-test (contracted (b-0 b) (ks-0 ks) (l-0 l)) k (2 1)
    (enc t l k a (ltk b ks)) (enc t l k b (ltk a ks)))
  (traces
    ((recv (cat (enc a t k) (enc t l k a (ltk b ks))))
      (send (enc t-prime k)))
    ((recv (cat a b))
      (send (cat (enc t l k b (ltk a ks)) (enc t l k a (ltk b ks)))))
    ((send (cat a b))
      (recv (cat (enc t l k b (ltk a ks)) (enc t l k a (ltk b ks))))
      (send (cat (enc a t k) (enc t l k a (ltk b ks))))))
  (label 31)
  (parent 23)
  (realized)
  (shape)
  (maps ((0) ((a a) (b b) (ks ks) (t t) (t-prime t-prime) (l l) (k k))))
  (origs (k (1 1))))

(comment "Nothing left to do")

(defprotocol kerberos basic
  (defrole init
    (vars (a b ks name) (t t-prime l text) (k skey))
    (trace (send (cat a b))
      (recv (cat (enc t l k b (ltk a ks)) (enc t l k a (ltk b ks))))
      (send (cat (enc a t k) (enc t l k a (ltk b ks))))
      (recv (enc t-prime k))))
  (defrole resp
    (vars (a b ks name) (t t-prime l text) (k skey))
    (trace (recv (cat (enc a t k) (enc t l k a (ltk b ks))))
      (send (enc t-prime k))))
  (defrole keyserver
    (vars (a b ks name) (t l text) (k skey))
    (trace (recv (cat a b))
      (send (cat (enc t l k b (ltk a ks)) (enc t l k a (ltk b ks)))))
    (uniq-orig k))
  (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 kerberos
  (vars (k skey) (t l text) (a b ks name))
  (defstrand keyserver 2 (k k) (t t) (l l) (a a) (b b) (ks ks))
  (non-orig (ltk a ks) (ltk b ks))
  (uniq-orig k)
  (traces
    ((recv (cat a b))
      (send (cat (enc t l k b (ltk a ks)) (enc t l k a (ltk b ks))))))
  (label 32)
  (realized)
  (shape)
  (maps ((0) ((a a) (b b) (ks ks) (t t) (l l) (k k))))
  (origs (k (0 1))))

(comment "Nothing left to do")