---

PropertyF ==
  es:EO+(Info)
    ((n:E(New). e:E.  ((e has New(n))  ses-flow(s;es;New(n);n;e)))
     (e1:E(Sign). b:E.
         ((b has signature(e1))
          (e2:E(Sign)
              ((Sign(e2) = Sign(e1))  ses-flow(s;es;signature(e2);e2;b)))))
     (e1:E(Encrypt). b:E.
         ((b has cipherText(e1))
          (e2:E(Encrypt)
              ((Encrypt(e2) = Encrypt(e1))
               ses-flow(s;es;cipherText(e2);e2;b))))))

---

Definitions :  event-ordering+: EO+(Info),  ses-info: Info,  ses-new: New,  Id: Id,  ses-sign: Sign,  ses-sig: signature(e),  all: x:A. B[x],  es-E: E,  implies: P  Q,  event-has: (e has a),  exists: x:A. B[x],  es-E-interface: E(X),  and: P  Q,  equal: s = t,  sdata: SecurityData,  product: x:A  B[x],  encryption-key: Key,  atom: Atom$n,  eclass-val: X(e),  ses-encrypt: Encrypt,  ses-flow: Error :ses-flow,  ses-crypt: cipherText(e)
FDL editor aliases :  ses-flow-axiom

---

PropertyF  ==
    \mforall{}es:EO+(Info)
        ((\mforall{}n:E(New).  \mforall{}e:E.    ((e  has  New(n))  {}\mRightarrow{}  ses-flow(s;es;New(n);n;e)))
        \mwedge{}  (\mforall{}e1:E(Sign).  \mforall{}b:E.
                  ((b  has  signature(e1))
                  {}\mRightarrow{}  (\mexists{}e2:E(Sign).  ((Sign(e2)  =  Sign(e1))  \mwedge{}  ses-flow(s;es;signature(e2);e2;b)))))
        \mwedge{}  (\mforall{}e1:E(Encrypt).  \mforall{}b:E.
                  ((b  has  cipherText(e1))
                  {}\mRightarrow{}  (\mexists{}e2:E(Encrypt).  ((Encrypt(e2)  =  Encrypt(e1))  \mwedge{}  ses-flow(s;es;cipherText(e2);e2;b))))))


Date html generated: 2010_08_28-AM-02_13_02
Last ObjectModification: 2010_03_09-PM-12_41_38

Home Index