|
1 theory Needham_Schroeder_Unguided_Attacker_Example |
|
2 imports Needham_Schroeder_Base |
|
3 begin |
|
4 |
|
5 inductive_set ns_public :: "event list set" |
|
6 where |
|
7 (*Initial trace is empty*) |
|
8 Nil: "[] \<in> ns_public" |
|
9 |
|
10 | Fake: "\<lbrakk>evs1 \<in> ns_public; X \<in> synth (analz (spies evs1)) \<rbrakk> |
|
11 \<Longrightarrow> Says Spy A X # evs1 \<in> ns_public" |
|
12 |
|
13 (*Alice initiates a protocol run, sending a nonce to Bob*) |
|
14 | NS1: "\<lbrakk>evs1 \<in> ns_public; Nonce NA \<notin> used evs1\<rbrakk> |
|
15 \<Longrightarrow> Says A B (Crypt (pubEK B) \<lbrace>Nonce NA, Agent A\<rbrace>) |
|
16 # evs1 \<in> ns_public" |
|
17 (*Bob responds to Alice's message with a further nonce*) |
|
18 | NS2: "\<lbrakk>evs2 \<in> ns_public; Nonce NB \<notin> used evs2; |
|
19 Says A' B (Crypt (pubEK B) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> set evs2\<rbrakk> |
|
20 \<Longrightarrow> Says B A (Crypt (pubEK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) |
|
21 # evs2 \<in> ns_public" |
|
22 |
|
23 (*Alice proves her existence by sending NB back to Bob.*) |
|
24 | NS3: "\<lbrakk>evs3 \<in> ns_public; |
|
25 Says A B (Crypt (pubEK B) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> set evs3; |
|
26 Says B' A (Crypt (pubEK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) \<in> set evs3\<rbrakk> |
|
27 \<Longrightarrow> Says A B (Crypt (pubEK B) (Nonce NB)) # evs3 \<in> ns_public" |
|
28 |
|
29 declare ListMem_iff[symmetric, code_pred_inline] |
|
30 |
|
31 lemmas [code_pred_intro] = ns_publicp.intros[folded synth'_def] |
|
32 |
|
33 code_pred [skip_proof] ns_publicp unfolding synth'_def by (rule ns_publicp.cases) fastforce+ |
|
34 thm ns_publicp.equation |
|
35 |
|
36 code_pred [generator_cps] ns_publicp . |
|
37 thm ns_publicp.generator_cps_equation |
|
38 |
|
39 |
|
40 lemma "ns_publicp evs ==> \<not> (Says Alice Bob (Crypt (pubEK Bob) (Nonce NB))) : set evs" |
|
41 quickcheck[smart_exhaustive, depth = 5, timeout = 200, expect = counterexample] |
|
42 (*quickcheck[narrowing, size = 6, timeout = 200, verbose, expect = no_counterexample]*) |
|
43 oops |
|
44 |
|
45 lemma |
|
46 "\<lbrakk>ns_publicp evs\<rbrakk> |
|
47 \<Longrightarrow> Says B A (Crypt (pubEK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) : set evs |
|
48 \<Longrightarrow> A \<noteq> Spy \<Longrightarrow> B \<noteq> Spy \<Longrightarrow> A \<noteq> B |
|
49 \<Longrightarrow> Nonce NB \<notin> analz (spies evs)" |
|
50 quickcheck[smart_exhaustive, depth = 6, timeout = 100, expect = no_counterexample] |
|
51 (*quickcheck[narrowing, size = 7, timeout = 200, expect = no_counterexample]*) |
|
52 oops |
|
53 |
|
54 section {* Proving the counterexample trace for validation *} |
|
55 |
|
56 lemma |
|
57 assumes "A = Alice" "B = Bob" "C = Spy" "NA = 0" "NB = 1" |
|
58 assumes "evs = |
|
59 [Says Alice Spy (Crypt (pubEK Spy) (Nonce 1)), |
|
60 Says Bob Alice (Crypt (pubEK Alice) {|Nonce 0, Nonce 1|}), |
|
61 Says Spy Bob (Crypt (pubEK Bob) {|Nonce 0, Agent Alice|}), |
|
62 Says Alice Spy (Crypt (pubEK Spy) {|Nonce 0, Agent Alice|})]" (is "_ = [?e3, ?e2, ?e1, ?e0]") |
|
63 shows "A \<noteq> Spy" "B \<noteq> Spy" "evs : ns_public" "Nonce NB : analz (knows Spy evs)" |
|
64 proof - |
|
65 from assms show "A \<noteq> Spy" by auto |
|
66 from assms show "B \<noteq> Spy" by auto |
|
67 have "[] : ns_public" by (rule Nil) |
|
68 then have first_step: "[?e0] : ns_public" |
|
69 proof (rule NS1) |
|
70 show "Nonce 0 ~: used []" by eval |
|
71 qed |
|
72 then have "[?e1, ?e0] : ns_public" |
|
73 proof (rule Fake) |
|
74 show "Crypt (pubEK Bob) {|Nonce 0, Agent Alice|} : synth (analz (knows Spy [?e0]))" |
|
75 by (intro synth.intros(2,3,4,1)) eval+ |
|
76 qed |
|
77 then have "[?e2, ?e1, ?e0] : ns_public" |
|
78 proof (rule NS2) |
|
79 show "Says Spy Bob (Crypt (pubEK Bob) {|Nonce 0, Agent Alice|}) \<in> set [?e1, ?e0]" by simp |
|
80 show " Nonce 1 ~: used [?e1, ?e0]" by eval |
|
81 qed |
|
82 then show "evs : ns_public" |
|
83 unfolding assms |
|
84 proof (rule NS3) |
|
85 show " Says Alice Spy (Crypt (pubEK Spy) {|Nonce 0, Agent Alice|}) \<in> set [?e2, ?e1, ?e0]" by simp |
|
86 show "Says Bob Alice (Crypt (pubEK Alice) {|Nonce 0, Nonce 1|}) : set [?e2, ?e1, ?e0]" by simp |
|
87 qed |
|
88 from assms show "Nonce NB : analz (knows Spy evs)" |
|
89 apply simp |
|
90 apply (rule analz.intros(4)) |
|
91 apply (rule analz.intros(1)) |
|
92 apply (auto simp add: bad_def) |
|
93 done |
|
94 qed |
|
95 |
|
96 end |