---

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

∀s:SES
  (ActionsDisjoint
  ⇒ (∀pas:ProtocolAction List. ∀es:EO+(Info). ∀thr:Thread. ∀A:Id.
        (pas(thr) ⇒ (∀f:SecurityData ─→ (Atom1?). (ses-fresh-sequence(f;A;pas) ⇒ ses-fresh-thread(s;es;f;A;thr))))))
BY
{ (Auto
   THEN All (Unfolds ``ses-is-protocol-actions ses-thread``)
   THEN All (Unfolds ``ses-fresh-sequence ses-fresh-thread``)
   THEN ParallelLast
   THEN (D 0 THENA Auto)
   THEN (D -2 THENA 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
⊢ (fst(pas[i])) = "sign" ∈ Atom

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:ℕ||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))))))

---

Latex:

---

Latex:
\mforall{}s:SES
    (ActionsDisjoint
    {}\mRightarrow{}  (\mforall{}pas:ProtocolAction  List.  \mforall{}es:EO+(Info).  \mforall{}thr:Thread.  \mforall{}A:Id.
                (pas(thr)
                {}\mRightarrow{}  (\mforall{}f:SecurityData  {}\mrightarrow{}  (Atom1?)
                            (ses-fresh-sequence(f;A;pas)  {}\mRightarrow{}  ses-fresh-thread(s;es;f;A;thr))))))


By

---

Latex:
(Auto
  THEN  All  (Unfolds  ``ses-is-protocol-actions  ses-thread``)
  THEN  All  (Unfolds  ``ses-fresh-sequence  ses-fresh-thread``)
  THEN  ParallelLast
  THEN  (D  0  THENA  Auto)
  THEN  (D  -2  THENA  Auto))

---

Home Index