{ 
[s:SES]. [A,B:Id]. uiff(PublicKey(A) = PrivateKey(B);False) }
{ Proof }
Definitions occuring in Statement :
ses-public-key: PublicKey(A),
ses-private-key: PrivateKey(A),
security-event-structure: SES,
encryption-key: Key,
Id: Id,
uiff: uiff(P;Q),
uall: [x:A]. B[x],
false: False,
equal: s = t
Definitions :
uall: [x:A]. B[x],
uiff: uiff(P;Q),
encryption-key: Key,
ses-public-key: PublicKey(A),
ses-private-key: PrivateKey(A),
false: False,
member: t 
T,
and: P 
Q,
uimplies: b supposing a,
prop: 
Lemmas :
Id_wf,
ses-private_wf,
false_wf,
security-event-structure_wf
\mforall{}[s:SES]. \mforall{}[A,B:Id]. uiff(PublicKey(A) = PrivateKey(B);False)
Date html generated:
2011_08_17-PM-07_16_44
Last ObjectModification:
2011_06_18-PM-01_06_46
Home
Index