Nuprl Definition : ses-flow

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) ∈ SecurityData)
                          ∧ (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) ∈ SecurityData)
                            ∧ (cipherText(decr) = cipherText(encr) ∈ Atom1)
                            ∧ MatchingKeys(key(decr);key(encr)))
                          ∧ (¬(key(decr) = symmetric-key(a) ∈ Key))
                          ∧ (ses-flow a e1 encr)
                          ∧ (ses-flow cipherText(encr) encr decr)
                          ∧ (ses-flow a decr e2))))) 
  a 
  e1 
  e2


Definitions occuring in Statement :  event-has: (e has a),  ses-key-rel: MatchingKeys(k1;k2),  ses-cipher: cipherText(e),  ses-decryption-key: key(e),  ses-decrypted: plainText(e),  ses-decrypt: Decrypt,  ses-crypt: cipherText(e),  ses-encryption-key: key(e),  ses-encrypted: plainText(e),  ses-encrypt: Encrypt,  ses-rcv: Rcv,  ses-send: Send,  symmetric-key: symmetric-key(a),  encryption-key: Key,  sdata: SecurityData,  es-E-interface: E(X),  eclass-val: X(e),  es-causle: e c≤ e',  es-le: e ≤loc e' ,  es-locl: (e <loc e'),  es-causl: (e < e'),  atom: Atom$n,  ycomb: Y,  exists: ∃x:A. B[x],  not: ¬A,  or: P ∨ Q,  and: P ∧ Q,  apply: f a,  lambda: λx.A[x],  equal: s = t ∈ T
FDL editor aliases :  ses-flow
Latex:
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: 2015_07_23-PM-00_04_58
Last ObjectModification: 2012_08_30-PM-02_30_23

Home Index