PropertyV ==
es:EO+(Info). e:E(Verify). 
e':E(Sign). ((e' < e) 
(Verify(e) = Sign(e')))
Definitions :
event-ordering+: EO+(Info),
ses-info: Info,
all: x:A. B[x],
exists: x:A. B[x],
es-E-interface: E(X),
and: P Q,
es-causl: (e < e'),
equal: s = t,
sdata: SecurityData,
product: x:A 
B[x],
Id: Id,
atom: Atom$n,
ses-verify: Verify,
eclass-val: X(e),
ses-sign: Sign
FDL editor aliases :
ses-V
PropertyV == \mforall{}es:EO+(Info). \mforall{}e:E(Verify). \mexists{}e':E(Sign). ((e' < e) \mwedge{} (Verify(e) = Sign(e')))
Date html generated:
2010_08_28-AM-02_33_40
Last ObjectModification:
2010_02_22-PM-05_23_50
Home
Index