---

Step * 1 1 of Lemma ses-cipher-unique2


1. s : SES@i'
2. PropertyO@i'
3. ∀[es:EO+(Info)]. ∀[a,b:E(Encrypt)].
     Encrypt(a) = Encrypt(b) ∈ (SecurityData × Key × Atom1) supposing cipherText(a) = cipherText(b) ∈ Atom1
4. es : EO+(Info)@i'
5. ∀[a,b:E(Encrypt)].
     Encrypt(a) = Encrypt(b) ∈ (SecurityData × Key × Atom1) supposing cipherText(a) = cipherText(b) ∈ Atom1
6. a : E(Encrypt)@i
7. ∀[b:E(Encrypt)]
     Encrypt(a) = Encrypt(b) ∈ (SecurityData × Key × Atom1) supposing cipherText(a) = cipherText(b) ∈ Atom1
8. b : E(Encrypt)@i
9. Encrypt(a) = Encrypt(b) ∈ (SecurityData × Key × Atom1) supposing cipherText(a) = cipherText(b) ∈ Atom1
⊢ (cipherText(a) = cipherText(b) ∈ Atom1) ⇒ {(plainText(a) = plainText(b) ∈ SecurityData) ∧ (key(a) = key(b) ∈ Key)}
BY
{ (ParallelLast THEN RepUR ``ses-encrypted ses-encryption-key guard`` 0 THEN Auto) }

---

Latex:

---

Latex:

1.  s  :  SES@i'
2.  PropertyO@i'
3.  \mforall{}[es:EO+(Info)].  \mforall{}[a,b:E(Encrypt)].
          Encrypt(a)  =  Encrypt(b)  supposing  cipherText(a)  =  cipherText(b)
4.  es  :  EO+(Info)@i'
5.  \mforall{}[a,b:E(Encrypt)].    Encrypt(a)  =  Encrypt(b)  supposing  cipherText(a)  =  cipherText(b)
6.  a  :  E(Encrypt)@i
7.  \mforall{}[b:E(Encrypt)].  Encrypt(a)  =  Encrypt(b)  supposing  cipherText(a)  =  cipherText(b)
8.  b  :  E(Encrypt)@i
9.  Encrypt(a)  =  Encrypt(b)  supposing  cipherText(a)  =  cipherText(b)
\mvdash{}  (cipherText(a)  =  cipherText(b))  {}\mRightarrow{}  \{(plainText(a)  =  plainText(b))  \mwedge{}  (key(a)  =  key(b))\}


By

---

Latex:
(ParallelLast  THEN  RepUR  ``ses-encrypted  ses-encryption-key  guard``  0  THEN  Auto)

---

Home Index