---

Step * 1 2 2 1 1 2 of Lemma cabal-theorem


1. s : SES@i'
2. A : SecurityAxioms@i'
3. s2 : Top@i'
4. es : EO+(Info)@i'
5. C : Id List@i
6. (∀A@0∈C.Honest(A@0))
7. ns : Atom1 List@i
8. (∀a∈ns.(∃i∈C. ∃e:E
                  ((loc(e) = i ∈ Id)
                  ∧ (((↑e ∈b New) ∧ (a = New(e) ∈ Atom1))
                    ∨ ((↑e ∈b Encrypt) ∧ (a = cipherText(e) ∈ Atom1) ∧ (∃b∈ns. (¬(b = a ∈ Atom1)) ∧ (e has b))))))
      ∧ (∀e:E(Send). ((loc(e) ∈ C) ⇒ (¬(e has a))))
      ∧ (∀e:E(Encrypt)
           ((loc(e) ∈ C)
           ⇒ (e has a)
           ⇒ ((∃A∈C. key(e) = PublicKey(A) ∈ Key)
              ∨ (∃k∈ns. key(e) = symmetric-key(k) ∈ Key)
              ∨ (cipherText(e) ∈ ns)))))@i
9. PropertyF
10. e : E@i
11. ∀e1:E. ((e1 < e) ⇒ (∃a∈ns. (e1 has a)) ⇒ (loc(e1) ∈ C))
12. a : Atom1
13. (a ∈ ns)
14. (e has a)
15. ∀x,y:E. ∀a:Atom1.  (ses-flow(s;es;a;x;y) ⇒ y c≤ e ⇒ (a ∈ ns) ⇒ (loc(x) ∈ C) ⇒ (loc(y) ∈ C))
16. i : Id
17. (i ∈ C)
18. encr : E
19. loc(encr) = i ∈ Id
20. ↑encr ∈b Encrypt
21. a = cipherText(encr) ∈ Atom1
22. b : Atom1
23. (b ∈ ns) ∧ (¬(b = a ∈ Atom1)) ∧ (encr has b)
24. e2 : E(Encrypt)
25. Encrypt(e2) = Encrypt(encr) ∈ (SecurityData × Key × Atom1)
26. ses-flow(s;es;cipherText(e2);e2;e)
27. (e2 has b)
⊢ ∃e:E. ((e <loc e2) ∧ (e has b))
BY
{ Assert ⌈∃e:E. ((¬(e = e2 ∈ E)) ∧ ses-flow(s;es;b;e;e2))⌉⋅ }

1
.....assertion..... 
1. s : SES@i'
2. A : SecurityAxioms@i'
3. s2 : Top@i'
4. es : EO+(Info)@i'
5. C : Id List@i
6. (∀A@0∈C.Honest(A@0))
7. ns : Atom1 List@i
8. (∀a∈ns.(∃i∈C. ∃e:E
                  ((loc(e) = i ∈ Id)
                  ∧ (((↑e ∈b New) ∧ (a = New(e) ∈ Atom1))
                    ∨ ((↑e ∈b Encrypt) ∧ (a = cipherText(e) ∈ Atom1) ∧ (∃b∈ns. (¬(b = a ∈ Atom1)) ∧ (e has b))))))
      ∧ (∀e:E(Send). ((loc(e) ∈ C) ⇒ (¬(e has a))))
      ∧ (∀e:E(Encrypt)
           ((loc(e) ∈ C)
           ⇒ (e has a)
           ⇒ ((∃A∈C. key(e) = PublicKey(A) ∈ Key)
              ∨ (∃k∈ns. key(e) = symmetric-key(k) ∈ Key)
              ∨ (cipherText(e) ∈ ns)))))@i
9. PropertyF
10. e : E@i
11. ∀e1:E. ((e1 < e) ⇒ (∃a∈ns. (e1 has a)) ⇒ (loc(e1) ∈ C))
12. a : Atom1
13. (a ∈ ns)
14. (e has a)
15. ∀x,y:E. ∀a:Atom1.  (ses-flow(s;es;a;x;y) ⇒ y c≤ e ⇒ (a ∈ ns) ⇒ (loc(x) ∈ C) ⇒ (loc(y) ∈ C))
16. i : Id
17. (i ∈ C)
18. encr : E
19. loc(encr) = i ∈ Id
20. ↑encr ∈b Encrypt
21. a = cipherText(encr) ∈ Atom1
22. b : Atom1
23. (b ∈ ns) ∧ (¬(b = a ∈ Atom1)) ∧ (encr has b)
24. e2 : E(Encrypt)
25. Encrypt(e2) = Encrypt(encr) ∈ (SecurityData × Key × Atom1)
26. ses-flow(s;es;cipherText(e2);e2;e)
27. (e2 has b)
⊢ ∃e:E. ((¬(e = e2 ∈ E)) ∧ ses-flow(s;es;b;e;e2))

2
1. s : SES@i'
2. A : SecurityAxioms@i'
3. s2 : Top@i'
4. es : EO+(Info)@i'
5. C : Id List@i
6. (∀A@0∈C.Honest(A@0))
7. ns : Atom1 List@i
8. (∀a∈ns.(∃i∈C. ∃e:E
                  ((loc(e) = i ∈ Id)
                  ∧ (((↑e ∈b New) ∧ (a = New(e) ∈ Atom1))
                    ∨ ((↑e ∈b Encrypt) ∧ (a = cipherText(e) ∈ Atom1) ∧ (∃b∈ns. (¬(b = a ∈ Atom1)) ∧ (e has b))))))
      ∧ (∀e:E(Send). ((loc(e) ∈ C) ⇒ (¬(e has a))))
      ∧ (∀e:E(Encrypt)
           ((loc(e) ∈ C)
           ⇒ (e has a)
           ⇒ ((∃A∈C. key(e) = PublicKey(A) ∈ Key)
              ∨ (∃k∈ns. key(e) = symmetric-key(k) ∈ Key)
              ∨ (cipherText(e) ∈ ns)))))@i
9. PropertyF
10. e : E@i
11. ∀e1:E. ((e1 < e) ⇒ (∃a∈ns. (e1 has a)) ⇒ (loc(e1) ∈ C))
12. a : Atom1
13. (a ∈ ns)
14. (e has a)
15. ∀x,y:E. ∀a:Atom1.  (ses-flow(s;es;a;x;y) ⇒ y c≤ e ⇒ (a ∈ ns) ⇒ (loc(x) ∈ C) ⇒ (loc(y) ∈ C))
16. i : Id
17. (i ∈ C)
18. encr : E
19. loc(encr) = i ∈ Id
20. ↑encr ∈b Encrypt
21. a = cipherText(encr) ∈ Atom1
22. b : Atom1
23. (b ∈ ns) ∧ (¬(b = a ∈ Atom1)) ∧ (encr has b)
24. e2 : E(Encrypt)
25. Encrypt(e2) = Encrypt(encr) ∈ (SecurityData × Key × Atom1)
26. ses-flow(s;es;cipherText(e2);e2;e)
27. (e2 has b)
28. ∃e:E. ((¬(e = e2 ∈ E)) ∧ ses-flow(s;es;b;e;e2))
⊢ ∃e:E. ((e <loc e2) ∧ (e has b))

---

Latex:

---

Latex:

1.  s  :  SES@i'
2.  A  :  SecurityAxioms@i'
3.  s2  :  Top@i'
4.  es  :  EO+(Info)@i'
5.  C  :  Id  List@i
6.  (\mforall{}A@0\mmember{}C.Honest(A@0))
7.  ns  :  Atom1  List@i
8.  (\mforall{}a\mmember{}ns.(\mexists{}i\mmember{}C.  \mexists{}e:E
                                    ((loc(e)  =  i)
                                    \mwedge{}  (((\muparrow{}e  \mmember{}\msubb{}  New)  \mwedge{}  (a  =  New(e)))
                                        \mvee{}  ((\muparrow{}e  \mmember{}\msubb{}  Encrypt)  \mwedge{}  (a  =  cipherText(e))  \mwedge{}  (\mexists{}b\mmember{}ns.  (\mneg{}(b  =  a))  \mwedge{}  (e  has  b))))))
            \mwedge{}  (\mforall{}e:E(Send).  ((loc(e)  \mmember{}  C)  {}\mRightarrow{}  (\mneg{}(e  has  a))))
            \mwedge{}  (\mforall{}e:E(Encrypt)
                      ((loc(e)  \mmember{}  C)
                      {}\mRightarrow{}  (e  has  a)
                      {}\mRightarrow{}  ((\mexists{}A\mmember{}C.  key(e)  =  PublicKey(A))
                            \mvee{}  (\mexists{}k\mmember{}ns.  key(e)  =  symmetric-key(k))
                            \mvee{}  (cipherText(e)  \mmember{}  ns)))))@i
9.  PropertyF
10.  e  :  E@i
11.  \mforall{}e1:E.  ((e1  <  e)  {}\mRightarrow{}  (\mexists{}a\mmember{}ns.  (e1  has  a))  {}\mRightarrow{}  (loc(e1)  \mmember{}  C))
12.  a  :  Atom1
13.  (a  \mmember{}  ns)
14.  (e  has  a)
15.  \mforall{}x,y:E.  \mforall{}a:Atom1.    (ses-flow(s;es;a;x;y)  {}\mRightarrow{}  y  c\mleq{}  e  {}\mRightarrow{}  (a  \mmember{}  ns)  {}\mRightarrow{}  (loc(x)  \mmember{}  C)  {}\mRightarrow{}  (loc(y)  \mmember{}  C))
16.  i  :  Id
17.  (i  \mmember{}  C)
18.  encr  :  E
19.  loc(encr)  =  i
20.  \muparrow{}encr  \mmember{}\msubb{}  Encrypt
21.  a  =  cipherText(encr)
22.  b  :  Atom1
23.  (b  \mmember{}  ns)  \mwedge{}  (\mneg{}(b  =  a))  \mwedge{}  (encr  has  b)
24.  e2  :  E(Encrypt)
25.  Encrypt(e2)  =  Encrypt(encr)
26.  ses-flow(s;es;cipherText(e2);e2;e)
27.  (e2  has  b)
\mvdash{}  \mexists{}e:E.  ((e  <loc  e2)  \mwedge{}  (e  has  b))


By

---

Latex:
Assert  \mkleeneopen{}\mexists{}e:E.  ((\mneg{}(e  =  e2))  \mwedge{}  ses-flow(s;es;b;e;e2))\mkleeneclose{}\mcdot{}

---

Home Index