---

send-rcv-match(m1;m2) ==
  (m1  Send)  (m2  Rcv)  (m1 < m2)  (Send(m1) = Rcv(m2))

---

Definitions :  assert: b,  in-eclass: e  X,  and: P  Q,  es-causl: (e < e'),  equal: s = t,  sdata: SecurityData,  ses-send: Send,  eclass-val: X(e),  ses-rcv: Rcv
FDL editor aliases :  send-rcv-match

---

send-rcv-match(m1;m2)  ==    (\muparrow{}m1  \mmember{}\msubb{}  Send)  \mwedge{}  (\muparrow{}m2  \mmember{}\msubb{}  Rcv)  \mwedge{}  (m1  <  m2)  \mwedge{}  (Send(m1)  =  Rcv(m2))


Date html generated: 2010_08_28-AM-02_39_28
Last ObjectModification: 2010_02_22-PM-10_46_26

Home Index