---

Step * 2 2 1 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
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
14. (fst(pas[j])) = "new" ∈ Atom
15. ↑isl(f (fst(snd(pas[i]))))
16. outl(f (fst(snd(pas[i])))) = (snd(pas[j])) ∈ Atom1
17. ∀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)))
18. signer(thr[i]) = A ∈ Id
⊢ (↑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
{ (Assert (↑thr[j] ∈b New) ∧ (New(thr[j]) = (snd(pas[j])) ∈ Atom1) BY
         ((Assert pas[j](thr[j]) BY
                 Auto⋅)
          THEN (RepUR ``ses-is-protocol-action`` -1
                THEN MoveToConcl (-1)
                THEN MoveToConcl (-5)
                THEN GenConclAtAddr [1;2;1]
                THEN D -2
                THEN Reduce 0
                THEN (D 0 THENA Auto)
                THEN Thin (-2) 
                THEN MoveToConcl (-2)
                THEN HypSubst' (-1) 0
                THEN Reduce 0
                THEN All Thin
                THEN 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
14. (fst(pas[j])) = "new" ∈ Atom
15. ↑isl(f (fst(snd(pas[i]))))
16. outl(f (fst(snd(pas[i])))) = (snd(pas[j])) ∈ Atom1
17. ∀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)))
18. signer(thr[i]) = A ∈ Id
19. (↑thr[j] ∈b New) ∧ (New(thr[j]) = (snd(pas[j])) ∈ Atom1)
⊢ (↑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||@i
8.  \mforall{}i:\mBbbN{}||pas||.  pas[i](thr[i])@i
9.  f  :  SecurityData  {}\mrightarrow{}  (Atom1?)@i
10.  i  :  \mBbbN{}||thr||@i
11.  \muparrow{}thr[i]  \mmember{}\msubb{}  Sign@i
12.  (fst(snd(snd(pas[i]))))  =  A
13.  j  :  \mBbbN{}i
14.  (fst(pas[j]))  =  "new"
15.  \muparrow{}isl(f  (fst(snd(pas[i]))))
16.  outl(f  (fst(snd(pas[i]))))  =  (snd(pas[j]))
17.  \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])))))
18.  signer(thr[i])  =  A
\mvdash{}  (\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:
(Assert  (\muparrow{}thr[j]  \mmember{}\msubb{}  New)  \mwedge{}  (New(thr[j])  =  (snd(pas[j])))  BY
              ((Assert  pas[j](thr[j])  BY
                              Auto\mcdot{})
                THEN  (RepUR  ``ses-is-protocol-action``  -1
                            THEN  MoveToConcl  (-1)
                            THEN  MoveToConcl  (-5)
                            THEN  GenConclAtAddr  [1;2;1]
                            THEN  D  -2
                            THEN  Reduce  0
                            THEN  (D  0  THENA  Auto)
                            THEN  Thin  (-2) 
                            THEN  MoveToConcl  (-2)
                            THEN  HypSubst'  (-1)  0
                            THEN  Reduce  0
                            THEN  All  Thin
                            THEN  Auto)\mcdot{}
                ))

---

Home Index