Step
*
1
of Lemma
ses-flow-implies'
1. s : SES@i'
2. es : EO+(Info)@i'
3. [P] : E ─→ E ─→ Atom1 ─→ ℙ
4. ∀e1,e2:E. ∀a:Atom1. (((e1 has a) ∧ (e2 has a) ∧ e1 ≤loc e2 ) ⇒ P[e1;e2;a])@i
5. ∀e1,e2:E. ∀snd:E(Send). ∀rcv:E(Rcv). ∀a:Atom1.
((e1 c≤ snd
∧ rcv c≤ e2
∧ (snd < rcv)
∧ (Send(snd) = Rcv(rcv) ∈ SecurityData)
∧ (P[e1;snd;a] ∧ ses-flow(s;es;a;e1;snd))
∧ P[rcv;e2;a]
∧ ses-flow(s;es;a;rcv;e2))
⇒ P[e1;e2;a])@i
6. ∀e1,e2:E. ∀encr:E(Encrypt). ∀decr:E(Decrypt). ∀a:Atom1.
(((e1 <loc encr)
∧ decr c≤ e2
∧ (encr < decr)
∧ ((plainText(decr) = plainText(encr) ∈ SecurityData)
∧ (cipherText(decr) = cipherText(encr) ∈ Atom1)
∧ MatchingKeys(key(decr);key(encr)))
∧ (¬(key(decr) = symmetric-key(a) ∈ Key))
∧ (P[e1;encr;a] ∧ ses-flow(s;es;a;e1;encr))
∧ (P[encr;decr;cipherText(encr)] ∧ ses-flow(s;es;cipherText(encr);encr;decr))
∧ P[decr;e2;a]
∧ ses-flow(s;es;a;decr;e2))
⇒ P[e1;e2;a])@i
7. e1 : E@i
8. e2 : E@i
9. ∀x,y:E. (e1 c≤ x ⇒ x c≤ y ⇒ y c≤ e2 ⇒ ((e1 < x) ∨ (y < e2)) ⇒ (∀a:Atom1. (ses-flow(s;es;a;x;y) ⇒ P[x;y;a])))@i
10. a : Atom1@i
11. ses-flow(s;es;a;e1;e2)@i
⊢ P[e1;e2;a]
BY
{ (RecUnfold `ses-flow` (-1)⋅ THEN SplitOrHyps THEN ExRepD) }
1
1. s : SES@i'
2. es : EO+(Info)@i'
3. [P] : E ─→ E ─→ Atom1 ─→ ℙ
4. ∀e1,e2:E. ∀a:Atom1. (((e1 has a) ∧ (e2 has a) ∧ e1 ≤loc e2 ) ⇒ P[e1;e2;a])@i
5. ∀e1,e2:E. ∀snd:E(Send). ∀rcv:E(Rcv). ∀a:Atom1.
((e1 c≤ snd
∧ rcv c≤ e2
∧ (snd < rcv)
∧ (Send(snd) = Rcv(rcv) ∈ SecurityData)
∧ (P[e1;snd;a] ∧ ses-flow(s;es;a;e1;snd))
∧ P[rcv;e2;a]
∧ ses-flow(s;es;a;rcv;e2))
⇒ P[e1;e2;a])@i
6. ∀e1,e2:E. ∀encr:E(Encrypt). ∀decr:E(Decrypt). ∀a:Atom1.
(((e1 <loc encr)
∧ decr c≤ e2
∧ (encr < decr)
∧ ((plainText(decr) = plainText(encr) ∈ SecurityData)
∧ (cipherText(decr) = cipherText(encr) ∈ Atom1)
∧ MatchingKeys(key(decr);key(encr)))
∧ (¬(key(decr) = symmetric-key(a) ∈ Key))
∧ (P[e1;encr;a] ∧ ses-flow(s;es;a;e1;encr))
∧ (P[encr;decr;cipherText(encr)] ∧ ses-flow(s;es;cipherText(encr);encr;decr))
∧ P[decr;e2;a]
∧ ses-flow(s;es;a;decr;e2))
⇒ P[e1;e2;a])@i
7. e1 : E@i
8. e2 : E@i
9. ∀x,y:E. (e1 c≤ x ⇒ x c≤ y ⇒ y c≤ e2 ⇒ ((e1 < x) ∨ (y < e2)) ⇒ (∀a:Atom1. (ses-flow(s;es;a;x;y) ⇒ P[x;y;a])))@i
10. a : Atom1@i
11. (e1 has a)@i
12. (e2 has a)@i
13. e1 ≤loc e2 @i
⊢ P[e1;e2;a]
2
1. s : SES@i'
2. es : EO+(Info)@i'
3. [P] : E ─→ E ─→ Atom1 ─→ ℙ
4. ∀e1,e2:E. ∀a:Atom1. (((e1 has a) ∧ (e2 has a) ∧ e1 ≤loc e2 ) ⇒ P[e1;e2;a])@i
5. ∀e1,e2:E. ∀snd:E(Send). ∀rcv:E(Rcv). ∀a:Atom1.
((e1 c≤ snd
∧ rcv c≤ e2
∧ (snd < rcv)
∧ (Send(snd) = Rcv(rcv) ∈ SecurityData)
∧ (P[e1;snd;a] ∧ ses-flow(s;es;a;e1;snd))
∧ P[rcv;e2;a]
∧ ses-flow(s;es;a;rcv;e2))
⇒ P[e1;e2;a])@i
6. ∀e1,e2:E. ∀encr:E(Encrypt). ∀decr:E(Decrypt). ∀a:Atom1.
(((e1 <loc encr)
∧ decr c≤ e2
∧ (encr < decr)
∧ ((plainText(decr) = plainText(encr) ∈ SecurityData)
∧ (cipherText(decr) = cipherText(encr) ∈ Atom1)
∧ MatchingKeys(key(decr);key(encr)))
∧ (¬(key(decr) = symmetric-key(a) ∈ Key))
∧ (P[e1;encr;a] ∧ ses-flow(s;es;a;e1;encr))
∧ (P[encr;decr;cipherText(encr)] ∧ ses-flow(s;es;cipherText(encr);encr;decr))
∧ P[decr;e2;a]
∧ ses-flow(s;es;a;decr;e2))
⇒ P[e1;e2;a])@i
7. e1 : E@i
8. e2 : E@i
9. ∀x,y:E. (e1 c≤ x ⇒ x c≤ y ⇒ y c≤ e2 ⇒ ((e1 < x) ∨ (y < e2)) ⇒ (∀a:Atom1. (ses-flow(s;es;a;x;y) ⇒ P[x;y;a])))@i
10. a : Atom1@i
11. snd : E(Send)@i
12. rcv : E(Rcv)@i
13. e1 c≤ snd@i
14. rcv c≤ e2@i
15. (snd < rcv)@i
16. Send(snd) = Rcv(rcv) ∈ SecurityData@i
17. ses-flow(s;es;a;e1;snd)@i
18. ses-flow(s;es;a;rcv;e2)@i
⊢ P[e1;e2;a]
3
1. s : SES@i'
2. es : EO+(Info)@i'
3. [P] : E ─→ E ─→ Atom1 ─→ ℙ
4. ∀e1,e2:E. ∀a:Atom1. (((e1 has a) ∧ (e2 has a) ∧ e1 ≤loc e2 ) ⇒ P[e1;e2;a])@i
5. ∀e1,e2:E. ∀snd:E(Send). ∀rcv:E(Rcv). ∀a:Atom1.
((e1 c≤ snd
∧ rcv c≤ e2
∧ (snd < rcv)
∧ (Send(snd) = Rcv(rcv) ∈ SecurityData)
∧ (P[e1;snd;a] ∧ ses-flow(s;es;a;e1;snd))
∧ P[rcv;e2;a]
∧ ses-flow(s;es;a;rcv;e2))
⇒ P[e1;e2;a])@i
6. ∀e1,e2:E. ∀encr:E(Encrypt). ∀decr:E(Decrypt). ∀a:Atom1.
(((e1 <loc encr)
∧ decr c≤ e2
∧ (encr < decr)
∧ ((plainText(decr) = plainText(encr) ∈ SecurityData)
∧ (cipherText(decr) = cipherText(encr) ∈ Atom1)
∧ MatchingKeys(key(decr);key(encr)))
∧ (¬(key(decr) = symmetric-key(a) ∈ Key))
∧ (P[e1;encr;a] ∧ ses-flow(s;es;a;e1;encr))
∧ (P[encr;decr;cipherText(encr)] ∧ ses-flow(s;es;cipherText(encr);encr;decr))
∧ P[decr;e2;a]
∧ ses-flow(s;es;a;decr;e2))
⇒ P[e1;e2;a])@i
7. e1 : E@i
8. e2 : E@i
9. ∀x,y:E. (e1 c≤ x ⇒ x c≤ y ⇒ y c≤ e2 ⇒ ((e1 < x) ∨ (y < e2)) ⇒ (∀a:Atom1. (ses-flow(s;es;a;x;y) ⇒ P[x;y;a])))@i
10. a : Atom1@i
11. encr : E(Encrypt)@i
12. decr : E(Decrypt)@i
13. (e1 <loc encr)@i
14. decr c≤ e2@i
15. (encr < decr)@i
16. plainText(decr) = plainText(encr) ∈ SecurityData@i
17. cipherText(decr) = cipherText(encr) ∈ Atom1@i
18. MatchingKeys(key(decr);key(encr))@i
19. ¬(key(decr) = symmetric-key(a) ∈ Key)@i
20. ses-flow(s;es;a;e1;encr)@i
21. ses-flow(s;es;cipherText(encr);encr;decr)@i
22. ses-flow(s;es;a;decr;e2)@i
⊢ P[e1;e2;a]
Latex:
Latex:
1. s : SES@i'
2. es : EO+(Info)@i'
3. [P] : E {}\mrightarrow{} E {}\mrightarrow{} Atom1 {}\mrightarrow{} \mBbbP{}
4. \mforall{}e1,e2:E. \mforall{}a:Atom1. (((e1 has a) \mwedge{} (e2 has a) \mwedge{} e1 \mleq{}loc e2 ) {}\mRightarrow{} P[e1;e2;a])@i
5. \mforall{}e1,e2:E. \mforall{}snd:E(Send). \mforall{}rcv:E(Rcv). \mforall{}a:Atom1.
((e1 c\mleq{} snd
\mwedge{} rcv c\mleq{} e2
\mwedge{} (snd < rcv)
\mwedge{} (Send(snd) = Rcv(rcv))
\mwedge{} (P[e1;snd;a] \mwedge{} ses-flow(s;es;a;e1;snd))
\mwedge{} P[rcv;e2;a]
\mwedge{} ses-flow(s;es;a;rcv;e2))
{}\mRightarrow{} P[e1;e2;a])@i
6. \mforall{}e1,e2:E. \mforall{}encr:E(Encrypt). \mforall{}decr:E(Decrypt). \mforall{}a:Atom1.
(((e1 <loc encr)
\mwedge{} decr c\mleq{} e2
\mwedge{} (encr < decr)
\mwedge{} ((plainText(decr) = plainText(encr))
\mwedge{} (cipherText(decr) = cipherText(encr))
\mwedge{} MatchingKeys(key(decr);key(encr)))
\mwedge{} (\mneg{}(key(decr) = symmetric-key(a)))
\mwedge{} (P[e1;encr;a] \mwedge{} ses-flow(s;es;a;e1;encr))
\mwedge{} (P[encr;decr;cipherText(encr)] \mwedge{} ses-flow(s;es;cipherText(encr);encr;decr))
\mwedge{} P[decr;e2;a]
\mwedge{} ses-flow(s;es;a;decr;e2))
{}\mRightarrow{} P[e1;e2;a])@i
7. e1 : E@i
8. e2 : E@i
9. \mforall{}x,y:E.
(e1 c\mleq{} x
{}\mRightarrow{} x c\mleq{} y
{}\mRightarrow{} y c\mleq{} e2
{}\mRightarrow{} ((e1 < x) \mvee{} (y < e2))
{}\mRightarrow{} (\mforall{}a:Atom1. (ses-flow(s;es;a;x;y) {}\mRightarrow{} P[x;y;a])))@i
10. a : Atom1@i
11. ses-flow(s;es;a;e1;e2)@i
\mvdash{} P[e1;e2;a]
By
Latex:
(RecUnfold `ses-flow` (-1)\mcdot{} THEN SplitOrHyps THEN ExRepD)
Home
Index