Nuprl Definition : same-action
same-action(x;y) ==
((↑x ∈b New) ∧ (↑y ∈b New) ∧ (New(x) = New(y) ∈ Atom1))
∨ ((↑x ∈b Send) ∧ (↑y ∈b Send) ∧ (Send(x) = Send(y) ∈ SecurityData))
∨ ((↑x ∈b Rcv) ∧ (↑y ∈b Rcv) ∧ (Rcv(x) = Rcv(y) ∈ SecurityData))
∨ ((↑x ∈b Encrypt) ∧ (↑y ∈b Encrypt) ∧ (Encrypt(x) = Encrypt(y) ∈ (SecurityData × Key × Atom1)))
∨ ((↑x ∈b Decrypt) ∧ (↑y ∈b Decrypt) ∧ (Decrypt(x) = Decrypt(y) ∈ (SecurityData × Key × Atom1)))
∨ ((↑x ∈b Sign) ∧ (↑y ∈b Sign) ∧ (Sign(x) = Sign(y) ∈ (SecurityData × Id × Atom1)))
∨ ((↑x ∈b Verify) ∧ (↑y ∈b Verify) ∧ (Verify(x) = Verify(y) ∈ (SecurityData × Id × Atom1)))
Definitions occuring in Statement :
ses-decrypt: Decrypt,
ses-encrypt: Encrypt,
ses-verify: Verify,
ses-sign: Sign,
ses-rcv: Rcv,
ses-send: Send,
ses-new: New,
encryption-key: Key,
sdata: SecurityData,
eclass-val: X(e),
in-eclass: e ∈b X,
Id: Id,
atom: Atom$n,
assert: ↑b,
or: P ∨ Q,
and: P ∧ Q,
product: x:A × B[x],
equal: s = t ∈ T
FDL editor aliases :
same-action
Latex:
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:
2015_07_23-PM-00_04_53
Last ObjectModification:
2012_08_30-PM-02_30_23
Home
Index