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