Step
*
of Lemma
ses-public-one-one
∀[A,B:Id].  uiff(PublicKey(A) = PublicKey(B) ∈ Key;A = B ∈ Id)
BY
{ (Unfolds``encryption-key ses-public-key`` 0 THEN Auto) }
Latex:
Latex:
\mforall{}[A,B:Id].    uiff(PublicKey(A)  =  PublicKey(B);A  =  B)
By
Latex:
(Unfolds``encryption-key  ses-public-key``  0  THEN  Auto)
Home
Index