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

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

∀[s:SES]

  ∀[pa:ProtocolAction]. ∀[es:EO+(Info)]. ∀[e:E].  UseableAtoms(e) = pa-useable(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-useable ses-useable-atoms`` 0⋅
   THEN (MoveToConcl (-3)
         THEN Unfold `ses-disjoint` 2

         THEN (((InstHyp [⌜es⌝] 2⋅ THENM (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-sig ses-decrypted ses-crypt`` 0
THEN Auto

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

                                             THEN ((Decide n = "send" ∈ Atom THENA Auto) THENL [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 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

Latex:

Latex:
\mforall{}[s:SES] \mforall{}[pa:ProtocolAction]. \mforall{}[es:EO+(Info)]. \mforall{}[e:E]. UseableAtoms(e) = pa-useable(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-useable ses-useable-atoms`` 0\mcdot{} THEN (MoveToConcl (-3) THEN Unfold `ses-disjoint` 2 THEN (((InstHyp [\mkleeneopen{}es\mkleeneclose{}] 2\mcdot{} THENM (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 THENA Auto) THEN ThinTrivial THEN Auto)) THEN RepUR ``ses-sig ses-decrypted ses-crypt`` 0 THEN Auto THEN AutoSplit) in (((Decide n = "new" THENA Auto) THENL [tac; Id]) THEN ((Decide n = "send" THENA Auto) THENL [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