{ 
[s:SES]. [A:Id]. (encryption-key-atoms(PrivateKey(A)) ~ [Private(A)]) }
{ Proof }
Definitions occuring in Statement :
ses-private-key: PrivateKey(A),
ses-private: Private(A),
security-event-structure: SES,
encryption-key-atoms: encryption-key-atoms(k),
Id: Id,
uall: [x:A]. B[x],
cons: [car / cdr],
nil: [],
sqequal: s ~ t
Definitions :
uall: [x:A]. B[x],
encryption-key-atoms: encryption-key-atoms(k),
ses-private-key: PrivateKey(A),
member: t 
T
Lemmas :
Id_wf,
security-event-structure_wf
\mforall{}[s:SES]. \mforall{}[A:Id]. (encryption-key-atoms(PrivateKey(A)) \msim{} [Private(A)])
Date html generated:
2011_08_17-PM-07_17_24
Last ObjectModification:
2011_06_18-PM-01_07_58
Home
Index