---

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


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. noncelike-signatures(s;es;thr)@i
8. sg : E(Sign)@i
9. a : E@i
10. Action(a)
11. a ∈ thr@i
12. a has* signature(sg)@i
13. ∀e':E. ((e' < a) ⇒ Action(e') ⇒ e' has* signature(sg) ⇒ ((loc(e') = A ∈ Id) ∧ (¬↑e' ∈b Send)))
14. e : E@i
15. ∀e1:E
      ((e1 < e)
      ⇒ Action(e1)
      ⇒ e1 ∈ thr
      ⇒ e1 ≤loc a 
      ⇒ (∀m:ℕ. ∀e':E.
            ((e' ->>^m e1)
            ⇒ (e' has signature(sg))
            ⇒ ((∃e':E. ((e' <loc e1) ∧ Action(e') ∧ e' has* signature(sg) ∧ e' ∈ thr)) ∨ (e1 = sg ∈ E)))))
16. Action(e)@i
17. e ∈ thr@i
18. e ≤loc a @i
19. e' : E@i
20. e' ->>^0 e@i
21. (e' has signature(sg))@i
⊢ (∃e':E. ((e' <loc e) ∧ Action(e') ∧ e' has* signature(sg) ∧ e' ∈ thr)) ∨ (e = sg ∈ E)
BY
{ (RecUnfold `rel_exp` (-2)
   THEN Reduce (-2)
   THEN (HypSubst' (-2) (-1) THENA Auto)
   THEN (RepeatFor 2 (Thin (-2))
         THEN (FLemma `ses-legal-thread-has-atom` [6;-1] THENA Auto)
         THEN SplitOrHyps
         THEN ExRepD)⋅) }

1
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. noncelike-signatures(s;es;thr)@i
8. sg : E(Sign)@i
9. a : E@i
10. Action(a)
11. a ∈ thr@i
12. a has* signature(sg)@i
13. ∀e':E. ((e' < a) ⇒ Action(e') ⇒ e' has* signature(sg) ⇒ ((loc(e') = A ∈ Id) ∧ (¬↑e' ∈b Send)))
14. e : E@i
15. ∀e1:E
      ((e1 < e)
      ⇒ Action(e1)
      ⇒ e1 ∈ thr
      ⇒ e1 ≤loc a 
      ⇒ (∀m:ℕ. ∀e':E.
            ((e' ->>^m e1)
            ⇒ (e' has signature(sg))
            ⇒ ((∃e':E. ((e' <loc e1) ∧ Action(e') ∧ e' has* signature(sg) ∧ e' ∈ thr)) ∨ (e1 = sg ∈ E)))))
16. Action(e)@i
17. e ∈ thr@i
18. e ≤loc a @i
19. (e has signature(sg))
20. e' : Act
21. (e' <loc e)
22. (e' has signature(sg))
23. e' ∈ thr
⊢ (∃e':E. ((e' <loc e) ∧ Action(e') ∧ e' has* signature(sg) ∧ e' ∈ thr)) ∨ (e = sg ∈ 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. noncelike-signatures(s;es;thr)@i
8. sg : E(Sign)@i
9. a : E@i
10. Action(a)
11. a ∈ thr@i
12. a has* signature(sg)@i
13. ∀e':E. ((e' < a) ⇒ Action(e') ⇒ e' has* signature(sg) ⇒ ((loc(e') = A ∈ Id) ∧ (¬↑e' ∈b Send)))
14. e : E@i
15. ∀e1:E
      ((e1 < e)
      ⇒ Action(e1)
      ⇒ e1 ∈ thr
      ⇒ e1 ≤loc a 
      ⇒ (∀m:ℕ. ∀e':E.
            ((e' ->>^m e1)
            ⇒ (e' has signature(sg))
            ⇒ ((∃e':E. ((e' <loc e1) ∧ Action(e') ∧ e' has* signature(sg) ∧ e' ∈ thr)) ∨ (e1 = sg ∈ E)))))
16. Action(e)@i
17. e ∈ thr@i
18. e ≤loc a @i
19. (e has signature(sg))
20. (signature(sg) ∈ UseableAtoms(e))
⊢ (∃e':E. ((e' <loc e) ∧ Action(e') ∧ e' has* signature(sg) ∧ e' ∈ thr)) ∨ (e = sg ∈ E)

3
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. noncelike-signatures(s;es;thr)@i
8. sg : E(Sign)@i
9. a : E@i
10. Action(a)
11. a ∈ thr@i
12. a has* signature(sg)@i
13. ∀e':E. ((e' < a) ⇒ Action(e') ⇒ e' has* signature(sg) ⇒ ((loc(e') = A ∈ Id) ∧ (¬↑e' ∈b Send)))
14. e : E@i
15. ∀e1:E
      ((e1 < e)
      ⇒ Action(e1)
      ⇒ e1 ∈ thr
      ⇒ e1 ≤loc a 
      ⇒ (∀m:ℕ. ∀e':E.
            ((e' ->>^m e1)
            ⇒ (e' has signature(sg))
            ⇒ ((∃e':E. ((e' <loc e1) ∧ Action(e') ∧ e' has* signature(sg) ∧ e' ∈ thr)) ∨ (e1 = sg ∈ E)))))
16. Action(e)@i
17. e ∈ thr@i
18. e ≤loc a @i
19. (e has signature(sg))
20. signature(sg) = Private(A) ∈ Atom1
⊢ (∃e':E. ((e' <loc e) ∧ Action(e') ∧ e' has* signature(sg) ∧ e' ∈ thr)) ∨ (e = sg ∈ E)

---

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.  noncelike-signatures(s;es;thr)@i
8.  sg  :  E(Sign)@i
9.  a  :  E@i
10.  Action(a)
11.  a  \mmember{}  thr@i
12.  a  has*  signature(sg)@i
13.  \mforall{}e':E.  ((e'  <  a)  {}\mRightarrow{}  Action(e')  {}\mRightarrow{}  e'  has*  signature(sg)  {}\mRightarrow{}  ((loc(e')  =  A)  \mwedge{}  (\mneg{}\muparrow{}e'  \mmember{}\msubb{}  Send)))
14.  e  :  E@i
15.  \mforall{}e1:E
            ((e1  <  e)
            {}\mRightarrow{}  Action(e1)
            {}\mRightarrow{}  e1  \mmember{}  thr
            {}\mRightarrow{}  e1  \mleq{}loc  a 
            {}\mRightarrow{}  (\mforall{}m:\mBbbN{}.  \mforall{}e':E.
                        ((e'  rel\_exp(E;  ->>  m)  e1)
                        {}\mRightarrow{}  (e'  has  signature(sg))
                        {}\mRightarrow{}  ((\mexists{}e':E.  ((e'  <loc  e1)  \mwedge{}  Action(e')  \mwedge{}  e'  has*  signature(sg)  \mwedge{}  e'  \mmember{}  thr))
                              \mvee{}  (e1  =  sg)))))
16.  Action(e)@i
17.  e  \mmember{}  thr@i
18.  e  \mleq{}loc  a  @i
19.  e'  :  E@i
20.  e'  rel\_exp(E;  ->>  0)  e@i
21.  (e'  has  signature(sg))@i
\mvdash{}  (\mexists{}e':E.  ((e'  <loc  e)  \mwedge{}  Action(e')  \mwedge{}  e'  has*  signature(sg)  \mwedge{}  e'  \mmember{}  thr))  \mvee{}  (e  =  sg)


By

---

Latex:
(RecUnfold  `rel\_exp`  (-2)
  THEN  Reduce  (-2)
  THEN  (HypSubst'  (-2)  (-1)  THENA  Auto)
  THEN  (RepeatFor  2  (Thin  (-2))
              THEN  (FLemma  `ses-legal-thread-has-atom`  [6;-1]  THENA  Auto)
              THEN  SplitOrHyps
              THEN  ExRepD)\mcdot{})

---

Home Index