---

Step * 1 1 1 1 of Lemma nonce-release-lemma


1. ses : SES
2. ActionsDisjoint
3. NoncesCiphersAndKeysDisjoint
4. PropertyO
5. ∀es:EO+(Info). ∀n:E(New). ∀e:E.
     (e has* New(n)
     ⇒ (n c≤ e ∧ ((¬(loc(e) = loc(n) ∈ Id)) ⇒ (∃e':E(Send). ((n <loc e') ∧ e' has* New(n) ∧ (e' < e))))))
6. ses-ordering'(ses)
7. PropertyF
8. PropertyV
9. PropertyR
10. PropertyD
11. PropertyS
12. PropertyK
13. bss : Basic1 List
14. Legal(bss)
15. A : Id
16. Honest(A)
17. Protocol1(bss) A
18. es : EO+(Info)
19. thr : {thr:Act List| ∀i:ℕ||thr|| - 1. (thr[i] <loc thr[i + 1])} 
20. (thr is one of bss at A)
21. loc(thr)= A
22. i : ℕ||thr||
23. j : ℕi
24. ↑thr[j] ∈b New
25. ∀k:{j + 1..i-}. (¬↑thr[k] ∈b Send)
26. loc(thr[j]) = A ∈ Id
27. loc(thr[i]) = A ∈ Id
28. e : E@i
29. ∀e1:E
      ((e1 < e)
      ⇒ Action(e1)
      ⇒ e1 has* New(thr[j])
      ⇒ (((¬(loc(e1) = A ∈ Id)) ⇒ (thr[i] < e1)) ∧ ((e1 <loc thr[i]) ⇒ (e1 ∈ thr ∧ (¬↑e1 ∈b Send)))))
30. Action(e)@i
31. e has* New(thr[j])@i
32. ¬(loc(e) = A ∈ Id)@i
33. thr[j] c≤ e
34. e' : E(Send)
35. (thr[j] <loc e')
36. e' has* New(thr[j])
37. (e' < e)
⊢ (thr[i] < e)
BY
{ (Assert thr[i] ≤loc e'  BY
         (BLemma `es-le-not-locl` THEN Auto THEN (D 0 THENA Auto)))⋅ }

1
1. ses : SES
2. ActionsDisjoint
3. NoncesCiphersAndKeysDisjoint
4. PropertyO
5. ∀es:EO+(Info). ∀n:E(New). ∀e:E.
     (e has* New(n)
     ⇒ (n c≤ e ∧ ((¬(loc(e) = loc(n) ∈ Id)) ⇒ (∃e':E(Send). ((n <loc e') ∧ e' has* New(n) ∧ (e' < e))))))
6. ses-ordering'(ses)
7. PropertyF
8. PropertyV
9. PropertyR
10. PropertyD
11. PropertyS
12. PropertyK
13. bss : Basic1 List
14. Legal(bss)
15. A : Id
16. Honest(A)
17. Protocol1(bss) A
18. es : EO+(Info)
19. thr : {thr:Act List| ∀i:ℕ||thr|| - 1. (thr[i] <loc thr[i + 1])} 
20. (thr is one of bss at A)
21. loc(thr)= A
22. i : ℕ||thr||
23. j : ℕi
24. ↑thr[j] ∈b New
25. ∀k:{j + 1..i-}. (¬↑thr[k] ∈b Send)
26. loc(thr[j]) = A ∈ Id
27. loc(thr[i]) = A ∈ Id
28. e : E@i
29. ∀e1:E
      ((e1 < e)
      ⇒ Action(e1)
      ⇒ e1 has* New(thr[j])
      ⇒ (((¬(loc(e1) = A ∈ Id)) ⇒ (thr[i] < e1)) ∧ ((e1 <loc thr[i]) ⇒ (e1 ∈ thr ∧ (¬↑e1 ∈b Send)))))
30. Action(e)@i
31. e has* New(thr[j])@i
32. ¬(loc(e) = A ∈ Id)@i
33. thr[j] c≤ e
34. e' : E(Send)
35. (thr[j] <loc e')
36. e' has* New(thr[j])
37. (e' < e)
38. (e' <loc thr[i])@i
⊢ False

2
1. ses : SES
2. ActionsDisjoint
3. NoncesCiphersAndKeysDisjoint
4. PropertyO
5. ∀es:EO+(Info). ∀n:E(New). ∀e:E.
     (e has* New(n)
     ⇒ (n c≤ e ∧ ((¬(loc(e) = loc(n) ∈ Id)) ⇒ (∃e':E(Send). ((n <loc e') ∧ e' has* New(n) ∧ (e' < e))))))
6. ses-ordering'(ses)
7. PropertyF
8. PropertyV
9. PropertyR
10. PropertyD
11. PropertyS
12. PropertyK
13. bss : Basic1 List
14. Legal(bss)
15. A : Id
16. Honest(A)
17. Protocol1(bss) A
18. es : EO+(Info)
19. thr : {thr:Act List| ∀i:ℕ||thr|| - 1. (thr[i] <loc thr[i + 1])} 
20. (thr is one of bss at A)
21. loc(thr)= A
22. i : ℕ||thr||
23. j : ℕi
24. ↑thr[j] ∈b New
25. ∀k:{j + 1..i-}. (¬↑thr[k] ∈b Send)
26. loc(thr[j]) = A ∈ Id
27. loc(thr[i]) = A ∈ Id
28. e : E@i
29. ∀e1:E
      ((e1 < e)
      ⇒ Action(e1)
      ⇒ e1 has* New(thr[j])
      ⇒ (((¬(loc(e1) = A ∈ Id)) ⇒ (thr[i] < e1)) ∧ ((e1 <loc thr[i]) ⇒ (e1 ∈ thr ∧ (¬↑e1 ∈b Send)))))
30. Action(e)@i
31. e has* New(thr[j])@i
32. ¬(loc(e) = A ∈ Id)@i
33. thr[j] c≤ e
34. e' : E(Send)
35. (thr[j] <loc e')
36. e' has* New(thr[j])
37. (e' < e)
38. thr[i] ≤loc e' 
⊢ (thr[i] < e)

---

Latex:

---

Latex:

1.  ses  :  SES
2.  ActionsDisjoint
3.  NoncesCiphersAndKeysDisjoint
4.  PropertyO
5.  \mforall{}es:EO+(Info).  \mforall{}n:E(New).  \mforall{}e:E.
          (e  has*  New(n)
          {}\mRightarrow{}  (n  c\mleq{}  e
                \mwedge{}  ((\mneg{}(loc(e)  =  loc(n)))  {}\mRightarrow{}  (\mexists{}e':E(Send).  ((n  <loc  e')  \mwedge{}  e'  has*  New(n)  \mwedge{}  (e'  <  e))))))
6.  ses-ordering'(ses)
7.  PropertyF
8.  PropertyV
9.  PropertyR
10.  PropertyD
11.  PropertyS
12.  PropertyK
13.  bss  :  Basic1  List
14.  Legal(bss)
15.  A  :  Id
16.  Honest(A)
17.  Protocol1(bss)  A
18.  es  :  EO+(Info)
19.  thr  :  \{thr:Act  List|  \mforall{}i:\mBbbN{}||thr||  -  1.  (thr[i]  <loc  thr[i  +  1])\} 
20.  (thr  is  one  of  bss  at  A)
21.  loc(thr)=  A
22.  i  :  \mBbbN{}||thr||
23.  j  :  \mBbbN{}i
24.  \muparrow{}thr[j]  \mmember{}\msubb{}  New
25.  \mforall{}k:\{j  +  1..i\msupminus{}\}.  (\mneg{}\muparrow{}thr[k]  \mmember{}\msubb{}  Send)
26.  loc(thr[j])  =  A
27.  loc(thr[i])  =  A
28.  e  :  E@i
29.  \mforall{}e1:E
            ((e1  <  e)
            {}\mRightarrow{}  Action(e1)
            {}\mRightarrow{}  e1  has*  New(thr[j])
            {}\mRightarrow{}  (((\mneg{}(loc(e1)  =  A))  {}\mRightarrow{}  (thr[i]  <  e1))  \mwedge{}  ((e1  <loc  thr[i])  {}\mRightarrow{}  (e1  \mmember{}  thr  \mwedge{}  (\mneg{}\muparrow{}e1  \mmember{}\msubb{}  Send)))))
30.  Action(e)@i
31.  e  has*  New(thr[j])@i
32.  \mneg{}(loc(e)  =  A)@i
33.  thr[j]  c\mleq{}  e
34.  e'  :  E(Send)
35.  (thr[j]  <loc  e')
36.  e'  has*  New(thr[j])
37.  (e'  <  e)
\mvdash{}  (thr[i]  <  e)


By

---

Latex:
(Assert  thr[i]  \mleq{}loc  e'    BY
              (BLemma  `es-le-not-locl`  THEN  Auto  THEN  (D  0  THENA  Auto)))\mcdot{}

---

Home Index