---

Step * 1 of Lemma nonce-release-lemma

.....assertion..... 
1. ses : SES
2. ActionsDisjoint
3. NoncesCiphersAndKeysDisjoint
4. PropertyO
5. PropertyN
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)
⊢ ∀e:E
    (Action(e)
    ⇒ e has* New(thr[j])
    ⇒ (((¬(loc(e) = A ∈ Id)) ⇒ (thr[i] < e)) ∧ ((e <loc thr[i]) ⇒ (e ∈ thr ∧ (¬↑e ∈b Send)))))
BY
{ ((Assert loc(thr[j]) = A ∈ Id BY
          OnMaybeHyp 20 (\h. (UnfoldTopAb h
                              THEN BHyp h 
                              THEN Auto
                              THEN UnfoldTopAb 0
                              THEN Auto
                              THEN With ⌈j⌉ (D 0)⋅
                              THEN Auto)))
   THEN (Assert loc(thr[i]) = A ∈ Id BY
               OnMaybeHyp 20 (\h. (UnfoldTopAb h
                                   THEN BHyp h 
                                   THEN Auto
                                   THEN UnfoldTopAb 0
                                   THEN Auto
                                   THEN With ⌈i⌉ (D 0)⋅
                                   THEN Auto)))
   )⋅ }

1
1. ses : SES
2. ActionsDisjoint
3. NoncesCiphersAndKeysDisjoint
4. PropertyO
5. PropertyN
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
⊢ ∀e:E
    (Action(e)
    ⇒ e has* New(thr[j])
    ⇒ (((¬(loc(e) = A ∈ Id)) ⇒ (thr[i] < e)) ∧ ((e <loc thr[i]) ⇒ (e ∈ thr ∧ (¬↑e ∈b Send)))))

---

Latex:

---

Latex:
.....assertion..... 
1.  ses  :  SES
2.  ActionsDisjoint
3.  NoncesCiphersAndKeysDisjoint
4.  PropertyO
5.  PropertyN
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)
\mvdash{}  \mforall{}e:E
        (Action(e)
        {}\mRightarrow{}  e  has*  New(thr[j])
        {}\mRightarrow{}  (((\mneg{}(loc(e)  =  A))  {}\mRightarrow{}  (thr[i]  <  e))  \mwedge{}  ((e  <loc  thr[i])  {}\mRightarrow{}  (e  \mmember{}  thr  \mwedge{}  (\mneg{}\muparrow{}e  \mmember{}\msubb{}  Send)))))


By

---

Latex:
((Assert  loc(thr[j])  =  A  BY
                OnMaybeHyp  20  (\mbackslash{}h.  (UnfoldTopAb  h
                                                        THEN  BHyp  h 
                                                        THEN  Auto
                                                        THEN  UnfoldTopAb  0
                                                        THEN  Auto
                                                        THEN  With  \mkleeneopen{}j\mkleeneclose{}  (D  0)\mcdot{}
                                                        THEN  Auto)))
  THEN  (Assert  loc(thr[i])  =  A  BY
                          OnMaybeHyp  20  (\mbackslash{}h.  (UnfoldTopAb  h
                                                                  THEN  BHyp  h 
                                                                  THEN  Auto
                                                                  THEN  UnfoldTopAb  0
                                                                  THEN  Auto
                                                                  THEN  With  \mkleeneopen{}i\mkleeneclose{}  (D  0)\mcdot{}
                                                                  THEN  Auto)))
  )\mcdot{}

---

Home Index