Proof of Nuprl Lemma : fresh-sig-protocol1

Step * 1 1 1 1 1 1 of Lemma fresh-sig-protocol1_property

1. s : SES
2. ActionsDisjoint
3. PropertyO
4. PropertyS
5. bss : Basic1 List
6. f : SecurityData ⟶ (Atom1?)
7. A : Id@i
8. Honest(A)@i
9. ∀es:EO+(Info)
     (Honest(A)
     ⇒ (∀e:Act
           ((loc(e) = A ∈ Id)
           ⇒ ((∃thr:Thread. (e ∈ thr ∧ (thr is one of bss at A) ∧ loc(thr)= A))
              ∧ (∀thr1,thr2:Thread.
                   (e ∈ thr1
                   ⇒ (thr1 is one of bss at A)
                   ⇒ e ∈ thr2
                   ⇒ (thr2 is one of bss at A)
                   ⇒ (thr1 ≤ thr2 ∨ thr2 ≤ thr1)))))))@i'
10. es : EO+(Info)@i'
11. E(Sign) ⊆r Act
12. ∀thr:Thread. ∀A:Id.  ((thr is one of bss at A) ⇒ ses-fresh-thread(s;es;f;A;thr))
13. thr1 : {thr:Act List| ∀i:ℕ||thr|| - 1. (thr[i] <loc thr[i + 1])} @i
14. (thr1 is one of bss at A)@i'
15. e1 : E(Sign)@i
16. i : ℕ||thr1||@i
17. e1 = thr1[i] ∈ E@i
18. signer(e1) = A ∈ Id
19. e2 : E(Sign)
20. Sign(e2) = Sign(e1) ∈ (SecurityData × Id × Atom1)
21. signer(e2) = A ∈ Id
22. thr : Thread
23. e2 ∈ thr
24. (thr is one of bss at A)
25. loc(thr)= A
26. ∀thr1,thr2:Thread.
      (e2 ∈ thr1 ⇒ (thr1 is one of bss at A) ⇒ e2 ∈ thr2 ⇒ (thr2 is one of bss at A) ⇒ (thr1 ≤ thr2 ∨ thr2 ≤ thr1))
⊢ e2 = e1 ∈ E
BY
{ (D -4
   THEN OnMaybeHyp 11 (\h. (Unfold `ses-fresh-thread` h

                            THEN (InstHyp [⌜thr1⌝;⌜A⌝;⌜i⌝] h⋅ THENA Complete (Auto))

                            THEN (InstHyp [⌜thr⌝;⌜A⌝;⌜i1⌝] h⋅ THENA Complete (Auto))))

   THEN Auto
   THEN ExRepD) }

1
1. s : SES
2. ActionsDisjoint
3. PropertyO
4. PropertyS
5. bss : Basic1 List
6. f : SecurityData ⟶ (Atom1?)
7. A : Id@i
8. Honest(A)@i
9. ∀es:EO+(Info)
     (Honest(A)
     ⇒ (∀e:Act
           ((loc(e) = A ∈ Id)
           ⇒ ((∃thr:Thread. (e ∈ thr ∧ (thr is one of bss at A) ∧ loc(thr)= A))
              ∧ (∀thr1,thr2:Thread.
                   (e ∈ thr1
                   ⇒ (thr1 is one of bss at A)
                   ⇒ e ∈ thr2
                   ⇒ (thr2 is one of bss at A)
                   ⇒ (thr1 ≤ thr2 ∨ thr2 ≤ thr1)))))))@i'
10. es : EO+(Info)@i'
11. E(Sign) ⊆r Act
12. ∀thr:Thread. ∀A:Id.
      ((thr is one of bss at A)
      ⇒ (∀i:ℕ||thr||
            ((↑thr[i] ∈_b Sign)
            ⇒ ((signer(thr[i]) = A ∈ Id)
               ∧ (∃j:ℕi
                   ((↑thr[j] ∈_b New)
                   ∧ (↑isl(f signed(thr[i])))
                   ∧ (outl(f signed(thr[i])) = New(thr[j]) ∈ Atom1)
                   ∧ (∀k:{j + 1..i^-}
                        ((↑thr[k] ∈_b Sign)
                        ⇒ (↑isl(f signed(thr[k])))
                        ⇒ (¬(outl(f signed(thr[k])) = New(thr[j]) ∈ Atom1))))))))))
13. thr1 : {thr:Act List| ∀i:ℕ||thr|| - 1. (thr[i] <loc thr[i + 1])} @i
14. (thr1 is one of bss at A)@i'
15. e1 : E(Sign)@i
16. i : ℕ||thr1||@i
17. e1 = thr1[i] ∈ E@i
18. signer(e1) = A ∈ Id
19. e2 : E(Sign)
20. Sign(e2) = Sign(e1) ∈ (SecurityData × Id × Atom1)
21. signer(e2) = A ∈ Id
22. thr : Thread
23. i1 : ℕ||thr||
24. e2 = thr[i1] ∈ E
25. (thr is one of bss at A)
26. loc(thr)= A
27. ∀thr1,thr2:Thread.
      (e2 ∈ thr1 ⇒ (thr1 is one of bss at A) ⇒ e2 ∈ thr2 ⇒ (thr2 is one of bss at A) ⇒ (thr1 ≤ thr2 ∨ thr2 ≤ thr1))
28. signer(thr1[i]) = A ∈ Id
29. j1 : ℕi
30. ↑thr1[j1] ∈_b New
31. ↑isl(f signed(thr1[i]))
32. outl(f signed(thr1[i])) = New(thr1[j1]) ∈ Atom1
33. ∀k:{j1 + 1..i^-}
      ((↑thr1[k] ∈_b Sign) ⇒ (↑isl(f signed(thr1[k]))) ⇒ (¬(outl(f signed(thr1[k])) = New(thr1[j1]) ∈ Atom1)))
34. signer(thr[i1]) = A ∈ Id
35. j : ℕi1
36. ↑thr[j] ∈_b New
37. ↑isl(f signed(thr[i1]))
38. outl(f signed(thr[i1])) = New(thr[j]) ∈ Atom1
39. ∀k:{j + 1..i1^-}
      ((↑thr[k] ∈_b Sign) ⇒ (↑isl(f signed(thr[k]))) ⇒ (¬(outl(f signed(thr[k])) = New(thr[j]) ∈ Atom1)))
⊢ e2 = e1 ∈ E

Latex:

Latex:
1. s : SES 2. ActionsDisjoint 3. PropertyO 4. PropertyS 5. bss : Basic1 List 6. f : SecurityData {}\mrightarrow{} (Atom1?) 7. A : Id@i 8. Honest(A)@i 9. \mforall{}es:EO+(Info) (Honest(A) {}\mRightarrow{} (\mforall{}e:Act ((loc(e) = A) {}\mRightarrow{} ((\mexists{}thr:Thread. (e \mmember{} thr \mwedge{} (thr is one of bss at A) \mwedge{} loc(thr)= A)) \mwedge{} (\mforall{}thr1,thr2:Thread. (e \mmember{} thr1 {}\mRightarrow{} (thr1 is one of bss at A) {}\mRightarrow{} e \mmember{} thr2 {}\mRightarrow{} (thr2 is one of bss at A) {}\mRightarrow{} (thr1 \mleq{} thr2 \mvee{} thr2 \mleq{} thr1)))))))@i' 10. es : EO+(Info)@i' 11. E(Sign) \msubseteq{}r Act 12. \mforall{}thr:Thread. \mforall{}A:Id. ((thr is one of bss at A) {}\mRightarrow{} ses-fresh-thread(s;es;f;A;thr)) 13. thr1 : \{thr:Act List| \mforall{}i:\mBbbN{}||thr|| - 1. (thr[i] <loc thr[i + 1])\} @i 14. (thr1 is one of bss at A)@i' 15. e1 : E(Sign)@i 16. i : \mBbbN{}||thr1||@i 17. e1 = thr1[i]@i 18. signer(e1) = A 19. e2 : E(Sign) 20. Sign(e2) = Sign(e1) 21. signer(e2) = A 22. thr : Thread 23. e2 \mmember{} thr 24. (thr is one of bss at A) 25. loc(thr)= A 26. \mforall{}thr1,thr2:Thread. (e2 \mmember{} thr1 {}\mRightarrow{} (thr1 is one of bss at A) {}\mRightarrow{} e2 \mmember{} thr2 {}\mRightarrow{} (thr2 is one of bss at A) {}\mRightarrow{} (thr1 \mleq{} thr2 \mvee{} thr2 \mleq{} thr1)) \mvdash{} e2 = e1 By Latex: (D -4 THEN OnMaybeHyp 11 (\mbackslash{}h. (Unfold `ses-fresh-thread` h THEN (InstHyp [\mkleeneopen{}thr1\mkleeneclose{};\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}i\mkleeneclose{}] h\mcdot{} THENA Complete (Auto)) THEN (InstHyp [\mkleeneopen{}thr\mkleeneclose{};\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}i1\mkleeneclose{}] h\mcdot{} THENA Complete (Auto)))) THEN Auto THEN ExRepD) Home Index