Nuprl Definition : security-event-structure
SES ==
Info:Type
× New:EClass(Atom1)
× Send:EClass(SecurityData)
× Rcv:EClass(SecurityData)
× Encrypt:EClass(SecurityData × Key × Atom1)
× Decrypt:EClass(SecurityData × Key × Atom1)
× Sign:EClass(SecurityData × Id × Atom1)
× Verify:EClass(SecurityData × Id × Atom1)
× Honest:Id ─→ 𝔹
× KeyRel:Key ─→ Key ─→ 𝔹
× PrivKey:Id ─→ Atom1
× Top
Definitions occuring in Statement :
encryption-key: Key,
sdata: SecurityData,
eclass: EClass(A[eo; e]),
Id: Id,
atom: Atom$n,
bool: 𝔹,
top: Top,
function: x:A ─→ B[x],
product: x:A × B[x],
universe: Type
FDL editor aliases :
security-event-structure
Latex:
SES ==
Info:Type
\mtimes{} New:EClass(Atom1)
\mtimes{} Send:EClass(SecurityData)
\mtimes{} Rcv:EClass(SecurityData)
\mtimes{} Encrypt:EClass(SecurityData \mtimes{} Key \mtimes{} Atom1)
\mtimes{} Decrypt:EClass(SecurityData \mtimes{} Key \mtimes{} Atom1)
\mtimes{} Sign:EClass(SecurityData \mtimes{} Id \mtimes{} Atom1)
\mtimes{} Verify:EClass(SecurityData \mtimes{} Id \mtimes{} Atom1)
\mtimes{} Honest:Id {}\mrightarrow{} \mBbbB{}
\mtimes{} KeyRel:Key {}\mrightarrow{} Key {}\mrightarrow{} \mBbbB{}
\mtimes{} PrivKey:Id {}\mrightarrow{} Atom1
\mtimes{} Top
Date html generated:
2015_07_23-PM-00_01_58
Last ObjectModification:
2012_08_30-PM-02_30_15
Home
Index