cpsa-4.4.4: tst/neuman-stubblebine-reauth-tagged_shapes.tst

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

(herald neuman-stubblebine-reauth (bound 8))

(comment "CPSA 4.3.1")

(comment "All input read from tst/neuman-stubblebine-reauth-tagged.lsp")

(defprotocol neuman-stubblebine-reauth basic
  (defrole init
    (vars (a b ks name) (ra rb text) (k skey) (tb text))
    (trace (send (cat a ra))
      (recv (cat (enc b ra k tb (ltk a ks)) (enc a k tb (ltk b ks)) rb))
      (send (cat (enc a k tb (ltk b ks)) (enc "one" rb k)))))
  (defrole resp
    (vars (a b ks name) (ra rb text) (k skey) (tb text))
    (trace (recv (cat a ra)) (send (cat b rb (enc a ra tb (ltk b ks))))
      (recv (cat (enc a k tb (ltk b ks)) (enc "one" rb k)))))
  (defrole init-reauth
    (vars (a b ks name) (ra-prime rb-prime text) (k skey) (tb text))
    (trace (recv (enc a k tb (ltk b ks)))
      (send (cat (enc a k tb (ltk b ks)) ra-prime))
      (recv (cat rb-prime (enc "two" ra-prime k)))
      (send (enc "three" rb-prime k))))
  (defrole resp-reauth
    (vars (a b ks name) (ra-prime rb-prime text) (k skey) (tb text))
    (trace (recv (cat (enc a k tb (ltk b ks)) ra-prime))
      (send (cat rb-prime (enc "two" ra-prime k)))
      (recv (enc "three" rb-prime k))))
  (defrole keyserver
    (vars (a b ks name) (ra rb text) (k skey) (tb text))
    (trace (recv (cat b rb (enc a ra tb (ltk b ks))))
      (send
        (cat (enc b ra k tb (ltk a ks)) (enc a k tb (ltk b ks)) rb)))
    (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 neuman-stubblebine-reauth
  (vars (k skey) (ra tb rb ra-prime rb-prime tb-0 text) (a b ks name))
  (defstrand resp 3 (k k) (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks))
  (defstrand resp-reauth 3 (k k) (ra-prime ra-prime) (rb-prime rb-prime)
    (tb tb-0) (a a) (b b) (ks ks))
  (non-orig (ltk a ks) (ltk b ks))
  (uniq-orig k ra rb ra-prime rb-prime)
  (traces
    ((recv (cat a ra)) (send (cat b rb (enc a ra tb (ltk b ks))))
      (recv (cat (enc a k tb (ltk b ks)) (enc "one" rb k))))
    ((recv (cat (enc a k tb-0 (ltk b ks)) ra-prime))
      (send (cat rb-prime (enc "two" ra-prime k)))
      (recv (enc "three" rb-prime k))))
  (label 0)
  (unrealized (0 2) (1 0))
  (origs (rb (0 1)) (rb-prime (1 1)))
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton neuman-stubblebine-reauth
  (vars (k skey) (ra tb rb ra-prime rb-prime rb-0 text) (a b ks name))
  (defstrand resp 3 (k k) (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks))
  (defstrand resp-reauth 3 (k k) (ra-prime ra-prime) (rb-prime rb-prime)
    (tb tb) (a a) (b b) (ks ks))
  (defstrand keyserver 2 (k k) (ra ra) (rb rb-0) (tb tb) (a a) (b b)
    (ks ks))
  (defstrand init-reauth 4 (k k) (ra-prime ra-prime) (rb-prime rb-prime)
    (tb tb) (a a) (b b) (ks ks))
  (defstrand init 3 (k k) (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks))
  (precedes ((0 1) (2 0)) ((1 1) (3 2)) ((2 1) (3 0)) ((2 1) (4 1))
    ((3 1) (1 0)) ((3 3) (1 2)) ((4 0) (0 0)) ((4 2) (0 2)))
  (non-orig (ltk a ks) (ltk b ks))
  (uniq-orig k ra rb ra-prime rb-prime)
  (operation encryption-test (displaced 5 2 keyserver 2)
    (enc b ra-0 k tb (ltk a ks)) (4 1))
  (traces
    ((recv (cat a ra)) (send (cat b rb (enc a ra tb (ltk b ks))))
      (recv (cat (enc a k tb (ltk b ks)) (enc "one" rb k))))
    ((recv (cat (enc a k tb (ltk b ks)) ra-prime))
      (send (cat rb-prime (enc "two" ra-prime k)))
      (recv (enc "three" rb-prime k)))
    ((recv (cat b rb-0 (enc a ra tb (ltk b ks))))
      (send
        (cat (enc b ra k tb (ltk a ks)) (enc a k tb (ltk b ks)) rb-0)))
    ((recv (enc a k tb (ltk b ks)))
      (send (cat (enc a k tb (ltk b ks)) ra-prime))
      (recv (cat rb-prime (enc "two" ra-prime k)))
      (send (enc "three" rb-prime k)))
    ((send (cat a ra))
      (recv (cat (enc b ra k tb (ltk a ks)) (enc a k tb (ltk b ks)) rb))
      (send (cat (enc a k tb (ltk b ks)) (enc "one" rb k)))))
  (label 27)
  (parent 0)
  (realized)
  (shape)
  (maps
    ((0 1)
      ((ra ra) (tb tb) (rb rb) (a a) (b b) (ks ks) (k k)
        (ra-prime ra-prime) (rb-prime rb-prime) (tb-0 tb))))
  (origs (k (2 1)) (ra (4 0)) (rb (0 1)) (ra-prime (3 1))
    (rb-prime (1 1))))

(defskeleton neuman-stubblebine-reauth
  (vars (k skey)
    (ra tb rb ra-prime rb-prime rb-0 ra-prime-0 rb-prime-0 text)
    (a b ks name))
  (defstrand resp 3 (k k) (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks))
  (defstrand resp-reauth 3 (k k) (ra-prime ra-prime) (rb-prime rb-prime)
    (tb tb) (a a) (b b) (ks ks))
  (defstrand keyserver 2 (k k) (ra ra) (rb rb-0) (tb tb) (a a) (b b)
    (ks ks))
  (defstrand init-reauth 4 (k k) (ra-prime ra-prime-0)
    (rb-prime rb-prime) (tb tb) (a a) (b b) (ks ks))
  (defstrand resp-reauth 2 (k k) (ra-prime ra-prime-0)
    (rb-prime rb-prime-0) (tb tb) (a a) (b b) (ks ks))
  (defstrand init 3 (k k) (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks))
  (precedes ((0 1) (2 0)) ((1 1) (3 2)) ((2 1) (1 0)) ((2 1) (3 0))
    ((2 1) (4 0)) ((2 1) (5 1)) ((3 3) (1 2)) ((4 1) (3 2))
    ((5 0) (0 0)) ((5 2) (0 2)))
  (non-orig (ltk a ks) (ltk b ks))
  (uniq-orig k ra rb ra-prime rb-prime)
  (operation encryption-test (displaced 6 2 keyserver 2)
    (enc b ra-0 k tb (ltk a ks)) (5 1))
  (traces
    ((recv (cat a ra)) (send (cat b rb (enc a ra tb (ltk b ks))))
      (recv (cat (enc a k tb (ltk b ks)) (enc "one" rb k))))
    ((recv (cat (enc a k tb (ltk b ks)) ra-prime))
      (send (cat rb-prime (enc "two" ra-prime k)))
      (recv (enc "three" rb-prime k)))
    ((recv (cat b rb-0 (enc a ra tb (ltk b ks))))
      (send
        (cat (enc b ra k tb (ltk a ks)) (enc a k tb (ltk b ks)) rb-0)))
    ((recv (enc a k tb (ltk b ks)))
      (send (cat (enc a k tb (ltk b ks)) ra-prime-0))
      (recv (cat rb-prime (enc "two" ra-prime-0 k)))
      (send (enc "three" rb-prime k)))
    ((recv (cat (enc a k tb (ltk b ks)) ra-prime-0))
      (send (cat rb-prime-0 (enc "two" ra-prime-0 k))))
    ((send (cat a ra))
      (recv (cat (enc b ra k tb (ltk a ks)) (enc a k tb (ltk b ks)) rb))
      (send (cat (enc a k tb (ltk b ks)) (enc "one" rb k)))))
  (label 32)
  (parent 0)
  (realized)
  (shape)
  (maps
    ((0 1)
      ((ra ra) (tb tb) (rb rb) (a a) (b b) (ks ks) (k k)
        (ra-prime ra-prime) (rb-prime rb-prime) (tb-0 tb))))
  (origs (k (2 1)) (ra (5 0)) (rb (0 1)) (rb-prime (1 1))))

(defskeleton neuman-stubblebine-reauth
  (vars (k skey) (ra rb ra-prime rb-prime tb ra-0 rb-0 rb-1 text)
    (a b ks name))
  (defstrand resp 3 (k k) (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks))
  (defstrand resp-reauth 3 (k k) (ra-prime ra-prime) (rb-prime rb-prime)
    (tb tb) (a a) (b b) (ks ks))
  (defstrand keyserver 2 (k k) (ra ra-0) (rb rb-0) (tb tb) (a a) (b b)
    (ks ks))
  (defstrand resp 2 (ra ra-0) (rb rb-1) (tb tb) (a a) (b b) (ks ks))
  (defstrand init-reauth 4 (k k) (ra-prime ra-prime) (rb-prime rb-prime)
    (tb tb) (a a) (b b) (ks ks))
  (defstrand init 3 (k k) (ra ra-0) (rb rb) (tb tb) (a a) (b b) (ks ks))
  (precedes ((0 1) (5 1)) ((1 1) (4 2)) ((2 1) (4 0)) ((2 1) (5 1))
    ((3 1) (2 0)) ((4 1) (1 0)) ((4 3) (1 2)) ((5 2) (0 2)))
  (non-orig (ltk a ks) (ltk b ks))
  (uniq-orig k ra rb ra-prime rb-prime)
  (operation encryption-test (displaced 6 2 keyserver 2)
    (enc b ra-1 k tb (ltk a ks)) (5 1))
  (traces
    ((recv (cat a ra)) (send (cat b rb (enc a ra tb (ltk b ks))))
      (recv (cat (enc a k tb (ltk b ks)) (enc "one" rb k))))
    ((recv (cat (enc a k tb (ltk b ks)) ra-prime))
      (send (cat rb-prime (enc "two" ra-prime k)))
      (recv (enc "three" rb-prime k)))
    ((recv (cat b rb-0 (enc a ra-0 tb (ltk b ks))))
      (send
        (cat (enc b ra-0 k tb (ltk a ks)) (enc a k tb (ltk b ks))
          rb-0)))
    ((recv (cat a ra-0)) (send (cat b rb-1 (enc a ra-0 tb (ltk b ks)))))
    ((recv (enc a k tb (ltk b ks)))
      (send (cat (enc a k tb (ltk b ks)) ra-prime))
      (recv (cat rb-prime (enc "two" ra-prime k)))
      (send (enc "three" rb-prime k)))
    ((send (cat a ra-0))
      (recv
        (cat (enc b ra-0 k tb (ltk a ks)) (enc a k tb (ltk b ks)) rb))
      (send (cat (enc a k tb (ltk b ks)) (enc "one" rb k)))))
  (label 33)
  (parent 0)
  (realized)
  (shape)
  (maps
    ((0 1)
      ((ra ra) (tb tb) (rb rb) (a a) (b b) (ks ks) (k k)
        (ra-prime ra-prime) (rb-prime rb-prime) (tb-0 tb))))
  (origs (k (2 1)) (rb (0 1)) (ra-prime (4 1)) (rb-prime (1 1))))

(defskeleton neuman-stubblebine-reauth
  (vars (k skey)
    (ra rb ra-prime rb-prime tb ra-0 rb-0 rb-1 ra-prime-0 rb-prime-0
      text) (a b ks name))
  (defstrand resp 3 (k k) (ra ra) (rb rb) (tb tb) (a a) (b b) (ks ks))
  (defstrand resp-reauth 3 (k k) (ra-prime ra-prime) (rb-prime rb-prime)
    (tb tb) (a a) (b b) (ks ks))
  (defstrand keyserver 2 (k k) (ra ra-0) (rb rb-0) (tb tb) (a a) (b b)
    (ks ks))
  (defstrand resp 2 (ra ra-0) (rb rb-1) (tb tb) (a a) (b b) (ks ks))
  (defstrand init-reauth 4 (k k) (ra-prime ra-prime-0)
    (rb-prime rb-prime) (tb tb) (a a) (b b) (ks ks))
  (defstrand resp-reauth 2 (k k) (ra-prime ra-prime-0)
    (rb-prime rb-prime-0) (tb tb) (a a) (b b) (ks ks))
  (defstrand init 3 (k k) (ra ra-0) (rb rb) (tb tb) (a a) (b b) (ks ks))
  (precedes ((0 1) (6 1)) ((1 1) (4 2)) ((2 1) (1 0)) ((2 1) (4 0))
    ((2 1) (5 0)) ((2 1) (6 1)) ((3 1) (2 0)) ((4 3) (1 2))
    ((5 1) (4 2)) ((6 2) (0 2)))
  (non-orig (ltk a ks) (ltk b ks))
  (uniq-orig k ra rb ra-prime rb-prime)
  (operation encryption-test (displaced 7 2 keyserver 2)
    (enc b ra-1 k tb (ltk a ks)) (6 1))
  (traces
    ((recv (cat a ra)) (send (cat b rb (enc a ra tb (ltk b ks))))
      (recv (cat (enc a k tb (ltk b ks)) (enc "one" rb k))))
    ((recv (cat (enc a k tb (ltk b ks)) ra-prime))
      (send (cat rb-prime (enc "two" ra-prime k)))
      (recv (enc "three" rb-prime k)))
    ((recv (cat b rb-0 (enc a ra-0 tb (ltk b ks))))
      (send
        (cat (enc b ra-0 k tb (ltk a ks)) (enc a k tb (ltk b ks))
          rb-0)))
    ((recv (cat a ra-0)) (send (cat b rb-1 (enc a ra-0 tb (ltk b ks)))))
    ((recv (enc a k tb (ltk b ks)))
      (send (cat (enc a k tb (ltk b ks)) ra-prime-0))
      (recv (cat rb-prime (enc "two" ra-prime-0 k)))
      (send (enc "three" rb-prime k)))
    ((recv (cat (enc a k tb (ltk b ks)) ra-prime-0))
      (send (cat rb-prime-0 (enc "two" ra-prime-0 k))))
    ((send (cat a ra-0))
      (recv
        (cat (enc b ra-0 k tb (ltk a ks)) (enc a k tb (ltk b ks)) rb))
      (send (cat (enc a k tb (ltk b ks)) (enc "one" rb k)))))
  (label 35)
  (parent 0)
  (realized)
  (shape)
  (maps
    ((0 1)
      ((ra ra) (tb tb) (rb rb) (a a) (b b) (ks ks) (k k)
        (ra-prime ra-prime) (rb-prime rb-prime) (tb-0 tb))))
  (origs (k (2 1)) (rb (0 1)) (rb-prime (1 1))))

(comment "Nothing left to do")