Step
*
1
2
2
1
1
2
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)
28. ∃e:E. ((¬(e = e2 ∈ E)) ∧ ses-flow(s;es;b;e;e2))
⊢ ∃e:E. ((e <loc e2) ∧ (e has b))
BY
{ (ExRepD⋅
THEN Assert ⌈∀e1,e2:E. ∀b:Atom1.
(ses-flow(s;es;b;e1;e2) ⇒ (↑e2 ∈b Encrypt) ⇒ (¬(e1 = e2 ∈ E)) ⇒ (∃e:E. ((e <loc e2) ∧ (e has b))))⌉
⋅
) }
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)
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. e3 : E
31. ¬(e3 = e2 ∈ E)
32. ses-flow(s;es;b;e3;e2)
⊢ ∀e1,e2:E. ∀b:Atom1.
(ses-flow(s;es;b;e1;e2) ⇒ (↑e2 ∈b Encrypt) ⇒ (¬(e1 = e2 ∈ E)) ⇒ (∃e:E. ((e <loc e2) ∧ (e has b))))
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. e3 : E
31. ¬(e3 = e2 ∈ E)
32. ses-flow(s;es;b;e3;e2)
33. ∀e1,e2:E. ∀b:Atom1.
(ses-flow(s;es;b;e1;e2) ⇒ (↑e2 ∈b Encrypt) ⇒ (¬(e1 = e2 ∈ E)) ⇒ (∃e:E. ((e <loc e2) ∧ (e has b))))
⊢ ∃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)
28. \mexists{}e:E. ((\mneg{}(e = e2)) \mwedge{} ses-flow(s;es;b;e;e2))
\mvdash{} \mexists{}e:E. ((e <loc e2) \mwedge{} (e has b))
By
Latex:
(ExRepD\mcdot{}
THEN Assert \mkleeneopen{}\mforall{}e1,e2:E. \mforall{}b:Atom1.
(ses-flow(s;es;b;e1;e2)
{}\mRightarrow{} (\muparrow{}e2 \mmember{}\msubb{} Encrypt)
{}\mRightarrow{} (\mneg{}(e1 = e2))
{}\mRightarrow{} (\mexists{}e:E. ((e <loc e2) \mwedge{} (e has b))))\mkleeneclose{}\mcdot{}
)
Home
Index