Theory NS_Public_Bad_GA

section‹The Needham-Schroeder Public-Key Protocol against the General Attacker›

theory NS_Public_Bad_GA imports PublicGA begin

inductive_set ns_public :: "event list set"
  where

   Nil:  "[] ∈ ns_public"

 | Fake: "⟦evsf ∈ ns_public;  X ∈ synth (analz (knows A evsf))⟧
          ⟹ Says A B X  # evsf ∈ ns_public"

 | Reception: "⟦ evsr ∈ ns_public; Says A B X ∈ set evsr ⟧
                ⟹ Gets B X # evsr ∈ ns_public"

 | NS1:  "⟦evs1 ∈ ns_public;  Nonce NA ∉ used evs1⟧
          ⟹ Says A B (Crypt (pubEK B) ⦃Nonce NA, Agent A⦄)
                # evs1  ∈  ns_public"

 | NS2:  "⟦evs2 ∈ ns_public;  Nonce NB ∉ used evs2;
           Gets B (Crypt (pubEK B) ⦃Nonce NA, Agent A⦄) ∈ set evs2⟧
          ⟹ Says B A (Crypt (pubEK A) ⦃Nonce NA, Nonce NB⦄)
                # evs2  ∈  ns_public"

 | NS3:  "⟦evs3 ∈ ns_public;
           Says A  B (Crypt (pubEK B) ⦃Nonce NA, Agent A⦄) ∈ set evs3;
           Gets A (Crypt (pubEK A) ⦃Nonce NA, Nonce NB⦄) ∈ set evs3⟧
          ⟹ Says A B (Crypt (pubEK B) (Nonce NB)) # evs3 ∈ ns_public"


lemma NS_no_Notes:
 "evs ∈ ns_public ⟹ Notes A X ∉ set evs"
apply (erule ns_public.induct)
apply (simp_all)
done

text‹Confidentiality treatment in separate theory file›

end