author | wenzelm |
Fri, 18 Aug 2017 20:47:47 +0200 | |
changeset 66453 | cc19f7ca2ed6 |
parent 63146 | f1ecba0272f9 |
child 67613 | ce654b0e6d69 |
permissions | -rw-r--r-- |
37936 | 1 |
(* Title: HOL/UNITY/Simple/NSP_Bad.thy |
11195
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
2 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
3 |
Copyright 1996 University of Cambridge |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
4 |
|
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
5 |
Original file is ../Auth/NS_Public_Bad |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
6 |
*) |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
7 |
|
63146 | 8 |
section\<open>Analyzing the Needham-Schroeder Public-Key Protocol in UNITY\<close> |
14203 | 9 |
|
66453
cc19f7ca2ed6
session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks' -a;
wenzelm
parents:
63146
diff
changeset
|
10 |
theory NSP_Bad imports "HOL-Auth.Public" "../UNITY_Main" begin |
11195
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
11 |
|
63146 | 12 |
text\<open>This is the flawed version, vulnerable to Lowe's attack. |
14203 | 13 |
From page 260 of |
14 |
Burrows, Abadi and Needham. A Logic of Authentication. |
|
15 |
Proc. Royal Soc. 426 (1989). |
|
63146 | 16 |
\<close> |
14203 | 17 |
|
42463 | 18 |
type_synonym state = "event list" |
11195
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
19 |
|
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
20 |
(*The spy MAY say anything he CAN say. We do not expect him to |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
21 |
invent new nonces here, but he can also use NS1. Common to |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
22 |
all similar protocols.*) |
36866 | 23 |
definition |
11195
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
24 |
Fake :: "(state*state) set" |
36866 | 25 |
where "Fake = {(s,s'). |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32149
diff
changeset
|
26 |
\<exists>B X. s' = Says Spy B X # s |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32149
diff
changeset
|
27 |
& X \<in> synth (analz (spies s))}" |
14203 | 28 |
|
11195
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
29 |
(*The numeric suffixes on A identify the rule*) |
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
30 |
|
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
31 |
(*Alice initiates a protocol run, sending a nonce to Bob*) |
36866 | 32 |
definition |
11195
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
33 |
NS1 :: "(state*state) set" |
36866 | 34 |
where "NS1 = {(s1,s'). |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32149
diff
changeset
|
35 |
\<exists>A1 B NA. |
61956 | 36 |
s' = Says A1 B (Crypt (pubK B) \<lbrace>Nonce NA, Agent A1\<rbrace>) # s1 |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32149
diff
changeset
|
37 |
& Nonce NA \<notin> used s1}" |
14203 | 38 |
|
11195
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
39 |
(*Bob responds to Alice's message with a further nonce*) |
36866 | 40 |
definition |
11195
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
41 |
NS2 :: "(state*state) set" |
36866 | 42 |
where "NS2 = {(s2,s'). |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32149
diff
changeset
|
43 |
\<exists>A' A2 B NA NB. |
61956 | 44 |
s' = Says B A2 (Crypt (pubK A2) \<lbrace>Nonce NA, Nonce NB\<rbrace>) # s2 |
45 |
& Says A' B (Crypt (pubK B) \<lbrace>Nonce NA, Agent A2\<rbrace>) \<in> set s2 |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32149
diff
changeset
|
46 |
& Nonce NB \<notin> used s2}" |
14203 | 47 |
|
11195
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
48 |
(*Alice proves her existence by sending NB back to Bob.*) |
36866 | 49 |
definition |
11195
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
50 |
NS3 :: "(state*state) set" |
36866 | 51 |
where "NS3 = {(s3,s'). |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32149
diff
changeset
|
52 |
\<exists>A3 B' B NA NB. |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32149
diff
changeset
|
53 |
s' = Says A3 B (Crypt (pubK B) (Nonce NB)) # s3 |
61956 | 54 |
& Says A3 B (Crypt (pubK B) \<lbrace>Nonce NA, Agent A3\<rbrace>) \<in> set s3 |
55 |
& Says B' A3 (Crypt (pubK A3) \<lbrace>Nonce NA, Nonce NB\<rbrace>) \<in> set s3}" |
|
14203 | 56 |
|
57 |
||
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
32960
diff
changeset
|
58 |
definition Nprg :: "state program" where |
14203 | 59 |
(*Initial trace is empty*) |
36866 | 60 |
"Nprg = mk_total_program({[]}, {Fake, NS1, NS2, NS3}, UNIV)" |
14203 | 61 |
|
62 |
declare spies_partsEs [elim] |
|
63 |
declare analz_into_parts [dest] |
|
64 |
declare Fake_parts_insert_in_Un [dest] |
|
65 |
||
63146 | 66 |
text\<open>For other theories, e.g. Mutex and Lift, using [iff] slows proofs down. |
67 |
Here, it facilitates re-use of the Auth proofs.\<close> |
|
14203 | 68 |
|
69 |
declare Fake_def [THEN def_act_simp, iff] |
|
70 |
declare NS1_def [THEN def_act_simp, iff] |
|
71 |
declare NS2_def [THEN def_act_simp, iff] |
|
72 |
declare NS3_def [THEN def_act_simp, iff] |
|
73 |
||
74 |
declare Nprg_def [THEN def_prg_Init, simp] |
|
75 |
||
76 |
||
63146 | 77 |
text\<open>A "possibility property": there are traces that reach the end. |
78 |
Replace by LEADSTO proof!\<close> |
|
14203 | 79 |
lemma "A \<noteq> B ==> |
80 |
\<exists>NB. \<exists>s \<in> reachable Nprg. Says A B (Crypt (pubK B) (Nonce NB)) \<in> set s" |
|
81 |
apply (intro exI bexI) |
|
82 |
apply (rule_tac [2] act = "totalize_act NS3" in reachable.Acts) |
|
83 |
apply (rule_tac [3] act = "totalize_act NS2" in reachable.Acts) |
|
84 |
apply (rule_tac [4] act = "totalize_act NS1" in reachable.Acts) |
|
85 |
apply (rule_tac [5] reachable.Init) |
|
86 |
apply (simp_all (no_asm_simp) add: Nprg_def totalize_act_def) |
|
87 |
apply auto |
|
88 |
done |
|
89 |
||
90 |
||
63146 | 91 |
subsection\<open>Inductive Proofs about @{term ns_public}\<close> |
14203 | 92 |
|
93 |
lemma ns_constrainsI: |
|
94 |
"(!!act s s'. [| act \<in> {Id, Fake, NS1, NS2, NS3}; |
|
95 |
(s,s') \<in> act; s \<in> A |] ==> s' \<in> A') |
|
96 |
==> Nprg \<in> A co A'" |
|
97 |
apply (simp add: Nprg_def mk_total_program_def) |
|
98 |
apply (rule constrainsI, auto) |
|
99 |
done |
|
100 |
||
101 |
||
63146 | 102 |
text\<open>This ML code does the inductions directly.\<close> |
103 |
ML\<open> |
|
42767 | 104 |
fun ns_constrains_tac ctxt i = |
42793 | 105 |
SELECT_GOAL |
106 |
(EVERY |
|
60754 | 107 |
[REPEAT (eresolve_tac ctxt @{thms Always_ConstrainsI} 1), |
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
58963
diff
changeset
|
108 |
REPEAT (resolve_tac ctxt [@{thm StableI}, @{thm stableI}, @{thm constrains_imp_Constrains}] 1), |
60754 | 109 |
resolve_tac ctxt @{thms ns_constrainsI} 1, |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
42793
diff
changeset
|
110 |
full_simp_tac ctxt 1, |
60754 | 111 |
REPEAT (FIRSTGOAL (eresolve_tac ctxt [disjE])), |
42793 | 112 |
ALLGOALS (clarify_tac (ctxt delrules [impI, @{thm impCE}])), |
58963
26bf09b95dda
proper context for assume_tac (atac remains as fall-back without context);
wenzelm
parents:
58889
diff
changeset
|
113 |
REPEAT (FIRSTGOAL (analz_mono_contra_tac ctxt)), |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
42793
diff
changeset
|
114 |
ALLGOALS (asm_simp_tac ctxt)]) i; |
14203 | 115 |
|
116 |
(*Tactic for proving secrecy theorems*) |
|
42767 | 117 |
fun ns_induct_tac ctxt = |
42793 | 118 |
(SELECT_GOAL o EVERY) |
60754 | 119 |
[resolve_tac ctxt @{thms AlwaysI} 1, |
42793 | 120 |
force_tac ctxt 1, |
121 |
(*"reachable" gets in here*) |
|
60754 | 122 |
resolve_tac ctxt [@{thm Always_reachable} RS @{thm Always_ConstrainsI} RS @{thm StableI}] 1, |
42793 | 123 |
ns_constrains_tac ctxt 1]; |
63146 | 124 |
\<close> |
14203 | 125 |
|
63146 | 126 |
method_setup ns_induct = \<open> |
127 |
Scan.succeed (SIMPLE_METHOD' o ns_induct_tac)\<close> |
|
14203 | 128 |
"for inductive reasoning about the Needham-Schroeder protocol" |
129 |
||
63146 | 130 |
text\<open>Converts invariants into statements about reachable states\<close> |
14203 | 131 |
lemmas Always_Collect_reachableD = |
132 |
Always_includes_reachable [THEN subsetD, THEN CollectD] |
|
133 |
||
63146 | 134 |
text\<open>Spy never sees another agent's private key! (unless it's bad at start)\<close> |
14203 | 135 |
lemma Spy_see_priK: |
136 |
"Nprg \<in> Always {s. (Key (priK A) \<in> parts (spies s)) = (A \<in> bad)}" |
|
137 |
apply ns_induct |
|
138 |
apply blast |
|
139 |
done |
|
140 |
declare Spy_see_priK [THEN Always_Collect_reachableD, simp] |
|
141 |
||
142 |
lemma Spy_analz_priK: |
|
143 |
"Nprg \<in> Always {s. (Key (priK A) \<in> analz (spies s)) = (A \<in> bad)}" |
|
144 |
by (rule Always_reachable [THEN Always_weaken], auto) |
|
145 |
declare Spy_analz_priK [THEN Always_Collect_reachableD, simp] |
|
146 |
||
147 |
||
63146 | 148 |
subsection\<open>Authenticity properties obtained from NS2\<close> |
14203 | 149 |
|
63146 | 150 |
text\<open>It is impossible to re-use a nonce in both NS1 and NS2 provided the |
151 |
nonce is secret. (Honest users generate fresh nonces.)\<close> |
|
14203 | 152 |
lemma no_nonce_NS1_NS2: |
153 |
"Nprg |
|
61956 | 154 |
\<in> Always {s. Crypt (pubK C) \<lbrace>NA', Nonce NA\<rbrace> \<in> parts (spies s) --> |
155 |
Crypt (pubK B) \<lbrace>Nonce NA, Agent A\<rbrace> \<in> parts (spies s) --> |
|
14203 | 156 |
Nonce NA \<in> analz (spies s)}" |
157 |
apply ns_induct |
|
158 |
apply (blast intro: analz_insertI)+ |
|
159 |
done |
|
160 |
||
63146 | 161 |
text\<open>Adding it to the claset slows down proofs...\<close> |
14203 | 162 |
lemmas no_nonce_NS1_NS2_reachable = |
163 |
no_nonce_NS1_NS2 [THEN Always_Collect_reachableD, rule_format] |
|
164 |
||
165 |
||
63146 | 166 |
text\<open>Unicity for NS1: nonce NA identifies agents A and B\<close> |
14203 | 167 |
lemma unique_NA_lemma: |
168 |
"Nprg |
|
169 |
\<in> Always {s. Nonce NA \<notin> analz (spies s) --> |
|
61956 | 170 |
Crypt(pubK B) \<lbrace>Nonce NA, Agent A\<rbrace> \<in> parts(spies s) --> |
171 |
Crypt(pubK B') \<lbrace>Nonce NA, Agent A'\<rbrace> \<in> parts(spies s) --> |
|
14203 | 172 |
A=A' & B=B'}" |
173 |
apply ns_induct |
|
174 |
apply auto |
|
63146 | 175 |
txt\<open>Fake, NS1 are non-trivial\<close> |
14203 | 176 |
done |
177 |
||
63146 | 178 |
text\<open>Unicity for NS1: nonce NA identifies agents A and B\<close> |
14203 | 179 |
lemma unique_NA: |
61956 | 180 |
"[| Crypt(pubK B) \<lbrace>Nonce NA, Agent A\<rbrace> \<in> parts(spies s); |
181 |
Crypt(pubK B') \<lbrace>Nonce NA, Agent A'\<rbrace> \<in> parts(spies s); |
|
14203 | 182 |
Nonce NA \<notin> analz (spies s); |
183 |
s \<in> reachable Nprg |] |
|
184 |
==> A=A' & B=B'" |
|
185 |
by (blast dest: unique_NA_lemma [THEN Always_Collect_reachableD]) |
|
186 |
||
187 |
||
63146 | 188 |
text\<open>Secrecy: Spy does not see the nonce sent in msg NS1 if A and B are secure\<close> |
14203 | 189 |
lemma Spy_not_see_NA: |
190 |
"[| A \<notin> bad; B \<notin> bad |] |
|
191 |
==> Nprg \<in> Always |
|
61956 | 192 |
{s. Says A B (Crypt(pubK B) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> set s |
14203 | 193 |
--> Nonce NA \<notin> analz (spies s)}" |
194 |
apply ns_induct |
|
63146 | 195 |
txt\<open>NS3\<close> |
14203 | 196 |
prefer 4 apply (blast intro: no_nonce_NS1_NS2_reachable) |
63146 | 197 |
txt\<open>NS2\<close> |
14203 | 198 |
prefer 3 apply (blast dest: unique_NA) |
63146 | 199 |
txt\<open>NS1\<close> |
14203 | 200 |
prefer 2 apply blast |
63146 | 201 |
txt\<open>Fake\<close> |
14203 | 202 |
apply spy_analz |
203 |
done |
|
204 |
||
205 |
||
63146 | 206 |
text\<open>Authentication for A: if she receives message 2 and has used NA |
207 |
to start a run, then B has sent message 2.\<close> |
|
14203 | 208 |
lemma A_trusts_NS2: |
209 |
"[| A \<notin> bad; B \<notin> bad |] |
|
210 |
==> Nprg \<in> Always |
|
61956 | 211 |
{s. Says A B (Crypt(pubK B) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> set s & |
212 |
Crypt(pubK A) \<lbrace>Nonce NA, Nonce NB\<rbrace> \<in> parts (knows Spy s) |
|
213 |
--> Says B A (Crypt(pubK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) \<in> set s}" |
|
14203 | 214 |
(*insert an invariant for use in some of the subgoals*) |
215 |
apply (insert Spy_not_see_NA [of A B NA], simp, ns_induct) |
|
216 |
apply (auto dest: unique_NA) |
|
217 |
done |
|
218 |
||
219 |
||
63146 | 220 |
text\<open>If the encrypted message appears then it originated with Alice in NS1\<close> |
14203 | 221 |
lemma B_trusts_NS1: |
222 |
"Nprg \<in> Always |
|
223 |
{s. Nonce NA \<notin> analz (spies s) --> |
|
61956 | 224 |
Crypt (pubK B) \<lbrace>Nonce NA, Agent A\<rbrace> \<in> parts (spies s) |
225 |
--> Says A B (Crypt (pubK B) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> set s}" |
|
14203 | 226 |
apply ns_induct |
227 |
apply blast |
|
228 |
done |
|
229 |
||
230 |
||
63146 | 231 |
subsection\<open>Authenticity properties obtained from NS2\<close> |
14203 | 232 |
|
63146 | 233 |
text\<open>Unicity for NS2: nonce NB identifies nonce NA and agent A. |
234 |
Proof closely follows that of \<open>unique_NA\<close>.\<close> |
|
14203 | 235 |
lemma unique_NB_lemma: |
236 |
"Nprg |
|
237 |
\<in> Always {s. Nonce NB \<notin> analz (spies s) --> |
|
61956 | 238 |
Crypt (pubK A) \<lbrace>Nonce NA, Nonce NB\<rbrace> \<in> parts (spies s) --> |
239 |
Crypt(pubK A') \<lbrace>Nonce NA', Nonce NB\<rbrace> \<in> parts(spies s) --> |
|
14203 | 240 |
A=A' & NA=NA'}" |
241 |
apply ns_induct |
|
242 |
apply auto |
|
63146 | 243 |
txt\<open>Fake, NS2 are non-trivial\<close> |
14203 | 244 |
done |
245 |
||
246 |
lemma unique_NB: |
|
61956 | 247 |
"[| Crypt(pubK A) \<lbrace>Nonce NA, Nonce NB\<rbrace> \<in> parts(spies s); |
248 |
Crypt(pubK A') \<lbrace>Nonce NA', Nonce NB\<rbrace> \<in> parts(spies s); |
|
14203 | 249 |
Nonce NB \<notin> analz (spies s); |
250 |
s \<in> reachable Nprg |] |
|
251 |
==> A=A' & NA=NA'" |
|
252 |
apply (blast dest: unique_NB_lemma [THEN Always_Collect_reachableD]) |
|
253 |
done |
|
254 |
||
255 |
||
63146 | 256 |
text\<open>NB remains secret PROVIDED Alice never responds with round 3\<close> |
14203 | 257 |
lemma Spy_not_see_NB: |
258 |
"[| A \<notin> bad; B \<notin> bad |] |
|
259 |
==> Nprg \<in> Always |
|
61956 | 260 |
{s. Says B A (Crypt (pubK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) \<in> set s & |
14203 | 261 |
(ALL C. Says A C (Crypt (pubK C) (Nonce NB)) \<notin> set s) |
262 |
--> Nonce NB \<notin> analz (spies s)}" |
|
263 |
apply ns_induct |
|
264 |
apply (simp_all (no_asm_simp) add: all_conj_distrib) |
|
63146 | 265 |
txt\<open>NS3: because NB determines A\<close> |
14203 | 266 |
prefer 4 apply (blast dest: unique_NB) |
63146 | 267 |
txt\<open>NS2: by freshness and unicity of NB\<close> |
14203 | 268 |
prefer 3 apply (blast intro: no_nonce_NS1_NS2_reachable) |
63146 | 269 |
txt\<open>NS1: by freshness\<close> |
14203 | 270 |
prefer 2 apply blast |
63146 | 271 |
txt\<open>Fake\<close> |
14203 | 272 |
apply spy_analz |
273 |
done |
|
11195
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
274 |
|
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
275 |
|
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
276 |
|
63146 | 277 |
text\<open>Authentication for B: if he receives message 3 and has used NB |
278 |
in message 2, then A has sent message 3--to somebody....\<close> |
|
14203 | 279 |
lemma B_trusts_NS3: |
280 |
"[| A \<notin> bad; B \<notin> bad |] |
|
281 |
==> Nprg \<in> Always |
|
282 |
{s. Crypt (pubK B) (Nonce NB) \<in> parts (spies s) & |
|
61956 | 283 |
Says B A (Crypt (pubK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) \<in> set s |
14203 | 284 |
--> (\<exists>C. Says A C (Crypt (pubK C) (Nonce NB)) \<in> set s)}" |
285 |
(*insert an invariant for use in some of the subgoals*) |
|
286 |
apply (insert Spy_not_see_NB [of A B NA NB], simp, ns_induct) |
|
287 |
apply (simp_all (no_asm_simp) add: ex_disj_distrib) |
|
288 |
apply auto |
|
63146 | 289 |
txt\<open>NS3: because NB determines A. This use of \<open>unique_NB\<close> is robust.\<close> |
14203 | 290 |
apply (blast intro: unique_NB [THEN conjunct1]) |
291 |
done |
|
292 |
||
293 |
||
63146 | 294 |
text\<open>Can we strengthen the secrecy theorem? NO\<close> |
14203 | 295 |
lemma "[| A \<notin> bad; B \<notin> bad |] |
296 |
==> Nprg \<in> Always |
|
61956 | 297 |
{s. Says B A (Crypt (pubK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) \<in> set s |
14203 | 298 |
--> Nonce NB \<notin> analz (spies s)}" |
299 |
apply ns_induct |
|
300 |
apply auto |
|
63146 | 301 |
txt\<open>Fake\<close> |
14203 | 302 |
apply spy_analz |
63146 | 303 |
txt\<open>NS2: by freshness and unicity of NB\<close> |
14203 | 304 |
apply (blast intro: no_nonce_NS1_NS2_reachable) |
63146 | 305 |
txt\<open>NS3: unicity of NB identifies A and NA, but not B\<close> |
14203 | 306 |
apply (frule_tac A'=A in Says_imp_spies [THEN parts.Inj, THEN unique_NB]) |
307 |
apply (erule Says_imp_spies [THEN parts.Inj], auto) |
|
308 |
apply (rename_tac s B' C) |
|
63146 | 309 |
txt\<open>This is the attack! |
14203 | 310 |
@{subgoals[display,indent=0,margin=65]} |
63146 | 311 |
\<close> |
14203 | 312 |
oops |
313 |
||
314 |
||
315 |
(* |
|
316 |
THIS IS THE ATTACK! |
|
317 |
[| A \<notin> bad; B \<notin> bad |] |
|
318 |
==> Nprg |
|
319 |
\<in> Always |
|
61956 | 320 |
{s. Says B A (Crypt (pubK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) \<in> set s --> |
14203 | 321 |
Nonce NB \<notin> analz (knows Spy s)} |
322 |
1. !!s B' C. |
|
323 |
[| A \<notin> bad; B \<notin> bad; s \<in> reachable Nprg |
|
61956 | 324 |
Says A C (Crypt (pubK C) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> set s; |
325 |
Says B' A (Crypt (pubK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) \<in> set s; |
|
326 |
C \<in> bad; Says B A (Crypt (pubK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) \<in> set s; |
|
14203 | 327 |
Nonce NB \<notin> analz (knows Spy s) |] |
328 |
==> False |
|
329 |
*) |
|
11195
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
330 |
|
65ede8dfe304
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff
changeset
|
331 |
end |