---

Step * of Lemma signature-release-lemma2

∀s:SecurityTheory. ∀bss:Basic1 List.
  ((Legal(bss) ∧ FreshSignatures(bss))
  ⇒ (∀A:Id
        (Protocol1(bss) A)
        ⇒ (∀es:EO+(Info). ∀thr:Thread.
              ((thr is one of bss at A) ⇒ sig-release-thread(sth-es(s);es;A;thr) supposing loc(thr)= A)) 
        supposing Honest(A)))
BY
{ (Unfold `sig-release-thread` 0
   THEN ((D 0 THENA Auto) THEN RepeatFor 2 (D -1) THEN RepUR ``sth-es`` 0 ⋅)
   THEN (InstLemma `signature-release-lemma` [⌈ses⌉]⋅ THENA Auto)
   THEN ParallelLast
   THEN (D 0 THENA Auto)
   THEN (Assert UniqueSignatures(bss) BY
               ((BLemma `fresh-sig-protocol1_property` THEN Auto) THEN BLemma `ses-flow-axiom-ordering` THEN Auto))
   THEN (D (-3) THENA Auto)
   THEN ParallelLast
   THEN BasicUniformUnivCD Auto⋅
   THEN (D -2 THENA Auto)
   THEN RepeatFor 5 (ParallelLast)
   THEN (Unfold `ses-thread` (-4)
         THEN RepeatFor 2 (ParallelLast)
         THEN (D 0 THENA Auto)
         THEN ThinTrivial
         THEN ((D 0 THENA Auto) THEN ThinTrivial THEN Auto)⋅)⋅) }

1
1. ses : SES@i'
2. A : SecurityAxioms@i'
3. s2 : Top@i'
4. ∀[bss:Basic1 List]
     ∀[A:Id]
       (∀[es:EO+(Info)]. ∀[thr:Thread].
          (∀[i:ℕ||thr||]. ∀[j:ℕi].
             (¬(signature(thr[j]) released before thr[i])) supposing 
                ((∀k:{j + 1..i-}. (¬↑thr[k] ∈b Send)) and 
                (↑thr[j] ∈b Sign))) supposing 
             (loc(thr)= A and 
             (thr is one of bss at A))) supposing 
          ((Protocol1(bss) A) and 
          Honest(A)) 
     supposing Legal(bss) ∧ UniqueSignatures(bss)
5. bss : Basic1 List@i'
6. Legal(bss)@i'
7. FreshSignatures(bss)@i'
8. UniqueSignatures(bss)
9. A@0 : Id@i
10. Honest(A@0)
11. Protocol1(bss) A@0@i'
12. es : EO+(Info)@i'
13. thr : {thr:Act List| ∀i:ℕ||thr|| - 1. (thr[i] <loc thr[i + 1])} @i
14. (thr is one of bss at A@0)@i'
15. loc(thr)= A@0
16. ∀[i:ℕ||thr||]. ∀[j:ℕi].
      (¬(signature(thr[j]) released before thr[i])) supposing 
         ((∀k:{j + 1..i-}. (¬↑thr[k] ∈b Send)) and 
         (↑thr[j] ∈b Sign))
17. i : ℕ||thr||@i
18. ∀[j:ℕi]
      (¬(signature(thr[j]) released before thr[i])) supposing 
         ((∀k:{j + 1..i-}. (¬↑thr[k] ∈b Send)) and 
         (↑thr[j] ∈b Sign))
19. j : ℕi@i
20. ↑thr[j] ∈b Sign@i
21. ∀k:{j + 1..i-}. (¬↑thr[k] ∈b Send)@i
22. ¬(signature(thr[j]) released before thr[i])
23. e : E@i
24. ¬(loc(e) = A@0 ∈ Id)@i
25. (e has signature(thr[j]))@i
⊢ (thr[i] < e)

---

Latex:

---

Latex:
\mforall{}s:SecurityTheory.  \mforall{}bss:Basic1  List.
    ((Legal(bss)  \mwedge{}  FreshSignatures(bss))
    {}\mRightarrow{}  (\mforall{}A:Id
                (Protocol1(bss)  A)
                {}\mRightarrow{}  (\mforall{}es:EO+(Info).  \mforall{}thr:Thread.
                            ((thr  is  one  of  bss  at  A)
                            {}\mRightarrow{}  sig-release-thread(sth-es(s);es;A;thr)  supposing  loc(thr)=  A)) 
                supposing  Honest(A)))


By

---

Latex:
(Unfold  `sig-release-thread`  0
  THEN  ((D  0  THENA  Auto)  THEN  RepeatFor  2  (D  -1)  THEN  RepUR  ``sth-es``  0  \mcdot{})
  THEN  (InstLemma  `signature-release-lemma`  [\mkleeneopen{}ses\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  ParallelLast
  THEN  (D  0  THENA  Auto)
  THEN  (Assert  UniqueSignatures(bss)  BY
                          ((BLemma  `fresh-sig-protocol1\_property`  THEN  Auto)
                            THEN  BLemma  `ses-flow-axiom-ordering`
                            THEN  Auto))
  THEN  (D  (-3)  THENA  Auto)
  THEN  ParallelLast
  THEN  BasicUniformUnivCD  Auto\mcdot{}
  THEN  (D  -2  THENA  Auto)
  THEN  RepeatFor  5  (ParallelLast)
  THEN  (Unfold  `ses-thread`  (-4)
              THEN  RepeatFor  2  (ParallelLast)
              THEN  (D  0  THENA  Auto)
              THEN  ThinTrivial
              THEN  ((D  0  THENA  Auto)  THEN  ThinTrivial  THEN  Auto)\mcdot{})\mcdot{})

---

Home Index