---

Step * of Lemma nonce-release-lemma

∀[ses:SES]
  ∀[bss:Basic1 List]
    ∀[A:Id]
      (∀[es:EO+(Info)]. ∀[thr:Thread].
         (∀[i:ℕ||thr||]. ∀[j:ℕi].
            (¬(New(thr[j]) released before thr[i])) supposing 
               ((∀k:{j + 1..i-}. (¬↑thr[k] ∈b Send)) and 
               (↑thr[j] ∈b New))) supposing 
            (loc(thr)= A and 
            (thr is one of bss at A))) supposing 
         ((Protocol1(bss) A) and 
         Honest(A)) 
    supposing Legal(bss) 
  supposing SecurityAxioms
BY
{ (Auto
   THEN D 2
   THEN SplitAndHyps
   THEN All (Unfold `ses-thread`)
   THEN Auto
   THEN ((FLemma `ses-flow-axiom-ordering` [4] THENA Auto)
         THEN (FLemma `ses-ordering-ordering\'` [-1] THENA Auto)⋅
         THEN (FLemma `ses-nonce-from-ordering` [-2] THENA Auto)
         THEN PromoteHyp (-3) 4
         THEN PromoteHyp (-2) 5
         THEN PromoteHyp (-1) 5)⋅
   THEN Assert ⌜∀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)))))⌝⋅) }

1
.....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)))))

2
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. ∀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)))))
⊢ ¬(New(thr[j]) released before thr[i])

---

Latex:

---

Latex:
\mforall{}[ses:SES]
    \mforall{}[bss:Basic1  List]
        \mforall{}[A:Id]
            (\mforall{}[es:EO+(Info)].  \mforall{}[thr:Thread].
                  (\mforall{}[i:\mBbbN{}||thr||].  \mforall{}[j:\mBbbN{}i].
                        (\mneg{}(New(thr[j])  released  before  thr[i]))  supposing 
                              ((\mforall{}k:\{j  +  1..i\msupminus{}\}.  (\mneg{}\muparrow{}thr[k]  \mmember{}\msubb{}  Send))  and 
                              (\muparrow{}thr[j]  \mmember{}\msubb{}  New)))  supposing 
                        (loc(thr)=  A  and 
                        (thr  is  one  of  bss  at  A)))  supposing 
                  ((Protocol1(bss)  A)  and 
                  Honest(A)) 
        supposing  Legal(bss) 
    supposing  SecurityAxioms


By

---

Latex:
(Auto
  THEN  D  2
  THEN  SplitAndHyps
  THEN  All  (Unfold  `ses-thread`)
  THEN  Auto
  THEN  ((FLemma  `ses-flow-axiom-ordering`  [4]  THENA  Auto)
              THEN  (FLemma  `ses-ordering-ordering\mbackslash{}'`  [-1]  THENA  Auto)\mcdot{}
              THEN  (FLemma  `ses-nonce-from-ordering`  [-2]  THENA  Auto)
              THEN  PromoteHyp  (-3)  4
              THEN  PromoteHyp  (-2)  5
              THEN  PromoteHyp  (-1)  5)\mcdot{}
  THEN  Assert  \mkleeneopen{}\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)))))\mkleeneclose{}\mcdot{})

---

Home Index