cpsa-4.4.4: tst/DH_hack_shapes.tst

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

(herald "DH Hack" (bound 15))

(comment "CPSA 4.3.1")

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

(comment "Strand count bounded at 15")

(defprotocol DH_hack basic
  (defrole init1
    (vars (gcs name) (cek skey) (x y akey) (d data))
    (trace
      (send
        (enc x (enc cek (hash (invk x) y)) (enc d cek) (privk gcs))))
    (uniq-orig d cek x))
  (defrole resp
    (vars (gcs name) (cek skey) (x y akey) (d data))
    (trace
      (recv
        (enc x (enc cek (hash x (invk y))) (enc d cek) (privk gcs))))
    (non-orig (privk gcs)))
  (defrole commute
    (vars (gcs name) (cek skey) (x y akey) (d data))
    (trace
      (recv (enc x (enc cek (hash (invk x) y)) (enc d cek) (privk gcs)))
      (send
        (enc x (enc cek (hash x (invk y))) (enc d cek) (privk gcs))))
    (non-orig (privk gcs)))
  (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 DH_hack
  (vars (d data) (cek skey) (x y akey) (gcs name))
  (defstrand resp 1 (d d) (cek cek) (x x) (y y) (gcs gcs))
  (non-orig (invk x) (invk y) (privk gcs))
  (traces
    ((recv
       (enc x (enc cek (hash x (invk y))) (enc d cek) (privk gcs)))))
  (label 0)
  (unrealized (0 0))
  (origs)
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton DH_hack
  (vars (d data) (cek skey) (x y akey) (gcs name))
  (defstrand resp 1 (d d) (cek cek) (x x) (y y) (gcs gcs))
  (defstrand commute 2 (d d) (cek cek) (x x) (y y) (gcs gcs))
  (defstrand init1 1 (d d) (cek cek) (x x) (y y) (gcs gcs))
  (precedes ((1 1) (0 0)) ((2 0) (1 0)))
  (non-orig (invk x) (invk y) (privk gcs))
  (uniq-orig d cek x)
  (operation encryption-test (added-strand init1 1)
    (enc x (enc cek (hash (invk x) y)) (enc d cek) (privk gcs)) (1 0))
  (traces
    ((recv (enc x (enc cek (hash x (invk y))) (enc d cek) (privk gcs))))
    ((recv (enc x (enc cek (hash (invk x) y)) (enc d cek) (privk gcs)))
      (send
        (enc x (enc cek (hash x (invk y))) (enc d cek) (privk gcs))))
    ((send
       (enc x (enc cek (hash (invk x) y)) (enc d cek) (privk gcs)))))
  (label 2)
  (parent 0)
  (realized)
  (shape)
  (maps ((0) ((x x) (y y) (gcs gcs) (cek cek) (d d))))
  (origs (cek (2 0)) (d (2 0)) (x (2 0))))

(comment "Nothing left to do")

(defprotocol DH_hack basic
  (defrole init1
    (vars (gcs name) (cek skey) (x y akey) (d data))
    (trace
      (send
        (enc x (enc cek (hash (invk x) y)) (enc d cek) (privk gcs))))
    (uniq-orig d cek x))
  (defrole resp
    (vars (gcs name) (cek skey) (x y akey) (d data))
    (trace
      (recv
        (enc x (enc cek (hash x (invk y))) (enc d cek) (privk gcs))))
    (non-orig (privk gcs)))
  (defrole commute
    (vars (gcs name) (cek skey) (x y akey) (d data))
    (trace
      (recv (enc x (enc cek (hash (invk x) y)) (enc d cek) (privk gcs)))
      (send
        (enc x (enc cek (hash x (invk y))) (enc d cek) (privk gcs))))
    (non-orig (privk gcs)))
  (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 DH_hack
  (vars (d data) (cek skey) (x y akey) (gcs name))
  (defstrand resp 1 (d d) (cek cek) (x x) (y y) (gcs gcs))
  (non-orig (invk x) (privk gcs))
  (traces
    ((recv
       (enc x (enc cek (hash x (invk y))) (enc d cek) (privk gcs)))))
  (label 3)
  (unrealized (0 0))
  (origs)
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton DH_hack
  (vars (d data) (cek skey) (x y akey) (gcs name))
  (defstrand resp 1 (d d) (cek cek) (x x) (y y) (gcs gcs))
  (defstrand commute 2 (d d) (cek cek) (x x) (y y) (gcs gcs))
  (defstrand init1 1 (d d) (cek cek) (x x) (y y) (gcs gcs))
  (precedes ((1 1) (0 0)) ((2 0) (1 0)))
  (non-orig (invk x) (privk gcs))
  (uniq-orig d cek x)
  (operation encryption-test (added-strand init1 1)
    (enc x (enc cek (hash (invk x) y)) (enc d cek) (privk gcs)) (1 0))
  (traces
    ((recv (enc x (enc cek (hash x (invk y))) (enc d cek) (privk gcs))))
    ((recv (enc x (enc cek (hash (invk x) y)) (enc d cek) (privk gcs)))
      (send
        (enc x (enc cek (hash x (invk y))) (enc d cek) (privk gcs))))
    ((send
       (enc x (enc cek (hash (invk x) y)) (enc d cek) (privk gcs)))))
  (label 5)
  (parent 3)
  (realized)
  (shape)
  (maps ((0) ((cek cek) (x x) (gcs gcs) (y y) (d d))))
  (origs (cek (2 0)) (d (2 0)) (x (2 0))))

(comment "Nothing left to do")

(defprotocol DH_hack basic
  (defrole init1
    (vars (gcs name) (cek skey) (x y akey) (d data))
    (trace
      (send
        (enc x (enc cek (hash (invk x) y)) (enc d cek) (privk gcs))))
    (uniq-orig d cek x))
  (defrole resp
    (vars (gcs name) (cek skey) (x y akey) (d data))
    (trace
      (recv
        (enc x (enc cek (hash x (invk y))) (enc d cek) (privk gcs))))
    (non-orig (privk gcs)))
  (defrole commute
    (vars (gcs name) (cek skey) (x y akey) (d data))
    (trace
      (recv (enc x (enc cek (hash (invk x) y)) (enc d cek) (privk gcs)))
      (send
        (enc x (enc cek (hash x (invk y))) (enc d cek) (privk gcs))))
    (non-orig (privk gcs)))
  (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 DH_hack
  (vars (d data) (cek skey) (y x akey) (gcs name))
  (defstrand resp 1 (d d) (cek cek) (x x) (y y) (gcs gcs))
  (non-orig (invk y) (privk gcs))
  (traces
    ((recv
       (enc x (enc cek (hash x (invk y))) (enc d cek) (privk gcs)))))
  (label 6)
  (unrealized (0 0))
  (origs)
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton DH_hack
  (vars (d data) (cek skey) (y x akey) (gcs name))
  (defstrand resp 1 (d d) (cek cek) (x x) (y y) (gcs gcs))
  (defstrand commute 2 (d d) (cek cek) (x x) (y y) (gcs gcs))
  (defstrand init1 1 (d d) (cek cek) (x x) (y y) (gcs gcs))
  (precedes ((1 1) (0 0)) ((2 0) (1 0)))
  (non-orig (invk y) (privk gcs))
  (uniq-orig d cek x)
  (operation encryption-test (added-strand init1 1)
    (enc x (enc cek (hash (invk x) y)) (enc d cek) (privk gcs)) (1 0))
  (traces
    ((recv (enc x (enc cek (hash x (invk y))) (enc d cek) (privk gcs))))
    ((recv (enc x (enc cek (hash (invk x) y)) (enc d cek) (privk gcs)))
      (send
        (enc x (enc cek (hash x (invk y))) (enc d cek) (privk gcs))))
    ((send
       (enc x (enc cek (hash (invk x) y)) (enc d cek) (privk gcs)))))
  (label 8)
  (parent 6)
  (realized)
  (shape)
  (maps ((0) ((cek cek) (y y) (gcs gcs) (x x) (d d))))
  (origs (cek (2 0)) (d (2 0)) (x (2 0))))

(comment "Nothing left to do")

(defprotocol DH_hack basic
  (defrole init1
    (vars (gcs name) (cek skey) (x y akey) (d data))
    (trace
      (send
        (enc x (enc cek (hash (invk x) y)) (enc d cek) (privk gcs))))
    (uniq-orig d cek x))
  (defrole resp
    (vars (gcs name) (cek skey) (x y akey) (d data))
    (trace
      (recv
        (enc x (enc cek (hash x (invk y))) (enc d cek) (privk gcs))))
    (non-orig (privk gcs)))
  (defrole commute
    (vars (gcs name) (cek skey) (x y akey) (d data))
    (trace
      (recv (enc x (enc cek (hash (invk x) y)) (enc d cek) (privk gcs)))
      (send
        (enc x (enc cek (hash x (invk y))) (enc d cek) (privk gcs))))
    (non-orig (privk gcs)))
  (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 DH_hack
  (vars (d data) (cek skey) (x y akey) (gcs name))
  (defstrand resp 1 (d d) (cek cek) (x x) (y y) (gcs gcs))
  (deflistener cek)
  (non-orig (invk x) (invk y) (privk gcs))
  (traces
    ((recv (enc x (enc cek (hash x (invk y))) (enc d cek) (privk gcs))))
    ((recv cek) (send cek)))
  (label 9)
  (unrealized (0 0))
  (origs)
  (comment "1 in cohort - 1 not yet seen"))

(comment "Nothing left to do")

(defprotocol DH_hack basic
  (defrole init1
    (vars (gcs name) (cek skey) (x y akey) (d data))
    (trace
      (send
        (enc x (enc cek (hash (invk x) y)) (enc d cek) (privk gcs))))
    (uniq-orig d cek x))
  (defrole resp
    (vars (gcs name) (cek skey) (x y akey) (d data))
    (trace
      (recv
        (enc x (enc cek (hash x (invk y))) (enc d cek) (privk gcs))))
    (non-orig (privk gcs)))
  (defrole commute
    (vars (gcs name) (cek skey) (x y akey) (d data))
    (trace
      (recv (enc x (enc cek (hash (invk x) y)) (enc d cek) (privk gcs)))
      (send
        (enc x (enc cek (hash x (invk y))) (enc d cek) (privk gcs))))
    (non-orig (privk gcs)))
  (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 DH_hack
  (vars (d data) (cek skey) (x y akey) (gcs name))
  (defstrand resp 1 (d d) (cek cek) (x x) (y y) (gcs gcs))
  (deflistener cek)
  (non-orig (invk x) (privk gcs))
  (traces
    ((recv (enc x (enc cek (hash x (invk y))) (enc d cek) (privk gcs))))
    ((recv cek) (send cek)))
  (label 20)
  (unrealized (0 0))
  (origs)
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton DH_hack
  (vars (d data) (cek skey) (x y akey) (gcs name))
  (defstrand resp 1 (d d) (cek cek) (x x) (y y) (gcs gcs))
  (deflistener cek)
  (defstrand commute 2 (d d) (cek cek) (x x) (y y) (gcs gcs))
  (defstrand init1 1 (d d) (cek cek) (x x) (y y) (gcs gcs))
  (precedes ((2 1) (0 0)) ((2 1) (1 0)) ((3 0) (2 0)))
  (non-orig (invk x) (privk gcs))
  (uniq-orig d cek x)
  (operation nonce-test (displaced 4 2 commute 2) cek (1 0)
    (enc cek (hash (invk x) y)))
  (traces
    ((recv (enc x (enc cek (hash x (invk y))) (enc d cek) (privk gcs))))
    ((recv cek) (send cek))
    ((recv (enc x (enc cek (hash (invk x) y)) (enc d cek) (privk gcs)))
      (send
        (enc x (enc cek (hash x (invk y))) (enc d cek) (privk gcs))))
    ((send
       (enc x (enc cek (hash (invk x) y)) (enc d cek) (privk gcs)))))
  (label 23)
  (parent 20)
  (realized)
  (shape)
  (maps ((0 1) ((cek cek) (x x) (gcs gcs) (y y) (d d))))
  (origs (cek (3 0)) (d (3 0)) (x (3 0))))

(defskeleton DH_hack
  (vars (d data) (cek skey) (x y akey) (gcs name))
  (defstrand resp 1 (d d) (cek cek) (x x) (y y) (gcs gcs))
  (deflistener cek)
  (defstrand commute 2 (d d) (cek cek) (x x) (y y) (gcs gcs))
  (defstrand init1 1 (d d) (cek cek) (x x) (y y) (gcs gcs))
  (defstrand commute 2 (d d) (cek cek) (x x) (y y) (gcs gcs))
  (precedes ((2 1) (0 0)) ((3 0) (2 0)) ((3 0) (4 0)) ((4 1) (1 0)))
  (non-orig (invk x) (privk gcs))
  (uniq-orig d cek x)
  (operation encryption-test (displaced 5 3 init1 1)
    (enc x (enc cek (hash (invk x) y)) (enc d-0 cek) (privk gcs-0))
    (4 0))
  (traces
    ((recv (enc x (enc cek (hash x (invk y))) (enc d cek) (privk gcs))))
    ((recv cek) (send cek))
    ((recv (enc x (enc cek (hash (invk x) y)) (enc d cek) (privk gcs)))
      (send
        (enc x (enc cek (hash x (invk y))) (enc d cek) (privk gcs))))
    ((send (enc x (enc cek (hash (invk x) y)) (enc d cek) (privk gcs))))
    ((recv (enc x (enc cek (hash (invk x) y)) (enc d cek) (privk gcs)))
      (send
        (enc x (enc cek (hash x (invk y))) (enc d cek) (privk gcs)))))
  (label 26)
  (parent 20)
  (realized)
  (shape)
  (maps ((0 1) ((cek cek) (x x) (gcs gcs) (y y) (d d))))
  (origs (cek (3 0)) (d (3 0)) (x (3 0))))

(comment "Nothing left to do")

(defprotocol DH_hack basic
  (defrole init1
    (vars (gcs name) (cek skey) (x y akey) (d data))
    (trace
      (send
        (enc x (enc cek (hash (invk x) y)) (enc d cek) (privk gcs))))
    (uniq-orig d cek x))
  (defrole resp
    (vars (gcs name) (cek skey) (x y akey) (d data))
    (trace
      (recv
        (enc x (enc cek (hash x (invk y))) (enc d cek) (privk gcs))))
    (non-orig (privk gcs)))
  (defrole commute
    (vars (gcs name) (cek skey) (x y akey) (d data))
    (trace
      (recv (enc x (enc cek (hash (invk x) y)) (enc d cek) (privk gcs)))
      (send
        (enc x (enc cek (hash x (invk y))) (enc d cek) (privk gcs))))
    (non-orig (privk gcs)))
  (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 DH_hack
  (vars (d data) (cek skey) (y x akey) (gcs name))
  (defstrand resp 1 (d d) (cek cek) (x x) (y y) (gcs gcs))
  (deflistener cek)
  (non-orig (invk y) (privk gcs))
  (traces
    ((recv (enc x (enc cek (hash x (invk y))) (enc d cek) (privk gcs))))
    ((recv cek) (send cek)))
  (label 27)
  (unrealized (0 0))
  (origs)
  (comment "1 in cohort - 1 not yet seen"))

(defskeleton DH_hack
  (vars (d data) (cek skey) (y x akey) (gcs name))
  (defstrand resp 1 (d d) (cek cek) (x x) (y y) (gcs gcs))
  (deflistener cek)
  (defstrand commute 2 (d d) (cek cek) (x x) (y y) (gcs gcs))
  (defstrand init1 1 (d d) (cek cek) (x x) (y y) (gcs gcs))
  (precedes ((2 1) (0 0)) ((3 0) (1 0)) ((3 0) (2 0)))
  (non-orig (invk y) (privk gcs))
  (uniq-orig d cek x)
  (operation encryption-test (added-strand init1 1)
    (enc x (enc cek (hash (invk x) y)) (enc d cek) (privk gcs)) (2 0))
  (traces
    ((recv (enc x (enc cek (hash x (invk y))) (enc d cek) (privk gcs))))
    ((recv cek) (send cek))
    ((recv (enc x (enc cek (hash (invk x) y)) (enc d cek) (privk gcs)))
      (send
        (enc x (enc cek (hash x (invk y))) (enc d cek) (privk gcs))))
    ((send
       (enc x (enc cek (hash (invk x) y)) (enc d cek) (privk gcs)))))
  (label 29)
  (parent 27)
  (realized)
  (shape)
  (maps ((0 1) ((cek cek) (y y) (gcs gcs) (x x) (d d))))
  (origs (cek (3 0)) (d (3 0)) (x (3 0))))

(comment "Nothing left to do")