---

Step * of Lemma ses-cipher-unique

∀[s:SES]
  ∀[es:EO+(Info)]. ∀[a,b:E(Encrypt)].
    Encrypt(a) = Encrypt(b) ∈ (SecurityData × Key × Atom1) supposing cipherText(a) = cipherText(b) ∈ Atom1 
  supposing PropertyO
BY
{ RemoveUniform Auto Auto }

1
∀s:SES
  (PropertyO
  ⇒ (∀es:EO+(Info). ∀a,b:E(Encrypt).
        ((cipherText(a) = cipherText(b) ∈ Atom1) ⇒ (Encrypt(a) = Encrypt(b) ∈ (SecurityData × Key × Atom1)))))

---

Latex:

---

Latex:
\mforall{}[s:SES]
    \mforall{}[es:EO+(Info)].  \mforall{}[a,b:E(Encrypt)].
        Encrypt(a)  =  Encrypt(b)  supposing  cipherText(a)  =  cipherText(b) 
    supposing  PropertyO


By

---

Latex:
RemoveUniform  Auto  Auto

---

Home Index