Step
*
1
1
3
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:Atom1
((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))))))
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 : E@i
16. y : E@i
17. ∀x1,y1:E.
(x c≤ x1
⇒ x1 c≤ y1
⇒ y1 c≤ y
⇒ ((x < x1) ∨ (y1 < y))
⇒ (∀a:Atom1. (ses-flow(s;es;a;x1;y1) ⇒ y1 c≤ e ⇒ (a ∈ ns) ⇒ (loc(x1) ∈ C) ⇒ (loc(y1) ∈ C))))@i
18. a1 : Atom1@i
19. encr : E(Encrypt)@i
20. decr : E(Decrypt)@i
21. (x <loc encr)@i
22. decr c≤ y@i
23. (encr < decr)@i
24. plainText(decr) = plainText(encr) ∈ SecurityData@i
25. cipherText(decr) = cipherText(encr) ∈ Atom1@i
26. MatchingKeys(key(decr);key(encr))@i
27. ¬(key(decr) = symmetric-key(a1) ∈ Key)@i
28. ses-flow(s;es;a1;x;encr)@i
29. ses-flow(s;es;cipherText(encr);encr;decr)@i
30. ses-flow(s;es;a1;decr;y)@i
31. y c≤ e@i
32. (a1 ∈ ns)@i
33. (loc(x) ∈ C)@i
34. (loc(encr) ∈ C)
35. k : Atom1
36. (k ∈ ns) ∧ (key(encr) = symmetric-key(k) ∈ Key)
37. key(decr) = symmetric-key(k) ∈ Key
38. ¬(loc(decr) ∈ C)
⊢ (loc(decr) ∈ C)
BY
{ Assert ⌈∃e:E. ((e <loc decr) ∧ (e has k))⌉⋅ }
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:Atom1
((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))))))
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 : E@i
16. y : E@i
17. ∀x1,y1:E.
(x c≤ x1
⇒ x1 c≤ y1
⇒ y1 c≤ y
⇒ ((x < x1) ∨ (y1 < y))
⇒ (∀a:Atom1. (ses-flow(s;es;a;x1;y1) ⇒ y1 c≤ e ⇒ (a ∈ ns) ⇒ (loc(x1) ∈ C) ⇒ (loc(y1) ∈ C))))@i
18. a1 : Atom1@i
19. encr : E(Encrypt)@i
20. decr : E(Decrypt)@i
21. (x <loc encr)@i
22. decr c≤ y@i
23. (encr < decr)@i
24. plainText(decr) = plainText(encr) ∈ SecurityData@i
25. cipherText(decr) = cipherText(encr) ∈ Atom1@i
26. MatchingKeys(key(decr);key(encr))@i
27. ¬(key(decr) = symmetric-key(a1) ∈ Key)@i
28. ses-flow(s;es;a1;x;encr)@i
29. ses-flow(s;es;cipherText(encr);encr;decr)@i
30. ses-flow(s;es;a1;decr;y)@i
31. y c≤ e@i
32. (a1 ∈ ns)@i
33. (loc(x) ∈ C)@i
34. (loc(encr) ∈ C)
35. k : Atom1
36. (k ∈ ns) ∧ (key(encr) = symmetric-key(k) ∈ Key)
37. key(decr) = symmetric-key(k) ∈ Key
38. ¬(loc(decr) ∈ C)
⊢ ∃e:E. ((e <loc decr) ∧ (e has k))
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:Atom1
((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))))))
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 : E@i
16. y : E@i
17. ∀x1,y1:E.
(x c≤ x1
⇒ x1 c≤ y1
⇒ y1 c≤ y
⇒ ((x < x1) ∨ (y1 < y))
⇒ (∀a:Atom1. (ses-flow(s;es;a;x1;y1) ⇒ y1 c≤ e ⇒ (a ∈ ns) ⇒ (loc(x1) ∈ C) ⇒ (loc(y1) ∈ C))))@i
18. a1 : Atom1@i
19. encr : E(Encrypt)@i
20. decr : E(Decrypt)@i
21. (x <loc encr)@i
22. decr c≤ y@i
23. (encr < decr)@i
24. plainText(decr) = plainText(encr) ∈ SecurityData@i
25. cipherText(decr) = cipherText(encr) ∈ Atom1@i
26. MatchingKeys(key(decr);key(encr))@i
27. ¬(key(decr) = symmetric-key(a1) ∈ Key)@i
28. ses-flow(s;es;a1;x;encr)@i
29. ses-flow(s;es;cipherText(encr);encr;decr)@i
30. ses-flow(s;es;a1;decr;y)@i
31. y c≤ e@i
32. (a1 ∈ ns)@i
33. (loc(x) ∈ C)@i
34. (loc(encr) ∈ C)
35. k : Atom1
36. (k ∈ ns) ∧ (key(encr) = symmetric-key(k) ∈ Key)
37. key(decr) = symmetric-key(k) ∈ Key
38. ¬(loc(decr) ∈ C)
39. ∃e:E. ((e <loc decr) ∧ (e has k))
⊢ (loc(decr) ∈ C)
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:Atom1
((a \mmember{} ns)
{}\mRightarrow{} ((\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))))))
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. x : E@i
16. y : E@i
17. \mforall{}x1,y1:E.
(x c\mleq{} x1
{}\mRightarrow{} x1 c\mleq{} y1
{}\mRightarrow{} y1 c\mleq{} y
{}\mRightarrow{} ((x < x1) \mvee{} (y1 < y))
{}\mRightarrow{} (\mforall{}a:Atom1
(ses-flow(s;es;a;x1;y1) {}\mRightarrow{} y1 c\mleq{} e {}\mRightarrow{} (a \mmember{} ns) {}\mRightarrow{} (loc(x1) \mmember{} C) {}\mRightarrow{} (loc(y1) \mmember{} C))))@i
18. a1 : Atom1@i
19. encr : E(Encrypt)@i
20. decr : E(Decrypt)@i
21. (x <loc encr)@i
22. decr c\mleq{} y@i
23. (encr < decr)@i
24. plainText(decr) = plainText(encr)@i
25. cipherText(decr) = cipherText(encr)@i
26. MatchingKeys(key(decr);key(encr))@i
27. \mneg{}(key(decr) = symmetric-key(a1))@i
28. ses-flow(s;es;a1;x;encr)@i
29. ses-flow(s;es;cipherText(encr);encr;decr)@i
30. ses-flow(s;es;a1;decr;y)@i
31. y c\mleq{} e@i
32. (a1 \mmember{} ns)@i
33. (loc(x) \mmember{} C)@i
34. (loc(encr) \mmember{} C)
35. k : Atom1
36. (k \mmember{} ns) \mwedge{} (key(encr) = symmetric-key(k))
37. key(decr) = symmetric-key(k)
38. \mneg{}(loc(decr) \mmember{} C)
\mvdash{} (loc(decr) \mmember{} C)
By
Latex:
Assert \mkleeneopen{}\mexists{}e:E. ((e <loc decr) \mwedge{} (e has k))\mkleeneclose{}\mcdot{}
Home
Index