---

Step * 1 of Lemma ses-is-protocol-action-useable


1. s : SES
2. n : Atom
3. es : EO+(Info)
4. e : E
5. f : E ─→ ℤ
6. (↑e ∈b New) ⇒ ((f e) = 1 ∈ ℤ)
7. (↑e ∈b Send) ⇒ ((f e) = 2 ∈ ℤ)
8. (↑e ∈b Rcv) ⇒ ((f e) = 3 ∈ ℤ)
9. (↑e ∈b Sign) ⇒ ((f e) = 4 ∈ ℤ)
10. (↑e ∈b Verify) ⇒ ((f e) = 5 ∈ ℤ)
11. (↑e ∈b Encrypt) ⇒ ((f e) = 6 ∈ ℤ)
12. (↑e ∈b Decrypt) ⇒ ((f e) = 7 ∈ ℤ)
13. ¬(n = "new" ∈ Atom)
14. ¬(n = "send" ∈ Atom)
15. ¬(n = "rcv" ∈ Atom)
16. ¬(n = "sign" ∈ Atom)
17. ¬(n = "verify" ∈ Atom)
18. ¬(n = "encrypt" ∈ Atom)
19. ¬(n = "decrypt" ∈ Atom)
⊢ ∀p1: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 
    if e ∈b Rcv then sdata-atoms(Rcv(e))
    if e ∈b Sign then [signature(e)]
    if e ∈b Encrypt then [cipherText(e)]
    if e ∈b Decrypt then sdata-atoms(plainText(e))
    if e ∈b New then [New(e)]
    else []
    fi 
    = if n =a "new" then [p1]
      if n =a "rcv" then sdata-atoms(p1)
      if n =a "encrypt" then [snd(snd(p1))]
      if n =a "decrypt" then sdata-atoms(fst(p1))
      if n =a "sign" then [snd(snd(p1))]
      else []
      fi 
    ∈ (Atom1 List) 
    supposing if n =a "new" then (↑e ∈b New) ∧ (New(e) = p1 ∈ Atom1)
    if n =a "send" then (↑e ∈b Send) ∧ (Send(e) = p1 ∈ SecurityData)
    if n =a "rcv" then (↑e ∈b Rcv) ∧ (Rcv(e) = p1 ∈ SecurityData)
    if n =a "encrypt" then (↑e ∈b Encrypt) ∧ (Encrypt(e) = p1 ∈ (SecurityData × Key × Atom1))
    if n =a "decrypt" then (↑e ∈b Decrypt) ∧ (Decrypt(e) = p1 ∈ (SecurityData × Key × Atom1))
    if n =a "sign" then (↑e ∈b Sign) ∧ (Sign(e) = p1 ∈ (SecurityData × Id × Atom1))
    if n =a "verify" then (↑e ∈b Verify) ∧ (Verify(e) = p1 ∈ (SecurityData × Id × Atom1))
    else False
    fi 
BY
{ (Try ((RepeatFor 2 ((D 0 THENA Auto))
         THEN (Assert ⌈False⌉⋅ THEN Auto)
         THEN MoveToConcl (-1)
         THEN RepeatFor 7 (AutoSplit)))
   THEN Try (AutoSplit)
   )⋅ }

---

Latex:

---

Latex:

1.  s  :  SES
2.  n  :  Atom
3.  es  :  EO+(Info)
4.  e  :  E
5.  f  :  E  {}\mrightarrow{}  \mBbbZ{}
6.  (\muparrow{}e  \mmember{}\msubb{}  New)  {}\mRightarrow{}  ((f  e)  =  1)
7.  (\muparrow{}e  \mmember{}\msubb{}  Send)  {}\mRightarrow{}  ((f  e)  =  2)
8.  (\muparrow{}e  \mmember{}\msubb{}  Rcv)  {}\mRightarrow{}  ((f  e)  =  3)
9.  (\muparrow{}e  \mmember{}\msubb{}  Sign)  {}\mRightarrow{}  ((f  e)  =  4)
10.  (\muparrow{}e  \mmember{}\msubb{}  Verify)  {}\mRightarrow{}  ((f  e)  =  5)
11.  (\muparrow{}e  \mmember{}\msubb{}  Encrypt)  {}\mRightarrow{}  ((f  e)  =  6)
12.  (\muparrow{}e  \mmember{}\msubb{}  Decrypt)  {}\mRightarrow{}  ((f  e)  =  7)
13.  \mneg{}(n  =  "new")
14.  \mneg{}(n  =  "send")
15.  \mneg{}(n  =  "rcv")
16.  \mneg{}(n  =  "sign")
17.  \mneg{}(n  =  "verify")
18.  \mneg{}(n  =  "encrypt")
19.  \mneg{}(n  =  "decrypt")
\mvdash{}  \mforall{}p1: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 
        if  e  \mmember{}\msubb{}  Rcv  then  sdata-atoms(Rcv(e))
        if  e  \mmember{}\msubb{}  Sign  then  [signature(e)]
        if  e  \mmember{}\msubb{}  Encrypt  then  [cipherText(e)]
        if  e  \mmember{}\msubb{}  Decrypt  then  sdata-atoms(plainText(e))
        if  e  \mmember{}\msubb{}  New  then  [New(e)]
        else  []
        fi 
        =  if  n  =a  "new"  then  [p1]
            if  n  =a  "rcv"  then  sdata-atoms(p1)
            if  n  =a  "encrypt"  then  [snd(snd(p1))]
            if  n  =a  "decrypt"  then  sdata-atoms(fst(p1))
            if  n  =a  "sign"  then  [snd(snd(p1))]
            else  []
            fi   
        supposing  if  n  =a  "new"  then  (\muparrow{}e  \mmember{}\msubb{}  New)  \mwedge{}  (New(e)  =  p1)
        if  n  =a  "send"  then  (\muparrow{}e  \mmember{}\msubb{}  Send)  \mwedge{}  (Send(e)  =  p1)
        if  n  =a  "rcv"  then  (\muparrow{}e  \mmember{}\msubb{}  Rcv)  \mwedge{}  (Rcv(e)  =  p1)
        if  n  =a  "encrypt"  then  (\muparrow{}e  \mmember{}\msubb{}  Encrypt)  \mwedge{}  (Encrypt(e)  =  p1)
        if  n  =a  "decrypt"  then  (\muparrow{}e  \mmember{}\msubb{}  Decrypt)  \mwedge{}  (Decrypt(e)  =  p1)
        if  n  =a  "sign"  then  (\muparrow{}e  \mmember{}\msubb{}  Sign)  \mwedge{}  (Sign(e)  =  p1)
        if  n  =a  "verify"  then  (\muparrow{}e  \mmember{}\msubb{}  Verify)  \mwedge{}  (Verify(e)  =  p1)
        else  False
        fi 


By

---

Latex:
(Try  ((RepeatFor  2  ((D  0  THENA  Auto))
              THEN  (Assert  \mkleeneopen{}False\mkleeneclose{}\mcdot{}  THEN  Auto)
              THEN  MoveToConcl  (-1)
              THEN  RepeatFor  7  (AutoSplit)))
  THEN  Try  (AutoSplit)
  )\mcdot{}

---

Home Index