---

ses-ordering'(s) ==
  es:EO+(Info). b:E.
    ((n:E(New)
        (b has* New(n)
         (n loc b 
            (snd:E(Send). ((n <loc snd)  (snd < b)  snd has* New(n))))))
     (e1:E(Sign)
         (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 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,  es-E: E,  ses-new: New,  Id: Id,  ses-sign: Sign,  ses-sig: signature(e),  all: x:A. B[x],  implies: 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,  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'

---

ses-ordering'(s)  ==
    \mforall{}es:EO+(Info).  \mforall{}b:E.
        ((\mforall{}n:E(New)
                (b  has*  New(n)
                {}\mRightarrow{}  (n  \mleq{}loc  b    \mvee{}  (\mexists{}snd:E(Send).  ((n  <loc  snd)  \mwedge{}  (snd  <  b)  \mwedge{}  snd  has*  New(n))))))
        \mwedge{}  (\mforall{}e1:E(Sign)
                  (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)
                  (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_21
Last ObjectModification: 2010_02_22-PM-04_09_10

Home Index