author | haftmann |
Sat, 05 Jul 2014 11:01:53 +0200 | |
changeset 57514 | bdc2c6b40bf2 |
parent 55417 | 01fbfb60c33e |
child 58889 | 5b7a9633cfa8 |
permissions | -rw-r--r-- |
37936 | 1 |
(* Title: HOL/Auth/Kerberos_BAN.thy |
5053 | 2 |
Author: Giampaolo Bella, Cambridge University Computer Laboratory |
3 |
Copyright 1998 University of Cambridge |
|
4 |
*) |
|
5 |
||
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
6 |
header{*The Kerberos Protocol, BAN Version*} |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
7 |
|
16417 | 8 |
theory Kerberos_BAN imports Public begin |
5053 | 9 |
|
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
10 |
text{*From page 251 of |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
11 |
Burrows, Abadi and Needham (1989). A Logic of Authentication. |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
12 |
Proc. Royal Soc. 426 |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
13 |
|
18886 | 14 |
Confidentiality (secrecy) and authentication properties are also |
15 |
given in a termporal version: strong guarantees in a little abstracted |
|
16 |
- but very realistic - model. |
|
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
17 |
*} |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
18 |
|
18886 | 19 |
(* Temporal model of accidents: session keys can be leaked |
20 |
ONLY when they have expired *) |
|
5053 | 21 |
|
22 |
consts |
|
23 |
||
24 |
(*Duration of the session key*) |
|
18886 | 25 |
sesKlife :: nat |
5053 | 26 |
|
27 |
(*Duration of the authenticator*) |
|
18886 | 28 |
authlife :: nat |
5053 | 29 |
|
14126
28824746d046
Tidying and replacement of some axioms by specifications
paulson
parents:
13926
diff
changeset
|
30 |
text{*The ticket should remain fresh for two journeys on the network at least*} |
18886 | 31 |
specification (sesKlife) |
32 |
sesKlife_LB [iff]: "2 \<le> sesKlife" |
|
14126
28824746d046
Tidying and replacement of some axioms by specifications
paulson
parents:
13926
diff
changeset
|
33 |
by blast |
5053 | 34 |
|
14126
28824746d046
Tidying and replacement of some axioms by specifications
paulson
parents:
13926
diff
changeset
|
35 |
text{*The authenticator only for one journey*} |
18886 | 36 |
specification (authlife) |
25134
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25112
diff
changeset
|
37 |
authlife_LB [iff]: "authlife \<noteq> 0" |
14126
28824746d046
Tidying and replacement of some axioms by specifications
paulson
parents:
13926
diff
changeset
|
38 |
by blast |
28824746d046
Tidying and replacement of some axioms by specifications
paulson
parents:
13926
diff
changeset
|
39 |
|
20768 | 40 |
abbreviation |
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20768
diff
changeset
|
41 |
CT :: "event list=>nat" where |
20768 | 42 |
"CT == length " |
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
43 |
|
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20768
diff
changeset
|
44 |
abbreviation |
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20768
diff
changeset
|
45 |
expiredK :: "[nat, event list] => bool" where |
20768 | 46 |
"expiredK T evs == sesKlife + T < CT evs" |
18886 | 47 |
|
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20768
diff
changeset
|
48 |
abbreviation |
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
20768
diff
changeset
|
49 |
expiredA :: "[nat, event list] => bool" where |
20768 | 50 |
"expiredA T evs == authlife + T < CT evs" |
18886 | 51 |
|
52 |
||
36866 | 53 |
definition |
18886 | 54 |
(* A is the true creator of X if she has sent X and X never appeared on |
55 |
the trace before this event. Recall that traces grow from head. *) |
|
56 |
Issues :: "[agent, agent, msg, event list] => bool" |
|
36866 | 57 |
("_ Issues _ with _ on _") where |
58 |
"A Issues B with X on evs = |
|
59 |
(\<exists>Y. Says A B Y \<in> set evs & X \<in> parts {Y} & |
|
60 |
X \<notin> parts (spies (takeWhile (% z. z \<noteq> Says A B Y) (rev evs))))" |
|
5053 | 61 |
|
36866 | 62 |
definition |
18886 | 63 |
(* Yields the subtrace of a given trace from its beginning to a given event *) |
64 |
before :: "[event, event list] => event list" ("before _ on _") |
|
36866 | 65 |
where "before ev on evs = takeWhile (% z. z ~= ev) (rev evs)" |
18886 | 66 |
|
36866 | 67 |
definition |
18886 | 68 |
(* States than an event really appears only once on a trace *) |
69 |
Unique :: "[event, event list] => bool" ("Unique _ on _") |
|
36866 | 70 |
where "Unique ev on evs = (ev \<notin> set (tl (dropWhile (% z. z \<noteq> ev) evs)))" |
18886 | 71 |
|
72 |
||
23746 | 73 |
inductive_set bankerberos :: "event list set" |
74 |
where |
|
13926 | 75 |
|
18886 | 76 |
Nil: "[] \<in> bankerberos" |
13926 | 77 |
|
23746 | 78 |
| Fake: "\<lbrakk> evsf \<in> bankerberos; X \<in> synth (analz (spies evsf)) \<rbrakk> |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32406
diff
changeset
|
79 |
\<Longrightarrow> Says Spy B X # evsf \<in> bankerberos" |
13926 | 80 |
|
81 |
||
23746 | 82 |
| BK1: "\<lbrakk> evs1 \<in> bankerberos \<rbrakk> |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32406
diff
changeset
|
83 |
\<Longrightarrow> Says A Server \<lbrace>Agent A, Agent B\<rbrace> # evs1 |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32406
diff
changeset
|
84 |
\<in> bankerberos" |
18886 | 85 |
|
86 |
||
23746 | 87 |
| BK2: "\<lbrakk> evs2 \<in> bankerberos; Key K \<notin> used evs2; K \<in> symKeys; |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32406
diff
changeset
|
88 |
Says A' Server \<lbrace>Agent A, Agent B\<rbrace> \<in> set evs2 \<rbrakk> |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32406
diff
changeset
|
89 |
\<Longrightarrow> Says Server A |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32406
diff
changeset
|
90 |
(Crypt (shrK A) |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32406
diff
changeset
|
91 |
\<lbrace>Number (CT evs2), Agent B, Key K, |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32406
diff
changeset
|
92 |
(Crypt (shrK B) \<lbrace>Number (CT evs2), Agent A, Key K\<rbrace>)\<rbrace>) |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32406
diff
changeset
|
93 |
# evs2 \<in> bankerberos" |
13926 | 94 |
|
95 |
||
23746 | 96 |
| BK3: "\<lbrakk> evs3 \<in> bankerberos; |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32406
diff
changeset
|
97 |
Says S A (Crypt (shrK A) \<lbrace>Number Tk, Agent B, Key K, Ticket\<rbrace>) |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32406
diff
changeset
|
98 |
\<in> set evs3; |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32406
diff
changeset
|
99 |
Says A Server \<lbrace>Agent A, Agent B\<rbrace> \<in> set evs3; |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32406
diff
changeset
|
100 |
\<not> expiredK Tk evs3 \<rbrakk> |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32406
diff
changeset
|
101 |
\<Longrightarrow> Says A B \<lbrace>Ticket, Crypt K \<lbrace>Agent A, Number (CT evs3)\<rbrace> \<rbrace> |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32406
diff
changeset
|
102 |
# evs3 \<in> bankerberos" |
13926 | 103 |
|
104 |
||
23746 | 105 |
| BK4: "\<lbrakk> evs4 \<in> bankerberos; |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32406
diff
changeset
|
106 |
Says A' B \<lbrace>(Crypt (shrK B) \<lbrace>Number Tk, Agent A, Key K\<rbrace>), |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32406
diff
changeset
|
107 |
(Crypt K \<lbrace>Agent A, Number Ta\<rbrace>) \<rbrace>: set evs4; |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32406
diff
changeset
|
108 |
\<not> expiredK Tk evs4; \<not> expiredA Ta evs4 \<rbrakk> |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32406
diff
changeset
|
109 |
\<Longrightarrow> Says B A (Crypt K (Number Ta)) # evs4 |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32406
diff
changeset
|
110 |
\<in> bankerberos" |
5053 | 111 |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32406
diff
changeset
|
112 |
(*Old session keys may become compromised*) |
23746 | 113 |
| Oops: "\<lbrakk> evso \<in> bankerberos; |
18886 | 114 |
Says Server A (Crypt (shrK A) \<lbrace>Number Tk, Agent B, Key K, Ticket\<rbrace>) |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32406
diff
changeset
|
115 |
\<in> set evso; |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32406
diff
changeset
|
116 |
expiredK Tk evso \<rbrakk> |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32406
diff
changeset
|
117 |
\<Longrightarrow> Notes Spy \<lbrace>Number Tk, Key K\<rbrace> # evso \<in> bankerberos" |
13926 | 118 |
|
119 |
||
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
120 |
declare Says_imp_knows_Spy [THEN parts.Inj, dest] |
14200
d8598e24f8fa
Removal of the Key_supply axiom (affects many possbility proofs) and minor
paulson
parents:
14126
diff
changeset
|
121 |
declare parts.Body [dest] |
d8598e24f8fa
Removal of the Key_supply axiom (affects many possbility proofs) and minor
paulson
parents:
14126
diff
changeset
|
122 |
declare analz_into_parts [dest] |
d8598e24f8fa
Removal of the Key_supply axiom (affects many possbility proofs) and minor
paulson
parents:
14126
diff
changeset
|
123 |
declare Fake_parts_insert_in_Un [dest] |
13926 | 124 |
|
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
125 |
text{*A "possibility property": there are traces that reach the end.*} |
18886 | 126 |
lemma "\<lbrakk>Key K \<notin> used []; K \<in> symKeys\<rbrakk> |
127 |
\<Longrightarrow> \<exists>Timestamp. \<exists>evs \<in> bankerberos. |
|
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
128 |
Says B A (Crypt K (Number Timestamp)) |
13926 | 129 |
\<in> set evs" |
18886 | 130 |
apply (cut_tac sesKlife_LB) |
13926 | 131 |
apply (intro exI bexI) |
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
132 |
apply (rule_tac [2] |
18886 | 133 |
bankerberos.Nil [THEN bankerberos.BK1, THEN bankerberos.BK2, |
134 |
THEN bankerberos.BK3, THEN bankerberos.BK4]) |
|
25134
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
25112
diff
changeset
|
135 |
apply (possibility, simp_all (no_asm_simp) add: used_Cons) |
13926 | 136 |
done |
137 |
||
18886 | 138 |
subsection{*Lemmas for reasoning about predicate "Issues"*} |
13926 | 139 |
|
18886 | 140 |
lemma spies_Says_rev: "spies (evs @ [Says A B X]) = insert X (spies evs)" |
141 |
apply (induct_tac "evs") |
|
55417
01fbfb60c33e
adapted to 'xxx_{case,rec}' renaming, to new theorem names, and to new variable names in theorems
blanchet
parents:
42749
diff
changeset
|
142 |
apply (rename_tac [2] a b) |
18886 | 143 |
apply (induct_tac [2] "a", auto) |
144 |
done |
|
145 |
||
146 |
lemma spies_Gets_rev: "spies (evs @ [Gets A X]) = spies evs" |
|
147 |
apply (induct_tac "evs") |
|
55417
01fbfb60c33e
adapted to 'xxx_{case,rec}' renaming, to new theorem names, and to new variable names in theorems
blanchet
parents:
42749
diff
changeset
|
148 |
apply (rename_tac [2] a b) |
18886 | 149 |
apply (induct_tac [2] "a", auto) |
150 |
done |
|
151 |
||
152 |
lemma spies_Notes_rev: "spies (evs @ [Notes A X]) = |
|
153 |
(if A:bad then insert X (spies evs) else spies evs)" |
|
154 |
apply (induct_tac "evs") |
|
55417
01fbfb60c33e
adapted to 'xxx_{case,rec}' renaming, to new theorem names, and to new variable names in theorems
blanchet
parents:
42749
diff
changeset
|
155 |
apply (rename_tac [2] a b) |
18886 | 156 |
apply (induct_tac [2] "a", auto) |
157 |
done |
|
158 |
||
159 |
lemma spies_evs_rev: "spies evs = spies (rev evs)" |
|
160 |
apply (induct_tac "evs") |
|
55417
01fbfb60c33e
adapted to 'xxx_{case,rec}' renaming, to new theorem names, and to new variable names in theorems
blanchet
parents:
42749
diff
changeset
|
161 |
apply (rename_tac [2] a b) |
18886 | 162 |
apply (induct_tac [2] "a") |
163 |
apply (simp_all (no_asm_simp) add: spies_Says_rev spies_Gets_rev spies_Notes_rev) |
|
164 |
done |
|
165 |
||
166 |
lemmas parts_spies_evs_revD2 = spies_evs_rev [THEN equalityD2, THEN parts_mono] |
|
167 |
||
168 |
lemma spies_takeWhile: "spies (takeWhile P evs) <= spies evs" |
|
169 |
apply (induct_tac "evs") |
|
55417
01fbfb60c33e
adapted to 'xxx_{case,rec}' renaming, to new theorem names, and to new variable names in theorems
blanchet
parents:
42749
diff
changeset
|
170 |
apply (rename_tac [2] a b) |
18886 | 171 |
apply (induct_tac [2] "a", auto) |
172 |
txt{* Resembles @{text"used_subset_append"} in theory Event.*} |
|
173 |
done |
|
174 |
||
175 |
lemmas parts_spies_takeWhile_mono = spies_takeWhile [THEN parts_mono] |
|
176 |
||
177 |
||
178 |
text{*Lemmas for reasoning about predicate "before"*} |
|
39251
8756b44582e2
Tidied up proofs using sledgehammer, also deleting unnecessary semicolons
paulson
parents:
37936
diff
changeset
|
179 |
lemma used_Says_rev: "used (evs @ [Says A B X]) = parts {X} \<union> (used evs)" |
18886 | 180 |
apply (induct_tac "evs") |
181 |
apply simp |
|
55417
01fbfb60c33e
adapted to 'xxx_{case,rec}' renaming, to new theorem names, and to new variable names in theorems
blanchet
parents:
42749
diff
changeset
|
182 |
apply (rename_tac a b) |
18886 | 183 |
apply (induct_tac "a") |
184 |
apply auto |
|
185 |
done |
|
13926 | 186 |
|
39251
8756b44582e2
Tidied up proofs using sledgehammer, also deleting unnecessary semicolons
paulson
parents:
37936
diff
changeset
|
187 |
lemma used_Notes_rev: "used (evs @ [Notes A X]) = parts {X} \<union> (used evs)" |
18886 | 188 |
apply (induct_tac "evs") |
189 |
apply simp |
|
55417
01fbfb60c33e
adapted to 'xxx_{case,rec}' renaming, to new theorem names, and to new variable names in theorems
blanchet
parents:
42749
diff
changeset
|
190 |
apply (rename_tac a b) |
18886 | 191 |
apply (induct_tac "a") |
192 |
apply auto |
|
193 |
done |
|
194 |
||
39251
8756b44582e2
Tidied up proofs using sledgehammer, also deleting unnecessary semicolons
paulson
parents:
37936
diff
changeset
|
195 |
lemma used_Gets_rev: "used (evs @ [Gets B X]) = used evs" |
18886 | 196 |
apply (induct_tac "evs") |
197 |
apply simp |
|
55417
01fbfb60c33e
adapted to 'xxx_{case,rec}' renaming, to new theorem names, and to new variable names in theorems
blanchet
parents:
42749
diff
changeset
|
198 |
apply (rename_tac a b) |
18886 | 199 |
apply (induct_tac "a") |
200 |
apply auto |
|
201 |
done |
|
202 |
||
203 |
lemma used_evs_rev: "used evs = used (rev evs)" |
|
204 |
apply (induct_tac "evs") |
|
205 |
apply simp |
|
55417
01fbfb60c33e
adapted to 'xxx_{case,rec}' renaming, to new theorem names, and to new variable names in theorems
blanchet
parents:
42749
diff
changeset
|
206 |
apply (rename_tac a b) |
18886 | 207 |
apply (induct_tac "a") |
208 |
apply (simp add: used_Says_rev) |
|
209 |
apply (simp add: used_Gets_rev) |
|
210 |
apply (simp add: used_Notes_rev) |
|
211 |
done |
|
212 |
||
213 |
lemma used_takeWhile_used [rule_format]: |
|
214 |
"x : used (takeWhile P X) --> x : used X" |
|
215 |
apply (induct_tac "X") |
|
216 |
apply simp |
|
55417
01fbfb60c33e
adapted to 'xxx_{case,rec}' renaming, to new theorem names, and to new variable names in theorems
blanchet
parents:
42749
diff
changeset
|
217 |
apply (rename_tac a b) |
18886 | 218 |
apply (induct_tac "a") |
219 |
apply (simp_all add: used_Nil) |
|
220 |
apply (blast dest!: initState_into_used)+ |
|
221 |
done |
|
222 |
||
223 |
lemma set_evs_rev: "set evs = set (rev evs)" |
|
224 |
apply auto |
|
225 |
done |
|
226 |
||
227 |
lemma takeWhile_void [rule_format]: |
|
228 |
"x \<notin> set evs \<longrightarrow> takeWhile (\<lambda>z. z \<noteq> x) evs = evs" |
|
229 |
apply auto |
|
230 |
done |
|
231 |
||
232 |
(**** Inductive proofs about bankerberos ****) |
|
233 |
||
234 |
text{*Forwarding Lemma for reasoning about the encrypted portion of message BK3*} |
|
235 |
lemma BK3_msg_in_parts_spies: |
|
236 |
"Says S A (Crypt KA \<lbrace>Timestamp, B, K, X\<rbrace>) \<in> set evs |
|
237 |
\<Longrightarrow> X \<in> parts (spies evs)" |
|
238 |
apply blast |
|
239 |
done |
|
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
240 |
|
13926 | 241 |
lemma Oops_parts_spies: |
18886 | 242 |
"Says Server A (Crypt (shrK A) \<lbrace>Timestamp, B, K, X\<rbrace>) \<in> set evs |
243 |
\<Longrightarrow> K \<in> parts (spies evs)" |
|
244 |
apply blast |
|
245 |
done |
|
13926 | 246 |
|
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
247 |
text{*Spy never sees another agent's shared key! (unless it's bad at start)*} |
13926 | 248 |
lemma Spy_see_shrK [simp]: |
18886 | 249 |
"evs \<in> bankerberos \<Longrightarrow> (Key (shrK A) \<in> parts (spies evs)) = (A \<in> bad)" |
250 |
apply (erule bankerberos.induct) |
|
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
251 |
apply (frule_tac [7] Oops_parts_spies) |
18886 | 252 |
apply (frule_tac [5] BK3_msg_in_parts_spies, simp_all, blast+) |
13926 | 253 |
done |
5053 | 254 |
|
255 |
||
13926 | 256 |
lemma Spy_analz_shrK [simp]: |
18886 | 257 |
"evs \<in> bankerberos \<Longrightarrow> (Key (shrK A) \<in> analz (spies evs)) = (A \<in> bad)" |
258 |
apply auto |
|
259 |
done |
|
13926 | 260 |
|
261 |
lemma Spy_see_shrK_D [dest!]: |
|
18886 | 262 |
"\<lbrakk> Key (shrK A) \<in> parts (spies evs); |
263 |
evs \<in> bankerberos \<rbrakk> \<Longrightarrow> A:bad" |
|
264 |
apply (blast dest: Spy_see_shrK) |
|
265 |
done |
|
13926 | 266 |
|
267 |
lemmas Spy_analz_shrK_D = analz_subset_parts [THEN subsetD, THEN Spy_see_shrK_D, dest!] |
|
268 |
||
269 |
||
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
270 |
text{*Nobody can have used non-existent keys!*} |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
271 |
lemma new_keys_not_used [simp]: |
18886 | 272 |
"\<lbrakk>Key K \<notin> used evs; K \<in> symKeys; evs \<in> bankerberos\<rbrakk> |
273 |
\<Longrightarrow> K \<notin> keysFor (parts (spies evs))" |
|
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
274 |
apply (erule rev_mp) |
18886 | 275 |
apply (erule bankerberos.induct) |
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
276 |
apply (frule_tac [7] Oops_parts_spies) |
18886 | 277 |
apply (frule_tac [5] BK3_msg_in_parts_spies, simp_all) |
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
278 |
txt{*Fake*} |
13926 | 279 |
apply (force dest!: keysFor_parts_insert) |
18886 | 280 |
txt{*BK2, BK3, BK4*} |
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
281 |
apply (force dest!: analz_shrK_Decrypt)+ |
13926 | 282 |
done |
283 |
||
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
284 |
subsection{* Lemmas concerning the form of items passed in messages *} |
13926 | 285 |
|
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
286 |
text{*Describes the form of K, X and K' when the Server sends this message.*} |
13926 | 287 |
lemma Says_Server_message_form: |
18886 | 288 |
"\<lbrakk> Says Server A (Crypt K' \<lbrace>Number Tk, Agent B, Key K, Ticket\<rbrace>) |
289 |
\<in> set evs; evs \<in> bankerberos \<rbrakk> |
|
290 |
\<Longrightarrow> K' = shrK A & K \<notin> range shrK & |
|
291 |
Ticket = (Crypt (shrK B) \<lbrace>Number Tk, Agent A, Key K\<rbrace>) & |
|
292 |
Key K \<notin> used(before |
|
293 |
Says Server A (Crypt K' \<lbrace>Number Tk, Agent B, Key K, Ticket\<rbrace>) |
|
294 |
on evs) & |
|
295 |
Tk = CT(before |
|
296 |
Says Server A (Crypt K' \<lbrace>Number Tk, Agent B, Key K, Ticket\<rbrace>) |
|
297 |
on evs)" |
|
298 |
apply (unfold before_def) |
|
13926 | 299 |
apply (erule rev_mp) |
32406 | 300 |
apply (erule bankerberos.induct, simp_all add: takeWhile_tail) |
42749
47f283fcf2ae
Metis doesn't find an old proof in acceptable time now that higher-order equality reasoning is supported -- tuned proof script to help it
blanchet
parents:
39251
diff
changeset
|
301 |
apply auto |
47f283fcf2ae
Metis doesn't find an old proof in acceptable time now that higher-order equality reasoning is supported -- tuned proof script to help it
blanchet
parents:
39251
diff
changeset
|
302 |
apply (metis length_rev set_rev takeWhile_void used_evs_rev)+ |
13926 | 303 |
done |
5053 | 304 |
|
305 |
||
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
306 |
text{*If the encrypted message appears then it originated with the Server |
13926 | 307 |
PROVIDED that A is NOT compromised! |
18886 | 308 |
This allows A to verify freshness of the session key. |
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
309 |
*} |
18886 | 310 |
lemma Kab_authentic: |
311 |
"\<lbrakk> Crypt (shrK A) \<lbrace>Number Tk, Agent B, Key K, X\<rbrace> |
|
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
312 |
\<in> parts (spies evs); |
18886 | 313 |
A \<notin> bad; evs \<in> bankerberos \<rbrakk> |
314 |
\<Longrightarrow> Says Server A (Crypt (shrK A) \<lbrace>Number Tk, Agent B, Key K, X\<rbrace>) |
|
13926 | 315 |
\<in> set evs" |
316 |
apply (erule rev_mp) |
|
18886 | 317 |
apply (erule bankerberos.induct) |
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
318 |
apply (frule_tac [7] Oops_parts_spies) |
18886 | 319 |
apply (frule_tac [5] BK3_msg_in_parts_spies, simp_all, blast) |
13926 | 320 |
done |
321 |
||
322 |
||
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
323 |
text{*If the TICKET appears then it originated with the Server*} |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
324 |
text{*FRESHNESS OF THE SESSION KEY to B*} |
18886 | 325 |
lemma ticket_authentic: |
326 |
"\<lbrakk> Crypt (shrK B) \<lbrace>Number Tk, Agent A, Key K\<rbrace> \<in> parts (spies evs); |
|
327 |
B \<notin> bad; evs \<in> bankerberos \<rbrakk> |
|
328 |
\<Longrightarrow> Says Server A |
|
329 |
(Crypt (shrK A) \<lbrace>Number Tk, Agent B, Key K, |
|
330 |
Crypt (shrK B) \<lbrace>Number Tk, Agent A, Key K\<rbrace>\<rbrace>) |
|
13926 | 331 |
\<in> set evs" |
332 |
apply (erule rev_mp) |
|
18886 | 333 |
apply (erule bankerberos.induct) |
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
334 |
apply (frule_tac [7] Oops_parts_spies) |
18886 | 335 |
apply (frule_tac [5] BK3_msg_in_parts_spies, simp_all, blast) |
13926 | 336 |
done |
337 |
||
338 |
||
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
339 |
text{*EITHER describes the form of X when the following message is sent, |
13926 | 340 |
OR reduces it to the Fake case. |
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
341 |
Use @{text Says_Server_message_form} if applicable.*} |
13926 | 342 |
lemma Says_S_message_form: |
18886 | 343 |
"\<lbrakk> Says S A (Crypt (shrK A) \<lbrace>Number Tk, Agent B, Key K, X\<rbrace>) |
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
344 |
\<in> set evs; |
18886 | 345 |
evs \<in> bankerberos \<rbrakk> |
346 |
\<Longrightarrow> (K \<notin> range shrK & X = (Crypt (shrK B) \<lbrace>Number Tk, Agent A, Key K\<rbrace>)) |
|
13926 | 347 |
| X \<in> analz (spies evs)" |
348 |
apply (case_tac "A \<in> bad") |
|
349 |
apply (force dest!: Says_imp_spies [THEN analz.Inj]) |
|
350 |
apply (frule Says_imp_spies [THEN parts.Inj]) |
|
18886 | 351 |
apply (blast dest!: Kab_authentic Says_Server_message_form) |
13926 | 352 |
done |
353 |
||
5053 | 354 |
|
355 |
||
13926 | 356 |
(**** |
357 |
The following is to prove theorems of the form |
|
358 |
||
18886 | 359 |
Key K \<in> analz (insert (Key KAB) (spies evs)) \<Longrightarrow> |
13926 | 360 |
Key K \<in> analz (spies evs) |
361 |
||
362 |
A more general formula must be proved inductively. |
|
363 |
||
364 |
****) |
|
365 |
||
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
366 |
text{* Session keys are not used to encrypt other session keys *} |
13926 | 367 |
lemma analz_image_freshK [rule_format (no_asm)]: |
18886 | 368 |
"evs \<in> bankerberos \<Longrightarrow> |
369 |
\<forall>K KK. KK \<subseteq> - (range shrK) \<longrightarrow> |
|
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
370 |
(Key K \<in> analz (Key`KK Un (spies evs))) = |
13926 | 371 |
(K \<in> KK | Key K \<in> analz (spies evs))" |
18886 | 372 |
apply (erule bankerberos.induct) |
13926 | 373 |
apply (drule_tac [7] Says_Server_message_form) |
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
374 |
apply (erule_tac [5] Says_S_message_form [THEN disjE], analz_freshK, spy_analz, auto) |
13926 | 375 |
done |
376 |
||
377 |
||
378 |
lemma analz_insert_freshK: |
|
18886 | 379 |
"\<lbrakk> evs \<in> bankerberos; KAB \<notin> range shrK \<rbrakk> \<Longrightarrow> |
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
380 |
(Key K \<in> analz (insert (Key KAB) (spies evs))) = |
13926 | 381 |
(K = KAB | Key K \<in> analz (spies evs))" |
18886 | 382 |
apply (simp only: analz_image_freshK analz_image_freshK_simps) |
383 |
done |
|
13926 | 384 |
|
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
385 |
text{* The session key K uniquely identifies the message *} |
13926 | 386 |
lemma unique_session_keys: |
18886 | 387 |
"\<lbrakk> Says Server A |
388 |
(Crypt (shrK A) \<lbrace>Number Tk, Agent B, Key K, X\<rbrace>) \<in> set evs; |
|
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
389 |
Says Server A' |
18886 | 390 |
(Crypt (shrK A') \<lbrace>Number Tk', Agent B', Key K, X'\<rbrace>) \<in> set evs; |
391 |
evs \<in> bankerberos \<rbrakk> \<Longrightarrow> A=A' & Tk=Tk' & B=B' & X = X'" |
|
13926 | 392 |
apply (erule rev_mp) |
393 |
apply (erule rev_mp) |
|
18886 | 394 |
apply (erule bankerberos.induct) |
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
395 |
apply (frule_tac [7] Oops_parts_spies) |
18886 | 396 |
apply (frule_tac [5] BK3_msg_in_parts_spies, simp_all) |
397 |
txt{*BK2: it can't be a new key*} |
|
398 |
apply blast |
|
399 |
done |
|
400 |
||
401 |
lemma Server_Unique: |
|
402 |
"\<lbrakk> Says Server A |
|
403 |
(Crypt (shrK A) \<lbrace>Number Tk, Agent B, Key K, Ticket\<rbrace>) \<in> set evs; |
|
404 |
evs \<in> bankerberos \<rbrakk> \<Longrightarrow> |
|
405 |
Unique Says Server A (Crypt (shrK A) \<lbrace>Number Tk, Agent B, Key K, Ticket\<rbrace>) |
|
406 |
on evs" |
|
407 |
apply (erule rev_mp, erule bankerberos.induct, simp_all add: Unique_def) |
|
13926 | 408 |
apply blast |
409 |
done |
|
410 |
||
411 |
||
18886 | 412 |
subsection{*Non-temporal guarantees, explicitly relying on non-occurrence of |
413 |
oops events - refined below by temporal guarantees*} |
|
414 |
||
415 |
text{*Non temporal treatment of confidentiality*} |
|
416 |
||
417 |
text{* Lemma: the session key sent in msg BK2 would be lost by oops |
|
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
418 |
if the spy could see it! *} |
18886 | 419 |
lemma lemma_conf [rule_format (no_asm)]: |
420 |
"\<lbrakk> A \<notin> bad; B \<notin> bad; evs \<in> bankerberos \<rbrakk> |
|
421 |
\<Longrightarrow> Says Server A |
|
422 |
(Crypt (shrK A) \<lbrace>Number Tk, Agent B, Key K, |
|
423 |
Crypt (shrK B) \<lbrace>Number Tk, Agent A, Key K\<rbrace>\<rbrace>) |
|
424 |
\<in> set evs \<longrightarrow> |
|
425 |
Key K \<in> analz (spies evs) \<longrightarrow> Notes Spy \<lbrace>Number Tk, Key K\<rbrace> \<in> set evs" |
|
426 |
apply (erule bankerberos.induct) |
|
427 |
apply (frule_tac [7] Says_Server_message_form) |
|
428 |
apply (frule_tac [5] Says_S_message_form [THEN disjE]) |
|
429 |
apply (simp_all (no_asm_simp) add: analz_insert_eq analz_insert_freshK pushes) |
|
430 |
txt{*Fake*} |
|
431 |
apply spy_analz |
|
432 |
txt{*BK2*} |
|
433 |
apply (blast intro: parts_insertI) |
|
434 |
txt{*BK3*} |
|
435 |
apply (case_tac "Aa \<in> bad") |
|
436 |
prefer 2 apply (blast dest: Kab_authentic unique_session_keys) |
|
437 |
apply (blast dest: Says_imp_spies [THEN analz.Inj] Crypt_Spy_analz_bad elim!: MPair_analz) |
|
438 |
txt{*Oops*} |
|
439 |
apply (blast dest: unique_session_keys) |
|
440 |
done |
|
441 |
||
442 |
||
443 |
text{*Confidentiality for the Server: Spy does not see the keys sent in msg BK2 |
|
444 |
as long as they have not expired.*} |
|
445 |
lemma Confidentiality_S: |
|
446 |
"\<lbrakk> Says Server A |
|
447 |
(Crypt K' \<lbrace>Number Tk, Agent B, Key K, Ticket\<rbrace>) \<in> set evs; |
|
448 |
Notes Spy \<lbrace>Number Tk, Key K\<rbrace> \<notin> set evs; |
|
449 |
A \<notin> bad; B \<notin> bad; evs \<in> bankerberos |
|
450 |
\<rbrakk> \<Longrightarrow> Key K \<notin> analz (spies evs)" |
|
451 |
apply (frule Says_Server_message_form, assumption) |
|
452 |
apply (blast intro: lemma_conf) |
|
453 |
done |
|
454 |
||
455 |
text{*Confidentiality for Alice*} |
|
456 |
lemma Confidentiality_A: |
|
457 |
"\<lbrakk> Crypt (shrK A) \<lbrace>Number Tk, Agent B, Key K, X\<rbrace> \<in> parts (spies evs); |
|
458 |
Notes Spy \<lbrace>Number Tk, Key K\<rbrace> \<notin> set evs; |
|
459 |
A \<notin> bad; B \<notin> bad; evs \<in> bankerberos |
|
460 |
\<rbrakk> \<Longrightarrow> Key K \<notin> analz (spies evs)" |
|
461 |
apply (blast dest!: Kab_authentic Confidentiality_S) |
|
462 |
done |
|
463 |
||
464 |
text{*Confidentiality for Bob*} |
|
465 |
lemma Confidentiality_B: |
|
466 |
"\<lbrakk> Crypt (shrK B) \<lbrace>Number Tk, Agent A, Key K\<rbrace> |
|
467 |
\<in> parts (spies evs); |
|
468 |
Notes Spy \<lbrace>Number Tk, Key K\<rbrace> \<notin> set evs; |
|
469 |
A \<notin> bad; B \<notin> bad; evs \<in> bankerberos |
|
470 |
\<rbrakk> \<Longrightarrow> Key K \<notin> analz (spies evs)" |
|
471 |
apply (blast dest!: ticket_authentic Confidentiality_S) |
|
472 |
done |
|
473 |
||
474 |
text{*Non temporal treatment of authentication*} |
|
13926 | 475 |
|
18886 | 476 |
text{*Lemmas @{text lemma_A} and @{text lemma_B} in fact are common to both temporal and non-temporal treatments*} |
477 |
lemma lemma_A [rule_format]: |
|
478 |
"\<lbrakk> A \<notin> bad; B \<notin> bad; evs \<in> bankerberos \<rbrakk> |
|
479 |
\<Longrightarrow> |
|
480 |
Key K \<notin> analz (spies evs) \<longrightarrow> |
|
481 |
Says Server A (Crypt (shrK A) \<lbrace>Number Tk, Agent B, Key K, X\<rbrace>) |
|
482 |
\<in> set evs \<longrightarrow> |
|
483 |
Crypt K \<lbrace>Agent A, Number Ta\<rbrace> \<in> parts (spies evs) \<longrightarrow> |
|
484 |
Says A B \<lbrace>X, Crypt K \<lbrace>Agent A, Number Ta\<rbrace>\<rbrace> |
|
485 |
\<in> set evs" |
|
486 |
apply (erule bankerberos.induct) |
|
487 |
apply (frule_tac [7] Oops_parts_spies) |
|
488 |
apply (frule_tac [5] Says_S_message_form) |
|
489 |
apply (frule_tac [6] BK3_msg_in_parts_spies, analz_mono_contra) |
|
490 |
apply (simp_all (no_asm_simp) add: all_conj_distrib) |
|
491 |
txt{*Fake*} |
|
492 |
apply blast |
|
493 |
txt{*BK2*} |
|
494 |
apply (force dest: Crypt_imp_invKey_keysFor) |
|
495 |
txt{*BK3*} |
|
496 |
apply (blast dest: Kab_authentic unique_session_keys) |
|
497 |
done |
|
32406 | 498 |
|
18886 | 499 |
lemma lemma_B [rule_format]: |
500 |
"\<lbrakk> B \<notin> bad; evs \<in> bankerberos \<rbrakk> |
|
501 |
\<Longrightarrow> Key K \<notin> analz (spies evs) \<longrightarrow> |
|
502 |
Says Server A (Crypt (shrK A) \<lbrace>Number Tk, Agent B, Key K, X\<rbrace>) |
|
503 |
\<in> set evs \<longrightarrow> |
|
504 |
Crypt K (Number Ta) \<in> parts (spies evs) \<longrightarrow> |
|
505 |
Says B A (Crypt K (Number Ta)) \<in> set evs" |
|
506 |
apply (erule bankerberos.induct) |
|
507 |
apply (frule_tac [7] Oops_parts_spies) |
|
508 |
apply (frule_tac [5] Says_S_message_form) |
|
509 |
apply (drule_tac [6] BK3_msg_in_parts_spies, analz_mono_contra) |
|
510 |
apply (simp_all (no_asm_simp) add: all_conj_distrib) |
|
511 |
txt{*Fake*} |
|
512 |
apply blast |
|
513 |
txt{*BK2*} |
|
514 |
apply (force dest: Crypt_imp_invKey_keysFor) |
|
515 |
txt{*BK4*} |
|
516 |
apply (blast dest: ticket_authentic unique_session_keys |
|
517 |
Says_imp_spies [THEN analz.Inj] Crypt_Spy_analz_bad) |
|
518 |
done |
|
519 |
||
520 |
||
521 |
text{*The "r" suffix indicates theorems where the confidentiality assumptions are relaxed by the corresponding arguments.*} |
|
522 |
||
523 |
||
524 |
text{*Authentication of A to B*} |
|
525 |
lemma B_authenticates_A_r: |
|
526 |
"\<lbrakk> Crypt K \<lbrace>Agent A, Number Ta\<rbrace> \<in> parts (spies evs); |
|
527 |
Crypt (shrK B) \<lbrace>Number Tk, Agent A, Key K\<rbrace> \<in> parts (spies evs); |
|
528 |
Notes Spy \<lbrace>Number Tk, Key K\<rbrace> \<notin> set evs; |
|
529 |
A \<notin> bad; B \<notin> bad; evs \<in> bankerberos \<rbrakk> |
|
530 |
\<Longrightarrow> Says A B \<lbrace>Crypt (shrK B) \<lbrace>Number Tk, Agent A, Key K\<rbrace>, |
|
531 |
Crypt K \<lbrace>Agent A, Number Ta\<rbrace>\<rbrace> \<in> set evs" |
|
532 |
apply (blast dest!: ticket_authentic |
|
533 |
intro!: lemma_A |
|
534 |
elim!: Confidentiality_S [THEN [2] rev_notE]) |
|
535 |
done |
|
536 |
||
537 |
||
538 |
text{*Authentication of B to A*} |
|
539 |
lemma A_authenticates_B_r: |
|
540 |
"\<lbrakk> Crypt K (Number Ta) \<in> parts (spies evs); |
|
541 |
Crypt (shrK A) \<lbrace>Number Tk, Agent B, Key K, X\<rbrace> \<in> parts (spies evs); |
|
542 |
Notes Spy \<lbrace>Number Tk, Key K\<rbrace> \<notin> set evs; |
|
543 |
A \<notin> bad; B \<notin> bad; evs \<in> bankerberos \<rbrakk> |
|
544 |
\<Longrightarrow> Says B A (Crypt K (Number Ta)) \<in> set evs" |
|
545 |
apply (blast dest!: Kab_authentic |
|
546 |
intro!: lemma_B elim!: Confidentiality_S [THEN [2] rev_notE]) |
|
547 |
done |
|
548 |
||
549 |
lemma B_authenticates_A: |
|
550 |
"\<lbrakk> Crypt K \<lbrace>Agent A, Number Ta\<rbrace> \<in> parts (spies evs); |
|
551 |
Crypt (shrK B) \<lbrace>Number Tk, Agent A, Key K\<rbrace> \<in> parts (spies evs); |
|
552 |
Key K \<notin> analz (spies evs); |
|
553 |
A \<notin> bad; B \<notin> bad; evs \<in> bankerberos \<rbrakk> |
|
554 |
\<Longrightarrow> Says A B \<lbrace>Crypt (shrK B) \<lbrace>Number Tk, Agent A, Key K\<rbrace>, |
|
555 |
Crypt K \<lbrace>Agent A, Number Ta\<rbrace>\<rbrace> \<in> set evs" |
|
556 |
apply (blast dest!: ticket_authentic intro!: lemma_A) |
|
557 |
done |
|
558 |
||
559 |
lemma A_authenticates_B: |
|
560 |
"\<lbrakk> Crypt K (Number Ta) \<in> parts (spies evs); |
|
561 |
Crypt (shrK A) \<lbrace>Number Tk, Agent B, Key K, X\<rbrace> \<in> parts (spies evs); |
|
562 |
Key K \<notin> analz (spies evs); |
|
563 |
A \<notin> bad; B \<notin> bad; evs \<in> bankerberos \<rbrakk> |
|
564 |
\<Longrightarrow> Says B A (Crypt K (Number Ta)) \<in> set evs" |
|
565 |
apply (blast dest!: Kab_authentic intro!: lemma_B) |
|
566 |
done |
|
567 |
||
568 |
subsection{*Temporal guarantees, relying on a temporal check that insures that |
|
569 |
no oops event occurred. These are available in the sense of goal availability*} |
|
570 |
||
571 |
||
572 |
text{*Temporal treatment of confidentiality*} |
|
573 |
||
574 |
text{* Lemma: the session key sent in msg BK2 would be EXPIRED |
|
575 |
if the spy could see it! *} |
|
576 |
lemma lemma_conf_temporal [rule_format (no_asm)]: |
|
577 |
"\<lbrakk> A \<notin> bad; B \<notin> bad; evs \<in> bankerberos \<rbrakk> |
|
578 |
\<Longrightarrow> Says Server A |
|
579 |
(Crypt (shrK A) \<lbrace>Number Tk, Agent B, Key K, |
|
580 |
Crypt (shrK B) \<lbrace>Number Tk, Agent A, Key K\<rbrace>\<rbrace>) |
|
581 |
\<in> set evs \<longrightarrow> |
|
582 |
Key K \<in> analz (spies evs) \<longrightarrow> expiredK Tk evs" |
|
583 |
apply (erule bankerberos.induct) |
|
13926 | 584 |
apply (frule_tac [7] Says_Server_message_form) |
585 |
apply (frule_tac [5] Says_S_message_form [THEN disjE]) |
|
586 |
apply (simp_all (no_asm_simp) add: less_SucI analz_insert_eq analz_insert_freshK pushes) |
|
587 |
txt{*Fake*} |
|
588 |
apply spy_analz |
|
18886 | 589 |
txt{*BK2*} |
13926 | 590 |
apply (blast intro: parts_insertI less_SucI) |
18886 | 591 |
txt{*BK3*} |
32406 | 592 |
apply (metis Crypt_Spy_analz_bad Kab_authentic Says_imp_analz_Spy |
593 |
Says_imp_parts_knows_Spy analz.Snd less_SucI unique_session_keys) |
|
18886 | 594 |
txt{*Oops: PROOF FAILS if unsafe intro below*} |
13926 | 595 |
apply (blast dest: unique_session_keys intro!: less_SucI) |
596 |
done |
|
5053 | 597 |
|
598 |
||
18886 | 599 |
text{*Confidentiality for the Server: Spy does not see the keys sent in msg BK2 |
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
600 |
as long as they have not expired.*} |
18886 | 601 |
lemma Confidentiality_S_temporal: |
602 |
"\<lbrakk> Says Server A |
|
603 |
(Crypt K' \<lbrace>Number T, Agent B, Key K, X\<rbrace>) \<in> set evs; |
|
604 |
\<not> expiredK T evs; |
|
605 |
A \<notin> bad; B \<notin> bad; evs \<in> bankerberos |
|
606 |
\<rbrakk> \<Longrightarrow> Key K \<notin> analz (spies evs)" |
|
13926 | 607 |
apply (frule Says_Server_message_form, assumption) |
18886 | 608 |
apply (blast intro: lemma_conf_temporal) |
13926 | 609 |
done |
610 |
||
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
611 |
text{*Confidentiality for Alice*} |
18886 | 612 |
lemma Confidentiality_A_temporal: |
613 |
"\<lbrakk> Crypt (shrK A) \<lbrace>Number T, Agent B, Key K, X\<rbrace> \<in> parts (spies evs); |
|
614 |
\<not> expiredK T evs; |
|
615 |
A \<notin> bad; B \<notin> bad; evs \<in> bankerberos |
|
616 |
\<rbrakk> \<Longrightarrow> Key K \<notin> analz (spies evs)" |
|
617 |
apply (blast dest!: Kab_authentic Confidentiality_S_temporal) |
|
618 |
done |
|
13926 | 619 |
|
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
620 |
text{*Confidentiality for Bob*} |
18886 | 621 |
lemma Confidentiality_B_temporal: |
622 |
"\<lbrakk> Crypt (shrK B) \<lbrace>Number Tk, Agent A, Key K\<rbrace> |
|
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
623 |
\<in> parts (spies evs); |
18886 | 624 |
\<not> expiredK Tk evs; |
625 |
A \<notin> bad; B \<notin> bad; evs \<in> bankerberos |
|
626 |
\<rbrakk> \<Longrightarrow> Key K \<notin> analz (spies evs)" |
|
627 |
apply (blast dest!: ticket_authentic Confidentiality_S_temporal) |
|
628 |
done |
|
629 |
||
630 |
text{*Temporal treatment of authentication*} |
|
631 |
||
632 |
text{*Authentication of A to B*} |
|
633 |
lemma B_authenticates_A_temporal: |
|
634 |
"\<lbrakk> Crypt K \<lbrace>Agent A, Number Ta\<rbrace> \<in> parts (spies evs); |
|
635 |
Crypt (shrK B) \<lbrace>Number Tk, Agent A, Key K\<rbrace> |
|
636 |
\<in> parts (spies evs); |
|
637 |
\<not> expiredK Tk evs; |
|
638 |
A \<notin> bad; B \<notin> bad; evs \<in> bankerberos \<rbrakk> |
|
639 |
\<Longrightarrow> Says A B \<lbrace>Crypt (shrK B) \<lbrace>Number Tk, Agent A, Key K\<rbrace>, |
|
640 |
Crypt K \<lbrace>Agent A, Number Ta\<rbrace>\<rbrace> \<in> set evs" |
|
641 |
apply (blast dest!: ticket_authentic |
|
642 |
intro!: lemma_A |
|
643 |
elim!: Confidentiality_S_temporal [THEN [2] rev_notE]) |
|
644 |
done |
|
645 |
||
646 |
text{*Authentication of B to A*} |
|
647 |
lemma A_authenticates_B_temporal: |
|
648 |
"\<lbrakk> Crypt K (Number Ta) \<in> parts (spies evs); |
|
649 |
Crypt (shrK A) \<lbrace>Number Tk, Agent B, Key K, X\<rbrace> |
|
650 |
\<in> parts (spies evs); |
|
651 |
\<not> expiredK Tk evs; |
|
652 |
A \<notin> bad; B \<notin> bad; evs \<in> bankerberos \<rbrakk> |
|
653 |
\<Longrightarrow> Says B A (Crypt K (Number Ta)) \<in> set evs" |
|
654 |
apply (blast dest!: Kab_authentic |
|
655 |
intro!: lemma_B elim!: Confidentiality_S_temporal [THEN [2] rev_notE]) |
|
656 |
done |
|
657 |
||
658 |
subsection{*Treatment of the key distribution goal using trace inspection. All |
|
659 |
guarantees are in non-temporal form, hence non available, though their temporal |
|
660 |
form is trivial to derive. These guarantees also convey a stronger form of |
|
661 |
authentication - non-injective agreement on the session key*} |
|
13926 | 662 |
|
5053 | 663 |
|
18886 | 664 |
lemma B_Issues_A: |
665 |
"\<lbrakk> Says B A (Crypt K (Number Ta)) \<in> set evs; |
|
666 |
Key K \<notin> analz (spies evs); |
|
667 |
A \<notin> bad; B \<notin> bad; evs \<in> bankerberos \<rbrakk> |
|
668 |
\<Longrightarrow> B Issues A with (Crypt K (Number Ta)) on evs" |
|
669 |
apply (simp (no_asm) add: Issues_def) |
|
670 |
apply (rule exI) |
|
671 |
apply (rule conjI, assumption) |
|
672 |
apply (simp (no_asm)) |
|
673 |
apply (erule rev_mp) |
|
674 |
apply (erule rev_mp) |
|
675 |
apply (erule bankerberos.induct, analz_mono_contra) |
|
676 |
apply (simp_all (no_asm_simp)) |
|
677 |
txt{*fake*} |
|
13926 | 678 |
apply blast |
18886 | 679 |
txt{*K4 obviously is the non-trivial case*} |
680 |
apply (simp add: takeWhile_tail) |
|
681 |
apply (blast dest: ticket_authentic parts_spies_takeWhile_mono [THEN subsetD] parts_spies_evs_revD2 [THEN subsetD] intro: A_authenticates_B_temporal) |
|
682 |
done |
|
683 |
||
684 |
lemma A_authenticates_and_keydist_to_B: |
|
685 |
"\<lbrakk> Crypt K (Number Ta) \<in> parts (spies evs); |
|
686 |
Crypt (shrK A) \<lbrace>Number Tk, Agent B, Key K, X\<rbrace> \<in> parts (spies evs); |
|
687 |
Key K \<notin> analz (spies evs); |
|
688 |
A \<notin> bad; B \<notin> bad; evs \<in> bankerberos \<rbrakk> |
|
689 |
\<Longrightarrow> B Issues A with (Crypt K (Number Ta)) on evs" |
|
690 |
apply (blast dest!: A_authenticates_B B_Issues_A) |
|
13926 | 691 |
done |
692 |
||
693 |
||
18886 | 694 |
lemma A_Issues_B: |
695 |
"\<lbrakk> Says A B \<lbrace>Ticket, Crypt K \<lbrace>Agent A, Number Ta\<rbrace>\<rbrace> |
|
696 |
\<in> set evs; |
|
697 |
Key K \<notin> analz (spies evs); |
|
698 |
A \<notin> bad; B \<notin> bad; evs \<in> bankerberos \<rbrakk> |
|
699 |
\<Longrightarrow> A Issues B with (Crypt K \<lbrace>Agent A, Number Ta\<rbrace>) on evs" |
|
700 |
apply (simp (no_asm) add: Issues_def) |
|
701 |
apply (rule exI) |
|
702 |
apply (rule conjI, assumption) |
|
703 |
apply (simp (no_asm)) |
|
704 |
apply (erule rev_mp) |
|
705 |
apply (erule rev_mp) |
|
706 |
apply (erule bankerberos.induct, analz_mono_contra) |
|
707 |
apply (simp_all (no_asm_simp)) |
|
708 |
txt{*fake*} |
|
13926 | 709 |
apply blast |
18886 | 710 |
txt{*K3 is the non trivial case*} |
711 |
apply (simp add: takeWhile_tail) |
|
712 |
apply auto (*Technically unnecessary, merely clarifies the subgoal as it is presemted in the book*) |
|
713 |
apply (blast dest: Kab_authentic Says_Server_message_form parts_spies_takeWhile_mono [THEN subsetD] parts_spies_evs_revD2 [THEN subsetD] |
|
714 |
intro!: B_authenticates_A) |
|
13926 | 715 |
done |
716 |
||
18886 | 717 |
|
718 |
lemma B_authenticates_and_keydist_to_A: |
|
719 |
"\<lbrakk> Crypt K \<lbrace>Agent A, Number Ta\<rbrace> \<in> parts (spies evs); |
|
720 |
Crypt (shrK B) \<lbrace>Number Tk, Agent A, Key K\<rbrace> \<in> parts (spies evs); |
|
721 |
Key K \<notin> analz (spies evs); |
|
722 |
A \<notin> bad; B \<notin> bad; evs \<in> bankerberos \<rbrakk> |
|
723 |
\<Longrightarrow> A Issues B with (Crypt K \<lbrace>Agent A, Number Ta\<rbrace>) on evs" |
|
724 |
apply (blast dest: B_authenticates_A A_Issues_B) |
|
725 |
done |
|
726 |
||
727 |
||
728 |
||
5053 | 729 |
|
730 |
end |