---

Step * 1 of Lemma ses-cipher-unique2


∀s:SES
  (PropertyO
  ⇒ (∀es:EO+(Info). ∀a,b:E(Encrypt).
        ((cipherText(a) = cipherText(b) ∈ Atom1)
        ⇒ {(plainText(a) = plainText(b) ∈ SecurityData) ∧ (key(a) = key(b) ∈ Key)})))
BY
{ (InstLemma `ses-cipher-unique` []
   THEN RepeatFor 2 ((ParallelLast' THENA Auto))
   THEN RepeatFor 3 ((ParallelLast THENA Auto))) }

1
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)}

---

Latex:

---

Latex:

\mforall{}s:SES
    (PropertyO
    {}\mRightarrow{}  (\mforall{}es:EO+(Info).  \mforall{}a,b:E(Encrypt).
                ((cipherText(a)  =  cipherText(b))  {}\mRightarrow{}  \{(plainText(a)  =  plainText(b))  \mwedge{}  (key(a)  =  key(b))\})))


By

---

Latex:
(InstLemma  `ses-cipher-unique`  []
  THEN  RepeatFor  2  ((ParallelLast'  THENA  Auto))
  THEN  RepeatFor  3  ((ParallelLast  THENA  Auto)))

---

Home Index