---

{ [s:SES]. [A:Id].  (PrivateKey(A)  Key) }

{ Proof }

---

Definitions occuring in Statement :  ses-private-key: PrivateKey(A),  security-event-structure: SES,  encryption-key: Key,  Id: Id,  uall: [x:A]. B[x],  member: t  T
Definitions :  uall: [x:A]. B[x],  member: t  T,  encryption-key: Key,  ses-private-key: PrivateKey(A)
Lemmas :  ses-private_wf,  Id_wf,  security-event-structure_wf

---

\mforall{}[s:SES].  \mforall{}[A:Id].    (PrivateKey(A)  \mmember{}  Key)


Date html generated: 2011_08_17-PM-07_16_25
Last ObjectModification: 2011_06_18-PM-01_04_58

Home Index