---

Step * 2 of Lemma ses-is-protocol-actions-fresh


1. s : SES@i'
2. ActionsDisjoint@i'
3. pas : ProtocolAction List@i
4. es : EO+(Info)@i'
5. thr : {thr:Act List| ∀i:ℕ||thr|| - 1. (thr[i] <loc thr[i + 1])} @i
6. A : Id@i
7. (||thr|| = ||pas|| ∈ ℤ) ∧ (∀i:ℕ||pas||. pas[i](thr[i]))@i
8. f : SecurityData ─→ (Atom1?)@i
9. i : ℕ||thr||@i
10. ↑thr[i] ∈b Sign@i
11. ((fst(snd(snd(pas[i])))) = A ∈ Id)
∧ (∃j:ℕi
    (((fst(pas[j])) = "new" ∈ Atom)
    ∧ ((↑isl(f (fst(snd(pas[i]))))) ∧ (outl(f (fst(snd(pas[i])))) = (snd(pas[j])) ∈ Atom1))
    ∧ (∀k:{j + 1..i-}
         (((fst(pas[k])) = "sign" ∈ Atom)
         ⇒ (↑isl(f (fst(snd(pas[k])))))
         ⇒ (¬(outl(f (fst(snd(pas[k])))) = (snd(pas[j])) ∈ Atom1))))))
⊢ (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))))))
BY
{ Auto }

1
1. s : SES@i'
2. ActionsDisjoint@i'
3. pas : ProtocolAction List@i
4. es : EO+(Info)@i'
5. thr : {thr:Act List| ∀i:ℕ||thr|| - 1. (thr[i] <loc thr[i + 1])} @i
6. A : Id@i
7. ||thr|| = ||pas|| ∈ ℤ@i
8. ∀i:ℕ||pas||. pas[i](thr[i])@i
9. f : SecurityData ─→ (Atom1?)@i
10. i : ℕ||thr||@i
11. ↑thr[i] ∈b Sign@i
12. (fst(snd(snd(pas[i])))) = A ∈ Id
13. ∃j:ℕi
     (((fst(pas[j])) = "new" ∈ Atom)
     ∧ ((↑isl(f (fst(snd(pas[i]))))) ∧ (outl(f (fst(snd(pas[i])))) = (snd(pas[j])) ∈ Atom1))
     ∧ (∀k:{j + 1..i-}
          (((fst(pas[k])) = "sign" ∈ Atom)
          ⇒ (↑isl(f (fst(snd(pas[k])))))
          ⇒ (¬(outl(f (fst(snd(pas[k])))) = (snd(pas[j])) ∈ Atom1)))))
⊢ signer(thr[i]) = A ∈ Id

2
1. s : SES@i'
2. ActionsDisjoint@i'
3. pas : ProtocolAction List@i
4. es : EO+(Info)@i'
5. thr : {thr:Act List| ∀i:ℕ||thr|| - 1. (thr[i] <loc thr[i + 1])} @i
6. A : Id@i
7. ||thr|| = ||pas|| ∈ ℤ@i
8. ∀i:ℕ||pas||. pas[i](thr[i])@i
9. f : SecurityData ─→ (Atom1?)@i
10. i : ℕ||thr||@i
11. ↑thr[i] ∈b Sign@i
12. (fst(snd(snd(pas[i])))) = A ∈ Id
13. ∃j:ℕi
     (((fst(pas[j])) = "new" ∈ Atom)
     ∧ ((↑isl(f (fst(snd(pas[i]))))) ∧ (outl(f (fst(snd(pas[i])))) = (snd(pas[j])) ∈ Atom1))
     ∧ (∀k:{j + 1..i-}
          (((fst(pas[k])) = "sign" ∈ Atom)
          ⇒ (↑isl(f (fst(snd(pas[k])))))
          ⇒ (¬(outl(f (fst(snd(pas[k])))) = (snd(pas[j])) ∈ Atom1)))))
14. 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)))))

---

Latex:

---

Latex:

1.  s  :  SES@i'
2.  ActionsDisjoint@i'
3.  pas  :  ProtocolAction  List@i
4.  es  :  EO+(Info)@i'
5.  thr  :  \{thr:Act  List|  \mforall{}i:\mBbbN{}||thr||  -  1.  (thr[i]  <loc  thr[i  +  1])\}  @i
6.  A  :  Id@i
7.  (||thr||  =  ||pas||)  \mwedge{}  (\mforall{}i:\mBbbN{}||pas||.  pas[i](thr[i]))@i
8.  f  :  SecurityData  {}\mrightarrow{}  (Atom1?)@i
9.  i  :  \mBbbN{}||thr||@i
10.  \muparrow{}thr[i]  \mmember{}\msubb{}  Sign@i
11.  ((fst(snd(snd(pas[i]))))  =  A)
\mwedge{}  (\mexists{}j:\mBbbN{}i
        (((fst(pas[j]))  =  "new")
        \mwedge{}  ((\muparrow{}isl(f  (fst(snd(pas[i])))))  \mwedge{}  (outl(f  (fst(snd(pas[i]))))  =  (snd(pas[j]))))
        \mwedge{}  (\mforall{}k:\{j  +  1..i\msupminus{}\}
                  (((fst(pas[k]))  =  "sign")
                  {}\mRightarrow{}  (\muparrow{}isl(f  (fst(snd(pas[k])))))
                  {}\mRightarrow{}  (\mneg{}(outl(f  (fst(snd(pas[k]))))  =  (snd(pas[j]))))))))
\mvdash{}  (signer(thr[i])  =  A)
\mwedge{}  (\mexists{}j:\mBbbN{}i
        ((\muparrow{}thr[j]  \mmember{}\msubb{}  New)
        \mwedge{}  (\muparrow{}isl(f  signed(thr[i])))
        \mwedge{}  (outl(f  signed(thr[i]))  =  New(thr[j]))
        \mwedge{}  (\mforall{}k:\{j  +  1..i\msupminus{}\}
                  ((\muparrow{}thr[k]  \mmember{}\msubb{}  Sign)
                  {}\mRightarrow{}  (\muparrow{}isl(f  signed(thr[k])))
                  {}\mRightarrow{}  (\mneg{}(outl(f  signed(thr[k]))  =  New(thr[j])))))))


By

---

Latex:
Auto

---

Home Index