Theory Needham_Schroeder_Guided_Attacker_Example

theory Needham_Schroeder_Guided_Attacker_Example
imports Needham_Schroeder_Base
begin

inductive_set ns_public :: "event list set"
  where
         (*Initial trace is empty*)
   Nil:  "[]  ns_public"

 | Fake_NS1:  "evs1  ns_public; Nonce NA  analz (spies evs1) 
           Says Spy B (Crypt (pubEK B) Nonce NA, Agent A)
                # evs1   ns_public"
 | Fake_NS2:  "evs1  ns_public; Nonce NA  analz (spies evs1); Nonce NB  analz (spies evs1) 
           Says Spy A (Crypt (pubEK A) Nonce NA, Nonce NB)
                # evs1   ns_public"

         (*Alice initiates a protocol run, sending a nonce to Bob*)
 | NS1:  "evs1  ns_public;  Nonce NA  used evs1
           Says A B (Crypt (pubEK B) Nonce NA, Agent A)
                # evs1    ns_public"
         (*Bob responds to Alice's message with a further nonce*)
 | NS2:  "evs2  ns_public;  Nonce NB  used evs2;
           Says A' B (Crypt (pubEK B) Nonce NA, Agent A)  set evs2
           Says B A (Crypt (pubEK A) Nonce NA, Nonce NB)
                # evs2    ns_public"

         (*Alice proves her existence by sending NB back to Bob.*)
 | NS3:  "evs3  ns_public;
           Says A  B (Crypt (pubEK B) Nonce NA, Agent A)  set evs3;
           Says B' A (Crypt (pubEK A) Nonce NA, Nonce NB)  set evs3
           Says A B (Crypt (pubEK B) (Nonce NB)) # evs3  ns_public"

declare ListMem_iff[symmetric, code_pred_inline]

lemmas [code_pred_intro] = ns_publicp.intros[folded synth'_def]

code_pred [skip_proof] ns_publicp unfolding synth'_def by (rule ns_publicp.cases) fastforce+
thm ns_publicp.equation

code_pred [generator_cps] ns_publicp .
thm ns_publicp.generator_cps_equation


lemma "ns_publicp evs ==> ¬ (Says Alice Bob (Crypt (pubEK Bob) (Nonce NB))) : set evs"
quickcheck[smart_exhaustive, depth = 5, timeout = 100, expect = counterexample]
(*quickcheck[narrowing, size = 6, timeout = 200, verbose, expect = no_counterexample]*)
oops

lemma
  "ns_publicp evs            
        Says B A (Crypt (pubEK A) Nonce NA, Nonce NB) : set evs
        A  Spy  B  Spy  A  B 
            Nonce NB  analz (spies evs)"
(*quickcheck[smart_exhaustive, depth = 6, timeout = 100, expect = counterexample]
quickcheck[narrowing, size = 7, timeout = 200, expect = no_counterexample]*)
oops

section ‹Proving the counterexample trace for validation›

lemma
  assumes "A = Alice" "B = Bob" "C = Spy" "NA = 0" "NB = 1"
  assumes "evs = 
  [Says Alice Spy (Crypt (pubEK Spy) (Nonce 1)),
   Says Bob Alice (Crypt (pubEK Alice) Nonce 0, Nonce 1),
   Says Spy Bob (Crypt (pubEK Bob) Nonce 0, Agent Alice),
   Says Alice Spy (Crypt (pubEK Spy) Nonce 0, Agent Alice)]" (is "_ = [?e3, ?e2, ?e1, ?e0]")
  shows "A  Spy" "B  Spy" "evs : ns_public" "Nonce NB : analz (knows Spy evs)"
proof -
  from assms show "A  Spy" by auto
  from assms show "B  Spy" by auto
  have "[] : ns_public" by (rule Nil)
  then have first_step: "[?e0] : ns_public"
  proof (rule NS1)
    show "Nonce 0 ~: used []" by eval
  qed
  then have "[?e1, ?e0] : ns_public"
  proof (rule Fake_NS1)
    show "Nonce 0 : analz (knows Spy [?e0])" by eval
  qed
  then have "[?e2, ?e1, ?e0] : ns_public"
  proof (rule NS2)
    show "Says Spy Bob (Crypt (pubEK Bob) Nonce 0, Agent Alice)  set [?e1, ?e0]" by simp
    show " Nonce 1 ~: used [?e1, ?e0]" by eval
  qed
  then show "evs : ns_public"
  unfolding assms
  proof (rule NS3)
    show "  Says Alice Spy (Crypt (pubEK Spy) Nonce 0, Agent Alice)  set [?e2, ?e1, ?e0]" by simp
    show "Says Bob Alice (Crypt (pubEK Alice) Nonce 0, Nonce 1)
    : set [?e2, ?e1, ?e0]" by simp
  qed
  from assms show "Nonce NB : analz (knows Spy evs)"
    apply simp
    apply (rule analz.intros(4))
    apply (rule analz.intros(1))
    apply (auto simp add: bad_def)
    done
qed

end