---

{ [s:SES]. [A,B:Id].  uiff(PrivateKey(B) = PublicKey(A);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-private-key: PrivateKey(A),  ses-public-key: PublicKey(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(PrivateKey(B)  =  PublicKey(A);False)


Date html generated: 2011_08_17-PM-07_16_54
Last ObjectModification: 2011_06_18-PM-01_07_04

Home Index