---

Step * of Lemma ses-public-not-private

∀[s:SES]. ∀[A,B:Id].  uiff(PublicKey(A) = PrivateKey(B) ∈ 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(PublicKey(A)  =  PrivateKey(B);False)


By

---

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

---

Home Index