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 imports Guard_Shared begin |
|
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 |
|