---

Step * of Lemma decidable-ses-fresh-sequence

∀f:SecurityData ─→ (Atom1?). ∀A:Id. ∀pas:ProtocolAction List.  Dec(ses-fresh-sequence(f;A;pas))
BY
{ (Auto
   THEN (Subst' ses-fresh-sequence(f;A;pas) ~ ∀i:ℕ||pas||
                                                pa-is-sign-implies(pas[i];v.((fst(snd(v))) = A ∈ Id)
                                                ∧ (∃j:ℕi
                                                    pa-is-new-and(pas[j];n.((↑isl(f (fst(v))))
                                                    ∧ (outl(f (fst(v))) = n ∈ Atom1))
                                                    ∧ (∀k:{j + 1..i-}
                                                         pa-is-sign-implies(pas[k];v'.(↑isl(f (fst(v'))))
                                                         ⇒ (¬(outl(f (fst(v'))) = n ∈ Atom1))))))) 0
         THENA (RepUR ``ses-fresh-sequence pa-is-sign-implies pa-is-new-and`` 0 THEN Auto)
         )
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}f:SecurityData  {}\mrightarrow{}  (Atom1?).  \mforall{}A:Id.  \mforall{}pas:ProtocolAction  List.    Dec(ses-fresh-sequence(f;A;pas))


By

---

Latex:
(Auto
  THEN  (Subst'  ses-fresh-sequence(f;A;pas) 
              \msim{}  \mforall{}i:\mBbbN{}||pas||
                      pa-is-sign-implies(pas[i];v.((fst(snd(v)))  =  A)
                      \mwedge{}  (\mexists{}j:\mBbbN{}i
                              pa-is-new-and(pas[j];n.((\muparrow{}isl(f  (fst(v))))  \mwedge{}  (outl(f  (fst(v)))  =  n))
                              \mwedge{}  (\mforall{}k:\{j  +  1..i\msupminus{}\}
                                        pa-is-sign-implies(pas[k];v'.(\muparrow{}isl(f  (fst(v'))))
                                        {}\mRightarrow{}  (\mneg{}(outl(f  (fst(v')))  =  n)))))))  0
              THENA  (RepUR  ``ses-fresh-sequence  pa-is-sign-implies  pa-is-new-and``  0  THEN  Auto)
              )
  THEN  Auto)

---

Home Index