author | paulson <lp15@cam.ac.uk> |
Fri, 14 Oct 2022 14:57:28 +0100 | |
changeset 76297 | e7f9e5b3a36a |
parent 76291 | 616405057951 |
child 76299 | 0ad6f6508274 |
permissions | -rw-r--r-- |
37936 | 1 |
(* Title: HOL/Auth/NS_Public_Bad.thy |
2318 | 2 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
3 |
Copyright 1996 University of Cambridge |
|
4 |
*) |
|
5 |
||
61830 | 6 |
section\<open>Verifying the Needham-Schroeder Public-Key Protocol\<close> |
13956 | 7 |
|
76297 | 8 |
text \<open>Flawed version, vulnerable to Lowe's attack. |
9 |
From Burrows, Abadi and Needham. A Logic of Authentication. |
|
10 |
Proc. Royal Soc. 426 (1989), p. 260\<close> |
|
11 |
||
16417 | 12 |
theory NS_Public_Bad imports Public begin |
2318 | 13 |
|
23746 | 14 |
inductive_set ns_public :: "event list set" |
15 |
where |
|
76297 | 16 |
Nil: "[] \<in> ns_public" |
17 |
\<comment> \<open>Initial trace is empty\<close> |
|
23746 | 18 |
| Fake: "\<lbrakk>evsf \<in> ns_public; X \<in> synth (analz (spies evsf))\<rbrakk> |
11366 | 19 |
\<Longrightarrow> Says Spy B X # evsf \<in> ns_public" |
76297 | 20 |
\<comment> \<open>The spy can say almost anything.\<close> |
23746 | 21 |
| NS1: "\<lbrakk>evs1 \<in> ns_public; Nonce NA \<notin> used evs1\<rbrakk> |
13922 | 22 |
\<Longrightarrow> Says A B (Crypt (pubEK B) \<lbrace>Nonce NA, Agent A\<rbrace>) |
11104 | 23 |
# evs1 \<in> ns_public" |
76297 | 24 |
\<comment> \<open>Alice initiates a protocol run, sending a nonce to Bob\<close> |
23746 | 25 |
| NS2: "\<lbrakk>evs2 \<in> ns_public; Nonce NB \<notin> used evs2; |
13922 | 26 |
Says A' B (Crypt (pubEK B) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> set evs2\<rbrakk> |
27 |
\<Longrightarrow> Says B A (Crypt (pubEK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) |
|
11104 | 28 |
# evs2 \<in> ns_public" |
76297 | 29 |
\<comment> \<open>Bob responds to Alice's message with a further nonce\<close> |
23746 | 30 |
| NS3: "\<lbrakk>evs3 \<in> ns_public; |
13922 | 31 |
Says A B (Crypt (pubEK B) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> set evs3; |
32 |
Says B' A (Crypt (pubEK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) \<in> set evs3\<rbrakk> |
|
33 |
\<Longrightarrow> Says A B (Crypt (pubEK B) (Nonce NB)) # evs3 \<in> ns_public" |
|
76297 | 34 |
\<comment> \<open>Alice proves her existence by sending @{term NB} back to Bob.\<close> |
11104 | 35 |
|
36 |
declare knows_Spy_partsEs [elim] |
|
14200
d8598e24f8fa
Removal of the Key_supply axiom (affects many possbility proofs) and minor
paulson
parents:
13956
diff
changeset
|
37 |
declare analz_into_parts [dest] |
56681 | 38 |
declare Fake_parts_insert_in_Un [dest] |
11104 | 39 |
|
76297 | 40 |
text \<open>A "possibility property": there are traces that reach the end\<close> |
13922 | 41 |
lemma "\<exists>NB. \<exists>evs \<in> ns_public. Says A B (Crypt (pubEK B) (Nonce NB)) \<in> set evs" |
76297 | 42 |
apply (intro exI bexI) |
43 |
apply (rule_tac [2] ns_public.Nil [THEN ns_public.NS1, THEN ns_public.NS2, THEN ns_public.NS3]) |
|
44 |
by possibility |
|
11104 | 45 |
|
46 |
||
76297 | 47 |
subsection \<open>Inductive proofs about @{term ns_public}\<close> |
11104 | 48 |
|
49 |
(** Theorems of the form X \<notin> parts (spies evs) imply that NOBODY |
|
50 |
sends messages containing X! **) |
|
51 |
||
76297 | 52 |
text \<open>Spy never sees another agent's private key! (unless it's bad at start)\<close> |
13922 | 53 |
lemma Spy_see_priEK [simp]: |
76297 | 54 |
"evs \<in> ns_public \<Longrightarrow> (Key (priEK A) \<in> parts (spies evs)) = (A \<in> bad)" |
55 |
by (erule ns_public.induct, auto) |
|
11104 | 56 |
|
13922 | 57 |
lemma Spy_analz_priEK [simp]: |
76297 | 58 |
"evs \<in> ns_public \<Longrightarrow> (Key (priEK A) \<in> analz (spies evs)) = (A \<in> bad)" |
59 |
by auto |
|
11104 | 60 |
|
61 |
||
76297 | 62 |
subsection \<open>Authenticity properties obtained from {term NS1}\<close> |
11104 | 63 |
|
76297 | 64 |
text \<open>It is impossible to re-use a nonce in both {term NS1} and {term NS2}, provided the nonce |
65 |
is secret. (Honest users generate fresh nonces.)\<close> |
|
11104 | 66 |
lemma no_nonce_NS1_NS2 [rule_format]: |
67 |
"evs \<in> ns_public |
|
13922 | 68 |
\<Longrightarrow> Crypt (pubEK C) \<lbrace>NA', Nonce NA\<rbrace> \<in> parts (spies evs) \<longrightarrow> |
69 |
Crypt (pubEK B) \<lbrace>Nonce NA, Agent A\<rbrace> \<in> parts (spies evs) \<longrightarrow> |
|
11104 | 70 |
Nonce NA \<in> analz (spies evs)" |
76291
616405057951
Trying to clean up some messy proofs
paulson <lp15@cam.ac.uk>
parents:
61830
diff
changeset
|
71 |
by (induct rule: ns_public.induct) (auto intro: analz_insertI) |
11104 | 72 |
|
73 |
||
76297 | 74 |
text \<open>Unicity for {term NS1}: nonce {term NA} identifies agents {term A} and {term B}\<close> |
11104 | 75 |
lemma unique_NA: |
76297 | 76 |
assumes NA: "Crypt(pubEK B) \<lbrace>Nonce NA, Agent A \<rbrace> \<in> parts(spies evs)" |
77 |
"Crypt(pubEK B') \<lbrace>Nonce NA, Agent A'\<rbrace> \<in> parts(spies evs)" |
|
78 |
"Nonce NA \<notin> analz (spies evs)" |
|
79 |
and evs: "evs \<in> ns_public" |
|
80 |
shows "A=A' \<and> B=B'" |
|
81 |
using evs NA |
|
82 |
by (induction rule: ns_public.induct) (auto intro!: analz_insertI split: if_split_asm) |
|
11104 | 83 |
|
84 |
||
76297 | 85 |
text \<open>Secrecy: Spy does not see the nonce sent in msg {term NS1} if {term A} and {term B} are secure |
86 |
The major premise "Says A B ..." makes it a dest-rule, hence the given assumption order. \<close> |
|
11104 | 87 |
theorem Spy_not_see_NA: |
76297 | 88 |
assumes NA: "Says A B (Crypt(pubEK B) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> set evs" |
89 |
"A \<notin> bad" "B \<notin> bad" |
|
90 |
and evs: "evs \<in> ns_public" |
|
91 |
shows "Nonce NA \<notin> analz (spies evs)" |
|
92 |
using evs NA |
|
93 |
proof (induction rule: ns_public.induct) |
|
94 |
case (Fake evsf X B) |
|
95 |
then show ?case |
|
96 |
by spy_analz |
|
97 |
next |
|
98 |
case (NS2 evs2 NB A' B NA A) |
|
99 |
then show ?case |
|
100 |
by simp (metis Says_imp_analz_Spy analz_into_parts parts.simps unique_NA usedI) |
|
101 |
next |
|
102 |
case (NS3 evs3 A B NA B' NB) |
|
103 |
then show ?case |
|
104 |
by simp (meson Says_imp_analz_Spy analz_into_parts no_nonce_NS1_NS2) |
|
105 |
qed auto |
|
11104 | 106 |
|
107 |
||
76297 | 108 |
text \<open>Authentication for {term A}: if she receives message 2 and has used {term NA} |
109 |
to start a run, then {term B} has sent message 2.\<close> |
|
11104 | 110 |
lemma A_trusts_NS2_lemma [rule_format]: |
111 |
"\<lbrakk>A \<notin> bad; B \<notin> bad; evs \<in> ns_public\<rbrakk> |
|
13922 | 112 |
\<Longrightarrow> Crypt (pubEK A) \<lbrace>Nonce NA, Nonce NB\<rbrace> \<in> parts (spies evs) \<longrightarrow> |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
23746
diff
changeset
|
113 |
Says A B (Crypt(pubEK B) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> set evs \<longrightarrow> |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
23746
diff
changeset
|
114 |
Says B A (Crypt(pubEK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) \<in> set evs" |
76291
616405057951
Trying to clean up some messy proofs
paulson <lp15@cam.ac.uk>
parents:
61830
diff
changeset
|
115 |
by (erule ns_public.induct) (auto dest: Spy_not_see_NA unique_NA) |
11104 | 116 |
|
117 |
theorem A_trusts_NS2: |
|
13922 | 118 |
"\<lbrakk>Says A B (Crypt(pubEK B) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> set evs; |
119 |
Says B' A (Crypt(pubEK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) \<in> set evs; |
|
11104 | 120 |
A \<notin> bad; B \<notin> bad; evs \<in> ns_public\<rbrakk> |
13922 | 121 |
\<Longrightarrow> Says B A (Crypt(pubEK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) \<in> set evs" |
76297 | 122 |
by (blast intro: A_trusts_NS2_lemma) |
11104 | 123 |
|
2318 | 124 |
|
76297 | 125 |
text \<open>If the encrypted message appears then it originated with Alice in {term NS1}\<close> |
11104 | 126 |
lemma B_trusts_NS1 [rule_format]: |
127 |
"evs \<in> ns_public |
|
13922 | 128 |
\<Longrightarrow> Crypt (pubEK B) \<lbrace>Nonce NA, Agent A\<rbrace> \<in> parts (spies evs) \<longrightarrow> |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
23746
diff
changeset
|
129 |
Nonce NA \<notin> analz (spies evs) \<longrightarrow> |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
23746
diff
changeset
|
130 |
Says A B (Crypt (pubEK B) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> set evs" |
76291
616405057951
Trying to clean up some messy proofs
paulson <lp15@cam.ac.uk>
parents:
61830
diff
changeset
|
131 |
by (induction evs rule: ns_public.induct) (use analz_insertI in auto) |
11104 | 132 |
|
133 |
||
76297 | 134 |
subsection \<open>Authenticity properties obtained from {term NS2}\<close> |
11104 | 135 |
|
76297 | 136 |
text \<open>Unicity for {term NS2}: nonce {term NB} identifies nonce {term NA} and agent {term A} |
137 |
[proof closely follows that for @{thm [source] unique_NA}]\<close> |
|
138 |
||
11104 | 139 |
lemma unique_NB [dest]: |
76297 | 140 |
assumes NB: "Crypt(pubEK A) \<lbrace>Nonce NA, Nonce NB\<rbrace> \<in> parts(spies evs)" |
141 |
"Crypt(pubEK A') \<lbrace>Nonce NA', Nonce NB\<rbrace> \<in> parts(spies evs)" |
|
142 |
"Nonce NB \<notin> analz (spies evs)" |
|
143 |
and evs: "evs \<in> ns_public" |
|
144 |
shows "A=A' \<and> NA=NA'" |
|
145 |
using evs NB |
|
146 |
by (induction rule: ns_public.induct) (auto intro!: analz_insertI split: if_split_asm) |
|
11104 | 147 |
|
148 |
||
76297 | 149 |
text \<open>{term NB} remains secret \emph{provided} Alice never responds with round 3\<close> |
11104 | 150 |
theorem Spy_not_see_NB [dest]: |
76297 | 151 |
assumes NB: "Says B A (Crypt (pubEK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) \<in> set evs" |
152 |
"\<forall>C. Says A C (Crypt (pubEK C) (Nonce NB)) \<notin> set evs" |
|
153 |
"A \<notin> bad" "B \<notin> bad" |
|
154 |
and evs: "evs \<in> ns_public" |
|
155 |
shows "Nonce NB \<notin> analz (spies evs)" |
|
156 |
using evs NB evs |
|
157 |
proof (induction rule: ns_public.induct) |
|
158 |
case Fake |
|
159 |
then show ?case by spy_analz |
|
160 |
next |
|
161 |
case NS2 |
|
162 |
then show ?case |
|
163 |
by (auto intro!: no_nonce_NS1_NS2) |
|
164 |
qed auto |
|
11104 | 165 |
|
166 |
||
76297 | 167 |
text \<open>Authentication for {term B}: if he receives message 3 and has used {term NB} |
168 |
in message 2, then {term A} has sent message 3 (to somebody) \<close> |
|
11104 | 169 |
lemma B_trusts_NS3_lemma [rule_format]: |
76297 | 170 |
"\<lbrakk>evs \<in> ns_public; |
171 |
Crypt (pubEK B) (Nonce NB) \<in> parts (spies evs); |
|
172 |
Says B A (Crypt (pubEK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) \<in> set evs; |
|
173 |
A \<notin> bad; B \<notin> bad\<rbrakk> |
|
174 |
\<Longrightarrow> \<exists>C. Says A C (Crypt (pubEK C) (Nonce NB)) \<in> set evs" |
|
175 |
proof (induction rule: ns_public.induct) |
|
176 |
case (NS3 evs3 A B NA B' NB) |
|
177 |
then show ?case |
|
178 |
by simp (blast intro: no_nonce_NS1_NS2) |
|
179 |
qed auto |
|
11104 | 180 |
|
181 |
theorem B_trusts_NS3: |
|
13922 | 182 |
"\<lbrakk>Says B A (Crypt (pubEK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) \<in> set evs; |
183 |
Says A' B (Crypt (pubEK B) (Nonce NB)) \<in> set evs; |
|
11104 | 184 |
A \<notin> bad; B \<notin> bad; evs \<in> ns_public\<rbrakk> |
13922 | 185 |
\<Longrightarrow> \<exists>C. Says A C (Crypt (pubEK C) (Nonce NB)) \<in> set evs" |
76297 | 186 |
by (blast intro: B_trusts_NS3_lemma) |
11104 | 187 |
|
188 |
||
76297 | 189 |
text \<open>Can we strengthen the secrecy theorem @{thm[source]Spy_not_see_NB}? NO\<close> |
190 |
lemma "\<lbrakk>evs \<in> ns_public; |
|
191 |
Says B A (Crypt (pubEK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) \<in> set evs; |
|
192 |
A \<notin> bad; B \<notin> bad\<rbrakk> |
|
193 |
\<Longrightarrow> Nonce NB \<notin> analz (spies evs)" |
|
194 |
apply (induction rule: ns_public.induct, simp_all, spy_analz) |
|
195 |
(*{term NS1}: by freshness*) |
|
11150 | 196 |
apply blast |
76297 | 197 |
(*{term NS2}: by freshness and unicity of {term NB}*) |
11104 | 198 |
apply (blast intro: no_nonce_NS1_NS2) |
76297 | 199 |
(*{term NS3}: unicity of {term NB} identifies {term A} and {term NA}, but not {term B}*) |
11104 | 200 |
apply clarify |
13507 | 201 |
apply (frule_tac A' = A in |
202 |
Says_imp_knows_Spy [THEN parts.Inj, THEN unique_NB], auto) |
|
38964 | 203 |
apply (rename_tac evs3 B' C) |
61830 | 204 |
txt\<open>This is the attack! |
14200
d8598e24f8fa
Removal of the Key_supply axiom (affects many possbility proofs) and minor
paulson
parents:
13956
diff
changeset
|
205 |
@{subgoals[display,indent=0,margin=65]} |
61830 | 206 |
\<close> |
11104 | 207 |
oops |
208 |
||
209 |
(* |
|
210 |
THIS IS THE ATTACK! |
|
211 |
Level 8 |
|
212 |
!!evs. \<lbrakk>A \<notin> bad; B \<notin> bad; evs \<in> ns_public\<rbrakk> |
|
13922 | 213 |
\<Longrightarrow> Says B A (Crypt (pubEK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) \<in> set evs \<longrightarrow> |
11104 | 214 |
Nonce NB \<notin> analz (spies evs) |
215 |
1. !!C B' evs3. |
|
216 |
\<lbrakk>A \<notin> bad; B \<notin> bad; evs3 \<in> ns_public |
|
13922 | 217 |
Says A C (Crypt (pubEK C) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> set evs3; |
218 |
Says B' A (Crypt (pubEK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) \<in> set evs3; |
|
11104 | 219 |
C \<in> bad; |
13922 | 220 |
Says B A (Crypt (pubEK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) \<in> set evs3; |
11104 | 221 |
Nonce NB \<notin> analz (spies evs3)\<rbrakk> |
222 |
\<Longrightarrow> False |
|
223 |
*) |
|
2318 | 224 |
|
225 |
end |