cpsa-4.4.4: tst/dhcr_um_exercise_resolved_bug_shapes.tst

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

(herald "DHCR: unified model (UM) original" (bound 20) (limit 12000)
  (algebra diffie-hellman))

(comment "CPSA 4.3.1")

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

(comment "Step count limited to 12000")

(comment "Strand count bounded at 20")

(defprotocol dhcr-um diffie-hellman
  (defrole init
    (vars (l x rndx) (gb gy base) (a b name) (na nb data)
      (priv-stor locn))
    (trace (load priv-stor (pv a l))
      (recv (sig (body b gb (pubk "sig" b)) (privk "sig" b)))
      (send (cat na a b (exp (gen) x)))
      (recv (cat gy (enc na nb a b (hash (exp gb l) (exp gy x)))))
      (send nb))
    (uniq-orig na)
    (uniq-gen x)
    (absent (x l))
    (gen-st (pv a l))
    (fn-of ("principal-of" (ltxa a) (ltxb b))
      ("ltx-of" (a ltxa) (b ltxb))))
  (defrole resp
    (vars (l y rndx) (ga gx base) (a b name) (na nb data)
      (priv-stor locn))
    (trace (load priv-stor (pv b l))
      (recv (sig (body a ga (pubk "sig" a)) (privk "sig" a)))
      (recv (cat na a b gx))
      (send
        (cat (exp (gen) y)
          (enc na nb a b (hash (exp ga l) (exp gx y))))) (recv nb))
    (uniq-orig nb)
    (uniq-gen y)
    (absent (y l))
    (facts (neq gx (gen)))
    (gen-st (pv b l))
    (fn-of ("principal-of" (ltxa a) (ltxb b))
      ("ltx-of" (a ltxa) (b ltxb))))
  (defrole ltx-gen
    (vars (self name) (l rndx) (priv-stor locn) (ignore mesg))
    (trace (load priv-stor ignore) (stor priv-stor (pv self l))
      (send
        (sig (body self (exp (gen) l) (pubk "sig" self))
          (privk "sig" self))))
    (uniq-orig l)
    (fn-of ("principal-of" (l self)) ("ltx-of" (self l))))
  (defrole ltx-disclose
    (vars (self name) (l rndx) (priv-stor locn))
    (trace (load priv-stor (pv self l)) (stor priv-stor "nil") (send l))
    (gen-st (pv self l))
    (fn-of ("principal-of" (l self)) ("ltx-of" (self l))))
  (defrule fact-resp-silly
    (forall ((z strd) (gx base))
      (implies
        (and (p "resp" z 3) (p "resp" "gx" z gx))
        (fact silly gx))))
  (defrule fact-resp-neq0
    (forall ((z strd))
      (implies (and (p "resp" z 3) (p "resp" "gx" z (gen))) (false))))
  (defrule fact-init-neq0
    (forall ((z strd))
      (implies (and (p "init" z 4) (p "init" "gy" z (gen))) (false))))
  (defrule undisclosed-not-disclosed
    (forall ((z strd) (l rndx))
      (implies
        (and (fact undisclosed l) (p "ltx-disclose" z 2)
          (p "ltx-disclose" "l" z l))
        (false))))
  (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))))
  (defgenrule shearsRule
    (forall ((z0 z1 z2 strd) (i0 i1 i2 indx))
      (implies
        (and (trans z0 i0) (trans z1 i1) (trans z2 i2)
          (leads-to z0 i0 z1 i1) (same-locn z0 i0 z2 i2)
          (prec z0 i0 z2 i2))
        (or (and (= z1 z2) (= i1 i2)) (prec z1 i1 z2 i2)))))
  (defgenrule invShearsRule
    (forall ((z0 z1 z2 strd) (i0 i1 i2 indx))
      (implies
        (and (trans z0 i0) (trans z1 i1) (same-locn z0 i0 z1 i1)
          (leads-to z1 i1 z2 i2) (prec z0 i0 z2 i2))
        (or (and (= z0 z1) (= i0 i1)) (prec z0 i0 z1 i1)))))
  (defgenrule fact-resp-neq0
    (forall ((z strd) (gx base))
      (implies (and (p "resp" z 3) (p "resp" "gx" z gx))
        (fact neq gx (gen)))))
  (defgenrule trRl_ltx-gen-at-1
    (forall ((z strd)) (implies (p "ltx-gen" z 2) (trans z 1))))
  (defgenrule trRl_ltx-gen-at-0
    (forall ((z strd)) (implies (p "ltx-gen" z 2) (trans z 0))))
  (defgenrule trRl_ltx-disclose-at-1
    (forall ((z strd)) (implies (p "ltx-disclose" z 2) (trans z 1))))
  (defgenrule trRl_ltx-disclose-at-0
    (forall ((z strd)) (implies (p "ltx-disclose" z 2) (trans z 0))))
  (defgenrule gen-st-init-0
    (forall ((z strd) (l rndx) (a name))
      (implies
        (and (p "init" z 1) (p "init" "l" z l) (p "init" "a" z a))
        (gen-st (pv a l)))))
  (defgenrule gen-st-resp-0
    (forall ((z strd) (l rndx) (b name))
      (implies
        (and (p "resp" z 1) (p "resp" "l" z l) (p "resp" "b" z b))
        (gen-st (pv b l)))))
  (defgenrule gen-st-ltx-disclose-0
    (forall ((z strd) (l rndx) (self name))
      (implies
        (and (p "ltx-disclose" z 1) (p "ltx-disclose" "l" z l)
          (p "ltx-disclose" "self" z self)) (gen-st (pv self l)))))
  (lang (sig sign) (body (tuple 3)) (pv (tuple 2))))

(defskeleton dhcr-um
  (vars (na nb data) (a b name) (pt pval) (gy base) (priv-stor locn)
    (l l-peer x rndx))
  (defstrand init 4 (na na) (nb nb) (a a) (b b) (gb (exp (gen) l-peer))
    (gy gy) (priv-stor priv-stor) (l l) (x x))
  (non-orig (privk "sig" b))
  (uniq-orig na)
  (uniq-gen x)
  (absent (x l))
  (facts (neq a b) (undisclosed l) (undisclosed l-peer))
  (traces
    ((load priv-stor (cat pt (pv a l)))
      (recv
        (sig (body b (exp (gen) l-peer) (pubk "sig" b))
          (privk "sig" b))) (send (cat na a b (exp (gen) x)))
      (recv
        (cat gy
          (enc na nb a b
            (hash (exp (gen) (mul l l-peer)) (exp gy x)))))))
  (label 0)
  (unrealized (0 1) (0 3))
  (origs (na (0 2)))
  (comment "Not closed under rules"))

(defskeleton dhcr-um
  (vars (ignore ignore-0 mesg) (na nb data) (b self name)
    (pt pt-0 pt-1 pt-2 pval) (priv-stor priv-stor-0 locn)
    (y l l-0 x rndx))
  (defstrand init 4 (na na) (nb nb) (a self) (b b) (gb (exp (gen) l))
    (gy (exp (gen) y)) (priv-stor priv-stor-0) (l l-0) (x x))
  (defstrand ltx-gen 3 (ignore ignore) (self b) (priv-stor priv-stor)
    (l l))
  (defstrand resp 4 (na na) (nb nb) (a self) (b b) (ga (exp (gen) l-0))
    (gx (exp (gen) x)) (priv-stor priv-stor) (l l) (y y))
  (defstrand ltx-gen 3 (ignore ignore-0) (self self)
    (priv-stor priv-stor-0) (l l-0))
  (precedes ((0 2) (2 2)) ((1 1) (2 0)) ((1 2) (0 1)) ((2 3) (0 3))
    ((3 1) (0 0)) ((3 2) (2 1)))
  (non-orig (privk "sig" b))
  (uniq-orig na nb l l-0)
  (uniq-gen y x)
  (absent (y l) (x l-0))
  (gen-st (pv b l) (pv self l-0))
  (facts (silly (exp (gen) x)) (neq (exp (gen) x) (gen)) (trans 1 1)
    (trans 1 0) (trans 3 1) (trans 3 0) (neq self b) (undisclosed l-0)
    (undisclosed l))
  (operation nonce-test (displaced 4 0 init 3) (exp (gen) x-0) (2 2))
  (traces
    ((load priv-stor-0 (cat pt-2 (pv self l-0)))
      (recv (sig (body b (exp (gen) l) (pubk "sig" b)) (privk "sig" b)))
      (send (cat na self b (exp (gen) x)))
      (recv
        (cat (exp (gen) y)
          (enc na nb self b
            (hash (exp (gen) (mul l l-0)) (exp (gen) (mul y x)))))))
    ((load priv-stor (cat pt ignore))
      (stor priv-stor (cat pt-0 (pv b l)))
      (send
        (sig (body b (exp (gen) l) (pubk "sig" b)) (privk "sig" b))))
    ((load priv-stor (cat pt-0 (pv b l)))
      (recv
        (sig (body self (exp (gen) l-0) (pubk "sig" self))
          (privk "sig" self))) (recv (cat na self b (exp (gen) x)))
      (send
        (cat (exp (gen) y)
          (enc na nb self b
            (hash (exp (gen) (mul l l-0)) (exp (gen) (mul y x)))))))
    ((load priv-stor-0 (cat pt-1 ignore-0))
      (stor priv-stor-0 (cat pt-2 (pv self l-0)))
      (send
        (sig (body self (exp (gen) l-0) (pubk "sig" self))
          (privk "sig" self)))))
  (label 18)
  (parent 0)
  (realized)
  (shape)
  (maps
    ((0)
      ((a self) (b b) (l l-0) (l-peer l) (x x) (gy (exp (gen) y))
        (na na) (nb nb) (priv-stor priv-stor-0) (pt pt-2))))
  (origs (na (0 2)) (l-0 (3 1)) (pt-2 (3 1)) (l (1 1)) (pt-0 (1 1))
    (nb (2 3))))

(defskeleton dhcr-um
  (vars (ignore ignore-0 mesg) (na nb data) (b self name)
    (pt pt-0 pt-1 pt-2 pval) (priv-stor priv-stor-0 locn) (y l rndx)
    (w expt) (l-0 x rndx))
  (defstrand init 4 (na na) (nb nb) (a self) (b b) (gb (exp (gen) l))
    (gy (exp (gen) (mul y w))) (priv-stor priv-stor-0) (l l-0) (x x))
  (defstrand ltx-gen 3 (ignore ignore) (self b) (priv-stor priv-stor)
    (l l))
  (defstrand resp 4 (na na) (nb nb) (a self) (b b) (ga (exp (gen) l-0))
    (gx (exp (gen) (mul w x))) (priv-stor priv-stor) (l l) (y y))
  (defstrand ltx-gen 3 (ignore ignore-0) (self self)
    (priv-stor priv-stor-0) (l l-0))
  (precedes ((0 2) (2 2)) ((1 1) (2 0)) ((1 2) (0 1)) ((2 3) (0 3))
    ((3 1) (0 0)) ((3 2) (2 1)))
  (non-orig (privk "sig" b))
  (uniq-orig na nb l l-0)
  (uniq-gen y x)
  (absent (y l) (x l-0))
  (gen-st (pv b l) (pv self l-0))
  (facts (silly (exp (gen) (mul w x))) (neq (exp (gen) (mul w x)) (gen))
    (trans 1 1) (trans 1 0) (trans 3 1) (trans 3 0) (neq self b)
    (undisclosed l-0) (undisclosed l))
  (operation generalization deleted (4 0))
  (traces
    ((load priv-stor-0 (cat pt-2 (pv self l-0)))
      (recv (sig (body b (exp (gen) l) (pubk "sig" b)) (privk "sig" b)))
      (send (cat na self b (exp (gen) x)))
      (recv
        (cat (exp (gen) (mul y w))
          (enc na nb self b
            (hash (exp (gen) (mul l l-0)) (exp (gen) (mul y w x)))))))
    ((load priv-stor (cat pt ignore))
      (stor priv-stor (cat pt-0 (pv b l)))
      (send
        (sig (body b (exp (gen) l) (pubk "sig" b)) (privk "sig" b))))
    ((load priv-stor (cat pt-0 (pv b l)))
      (recv
        (sig (body self (exp (gen) l-0) (pubk "sig" self))
          (privk "sig" self)))
      (recv (cat na self b (exp (gen) (mul w x))))
      (send
        (cat (exp (gen) y)
          (enc na nb self b
            (hash (exp (gen) (mul l l-0)) (exp (gen) (mul y w x)))))))
    ((load priv-stor-0 (cat pt-1 ignore-0))
      (stor priv-stor-0 (cat pt-2 (pv self l-0)))
      (send
        (sig (body self (exp (gen) l-0) (pubk "sig" self))
          (privk "sig" self)))))
  (label 90)
  (parent 0)
  (realized)
  (shape)
  (maps
    ((0)
      ((a self) (b b) (l l-0) (l-peer l) (x x)
        (gy (exp (gen) (mul y w))) (na na) (nb nb)
        (priv-stor priv-stor-0) (pt pt-2))))
  (origs (na (0 2)) (l-0 (3 1)) (pt-2 (3 1)) (l (1 1)) (pt-0 (1 1))
    (nb (2 3))))

(comment "Nothing left to do")