---

Step * 1 of Lemma ses-legal-thread-has*-nonce


1. s : SES@i'
2. SecurityAxioms@i'
3. es : EO+(Info)@i'
4. A : Id@i
5. thr : Thread@i
6. Legal(thr)@A@i
7. n : E(New)@i
8. a : E@i
9. Action(a)
10. a ∈ thr@i
11. a has* New(n)@i
12. ∀e':E. ((e' < a) ⇒ Action(e') ⇒ e' has* New(n) ⇒ ((loc(e') = A ∈ Id) ∧ (¬↑e' ∈b Send)))
13. ¬(a = n ∈ E)
⊢ ∃e':E. ((e' <loc a) ∧ Action(e') ∧ e' has* New(n) ∧ e' ∈ thr)
BY
{ Assert ⌜∀e:E
            (Action(e)
            ⇒ e ∈ thr
            ⇒ e ≤loc a 
            ⇒ (∀m:ℕ. ∀e':E.
                  ((e' ->>^m e)
                  ⇒ (e' has New(n))
                  ⇒ ((∃e':E. ((e' <loc e) ∧ Action(e') ∧ e' has* New(n) ∧ e' ∈ thr)) ∨ (e = n ∈ E)))))⌝⋅ }

1
.....assertion..... 
1. s : SES@i'
2. SecurityAxioms@i'
3. es : EO+(Info)@i'
4. A : Id@i
5. thr : Thread@i
6. Legal(thr)@A@i
7. n : E(New)@i
8. a : E@i
9. Action(a)
10. a ∈ thr@i
11. a has* New(n)@i
12. ∀e':E. ((e' < a) ⇒ Action(e') ⇒ e' has* New(n) ⇒ ((loc(e') = A ∈ Id) ∧ (¬↑e' ∈b Send)))
13. ¬(a = n ∈ E)
⊢ ∀e:E
    (Action(e)
    ⇒ e ∈ thr
    ⇒ e ≤loc a 
    ⇒ (∀m:ℕ. ∀e':E.
          ((e' ->>^m e)
          ⇒ (e' has New(n))
          ⇒ ((∃e':E. ((e' <loc e) ∧ Action(e') ∧ e' has* New(n) ∧ e' ∈ thr)) ∨ (e = n ∈ E)))))

2
1. s : SES@i'
2. SecurityAxioms@i'
3. es : EO+(Info)@i'
4. A : Id@i
5. thr : Thread@i
6. Legal(thr)@A@i
7. n : E(New)@i
8. a : E@i
9. Action(a)
10. a ∈ thr@i
11. a has* New(n)@i
12. ∀e':E. ((e' < a) ⇒ Action(e') ⇒ e' has* New(n) ⇒ ((loc(e') = A ∈ Id) ∧ (¬↑e' ∈b Send)))
13. ¬(a = n ∈ E)
14. ∀e:E
      (Action(e)
      ⇒ e ∈ thr
      ⇒ e ≤loc a 
      ⇒ (∀m:ℕ. ∀e':E.
            ((e' ->>^m e)
            ⇒ (e' has New(n))
            ⇒ ((∃e':E. ((e' <loc e) ∧ Action(e') ∧ e' has* New(n) ∧ e' ∈ thr)) ∨ (e = n ∈ E)))))
⊢ ∃e':E. ((e' <loc a) ∧ Action(e') ∧ e' has* New(n) ∧ e' ∈ thr)

---

Latex:

---

Latex:

1.  s  :  SES@i'
2.  SecurityAxioms@i'
3.  es  :  EO+(Info)@i'
4.  A  :  Id@i
5.  thr  :  Thread@i
6.  Legal(thr)@A@i
7.  n  :  E(New)@i
8.  a  :  E@i
9.  Action(a)
10.  a  \mmember{}  thr@i
11.  a  has*  New(n)@i
12.  \mforall{}e':E.  ((e'  <  a)  {}\mRightarrow{}  Action(e')  {}\mRightarrow{}  e'  has*  New(n)  {}\mRightarrow{}  ((loc(e')  =  A)  \mwedge{}  (\mneg{}\muparrow{}e'  \mmember{}\msubb{}  Send)))
13.  \mneg{}(a  =  n)
\mvdash{}  \mexists{}e':E.  ((e'  <loc  a)  \mwedge{}  Action(e')  \mwedge{}  e'  has*  New(n)  \mwedge{}  e'  \mmember{}  thr)


By

---

Latex:
Assert  \mkleeneopen{}\mforall{}e:E
                    (Action(e)
                    {}\mRightarrow{}  e  \mmember{}  thr
                    {}\mRightarrow{}  e  \mleq{}loc  a 
                    {}\mRightarrow{}  (\mforall{}m:\mBbbN{}.  \mforall{}e':E.
                                ((e'  rel\_exp(E;  ->>  m)  e)
                                {}\mRightarrow{}  (e'  has  New(n))
                                {}\mRightarrow{}  ((\mexists{}e':E.  ((e'  <loc  e)  \mwedge{}  Action(e')  \mwedge{}  e'  has*  New(n)  \mwedge{}  e'  \mmember{}  thr))  \mvee{}  (e  =  n)))))\mkleeneclose{}\mcdot{}

---

Home Index