---

Step * 1 of Lemma ses-cipher-unique


∀s:SES
  (PropertyO
  ⇒ (∀es:EO+(Info). ∀a,b:E(Encrypt).
        ((cipherText(a) = cipherText(b) ∈ Atom1) ⇒ (Encrypt(a) = Encrypt(b) ∈ (SecurityData × Key × Atom1)))))
BY
{ (RepeatFor 3 ((D 0 THENA Auto))
   THEN CausalInd'
   THEN Auto
   THEN (With ⌈es⌉ (D 2)⋅ THENA Auto)
   THEN ExRepD
   THEN (InstHyp [⌈b⌉;⌈a⌉] (-1)⋅ THENA Auto)) }

1
.....antecedent..... 
1. s : SES@i'
2. es : EO+(Info)@i'
3. a : E(Encrypt)@i
4. ∀a1:E(Encrypt)
     ((a1 < a)
     ⇒ (∀b:E(Encrypt)
           ((cipherText(a1) = cipherText(b) ∈ Atom1) ⇒ (Encrypt(a1) = Encrypt(b) ∈ (SecurityData × Key × Atom1)))))
5. b : E(Encrypt)@i
6. cipherText(a) = cipherText(b) ∈ Atom1@i
7. ∀n:E(New). ∀e:E.  ((e has New(n)) ⇒ (n ≤loc e  ∨ (∃snd:E(Send). ((n <loc snd) ∧ (snd < e) ∧ snd has* New(n)))))@i'
8. ∀e1:E(Sign). ∀b:E.
     ((b has signature(e1))
     ⇒ (∃e2:E(Sign)
          ((Sign(e2) = Sign(e1) ∈ (SecurityData × Id × Atom1))
          ∧ (e2 ≤loc b  ∨ (∃snd:E(Send). ((e2 <loc snd) ∧ (snd < b) ∧ snd has* signature(e1)))))))@i'
9. ∀e1:E(Encrypt). ∀b:E.
     ((b has cipherText(e1))
     ⇒ (∃e2:E(Encrypt)
          ((Encrypt(e2) = Encrypt(e1) ∈ (SecurityData × Key × Atom1))
          ∧ (e2 ≤loc b  ∨ (∃snd:E(Send). ((e2 <loc snd) ∧ (snd < b) ∧ snd has* cipherText(e1)))))))@i'
⊢ (a has cipherText(b))

2
1. s : SES@i'
2. es : EO+(Info)@i'
3. a : E(Encrypt)@i
4. ∀a1:E(Encrypt)
     ((a1 < a)
     ⇒ (∀b:E(Encrypt)
           ((cipherText(a1) = cipherText(b) ∈ Atom1) ⇒ (Encrypt(a1) = Encrypt(b) ∈ (SecurityData × Key × Atom1)))))
5. b : E(Encrypt)@i
6. cipherText(a) = cipherText(b) ∈ Atom1@i
7. ∀n:E(New). ∀e:E.  ((e has New(n)) ⇒ (n ≤loc e  ∨ (∃snd:E(Send). ((n <loc snd) ∧ (snd < e) ∧ snd has* New(n)))))@i'
8. ∀e1:E(Sign). ∀b:E.
     ((b has signature(e1))
     ⇒ (∃e2:E(Sign)
          ((Sign(e2) = Sign(e1) ∈ (SecurityData × Id × Atom1))
          ∧ (e2 ≤loc b  ∨ (∃snd:E(Send). ((e2 <loc snd) ∧ (snd < b) ∧ snd has* signature(e1)))))))@i'
9. ∀e1:E(Encrypt). ∀b:E.
     ((b has cipherText(e1))
     ⇒ (∃e2:E(Encrypt)
          ((Encrypt(e2) = Encrypt(e1) ∈ (SecurityData × Key × Atom1))
          ∧ (e2 ≤loc b  ∨ (∃snd:E(Send). ((e2 <loc snd) ∧ (snd < b) ∧ snd has* cipherText(e1)))))))@i'
10. ∃e2:E(Encrypt)
     ((Encrypt(e2) = Encrypt(b) ∈ (SecurityData × Key × Atom1))
     ∧ (e2 ≤loc a  ∨ (∃snd:E(Send). ((e2 <loc snd) ∧ (snd < a) ∧ snd has* cipherText(b)))))
⊢ Encrypt(a) = Encrypt(b) ∈ (SecurityData × Key × Atom1)

---

Latex:

---

Latex:

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


By

---

Latex:
(RepeatFor  3  ((D  0  THENA  Auto))
  THEN  CausalInd'
  THEN  Auto
  THEN  (With  \mkleeneopen{}es\mkleeneclose{}  (D  2)\mcdot{}  THENA  Auto)
  THEN  ExRepD
  THEN  (InstHyp  [\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{}]  (-1)\mcdot{}  THENA  Auto))

---

Home Index