---

same-action(x;y) ==
  ((x  New)  (y  New)  (New(x) = New(y)))
   ((x  Send)  (y  Send)  (Send(x) = Send(y)))
   ((x  Rcv)  (y  Rcv)  (Rcv(x) = Rcv(y)))
   ((x  Encrypt)  (y  Encrypt)  (Encrypt(x) = Encrypt(y)))
   ((x  Decrypt)  (y  Decrypt)  (Decrypt(x) = Decrypt(y)))
   ((x  Sign)  (y  Sign)  (Sign(x) = Sign(y)))
   ((x  Verify)  (y  Verify)  (Verify(x) = Verify(y)))

---

Definitions :  ses-new: New,  ses-send: Send,  ses-rcv: Rcv,  ses-encrypt: Encrypt,  encryption-key: Key,  ses-decrypt: Decrypt,  or: P  Q,  ses-sign: Sign,  and: P  Q,  assert: b,  in-eclass: e  X,  equal: s = t,  sdata: SecurityData,  product: x:A  B[x],  Id: Id,  atom: Atom$n,  eclass-val: X(e),  ses-verify: Verify
FDL editor aliases :  same-action

---

same-action(x;y)  ==
    ((\muparrow{}x  \mmember{}\msubb{}  New)  \mwedge{}  (\muparrow{}y  \mmember{}\msubb{}  New)  \mwedge{}  (New(x)  =  New(y)))
    \mvee{}  ((\muparrow{}x  \mmember{}\msubb{}  Send)  \mwedge{}  (\muparrow{}y  \mmember{}\msubb{}  Send)  \mwedge{}  (Send(x)  =  Send(y)))
    \mvee{}  ((\muparrow{}x  \mmember{}\msubb{}  Rcv)  \mwedge{}  (\muparrow{}y  \mmember{}\msubb{}  Rcv)  \mwedge{}  (Rcv(x)  =  Rcv(y)))
    \mvee{}  ((\muparrow{}x  \mmember{}\msubb{}  Encrypt)  \mwedge{}  (\muparrow{}y  \mmember{}\msubb{}  Encrypt)  \mwedge{}  (Encrypt(x)  =  Encrypt(y)))
    \mvee{}  ((\muparrow{}x  \mmember{}\msubb{}  Decrypt)  \mwedge{}  (\muparrow{}y  \mmember{}\msubb{}  Decrypt)  \mwedge{}  (Decrypt(x)  =  Decrypt(y)))
    \mvee{}  ((\muparrow{}x  \mmember{}\msubb{}  Sign)  \mwedge{}  (\muparrow{}y  \mmember{}\msubb{}  Sign)  \mwedge{}  (Sign(x)  =  Sign(y)))
    \mvee{}  ((\muparrow{}x  \mmember{}\msubb{}  Verify)  \mwedge{}  (\muparrow{}y  \mmember{}\msubb{}  Verify)  \mwedge{}  (Verify(x)  =  Verify(y)))


Date html generated: 2010_08_28-AM-02_06_47
Last ObjectModification: 2010_02_22-PM-02_07_17

Home Index