---

Step * 1 1 1 2 1 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)
14. e : E@i
15. ∀e1:E
      ((e1 < e)
      ⇒ Action(e1)
      ⇒ e1 ∈ thr
      ⇒ e1 ≤loc a 
      ⇒ (∀m:ℕ. ∀e':E.
            ((e' ->>^m e1)
            ⇒ (e' has New(n))
            ⇒ ((∃e':E. ((e' <loc e1) ∧ Action(e') ∧ e' has* New(n) ∧ e' ∈ thr)) ∨ (e1 = n ∈ E)))))
16. Action(e)@i
17. e ∈ thr@i
18. e ≤loc a @i
19. (e has New(n))
20. ↑e ∈b Rcv
21. (New(n) ∈ sdata-atoms(Rcv(e)))
22. ∀es:EO+(Info). ∀e:E(Rcv).  ∃e':E(Send). ((e' < e) ∧ (Rcv(e) = Send(e') ∈ SecurityData))
23. e' : E(Send)
24. (e' < e)
25. Rcv(e) = Send(e') ∈ SecurityData
⊢ False
BY
{ (D -3
   THEN OnMaybeHyp 12 (\h. (InstHyp [⌈e'⌉] h⋅
                            THEN Auto
                            THEN Try ((Unfold `ses-action` 0 THEN Auto))
                            THEN (BLemma `event-has*-iff` THENM OrLeft)
                            THEN Auto))
   )⋅ }

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. 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@i
15. ∀e1:E
      ((e1 < e)
      ⇒ Action(e1)
      ⇒ e1 ∈ thr
      ⇒ e1 ≤loc a 
      ⇒ (∀m:ℕ. ∀e':E.
            ((e' ->>^m e1)
            ⇒ (e' has New(n))
            ⇒ ((∃e':E. ((e' <loc e1) ∧ Action(e') ∧ e' has* New(n) ∧ e' ∈ thr)) ∨ (e1 = n ∈ E)))))
16. Action(e)@i
17. e ∈ thr@i
18. e ≤loc a @i
19. (e has New(n))
20. ↑e ∈b Rcv
21. (New(n) ∈ sdata-atoms(Rcv(e)))
22. ∀es:EO+(Info). ∀e:E(Rcv).  ∃e':E(Send). ((e' < e) ∧ (Rcv(e) = Send(e') ∈ SecurityData))
23. e' : E
24. ↑e' ∈b Send
25. (e' < e)
26. Rcv(e) = Send(e') ∈ SecurityData
⊢ (e' has New(n))

---

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)
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  New(n))
                        {}\mRightarrow{}  ((\mexists{}e':E.  ((e'  <loc  e1)  \mwedge{}  Action(e')  \mwedge{}  e'  has*  New(n)  \mwedge{}  e'  \mmember{}  thr))  \mvee{}  (e1  =  n)))))
16.  Action(e)@i
17.  e  \mmember{}  thr@i
18.  e  \mleq{}loc  a  @i
19.  (e  has  New(n))
20.  \muparrow{}e  \mmember{}\msubb{}  Rcv
21.  (New(n)  \mmember{}  sdata-atoms(Rcv(e)))
22.  \mforall{}es:EO+(Info).  \mforall{}e:E(Rcv).    \mexists{}e':E(Send).  ((e'  <  e)  \mwedge{}  (Rcv(e)  =  Send(e')))
23.  e'  :  E(Send)
24.  (e'  <  e)
25.  Rcv(e)  =  Send(e')
\mvdash{}  False


By

---

Latex:
(D  -3
  THEN  OnMaybeHyp  12  (\mbackslash{}h.  (InstHyp  [\mkleeneopen{}e'\mkleeneclose{}]  h\mcdot{}
                                                    THEN  Auto
                                                    THEN  Try  ((Unfold  `ses-action`  0  THEN  Auto))
                                                    THEN  (BLemma  `event-has*-iff`  THENM  OrLeft)
                                                    THEN  Auto))
  )\mcdot{}

---

Home Index