---

Step * of Lemma ses-private-not-public

∀[s:SES]. ∀[A,B:Id].  uiff(PrivateKey(B) = PublicKey(A) ∈ Key;False)
BY
{ (Unfolds``encryption-key ses-public-key ses-private-key`` 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[s:SES].  \mforall{}[A,B:Id].    uiff(PrivateKey(B)  =  PublicKey(A);False)


By

---

Latex:
(Unfolds``encryption-key  ses-public-key  ses-private-key``  0  THEN  Auto)

---

Home Index