---

ses-flow(s;es;a;e1;e2) ==
  Y 
  (ses-flow,a,e1,e2.
    (((e1 has a)  (e2 has a)  e1 loc e2 )
     (snd:E(Send)
        rcv:E(Rcv)
         (e1 c snd
          rcv c e2
          (snd < rcv)
          (Send(snd) = Rcv(rcv))
          (ses-flow a e1 snd)
          (ses-flow a rcv e2)))
     (encr:E(Encrypt)
        decr:E(Decrypt)
         ((e1 <loc encr)
          decr c e2
          (encr < decr)
          ((plainText(decr) = plainText(encr))
            (cipherText(decr) = cipherText(encr))
            MatchingKeys(key(decr);key(encr)))
          ((key(decr) = symmetric-key(a)))
          (ses-flow a e1 encr)
          (ses-flow cipherText(encr) encr decr)
          (ses-flow a decr e2))))) 
  a 
  e1 
  e2

---

Definitions :  ycomb: Y,  lambda: x.A[x],  event-has: (e has a),  es-le: e loc e' ,  or: P  Q,  ses-send: Send,  eclass-val: X(e),  ses-rcv: Rcv,  ses-encrypt: Encrypt,  exists: x:A. B[x],  es-E-interface: E(X),  ses-decrypt: Decrypt,  es-locl: (e <loc e'),  es-causle: e c e',  es-causl: (e < e'),  sdata: SecurityData,  ses-decrypted: plainText(e),  ses-encrypted: plainText(e),  atom: Atom$n,  ses-cipher: cipherText(e),  ses-key-rel: MatchingKeys(k1;k2),  ses-encryption-key: key(e),  not: A,  equal: s = t,  encryption-key: Key,  ses-decryption-key: key(e),  symmetric-key: symmetric-key(a),  and: P  Q,  ses-crypt: cipherText(e),  apply: f a
FDL editor aliases :  ses-flow

---

ses-flow(s;es;a;e1;e2)  ==
    Y 
    (\mlambda{}ses-flow,a,e1,e2.
        (((e1  has  a)  \mwedge{}  (e2  has  a)  \mwedge{}  e1  \mleq{}loc  e2  )
        \mvee{}  (\mexists{}snd:E(Send)
                \mexists{}rcv:E(Rcv)
                  (e1  c\mleq{}  snd
                  \mwedge{}  rcv  c\mleq{}  e2
                  \mwedge{}  (snd  <  rcv)
                  \mwedge{}  (Send(snd)  =  Rcv(rcv))
                  \mwedge{}  (ses-flow  a  e1  snd)
                  \mwedge{}  (ses-flow  a  rcv  e2)))
        \mvee{}  (\mexists{}encr:E(Encrypt)
                \mexists{}decr:E(Decrypt)
                  ((e1  <loc  encr)
                  \mwedge{}  decr  c\mleq{}  e2
                  \mwedge{}  (encr  <  decr)
                  \mwedge{}  ((plainText(decr)  =  plainText(encr))
                      \mwedge{}  (cipherText(decr)  =  cipherText(encr))
                      \mwedge{}  MatchingKeys(key(decr);key(encr)))
                  \mwedge{}  (\mneg{}(key(decr)  =  symmetric-key(a)))
                  \mwedge{}  (ses-flow  a  e1  encr)
                  \mwedge{}  (ses-flow  cipherText(encr)  encr  decr)
                  \mwedge{}  (ses-flow  a  decr  e2))))) 
    a 
    e1 
    e2


Date html generated: 2010_08_28-AM-02_07_00
Last ObjectModification: 2010_03_11-AM-11_54_46

Home Index