13508
|
1 |
(******************************************************************************
|
|
2 |
date: march 2002
|
|
3 |
author: Frederic Blanqui
|
|
4 |
email: blanqui@lri.fr
|
|
5 |
webpage: http://www.lri.fr/~blanqui/
|
|
6 |
|
|
7 |
University of Cambridge, Computer Laboratory
|
|
8 |
William Gates Building, JJ Thomson Avenue
|
|
9 |
Cambridge CB3 0FD, United Kingdom
|
|
10 |
******************************************************************************)
|
|
11 |
|
|
12 |
header{*Yahalom Protocol*}
|
|
13 |
|
|
14 |
theory Yahalom = Guard_Shared:
|
|
15 |
|
|
16 |
subsection{*messages used in the protocol*}
|
|
17 |
|
|
18 |
syntax ya1 :: "agent => agent => nat => event"
|
|
19 |
|
|
20 |
translations "ya1 A B NA" => "Says A B {|Agent A, Nonce NA|}"
|
|
21 |
|
|
22 |
syntax ya1' :: "agent => agent => agent => nat => event"
|
|
23 |
|
|
24 |
translations "ya1' A' A B NA" => "Says A' B {|Agent A, Nonce NA|}"
|
|
25 |
|
|
26 |
syntax ya2 :: "agent => agent => nat => nat => event"
|
|
27 |
|
|
28 |
translations "ya2 A B NA NB"
|
|
29 |
=> "Says B Server {|Agent B, Ciph B {|Agent A, Nonce NA, Nonce NB|}|}"
|
|
30 |
|
|
31 |
syntax ya2' :: "agent => agent => agent => nat => nat => event"
|
|
32 |
|
|
33 |
translations "ya2' B' A B NA NB"
|
|
34 |
=> "Says B' Server {|Agent B, Ciph B {|Agent A, Nonce NA, Nonce NB|}|}"
|
|
35 |
|
|
36 |
syntax ya3 :: "agent => agent => nat => nat => key => event"
|
|
37 |
|
|
38 |
translations "ya3 A B NA NB K"
|
|
39 |
=> "Says Server A {|Ciph A {|Agent B, Key K, Nonce NA, Nonce NB|},
|
|
40 |
Ciph B {|Agent A, Key K|}|}"
|
|
41 |
|
|
42 |
syntax ya3':: "agent => msg => agent => agent => nat => nat => key => event"
|
|
43 |
|
|
44 |
translations "ya3' S Y A B NA NB K"
|
|
45 |
=> "Says S A {|Ciph A {|Agent B, Key K, Nonce NA, Nonce NB|}, Y|}"
|
|
46 |
|
|
47 |
syntax ya4 :: "agent => agent => nat => nat => msg => event"
|
|
48 |
|
|
49 |
translations "ya4 A B K NB Y" => "Says A B {|Y, Crypt K (Nonce NB)|}"
|
|
50 |
|
|
51 |
syntax ya4' :: "agent => agent => nat => nat => msg => event"
|
|
52 |
|
|
53 |
translations "ya4' A' B K NB Y" => "Says A' B {|Y, Crypt K (Nonce NB)|}"
|
|
54 |
|
|
55 |
subsection{*definition of the protocol*}
|
|
56 |
|
|
57 |
consts ya :: "event list set"
|
|
58 |
|
|
59 |
inductive ya
|
|
60 |
intros
|
|
61 |
|
|
62 |
Nil: "[]:ya"
|
|
63 |
|
|
64 |
Fake: "[| evs:ya; X:synth (analz (spies evs)) |] ==> Says Spy B X # evs:ya"
|
|
65 |
|
|
66 |
YA1: "[| evs1:ya; Nonce NA ~:used evs1 |] ==> ya1 A B NA # evs1:ya"
|
|
67 |
|
|
68 |
YA2: "[| evs2:ya; ya1' A' A B NA:set evs2; Nonce NB ~:used evs2 |]
|
|
69 |
==> ya2 A B NA NB # evs2:ya"
|
|
70 |
|
|
71 |
YA3: "[| evs3:ya; ya2' B' A B NA NB:set evs3; Key K ~:used evs3 |]
|
|
72 |
==> ya3 A B NA NB K # evs3:ya"
|
|
73 |
|
|
74 |
YA4: "[| evs4:ya; ya1 A B NA:set evs4; ya3' S Y A B NA NB K:set evs4 |]
|
|
75 |
==> ya4 A B K NB Y # evs4:ya"
|
|
76 |
|
|
77 |
subsection{*declarations for tactics*}
|
|
78 |
|
|
79 |
declare knows_Spy_partsEs [elim]
|
|
80 |
declare Fake_parts_insert [THEN subsetD, dest]
|
|
81 |
declare initState.simps [simp del]
|
|
82 |
|
|
83 |
subsection{*general properties of ya*}
|
|
84 |
|
|
85 |
lemma ya_has_no_Gets: "evs:ya ==> ALL A X. Gets A X ~:set evs"
|
|
86 |
by (erule ya.induct, auto)
|
|
87 |
|
|
88 |
lemma ya_is_Gets_correct [iff]: "Gets_correct ya"
|
|
89 |
by (auto simp: Gets_correct_def dest: ya_has_no_Gets)
|
|
90 |
|
|
91 |
lemma ya_is_one_step [iff]: "one_step ya"
|
|
92 |
by (unfold one_step_def, clarify, ind_cases "ev#evs:ya", auto)
|
|
93 |
|
|
94 |
lemma ya_has_only_Says' [rule_format]: "evs:ya ==>
|
|
95 |
ev:set evs --> (EX A B X. ev=Says A B X)"
|
|
96 |
by (erule ya.induct, auto)
|
|
97 |
|
|
98 |
lemma ya_has_only_Says [iff]: "has_only_Says ya"
|
|
99 |
by (auto simp: has_only_Says_def dest: ya_has_only_Says')
|
|
100 |
|
|
101 |
lemma ya_is_regular [iff]: "regular ya"
|
|
102 |
apply (simp only: regular_def, clarify)
|
|
103 |
apply (erule ya.induct, simp_all add: initState.simps knows.simps)
|
|
104 |
by (auto dest: parts_sub)
|
|
105 |
|
|
106 |
subsection{*guardedness of KAB*}
|
|
107 |
|
|
108 |
lemma Guard_KAB [rule_format]: "[| evs:ya; A ~:bad; B ~:bad |] ==>
|
|
109 |
ya3 A B NA NB K:set evs --> GuardK K {shrK A,shrK B} (spies evs)"
|
|
110 |
apply (erule ya.induct)
|
|
111 |
(* Nil *)
|
|
112 |
apply simp_all
|
|
113 |
(* Fake *)
|
|
114 |
apply (clarify, erule in_synth_GuardK, erule GuardK_analz, simp)
|
|
115 |
(* YA1 *)
|
|
116 |
(* YA2 *)
|
|
117 |
apply safe
|
|
118 |
apply (blast dest: Says_imp_spies)
|
|
119 |
(* YA3 *)
|
|
120 |
apply blast
|
|
121 |
apply (drule_tac A=Server in Key_neq, simp+, rule No_Key, simp)
|
|
122 |
apply (drule_tac A=Server in Key_neq, simp+, rule No_Key, simp)
|
|
123 |
(* YA4 *)
|
|
124 |
apply (blast dest: Says_imp_spies in_GuardK_kparts)
|
|
125 |
by blast
|
|
126 |
|
|
127 |
subsection{*session keys are not symmetric keys*}
|
|
128 |
|
|
129 |
lemma KAB_isnt_shrK [rule_format]: "evs:ya ==>
|
|
130 |
ya3 A B NA NB K:set evs --> K ~:range shrK"
|
|
131 |
by (erule ya.induct, auto)
|
|
132 |
|
|
133 |
lemma ya3_shrK: "evs:ya ==> ya3 A B NA NB (shrK C) ~:set evs"
|
|
134 |
by (blast dest: KAB_isnt_shrK)
|
|
135 |
|
|
136 |
subsection{*ya2' implies ya1'*}
|
|
137 |
|
|
138 |
lemma ya2'_parts_imp_ya1'_parts [rule_format]:
|
|
139 |
"[| evs:ya; B ~:bad |] ==>
|
|
140 |
Ciph B {|Agent A, Nonce NA, Nonce NB|}:parts (spies evs) -->
|
|
141 |
{|Agent A, Nonce NA|}:spies evs"
|
|
142 |
by (erule ya.induct, auto dest: Says_imp_spies intro: parts_parts)
|
|
143 |
|
|
144 |
lemma ya2'_imp_ya1'_parts: "[| ya2' B' A B NA NB:set evs; evs:ya; B ~:bad |]
|
|
145 |
==> {|Agent A, Nonce NA|}:spies evs"
|
|
146 |
by (blast dest: Says_imp_spies ya2'_parts_imp_ya1'_parts)
|
|
147 |
|
|
148 |
subsection{*uniqueness of NB*}
|
|
149 |
|
|
150 |
lemma NB_is_uniq_in_ya2'_parts [rule_format]: "[| evs:ya; B ~:bad; B' ~:bad |] ==>
|
|
151 |
Ciph B {|Agent A, Nonce NA, Nonce NB|}:parts (spies evs) -->
|
|
152 |
Ciph B' {|Agent A', Nonce NA', Nonce NB|}:parts (spies evs) -->
|
|
153 |
A=A' & B=B' & NA=NA'"
|
|
154 |
apply (erule ya.induct, simp_all, clarify)
|
|
155 |
apply (drule Crypt_synth_insert, simp+)
|
|
156 |
apply (drule Crypt_synth_insert, simp+, safe)
|
|
157 |
apply (drule not_used_parts_false, simp+)+
|
|
158 |
by (drule Says_not_parts, simp+)+
|
|
159 |
|
|
160 |
lemma NB_is_uniq_in_ya2': "[| ya2' C A B NA NB:set evs;
|
|
161 |
ya2' C' A' B' NA' NB:set evs; evs:ya; B ~:bad; B' ~:bad |]
|
|
162 |
==> A=A' & B=B' & NA=NA'"
|
|
163 |
by (drule NB_is_uniq_in_ya2'_parts, auto dest: Says_imp_spies)
|
|
164 |
|
|
165 |
subsection{*ya3' implies ya2'*}
|
|
166 |
|
|
167 |
lemma ya3'_parts_imp_ya2'_parts [rule_format]: "[| evs:ya; A ~:bad |] ==>
|
|
168 |
Ciph A {|Agent B, Key K, Nonce NA, Nonce NB|}:parts (spies evs)
|
|
169 |
--> Ciph B {|Agent A, Nonce NA, Nonce NB|}:parts (spies evs)"
|
|
170 |
apply (erule ya.induct, simp_all)
|
|
171 |
apply (clarify, drule Crypt_synth_insert, simp+)
|
|
172 |
apply (blast intro: parts_sub, blast)
|
|
173 |
by (auto dest: Says_imp_spies parts_parts)
|
|
174 |
|
|
175 |
lemma ya3'_parts_imp_ya2' [rule_format]: "[| evs:ya; A ~:bad |] ==>
|
|
176 |
Ciph A {|Agent B, Key K, Nonce NA, Nonce NB|}:parts (spies evs)
|
|
177 |
--> (EX B'. ya2' B' A B NA NB:set evs)"
|
|
178 |
apply (erule ya.induct, simp_all, safe)
|
|
179 |
apply (drule Crypt_synth_insert, simp+)
|
|
180 |
apply (drule Crypt_synth_insert, simp+, blast)
|
|
181 |
apply blast
|
|
182 |
apply blast
|
|
183 |
by (auto dest: Says_imp_spies2 parts_parts)
|
|
184 |
|
|
185 |
lemma ya3'_imp_ya2': "[| ya3' S Y A B NA NB K:set evs; evs:ya; A ~:bad |]
|
|
186 |
==> (EX B'. ya2' B' A B NA NB:set evs)"
|
|
187 |
by (drule ya3'_parts_imp_ya2', auto dest: Says_imp_spies)
|
|
188 |
|
|
189 |
subsection{*ya3' implies ya3*}
|
|
190 |
|
|
191 |
lemma ya3'_parts_imp_ya3 [rule_format]: "[| evs:ya; A ~:bad |] ==>
|
|
192 |
Ciph A {|Agent B, Key K, Nonce NA, Nonce NB|}:parts(spies evs)
|
|
193 |
--> ya3 A B NA NB K:set evs"
|
|
194 |
apply (erule ya.induct, simp_all, safe)
|
|
195 |
apply (drule Crypt_synth_insert, simp+)
|
|
196 |
by (blast dest: Says_imp_spies2 parts_parts)
|
|
197 |
|
|
198 |
lemma ya3'_imp_ya3: "[| ya3' S Y A B NA NB K:set evs; evs:ya; A ~:bad |]
|
|
199 |
==> ya3 A B NA NB K:set evs"
|
|
200 |
by (blast dest: Says_imp_spies ya3'_parts_imp_ya3)
|
|
201 |
|
|
202 |
subsection{*guardedness of NB*}
|
|
203 |
|
|
204 |
constdefs ya_keys :: "agent => agent => nat => nat => event list => key set"
|
|
205 |
"ya_keys A B NA NB evs == {shrK A,shrK B} Un {K. ya3 A B NA NB K:set evs}"
|
|
206 |
|
|
207 |
lemma Guard_NB [rule_format]: "[| evs:ya; A ~:bad; B ~:bad |] ==>
|
|
208 |
ya2 A B NA NB:set evs --> Guard NB (ya_keys A B NA NB evs) (spies evs)"
|
|
209 |
apply (erule ya.induct)
|
|
210 |
(* Nil *)
|
|
211 |
apply (simp_all add: ya_keys_def)
|
|
212 |
(* Fake *)
|
|
213 |
apply safe
|
|
214 |
apply (erule in_synth_Guard, erule Guard_analz, simp, clarify)
|
|
215 |
apply (frule_tac B=B in Guard_KAB, simp+)
|
|
216 |
apply (drule_tac p=ya in GuardK_Key_analz, simp+)
|
|
217 |
apply (blast dest: KAB_isnt_shrK, simp)
|
|
218 |
(* YA1 *)
|
|
219 |
apply (drule_tac n=NB in Nonce_neq, simp+, rule No_Nonce, simp)
|
|
220 |
(* YA2 *)
|
|
221 |
apply blast
|
|
222 |
apply (drule Says_imp_spies)
|
|
223 |
apply (drule_tac n=NB in Nonce_neq, simp+)
|
|
224 |
apply (drule_tac n'=NAa in in_Guard_kparts_neq, simp+)
|
|
225 |
apply (rule No_Nonce, simp)
|
|
226 |
(* YA3 *)
|
|
227 |
apply (rule Guard_extand, simp, blast)
|
|
228 |
apply (case_tac "NAa=NB", clarify)
|
|
229 |
apply (frule Says_imp_spies)
|
|
230 |
apply (frule in_Guard_kparts_Crypt, simp+, blast, simp+)
|
|
231 |
apply (frule_tac A=A and B=B and NA=NA and NB=NB and C=Ba in ya3_shrK, simp)
|
|
232 |
apply (drule ya2'_imp_ya1'_parts, simp, blast, blast)
|
|
233 |
apply (case_tac "NBa=NB", clarify)
|
|
234 |
apply (frule Says_imp_spies)
|
|
235 |
apply (frule in_Guard_kparts_Crypt, simp+, blast, simp+)
|
|
236 |
apply (frule_tac A=A and B=B and NA=NA and NB=NB and C=Ba in ya3_shrK, simp)
|
|
237 |
apply (drule NB_is_uniq_in_ya2', simp+, blast, simp+)
|
|
238 |
apply (simp add: No_Nonce, blast)
|
|
239 |
(* YA4 *)
|
|
240 |
apply (blast dest: Says_imp_spies)
|
|
241 |
apply (case_tac "NBa=NB", clarify)
|
|
242 |
apply (frule_tac A=S in Says_imp_spies)
|
|
243 |
apply (frule in_Guard_kparts_Crypt, simp+)
|
|
244 |
apply (blast dest: Says_imp_spies)
|
|
245 |
apply (case_tac "NBa=NB", clarify)
|
|
246 |
apply (frule_tac A=S in Says_imp_spies)
|
|
247 |
apply (frule in_Guard_kparts_Crypt, simp+, blast, simp+)
|
|
248 |
apply (frule_tac A=A and B=B and NA=NA and NB=NB and C=Aa in ya3_shrK, simp)
|
|
249 |
apply (frule ya3'_imp_ya2', simp+, blast, clarify)
|
|
250 |
apply (frule_tac A=B' in Says_imp_spies)
|
|
251 |
apply (rotate_tac -1, frule in_Guard_kparts_Crypt, simp+, blast, simp+)
|
|
252 |
apply (frule_tac A=A and B=B and NA=NA and NB=NB and C=Ba in ya3_shrK, simp)
|
|
253 |
apply (drule NB_is_uniq_in_ya2', simp+, blast, clarify)
|
|
254 |
apply (drule ya3'_imp_ya3, simp+)
|
|
255 |
apply (simp add: Guard_Nonce)
|
|
256 |
apply (simp add: No_Nonce)
|
|
257 |
done
|
|
258 |
|
|
259 |
end
|