Proof of Nuprl Lemma : ses-is-protocol-action-used

Step * of Lemma ses-is-protocol-action-used

∀[s:SES]

  ∀[pa:ProtocolAction]. ∀[es:EO+(Info)]. ∀[e:E].  UsedAtoms(e) = pa-used(pa) ∈ (Atom1 List) supposing pa(e)

  supposing ActionsDisjoint
BY
{ (RepeatFor 5 ((D 0 THENA Auto))
   THEN Unfold `ses-is-protocol-action` 0
   THEN D -3
   THEN RepUR ``pa-used ses-used-atoms`` 0⋅
   THEN (MoveToConcl (-3)
         THEN Unfold `ses-disjoint` 2
         THEN (InstHyp [⌈es⌉] 2⋅ THENA Auto)
         THEN Thin 2
         THEN D -1
         THEN (InstHyp  [⌈e⌉] (-1)⋅ THENA Auto)
         THEN Thin (-2)
         THEN SplitAndHyps
         THEN let tac = ((HypSubst' (-1) 0 THEN Reduce 0)
                         THEN (D 0 THENA Auto)
                         THEN (D 0 THENA Auto)
                         THEN D (-1)⋅
                         THEN ThinTrivial
                         THEN SplitAndHyps

                         THEN Repeat (((AutoSplit⋅ THENA Auto) THEN ThinTrivial THEN Auto))

                         THEN ((RepUR ``ses-signed ses-verify-sig ses-verify-signed ses-cipher`` 0

                                THEN RepUR ``ses-encryption-key  ses-decryption-key ses-encrypted`` 0

)
THEN Auto

                               THEN AutoSplit)⋅) in (((Decide n = "new" ∈ Atom THENA Auto) THENL [tac; Id])

                                                     THEN ((Decide n = "send" ∈ Atom THENA Auto) THENL [Try (tac); Id])

                                                     THEN ((Decide n = "rcv" ∈ Atom THENA Auto) THENL [tac; Id])

                                                     THEN ((Decide n = "sign" ∈ Atom THENA Auto) THENL [tac; Id])

                                                     THEN ((Decide n = "verify" ∈ Atom THENA Auto) THENL [tac; Id])

                                                     THEN ((Decide n = "encrypt" ∈ Atom THENA Auto) THENL [tac; Id])

                                                     THEN ((Decide n = "decrypt" ∈ Atom THENA Auto) THENL [tac; Id]))⋅)

   ⋅) }

1
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 Send then sdata-atoms(Send(e))
    if e ∈_b Sign then sdata-atoms(signed(e))
    if e ∈_b Verify then [signature(e) / sdata-atoms(signed(e))]
    if e ∈_b Encrypt then sdata-atoms(plainText(e)) @ encryption-key-atoms(key(e))
    if e ∈_b Decrypt then [cipherText(e) / encryption-key-atoms(key(e))]
    else []
    fi
    = if n =a "send" then sdata-atoms(p1)
      if n =a "encrypt" then sdata-atoms(fst(p1)) @ encryption-key-atoms(fst(snd(p1)))
      if n =a "sign" then sdata-atoms(fst(p1))
      if n =a "verify" then [snd(snd(p1)) / sdata-atoms(fst(p1))]
      if n =a "decrypt" then [snd(snd(p1)) / encryption-key-atoms(fst(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

Latex:

Latex:
\mforall{}[s:SES] \mforall{}[pa:ProtocolAction]. \mforall{}[es:EO+(Info)]. \mforall{}[e:E]. UsedAtoms(e) = pa-used(pa) supposing pa(e) supposing ActionsDisjoint By Latex: (RepeatFor 5 ((D 0 THENA Auto)) THEN Unfold `ses-is-protocol-action` 0 THEN D -3 THEN RepUR ``pa-used ses-used-atoms`` 0\mcdot{} THEN (MoveToConcl (-3) THEN Unfold `ses-disjoint` 2 THEN (InstHyp [\mkleeneopen{}es\mkleeneclose{}] 2\mcdot{} THENA Auto) THEN Thin 2 THEN D -1 THEN (InstHyp [\mkleeneopen{}e\mkleeneclose{}] (-1)\mcdot{} THENA Auto) THEN Thin (-2) THEN SplitAndHyps THEN let tac = ((HypSubst' (-1) 0 THEN Reduce 0) THEN (D 0 THENA Auto) THEN (D 0 THENA Auto) THEN D (-1)\mcdot{} THEN ThinTrivial THEN SplitAndHyps THEN Repeat (((AutoSplit\mcdot{} THENA Auto) THEN ThinTrivial THEN Auto)) THEN ((RepUR ``ses-signed ses-verify-sig ses-verify-signed ses-cipher`` 0 THEN RepUR ``ses-encryption-key ses-decryption-key ses-encrypted`` 0 ) THEN Auto THEN AutoSplit)\mcdot{}) in (((Decide n = "new" THENA Auto) THENL [tac; Id]) THEN ((Decide n = "send" THENA Auto) THENL [Try (tac); Id] ) THEN ((Decide n = "rcv" THENA Auto) THENL [tac; Id] ) THEN ((Decide n = "sign" THENA Auto) THENL [tac; Id] ) THEN ((Decide n = "verify" THENA Auto) THENL [tac; Id] ) THEN ((Decide n = "encrypt" THENA Auto) THENL [tac; Id] ) THEN ((Decide n = "decrypt" THENA Auto) THENL [tac; Id] ))\mcdot{})\mcdot{}) Home Index