---

Step * 1 of Lemma signature-release-lemma


1. ses : SES
2. SecurityAxioms
3. bss : Basic1 List
4. Legal(bss) ∧ UniqueSignatures(bss)
5. A : Id
6. Honest(A)
7. Protocol1(bss) A
8. es : EO+(Info)
9. thr : Thread
10. (thr is one of bss at A)
11. loc(thr)= A
12. i : ℕ||thr||
13. j : ℕi
14. ↑thr[j] ∈b Sign
15. ∀k:{j + 1..i-}. (¬↑thr[k] ∈b Send)
16. (signature(thr[j]) released before thr[i])@i
⊢ False
BY
{ (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] THEN Auto)
         THEN (FLemma `ses-nonce-from-ordering` [-2] THENA Auto)
         THEN RepeatFor 3 (PromoteHyp (-1) 5⋅))
   THEN Assert ⌜∀e:E
                  (Action(e)
                  ⇒ e has* signature(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. PropertyF
5. PropertyO
6. ses-ordering'(ses)
7. PropertyN
8. PropertyV
9. PropertyR
10. PropertyD
11. PropertyS
12. PropertyK
13. bss : Basic1 List
14. Legal(bss)
15. UniqueSignatures(bss)
16. A : Id
17. Honest(A)
18. Protocol1(bss) A
19. es : EO+(Info)
20. thr : {thr:Act List| ∀i:ℕ||thr|| - 1. (thr[i] <loc thr[i + 1])} 
21. (thr is one of bss at A)
22. loc(thr)= A
23. i : ℕ||thr||
24. j : ℕi
25. ↑thr[j] ∈b Sign
26. ∀k:{j + 1..i-}. (¬↑thr[k] ∈b Send)
27. (signature(thr[j]) released before thr[i])@i
⊢ ∀e:E
    (Action(e)
    ⇒ e has* signature(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. PropertyF
5. PropertyO
6. ses-ordering'(ses)
7. PropertyN
8. PropertyV
9. PropertyR
10. PropertyD
11. PropertyS
12. PropertyK
13. bss : Basic1 List
14. Legal(bss)
15. UniqueSignatures(bss)
16. A : Id
17. Honest(A)
18. Protocol1(bss) A
19. es : EO+(Info)
20. thr : {thr:Act List| ∀i:ℕ||thr|| - 1. (thr[i] <loc thr[i + 1])} 
21. (thr is one of bss at A)
22. loc(thr)= A
23. i : ℕ||thr||
24. j : ℕi
25. ↑thr[j] ∈b Sign
26. ∀k:{j + 1..i-}. (¬↑thr[k] ∈b Send)
27. (signature(thr[j]) released before thr[i])@i
28. ∀e:E
      (Action(e)
      ⇒ e has* signature(thr[j])
      ⇒ (((¬(loc(e) = A ∈ Id)) ⇒ (thr[i] < e)) ∧ ((e <loc thr[i]) ⇒ (e ∈ thr ∧ (¬↑e ∈b Send)))))
⊢ False

---

Latex:

---

Latex:

1.  ses  :  SES
2.  SecurityAxioms
3.  bss  :  Basic1  List
4.  Legal(bss)  \mwedge{}  UniqueSignatures(bss)
5.  A  :  Id
6.  Honest(A)
7.  Protocol1(bss)  A
8.  es  :  EO+(Info)
9.  thr  :  Thread
10.  (thr  is  one  of  bss  at  A)
11.  loc(thr)=  A
12.  i  :  \mBbbN{}||thr||
13.  j  :  \mBbbN{}i
14.  \muparrow{}thr[j]  \mmember{}\msubb{}  Sign
15.  \mforall{}k:\{j  +  1..i\msupminus{}\}.  (\mneg{}\muparrow{}thr[k]  \mmember{}\msubb{}  Send)
16.  (signature(thr[j])  released  before  thr[i])@i
\mvdash{}  False


By

---

Latex:
(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]  THEN  Auto)
              THEN  (FLemma  `ses-nonce-from-ordering`  [-2]  THENA  Auto)
              THEN  RepeatFor  3  (PromoteHyp  (-1)  5\mcdot{}))
  THEN  Assert  \mkleeneopen{}\mforall{}e:E
                                (Action(e)
                                {}\mRightarrow{}  e  has*  signature(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{})\mcdot{}

---

Home Index