Nuprl Definition : protocol-action
ProtocolAction ==
n:Atom × if n =a "new" then Atom1
if n =a "send" then SecurityData
if n =a "rcv" then SecurityData
if n =a "encrypt" then SecurityData × Key × Atom1
if n =a "decrypt" then SecurityData × Key × Atom1
if n =a "sign" then SecurityData × Id × Atom1
if n =a "verify" then SecurityData × Id × Atom1
else Top
fi
Definitions occuring in Statement :
encryption-key: Key,
sdata: SecurityData,
Id: Id,
atom: Atom$n,
ifthenelse: if b then t else f fi ,
eq_atom: x =a y,
top: Top,
product: x:A × B[x],
token: "$token",
atom: Atom
FDL editor aliases :
p-act
Latex:
ProtocolAction ==
n:Atom \mtimes{} if n =a "new" then Atom1
if n =a "send" then SecurityData
if n =a "rcv" then SecurityData
if n =a "encrypt" then SecurityData \mtimes{} Key \mtimes{} Atom1
if n =a "decrypt" then SecurityData \mtimes{} Key \mtimes{} Atom1
if n =a "sign" then SecurityData \mtimes{} Id \mtimes{} Atom1
if n =a "verify" then SecurityData \mtimes{} Id \mtimes{} Atom1
else Top
fi
Date html generated:
2015_07_23-PM-00_13_33
Last ObjectModification:
2012_08_30-PM-04_29_55
Home
Index