---

Step * 1 1 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. n : Atom@i
13. v1 : if n =a "new" then Atom1
if n =a "send" then SecurityData
if n =a "rcv" then SecurityData
if n =a "encrypt" then SecurityData × Key × Atom1
if n =a "decrypt" then SecurityData × Key × Atom1
if n =a "sign" then SecurityData × Id × Atom1
if n =a "verify" then SecurityData × Id × Atom1
else Top
fi @i
14. pas[i] = <n, v1> ∈ ProtocolAction@i
⊢ if n =a "new" then (↑thr[i] ∈b New) ∧ (New(thr[i]) = v1 ∈ Atom1)
if n =a "send" then (↑thr[i] ∈b Send) ∧ (Send(thr[i]) = v1 ∈ SecurityData)
if n =a "rcv" then (↑thr[i] ∈b Rcv) ∧ (Rcv(thr[i]) = v1 ∈ SecurityData)
if n =a "encrypt" then (↑thr[i] ∈b Encrypt) ∧ (Encrypt(thr[i]) = v1 ∈ (SecurityData × Key × Atom1))
if n =a "decrypt" then (↑thr[i] ∈b Decrypt) ∧ (Decrypt(thr[i]) = v1 ∈ (SecurityData × Key × Atom1))
if n =a "sign" then (↑thr[i] ∈b Sign) ∧ (Sign(thr[i]) = v1 ∈ (SecurityData × Id × Atom1))
if n =a "verify" then (↑thr[i] ∈b Verify) ∧ (Verify(thr[i]) = v1 ∈ (SecurityData × Id × Atom1))
else False
fi 
⇒ (n = "sign" ∈ Atom)
BY
{ (((With ⌈es⌉ (D 2)⋅ THENA Auto) THEN D -1)
   THEN (InstHyp [⌈thr[i]⌉] (-1)⋅ THENA Auto)
   THEN Subst' (f1 thr[i]) = 4 ∈ ℤ -1
   THEN MoveToConcl (-1)
   THEN (GenConclTerm ⌈thr[i]⌉⋅ THENA Auto)
   THEN (D 0 THENA Auto)
   THEN SplitAndHyps
   THEN Repeat (((\p. BoolCase (find_splitter (concl p)) p THENA Auto) THENL [CompleteAuto; Id]))
   THEN Auto) }

---

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.  n  :  Atom@i
13.  v1  :  if  n  =a  "new"  then  Atom1
if  n  =a  "send"  then  SecurityData
if  n  =a  "rcv"  then  SecurityData
if  n  =a  "encrypt"  then  SecurityData  \mtimes{}  Key  \mtimes{}  Atom1
if  n  =a  "decrypt"  then  SecurityData  \mtimes{}  Key  \mtimes{}  Atom1
if  n  =a  "sign"  then  SecurityData  \mtimes{}  Id  \mtimes{}  Atom1
if  n  =a  "verify"  then  SecurityData  \mtimes{}  Id  \mtimes{}  Atom1
else  Top
fi  @i
14.  pas[i]  =  <n,  v1>@i
\mvdash{}  if  n  =a  "new"  then  (\muparrow{}thr[i]  \mmember{}\msubb{}  New)  \mwedge{}  (New(thr[i])  =  v1)
if  n  =a  "send"  then  (\muparrow{}thr[i]  \mmember{}\msubb{}  Send)  \mwedge{}  (Send(thr[i])  =  v1)
if  n  =a  "rcv"  then  (\muparrow{}thr[i]  \mmember{}\msubb{}  Rcv)  \mwedge{}  (Rcv(thr[i])  =  v1)
if  n  =a  "encrypt"  then  (\muparrow{}thr[i]  \mmember{}\msubb{}  Encrypt)  \mwedge{}  (Encrypt(thr[i])  =  v1)
if  n  =a  "decrypt"  then  (\muparrow{}thr[i]  \mmember{}\msubb{}  Decrypt)  \mwedge{}  (Decrypt(thr[i])  =  v1)
if  n  =a  "sign"  then  (\muparrow{}thr[i]  \mmember{}\msubb{}  Sign)  \mwedge{}  (Sign(thr[i])  =  v1)
if  n  =a  "verify"  then  (\muparrow{}thr[i]  \mmember{}\msubb{}  Verify)  \mwedge{}  (Verify(thr[i])  =  v1)
else  False
fi 
{}\mRightarrow{}  (n  =  "sign")


By

---

Latex:
(((With  \mkleeneopen{}es\mkleeneclose{}  (D  2)\mcdot{}  THENA  Auto)  THEN  D  -1)
  THEN  (InstHyp  [\mkleeneopen{}thr[i]\mkleeneclose{}]  (-1)\mcdot{}  THENA  Auto)
  THEN  Subst'  (f1  thr[i])  =  4  -1
  THEN  MoveToConcl  (-1)
  THEN  (GenConclTerm  \mkleeneopen{}thr[i]\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (D  0  THENA  Auto)
  THEN  SplitAndHyps
  THEN  Repeat  (((\mbackslash{}p.  BoolCase  (find\_splitter  (concl  p))  p  THENA  Auto)  THENL  [CompleteAuto;  Id]))
  THEN  Auto)

---

Home Index