Nuprl Definition : ses-is-protocol-action
pa(e) ==
let n,v = pa
in if n =a "new" then (↑e ∈b New) ∧ (New(e) = v ∈ Atom1)
if n =a "send" then (↑e ∈b Send) ∧ (Send(e) = v ∈ SecurityData)
if n =a "rcv" then (↑e ∈b Rcv) ∧ (Rcv(e) = v ∈ SecurityData)
if n =a "encrypt" then (↑e ∈b Encrypt) ∧ (Encrypt(e) = v ∈ (SecurityData × Key × Atom1))
if n =a "decrypt" then (↑e ∈b Decrypt) ∧ (Decrypt(e) = v ∈ (SecurityData × Key × Atom1))
if n =a "sign" then (↑e ∈b Sign) ∧ (Sign(e) = v ∈ (SecurityData × Id × Atom1))
if n =a "verify" then (↑e ∈b Verify) ∧ (Verify(e) = v ∈ (SecurityData × Id × Atom1))
else False
fi
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,
ifthenelse: if b then t else f fi ,
eq_atom: x =a y,
and: P ∧ Q,
false: False,
spread: spread def,
product: x:A × B[x],
token: "$token",
equal: s = t ∈ T
FDL editor aliases :
is-p-act
Latex:
pa(e) ==
let n,v = pa
in if n =a "new" then (\muparrow{}e \mmember{}\msubb{} New) \mwedge{} (New(e) = v)
if n =a "send" then (\muparrow{}e \mmember{}\msubb{} Send) \mwedge{} (Send(e) = v)
if n =a "rcv" then (\muparrow{}e \mmember{}\msubb{} Rcv) \mwedge{} (Rcv(e) = v)
if n =a "encrypt" then (\muparrow{}e \mmember{}\msubb{} Encrypt) \mwedge{} (Encrypt(e) = v)
if n =a "decrypt" then (\muparrow{}e \mmember{}\msubb{} Decrypt) \mwedge{} (Decrypt(e) = v)
if n =a "sign" then (\muparrow{}e \mmember{}\msubb{} Sign) \mwedge{} (Sign(e) = v)
if n =a "verify" then (\muparrow{}e \mmember{}\msubb{} Verify) \mwedge{} (Verify(e) = v)
else False
fi
Date html generated:
2016_05_17-PM-00_39_42
Last ObjectModification:
2012_08_30-PM-04_31_08
Theory : event-logic-applications
Home
Index