---

Step * 2 5 1 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)))
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 < 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
BY
{ ((InstLemma `es-rank_le` [⌈es⌉;⌈decr⌉;⌈e2⌉]⋅ THENA Auto)
   THEN InstHyp [⌈es-rank(es;e2) - es-rank(es;decr)⌉;⌈decr⌉;⌈e2⌉;⌈a⌉] 3⋅
   THEN Auto)⋅ }

---

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)))
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  <  e2)
11.  (encr  <  decr)
12.  plainText(decr)  =  plainText(encr)
13.  cipherText(decr)  =  cipherText(encr)
14.  MatchingKeys(key(decr);key(encr))
15.  \mneg{}(key(decr)  =  symmetric-key(a))
16.  ses-flow(s;es;a;e1;encr)
17.  ses-flow(s;es;cipherText(encr);encr;decr)
\mvdash{}  ses-flow(s;es;a;decr;e2)  \mmember{}  Type


By

---

Latex:
((InstLemma  `es-rank\_le`  [\mkleeneopen{}es\mkleeneclose{};\mkleeneopen{}decr\mkleeneclose{};\mkleeneopen{}e2\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  InstHyp  [\mkleeneopen{}es-rank(es;e2)  -  es-rank(es;decr)\mkleeneclose{};\mkleeneopen{}decr\mkleeneclose{};\mkleeneopen{}e2\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{}]  3\mcdot{}
  THEN  Auto)\mcdot{}

---

Home Index