Step
*
2
of Lemma
ses-flow_wf
1. s : SES
2. es : EO+(Info)
3. ∀n:ℕ. ∀e1,e2:E. (((es-rank(es;e2) - es-rank(es;e1)) ≤ n)
⇒ (∀a:Atom1. (ses-flow(s;es;a;e1;e2) ∈ Type)))
⊢ ∀[e1,e2:E]. ∀[a:Atom1]. (ses-flow(s;es;a;e1;e2) ∈ ℙ)
BY
{ (Auto THEN RecUnfold `ses-flow` 0 THEN Auto) }
1
1. s : SES
2. es : EO+(Info)
3. ∀n:ℕ. ∀e1,e2:E. (((es-rank(es;e2) - es-rank(es;e1)) ≤ n)
⇒ (∀a:Atom1. (ses-flow(s;es;a;e1;e2) ∈ Type)))
4. e1 : E
5. e2 : E
6. a : Atom1
7. snd : E(Send)@i
8. rcv : E(Rcv)@i
9. e1 c≤ snd
10. rcv c≤ e2
11. (snd < rcv)
12. Send(snd) = Rcv(rcv) ∈ SecurityData
⊢ ses-flow(s;es;a;e1;snd) ∈ Type
2
1. s : SES
2. es : EO+(Info)
3. ∀n:ℕ. ∀e1,e2:E. (((es-rank(es;e2) - es-rank(es;e1)) ≤ n)
⇒ (∀a:Atom1. (ses-flow(s;es;a;e1;e2) ∈ Type)))
4. e1 : E
5. e2 : E
6. a : Atom1
7. snd : E(Send)@i
8. rcv : E(Rcv)@i
9. e1 c≤ snd
10. rcv c≤ e2
11. (snd < rcv)
12. Send(snd) = Rcv(rcv) ∈ SecurityData
13. ses-flow(s;es;a;e1;snd)
⊢ ses-flow(s;es;a;rcv;e2) ∈ Type
3
1. s : SES
2. es : EO+(Info)
3. ∀n:ℕ. ∀e1,e2:E. (((es-rank(es;e2) - es-rank(es;e1)) ≤ n)
⇒ (∀a:Atom1. (ses-flow(s;es;a;e1;e2) ∈ Type)))
4. e1 : E
5. e2 : E
6. a : Atom1
7. encr : E(Encrypt)@i
8. decr : E(Decrypt)@i
9. (e1 <loc encr)
10. decr c≤ e2
11. (encr < decr)
12. plainText(decr) = plainText(encr) ∈ SecurityData
13. cipherText(decr) = cipherText(encr) ∈ Atom1
14. MatchingKeys(key(decr);key(encr))
15. ¬(key(decr) = symmetric-key(a) ∈ Key)
⊢ ses-flow(s;es;a;e1;encr) ∈ Type
4
1. s : SES
2. es : EO+(Info)
3. ∀n:ℕ. ∀e1,e2:E. (((es-rank(es;e2) - es-rank(es;e1)) ≤ n)
⇒ (∀a:Atom1. (ses-flow(s;es;a;e1;e2) ∈ Type)))
4. e1 : E
5. e2 : E
6. a : Atom1
7. encr : E(Encrypt)@i
8. decr : E(Decrypt)@i
9. (e1 <loc encr)
10. decr c≤ e2
11. (encr < decr)
12. plainText(decr) = plainText(encr) ∈ SecurityData
13. cipherText(decr) = cipherText(encr) ∈ Atom1
14. MatchingKeys(key(decr);key(encr))
15. ¬(key(decr) = symmetric-key(a) ∈ Key)
16. ses-flow(s;es;a;e1;encr)
⊢ ses-flow(s;es;cipherText(encr);encr;decr) ∈ Type
5
1. s : SES
2. es : EO+(Info)
3. ∀n:ℕ. ∀e1,e2:E. (((es-rank(es;e2) - es-rank(es;e1)) ≤ n)
⇒ (∀a:Atom1. (ses-flow(s;es;a;e1;e2) ∈ Type)))
4. e1 : E
5. e2 : E
6. a : Atom1
7. encr : E(Encrypt)@i
8. decr : E(Decrypt)@i
9. (e1 <loc encr)
10. decr c≤ e2
11. (encr < decr)
12. plainText(decr) = plainText(encr) ∈ SecurityData
13. cipherText(decr) = cipherText(encr) ∈ Atom1
14. MatchingKeys(key(decr);key(encr))
15. ¬(key(decr) = symmetric-key(a) ∈ Key)
16. ses-flow(s;es;a;e1;encr)
17. ses-flow(s;es;cipherText(encr);encr;decr)
⊢ ses-flow(s;es;a;decr;e2) ∈ Type
Latex:
Latex:
1. s : SES
2. es : EO+(Info)
3. \mforall{}n:\mBbbN{}. \mforall{}e1,e2:E.
(((es-rank(es;e2) - es-rank(es;e1)) \mleq{} n) {}\mRightarrow{} (\mforall{}a:Atom1. (ses-flow(s;es;a;e1;e2) \mmember{} Type)))
\mvdash{} \mforall{}[e1,e2:E]. \mforall{}[a:Atom1]. (ses-flow(s;es;a;e1;e2) \mmember{} \mBbbP{})
By
Latex:
(Auto THEN RecUnfold `ses-flow` 0 THEN Auto)
Home
Index