---

Step * 1 1 1 of Lemma ses-cipher-unique


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. ↑a ∈b Encrypt
11. cipherText(b)#Encrypt(a):SecurityData × Key × Atom1@i
⊢ False
BY
{ Subst' Encrypt(a) ~ <plainText(a), key(a), cipherText(a)> -1⋅ }

1
.....equality..... 
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. ↑a ∈b Encrypt
11. cipherText(b)#Encrypt(a):SecurityData × Key × Atom1@i
⊢ Encrypt(a) ~ <plainText(a), key(a), cipherText(a)>

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. ↑a ∈b Encrypt
11. cipherText(b)#<plainText(a), key(a), cipherText(a)>:SecurityData × Key × Atom1@i
⊢ False

---

Latex:

---

Latex:

1.  s  :  SES@i'
2.  es  :  EO+(Info)@i'
3.  a  :  E(Encrypt)@i
4.  \mforall{}a1:E(Encrypt)
          ((a1  <  a)  {}\mRightarrow{}  (\mforall{}b:E(Encrypt).  ((cipherText(a1)  =  cipherText(b))  {}\mRightarrow{}  (Encrypt(a1)  =  Encrypt(b)))))
5.  b  :  E(Encrypt)@i
6.  cipherText(a)  =  cipherText(b)@i
7.  \mforall{}n:E(New).  \mforall{}e:E.
          ((e  has  New(n))
          {}\mRightarrow{}  (n  \mleq{}loc  e    \mvee{}  (\mexists{}snd:E(Send).  ((n  <loc  snd)  \mwedge{}  (snd  <  e)  \mwedge{}  snd  has*  New(n)))))@i'
8.  \mforall{}e1:E(Sign).  \mforall{}b:E.
          ((b  has  signature(e1))
          {}\mRightarrow{}  (\mexists{}e2:E(Sign)
                    ((Sign(e2)  =  Sign(e1))
                    \mwedge{}  (e2  \mleq{}loc  b 
                        \mvee{}  (\mexists{}snd:E(Send).  ((e2  <loc  snd)  \mwedge{}  (snd  <  b)  \mwedge{}  snd  has*  signature(e1)))))))@i'
9.  \mforall{}e1:E(Encrypt).  \mforall{}b:E.
          ((b  has  cipherText(e1))
          {}\mRightarrow{}  (\mexists{}e2:E(Encrypt)
                    ((Encrypt(e2)  =  Encrypt(e1))
                    \mwedge{}  (e2  \mleq{}loc  b 
                        \mvee{}  (\mexists{}snd:E(Send).  ((e2  <loc  snd)  \mwedge{}  (snd  <  b)  \mwedge{}  snd  has*  cipherText(e1)))))))@i'
10.  \muparrow{}a  \mmember{}\msubb{}  Encrypt
11.  cipherText(b)\#Encrypt(a):SecurityData  \mtimes{}  Key  \mtimes{}  Atom1@i
\mvdash{}  False


By

---

Latex:
Subst'  Encrypt(a)  \msim{}  <plainText(a),  key(a),  cipherText(a)>  -1\mcdot{}

---

Home Index