Theory Needham_Schroeder_Guided_Attacker_Example

theory Needham_Schroeder_Guided_Attacker_Example
imports Needham_Schroeder_Base
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) \<lbrace>Nonce NA, Agent A\<rbrace>)
# evs1 ∈ ns_public"

| Fake_NS2: "[|evs1 ∈ ns_public; Nonce NA ∈ analz (spies evs1); Nonce NB ∈ analz (spies evs1) |]
==> Says Spy A (Crypt (pubEK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>)
# 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) \<lbrace>Nonce NA, Agent A\<rbrace>)
# 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) \<lbrace>Nonce NA, Agent A\<rbrace>) ∈ set evs2|]
==> Says B A (Crypt (pubEK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>)
# evs2 ∈ ns_public"


(*Alice proves her existence by sending NB back to Bob.*)
| NS3: "[|evs3 ∈ ns_public;
Says A B (Crypt (pubEK B) \<lbrace>Nonce NA, Agent A\<rbrace>) ∈ set evs3;
Says B' A (Crypt (pubEK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) ∈ 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) \<lbrace>Nonce NA, Nonce NB\<rbrace>) : 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