---

PropertyO ==
  es:EO+(Info)
    ((n:E(New). e:E.
        ((e has New(n))
         (n loc e 
            (snd:E(Send). ((n <loc snd)  (snd < e)  snd has* New(n))))))
     (e1:E(Sign). b:E.
         ((b has signature(e1))
          (e2:E(Sign)
              ((Sign(e2) = Sign(e1))
               (e2 loc b 
                 (snd:E(Send)
                    ((e2 <loc snd)  (snd < b)  snd has* signature(e1))))))))
     (e1:E(Encrypt). b:E.
         ((b has cipherText(e1))
          (e2:E(Encrypt)
              ((Encrypt(e2) = Encrypt(e1))
               (e2 loc b 
                 (snd:E(Send)
                    ((e2 <loc snd)  (snd < b)  snd has* cipherText(e1)))))))))

---

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),  equal: s = t,  sdata: SecurityData,  product: x:A  B[x],  encryption-key: Key,  atom: Atom$n,  eclass-val: X(e),  ses-encrypt: Encrypt,  or: P  Q,  es-le: e loc e' ,  exists: x:A. B[x],  es-E-interface: E(X),  ses-send: Send,  es-locl: (e <loc e'),  and: P  Q,  es-causl: (e < e'),  event-has*: e has* a,  ses-crypt: cipherText(e)
FDL editor aliases :  ses-ordering

---

PropertyO  ==
    \mforall{}es:EO+(Info)
        ((\mforall{}n:E(New).  \mforall{}e:E.
                ((e  has  New(n))
                {}\mRightarrow{}  (n  \mleq{}loc  e    \mvee{}  (\mexists{}snd:E(Send).  ((n  <loc  snd)  \mwedge{}  (snd  <  e)  \mwedge{}  snd  has*  New(n))))))
        \mwedge{}  (\mforall{}e1:E(Sign).  \mforall{}b:E.
                  ((b  has  signature(e1))
                  {}\mRightarrow{}  (\mexists{}e2:E(Sign)
                            ((Sign(e2)  =  Sign(e1))
                            \mwedge{}  (e2  \mleq{}loc  b 
                                \mvee{}  (\mexists{}snd:E(Send).  ((e2  <loc  snd)  \mwedge{}  (snd  <  b)  \mwedge{}  snd  has*  signature(e1))))))))
        \mwedge{}  (\mforall{}e1:E(Encrypt).  \mforall{}b:E.
                  ((b  has  cipherText(e1))
                  {}\mRightarrow{}  (\mexists{}e2:E(Encrypt)
                            ((Encrypt(e2)  =  Encrypt(e1))
                            \mwedge{}  (e2  \mleq{}loc  b 
                                \mvee{}  (\mexists{}snd:E(Send).  ((e2  <loc  snd)  \mwedge{}  (snd  <  b)  \mwedge{}  snd  has*  cipherText(e1)))))))))


Date html generated: 2010_08_28-AM-02_09_09
Last ObjectModification: 2010_02_22-PM-04_02_56

Home Index