Step
*
1
2
2
1
1
2
1
1
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)
28. ∃i:Id
((i ∈ C)
∧ (∃e:E
((loc(e) = i ∈ Id)
∧ (((↑e ∈b New) ∧ (b = New(e) ∈ Atom1))
∨ ((↑e ∈b Encrypt) ∧ (b = cipherText(e) ∈ Atom1) ∧ (∃c∈ns. (¬(c = b ∈ Atom1)) ∧ (e has c)))))))
⊢ ∃e:E. ((¬(e = e2 ∈ E)) ∧ ses-flow(s;es;b;e;e2))
BY
{ RepeatFor 2 ((D (-1) THEN ExRepD)) }
1
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)
24. ¬(b = a ∈ Atom1)
25. (encr has b)
26. e2 : E(Encrypt)
27. Encrypt(e2) = Encrypt(encr) ∈ (SecurityData × Key × Atom1)
28. ses-flow(s;es;cipherText(e2);e2;e)
29. (e2 has b)
30. i1 : Id
31. (i1 ∈ C)
32. e3 : E
33. loc(e3) = i1 ∈ Id
34. ↑e3 ∈b New
35. b = New(e3) ∈ Atom1
⊢ ∃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)
24. ¬(b = a ∈ Atom1)
25. (encr has b)
26. e2 : E(Encrypt)
27. Encrypt(e2) = Encrypt(encr) ∈ (SecurityData × Key × Atom1)
28. ses-flow(s;es;cipherText(e2);e2;e)
29. (e2 has b)
30. i1 : Id
31. (i1 ∈ C)
32. e3 : E
33. loc(e3) = i1 ∈ Id
34. ↑e3 ∈b Encrypt
35. b = cipherText(e3) ∈ Atom1
36. (∃c∈ns. (¬(c = b ∈ Atom1)) ∧ (e3 has c))
⊢ ∃e:E. ((¬(e = e2 ∈ E)) ∧ ses-flow(s;es;b;e;e2))
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)
28. \mexists{}i:Id
((i \mmember{} C)
\mwedge{} (\mexists{}e:E
((loc(e) = i)
\mwedge{} (((\muparrow{}e \mmember{}\msubb{} New) \mwedge{} (b = New(e)))
\mvee{} ((\muparrow{}e \mmember{}\msubb{} Encrypt) \mwedge{} (b = cipherText(e)) \mwedge{} (\mexists{}c\mmember{}ns. (\mneg{}(c = b)) \mwedge{} (e has c)))))))
\mvdash{} \mexists{}e:E. ((\mneg{}(e = e2)) \mwedge{} ses-flow(s;es;b;e;e2))
By
Latex:
RepeatFor 2 ((D (-1) THEN ExRepD))
Home
Index