Theory Needham_Schroeder_Unguided_Attacker_Example

theory Needham_Schroeder_Unguided_Attacker_Example
imports Needham_Schroeder_Base
begin

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

 | Fake:  "⟦evs1 ∈ ns_public; X ∈ synth (analz (spies evs1)) ⟧
          ⟹ Says Spy A X # 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 = 200, 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 = no_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)
    show "Crypt (pubEK Bob) ⦃Nonce 0, Agent Alice⦄ : synth (analz (knows Spy [?e0]))"
      by (intro synth.intros(2,3,4,1)) 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