author | haftmann |
Fri, 17 Jun 2005 16:12:49 +0200 | |
changeset 16417 | 9bc16273c2d4 |
parent 14207 | f20fbb141673 |
child 18886 | 9f27383426db |
permissions | -rw-r--r-- |
5053 | 1 |
(* Title: HOL/Auth/Kerberos_BAN |
2 |
ID: $Id$ |
|
3 |
Author: Giampaolo Bella, Cambridge University Computer Laboratory |
|
4 |
Copyright 1998 University of Cambridge |
|
5 |
||
13926 | 6 |
Tidied and converted to Isar by lcp. |
5053 | 7 |
*) |
8 |
||
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
9 |
header{*The Kerberos Protocol, BAN Version*} |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
10 |
|
16417 | 11 |
theory Kerberos_BAN imports Public begin |
5053 | 12 |
|
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
13 |
text{*From page 251 of |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
14 |
Burrows, Abadi and Needham (1989). A Logic of Authentication. |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
15 |
Proc. Royal Soc. 426 |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
16 |
|
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
17 |
Confidentiality (secrecy) and authentication properties rely on |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
18 |
temporal checks: strong guarantees in a little abstracted - but |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
19 |
very realistic - model. |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
20 |
*} |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
21 |
|
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
22 |
(* Temporal modelization: session keys can be leaked |
5053 | 23 |
ONLY when they have expired *) |
24 |
||
25 |
syntax |
|
13926 | 26 |
CT :: "event list=>nat" |
27 |
Expired :: "[nat, event list] => bool" |
|
28 |
RecentAuth :: "[nat, event list] => bool" |
|
5053 | 29 |
|
30 |
consts |
|
31 |
||
32 |
(*Duration of the session key*) |
|
33 |
SesKeyLife :: nat |
|
34 |
||
35 |
(*Duration of the authenticator*) |
|
36 |
AutLife :: nat |
|
37 |
||
14126
28824746d046
Tidying and replacement of some axioms by specifications
paulson
parents:
13926
diff
changeset
|
38 |
text{*The ticket should remain fresh for two journeys on the network at least*} |
28824746d046
Tidying and replacement of some axioms by specifications
paulson
parents:
13926
diff
changeset
|
39 |
specification (SesKeyLife) |
28824746d046
Tidying and replacement of some axioms by specifications
paulson
parents:
13926
diff
changeset
|
40 |
SesKeyLife_LB [iff]: "2 \<le> SesKeyLife" |
28824746d046
Tidying and replacement of some axioms by specifications
paulson
parents:
13926
diff
changeset
|
41 |
by blast |
5053 | 42 |
|
14126
28824746d046
Tidying and replacement of some axioms by specifications
paulson
parents:
13926
diff
changeset
|
43 |
text{*The authenticator only for one journey*} |
28824746d046
Tidying and replacement of some axioms by specifications
paulson
parents:
13926
diff
changeset
|
44 |
specification (AutLife) |
28824746d046
Tidying and replacement of some axioms by specifications
paulson
parents:
13926
diff
changeset
|
45 |
AutLife_LB [iff]: "Suc 0 \<le> AutLife" |
28824746d046
Tidying and replacement of some axioms by specifications
paulson
parents:
13926
diff
changeset
|
46 |
by blast |
28824746d046
Tidying and replacement of some axioms by specifications
paulson
parents:
13926
diff
changeset
|
47 |
|
5053 | 48 |
|
49 |
translations |
|
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
50 |
"CT" == "length " |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
51 |
|
5053 | 52 |
"Expired T evs" == "SesKeyLife + T < CT evs" |
53 |
||
14126
28824746d046
Tidying and replacement of some axioms by specifications
paulson
parents:
13926
diff
changeset
|
54 |
"RecentAuth T evs" == "CT evs \<le> AutLife + T" |
5053 | 55 |
|
13926 | 56 |
consts kerberos_ban :: "event list set" |
5053 | 57 |
inductive "kerberos_ban" |
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
58 |
intros |
13926 | 59 |
|
60 |
Nil: "[] \<in> kerberos_ban" |
|
61 |
||
62 |
Fake: "[| evsf \<in> kerberos_ban; X \<in> synth (analz (spies evsf)) |] |
|
63 |
==> Says Spy B X # evsf \<in> kerberos_ban" |
|
64 |
||
65 |
||
66 |
Kb1: "[| evs1 \<in> kerberos_ban |] |
|
67 |
==> Says A Server {|Agent A, Agent B|} # evs1 |
|
68 |
\<in> kerberos_ban" |
|
69 |
||
70 |
||
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
71 |
Kb2: "[| evs2 \<in> kerberos_ban; Key KAB \<notin> used evs2; KAB \<in> symKeys; |
13926 | 72 |
Says A' Server {|Agent A, Agent B|} \<in> set evs2 |] |
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
73 |
==> Says Server A |
13926 | 74 |
(Crypt (shrK A) |
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
75 |
{|Number (CT evs2), Agent B, Key KAB, |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
76 |
(Crypt (shrK B) {|Number (CT evs2), Agent A, Key KAB|})|}) |
13926 | 77 |
# evs2 \<in> kerberos_ban" |
78 |
||
79 |
||
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
80 |
Kb3: "[| evs3 \<in> kerberos_ban; |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
81 |
Says S A (Crypt (shrK A) {|Number Ts, Agent B, Key K, X|}) |
13926 | 82 |
\<in> set evs3; |
83 |
Says A Server {|Agent A, Agent B|} \<in> set evs3; |
|
84 |
~ Expired Ts evs3 |] |
|
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
85 |
==> Says A B {|X, Crypt K {|Agent A, Number (CT evs3)|} |} |
13926 | 86 |
# evs3 \<in> kerberos_ban" |
87 |
||
88 |
||
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
89 |
Kb4: "[| evs4 \<in> kerberos_ban; |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
90 |
Says A' B {|(Crypt (shrK B) {|Number Ts, Agent A, Key K|}), |
13926 | 91 |
(Crypt K {|Agent A, Number Ta|}) |}: set evs4; |
92 |
~ Expired Ts evs4; RecentAuth Ta evs4 |] |
|
93 |
==> Says B A (Crypt K (Number Ta)) # evs4 |
|
94 |
\<in> kerberos_ban" |
|
5053 | 95 |
|
13926 | 96 |
(*Old session keys may become compromised*) |
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
97 |
Oops: "[| evso \<in> kerberos_ban; |
13926 | 98 |
Says Server A (Crypt (shrK A) {|Number Ts, Agent B, Key K, X|}) |
99 |
\<in> set evso; |
|
100 |
Expired Ts evso |] |
|
101 |
==> Notes Spy {|Number Ts, Key K|} # evso \<in> kerberos_ban" |
|
102 |
||
103 |
||
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
104 |
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
|
105 |
declare parts.Body [dest] |
d8598e24f8fa
Removal of the Key_supply axiom (affects many possbility proofs) and minor
paulson
parents:
14126
diff
changeset
|
106 |
declare analz_into_parts [dest] |
d8598e24f8fa
Removal of the Key_supply axiom (affects many possbility proofs) and minor
paulson
parents:
14126
diff
changeset
|
107 |
declare Fake_parts_insert_in_Un [dest] |
13926 | 108 |
|
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
109 |
text{*A "possibility property": there are traces that reach the end.*} |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
110 |
lemma "[|Key K \<notin> used []; K \<in> symKeys|] |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
111 |
==> \<exists>Timestamp. \<exists>evs \<in> kerberos_ban. |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
112 |
Says B A (Crypt K (Number Timestamp)) |
13926 | 113 |
\<in> set evs" |
114 |
apply (cut_tac SesKeyLife_LB) |
|
115 |
apply (intro exI bexI) |
|
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
116 |
apply (rule_tac [2] |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
117 |
kerberos_ban.Nil [THEN kerberos_ban.Kb1, THEN kerberos_ban.Kb2, |
14200
d8598e24f8fa
Removal of the Key_supply axiom (affects many possbility proofs) and minor
paulson
parents:
14126
diff
changeset
|
118 |
THEN kerberos_ban.Kb3, THEN kerberos_ban.Kb4]) |
d8598e24f8fa
Removal of the Key_supply axiom (affects many possbility proofs) and minor
paulson
parents:
14126
diff
changeset
|
119 |
apply (possibility, simp_all (no_asm_simp) add: used_Cons) |
13926 | 120 |
done |
121 |
||
122 |
||
123 |
(**** Inductive proofs about kerberos_ban ****) |
|
124 |
||
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
125 |
text{*Forwarding Lemma for reasoning about the encrypted portion of message Kb3*} |
13926 | 126 |
lemma Kb3_msg_in_parts_spies: |
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
127 |
"Says S A (Crypt KA {|Timestamp, B, K, X|}) \<in> set evs |
13926 | 128 |
==> X \<in> parts (spies evs)" |
129 |
by blast |
|
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
130 |
|
13926 | 131 |
lemma Oops_parts_spies: |
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
132 |
"Says Server A (Crypt (shrK A) {|Timestamp, B, K, X|}) \<in> set evs |
13926 | 133 |
==> K \<in> parts (spies evs)" |
134 |
by blast |
|
135 |
||
136 |
||
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
137 |
text{*Spy never sees another agent's shared key! (unless it's bad at start)*} |
13926 | 138 |
lemma Spy_see_shrK [simp]: |
139 |
"evs \<in> kerberos_ban ==> (Key (shrK A) \<in> parts (spies evs)) = (A \<in> bad)" |
|
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
140 |
apply (erule kerberos_ban.induct) |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
141 |
apply (frule_tac [7] Oops_parts_spies) |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
142 |
apply (frule_tac [5] Kb3_msg_in_parts_spies, simp_all, blast+) |
13926 | 143 |
done |
5053 | 144 |
|
145 |
||
13926 | 146 |
lemma Spy_analz_shrK [simp]: |
147 |
"evs \<in> kerberos_ban ==> (Key (shrK A) \<in> analz (spies evs)) = (A \<in> bad)" |
|
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
148 |
by auto |
13926 | 149 |
|
150 |
lemma Spy_see_shrK_D [dest!]: |
|
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
151 |
"[| Key (shrK A) \<in> parts (spies evs); |
13926 | 152 |
evs \<in> kerberos_ban |] ==> A:bad" |
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
153 |
by (blast dest: Spy_see_shrK) |
13926 | 154 |
|
155 |
lemmas Spy_analz_shrK_D = analz_subset_parts [THEN subsetD, THEN Spy_see_shrK_D, dest!] |
|
156 |
||
157 |
||
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
158 |
text{*Nobody can have used non-existent keys!*} |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
159 |
lemma new_keys_not_used [simp]: |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
160 |
"[|Key K \<notin> used evs; K \<in> symKeys; evs \<in> kerberos_ban|] |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
161 |
==> K \<notin> keysFor (parts (spies evs))" |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
162 |
apply (erule rev_mp) |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
163 |
apply (erule kerberos_ban.induct) |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
164 |
apply (frule_tac [7] Oops_parts_spies) |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
165 |
apply (frule_tac [5] Kb3_msg_in_parts_spies, simp_all) |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
166 |
txt{*Fake*} |
13926 | 167 |
apply (force dest!: keysFor_parts_insert) |
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
168 |
txt{*Kb2, Kb3, Kb4*} |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
169 |
apply (force dest!: analz_shrK_Decrypt)+ |
13926 | 170 |
done |
171 |
||
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
172 |
subsection{* Lemmas concerning the form of items passed in messages *} |
13926 | 173 |
|
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
174 |
text{*Describes the form of K, X and K' when the Server sends this message.*} |
13926 | 175 |
lemma Says_Server_message_form: |
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
176 |
"[| Says Server A (Crypt K' {|Number Ts, Agent B, Key K, X|}) |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
177 |
\<in> set evs; evs \<in> kerberos_ban |] |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
178 |
==> K \<notin> range shrK & |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
179 |
X = (Crypt (shrK B) {|Number Ts, Agent A, Key K|}) & |
13926 | 180 |
K' = shrK A" |
181 |
apply (erule rev_mp) |
|
182 |
apply (erule kerberos_ban.induct, auto) |
|
183 |
done |
|
5053 | 184 |
|
185 |
||
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
186 |
text{*If the encrypted message appears then it originated with the Server |
13926 | 187 |
PROVIDED that A is NOT compromised! |
188 |
||
189 |
This shows implicitly the FRESHNESS OF THE SESSION KEY to A |
|
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
190 |
*} |
13926 | 191 |
lemma A_trusts_K_by_Kb2: |
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
192 |
"[| Crypt (shrK A) {|Number Ts, Agent B, Key K, X|} |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
193 |
\<in> parts (spies evs); |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
194 |
A \<notin> bad; evs \<in> kerberos_ban |] |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
195 |
==> Says Server A (Crypt (shrK A) {|Number Ts, Agent B, Key K, X|}) |
13926 | 196 |
\<in> set evs" |
197 |
apply (erule rev_mp) |
|
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
198 |
apply (erule kerberos_ban.induct) |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
199 |
apply (frule_tac [7] Oops_parts_spies) |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
200 |
apply (frule_tac [5] Kb3_msg_in_parts_spies, simp_all, blast) |
13926 | 201 |
done |
202 |
||
203 |
||
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
204 |
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
|
205 |
text{*FRESHNESS OF THE SESSION KEY to B*} |
13926 | 206 |
lemma B_trusts_K_by_Kb3: |
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
207 |
"[| Crypt (shrK B) {|Number Ts, Agent A, Key K|} \<in> parts (spies evs); |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
208 |
B \<notin> bad; evs \<in> kerberos_ban |] |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
209 |
==> Says Server A |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
210 |
(Crypt (shrK A) {|Number Ts, Agent B, Key K, |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
211 |
Crypt (shrK B) {|Number Ts, Agent A, Key K|}|}) |
13926 | 212 |
\<in> set evs" |
213 |
apply (erule rev_mp) |
|
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
214 |
apply (erule kerberos_ban.induct) |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
215 |
apply (frule_tac [7] Oops_parts_spies) |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
216 |
apply (frule_tac [5] Kb3_msg_in_parts_spies, simp_all, blast) |
13926 | 217 |
done |
218 |
||
219 |
||
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
220 |
text{*EITHER describes the form of X when the following message is sent, |
13926 | 221 |
OR reduces it to the Fake case. |
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
222 |
Use @{text Says_Server_message_form} if applicable.*} |
13926 | 223 |
lemma Says_S_message_form: |
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
224 |
"[| Says S A (Crypt (shrK A) {|Number Ts, Agent B, Key K, X|}) |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
225 |
\<in> set evs; |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
226 |
evs \<in> kerberos_ban |] |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
227 |
==> (K \<notin> range shrK & X = (Crypt (shrK B) {|Number Ts, Agent A, Key K|})) |
13926 | 228 |
| X \<in> analz (spies evs)" |
229 |
apply (case_tac "A \<in> bad") |
|
230 |
apply (force dest!: Says_imp_spies [THEN analz.Inj]) |
|
231 |
apply (frule Says_imp_spies [THEN parts.Inj]) |
|
232 |
apply (blast dest!: A_trusts_K_by_Kb2 Says_Server_message_form) |
|
233 |
done |
|
234 |
||
5053 | 235 |
|
236 |
||
13926 | 237 |
(**** |
238 |
The following is to prove theorems of the form |
|
239 |
||
240 |
Key K \<in> analz (insert (Key KAB) (spies evs)) ==> |
|
241 |
Key K \<in> analz (spies evs) |
|
242 |
||
243 |
A more general formula must be proved inductively. |
|
244 |
||
245 |
****) |
|
246 |
||
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
247 |
text{* Session keys are not used to encrypt other session keys *} |
13926 | 248 |
lemma analz_image_freshK [rule_format (no_asm)]: |
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
249 |
"evs \<in> kerberos_ban ==> |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
250 |
\<forall>K KK. KK \<subseteq> - (range shrK) --> |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
251 |
(Key K \<in> analz (Key`KK Un (spies evs))) = |
13926 | 252 |
(K \<in> KK | Key K \<in> analz (spies evs))" |
253 |
apply (erule kerberos_ban.induct) |
|
254 |
apply (drule_tac [7] Says_Server_message_form) |
|
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
255 |
apply (erule_tac [5] Says_S_message_form [THEN disjE], analz_freshK, spy_analz, auto) |
13926 | 256 |
done |
257 |
||
258 |
||
259 |
lemma analz_insert_freshK: |
|
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
260 |
"[| evs \<in> kerberos_ban; KAB \<notin> range shrK |] ==> |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
261 |
(Key K \<in> analz (insert (Key KAB) (spies evs))) = |
13926 | 262 |
(K = KAB | Key K \<in> analz (spies evs))" |
263 |
by (simp only: analz_image_freshK analz_image_freshK_simps) |
|
264 |
||
265 |
||
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
266 |
text{* The session key K uniquely identifies the message *} |
13926 | 267 |
lemma unique_session_keys: |
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
268 |
"[| Says Server A |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
269 |
(Crypt (shrK A) {|Number Ts, Agent B, Key K, X|}) \<in> set evs; |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
270 |
Says Server A' |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
271 |
(Crypt (shrK A') {|Number Ts', Agent B', Key K, X'|}) \<in> set evs; |
13926 | 272 |
evs \<in> kerberos_ban |] ==> A=A' & Ts=Ts' & B=B' & X = X'" |
273 |
apply (erule rev_mp) |
|
274 |
apply (erule rev_mp) |
|
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
275 |
apply (erule kerberos_ban.induct) |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
276 |
apply (frule_tac [7] Oops_parts_spies) |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
277 |
apply (frule_tac [5] Kb3_msg_in_parts_spies, simp_all) |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
278 |
txt{*Kb2: it can't be a new key*} |
13926 | 279 |
apply blast |
280 |
done |
|
281 |
||
282 |
||
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
283 |
text{* Lemma: the session key sent in msg Kb2 would be EXPIRED |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
284 |
if the spy could see it! *} |
13926 | 285 |
|
286 |
lemma lemma2 [rule_format (no_asm)]: |
|
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
287 |
"[| A \<notin> bad; B \<notin> bad; evs \<in> kerberos_ban |] |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
288 |
==> Says Server A |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
289 |
(Crypt (shrK A) {|Number Ts, Agent B, Key K, |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
290 |
Crypt (shrK B) {|Number Ts, Agent A, Key K|}|}) |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
291 |
\<in> set evs --> |
13926 | 292 |
Key K \<in> analz (spies evs) --> Expired Ts evs" |
293 |
apply (erule kerberos_ban.induct) |
|
294 |
apply (frule_tac [7] Says_Server_message_form) |
|
295 |
apply (frule_tac [5] Says_S_message_form [THEN disjE]) |
|
296 |
apply (simp_all (no_asm_simp) add: less_SucI analz_insert_eq analz_insert_freshK pushes) |
|
297 |
txt{*Fake*} |
|
298 |
apply spy_analz |
|
299 |
txt{*Kb2*} |
|
300 |
apply (blast intro: parts_insertI less_SucI) |
|
301 |
txt{*Kb3*} |
|
302 |
apply (case_tac "Aa \<in> bad") |
|
303 |
prefer 2 apply (blast dest: A_trusts_K_by_Kb2 unique_session_keys) |
|
304 |
apply (blast dest: Says_imp_spies [THEN analz.Inj] Crypt_Spy_analz_bad elim!: MPair_analz intro: less_SucI) |
|
305 |
txt{*Oops: PROOF FAILED if addIs below*} |
|
306 |
apply (blast dest: unique_session_keys intro!: less_SucI) |
|
307 |
done |
|
5053 | 308 |
|
309 |
||
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
310 |
text{*Confidentiality for the Server: Spy does not see the keys sent in msg Kb2 |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
311 |
as long as they have not expired.*} |
13926 | 312 |
lemma Confidentiality_S: |
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
313 |
"[| Says Server A |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
314 |
(Crypt K' {|Number T, Agent B, Key K, X|}) \<in> set evs; |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
315 |
~ Expired T evs; |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
316 |
A \<notin> bad; B \<notin> bad; evs \<in> kerberos_ban |
13926 | 317 |
|] ==> Key K \<notin> analz (spies evs)" |
318 |
apply (frule Says_Server_message_form, assumption) |
|
319 |
apply (blast intro: lemma2) |
|
320 |
done |
|
321 |
||
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
322 |
(**** THE COUNTERPART OF CONFIDENTIALITY |
13926 | 323 |
[|...; Expired Ts evs; ...|] ==> Key K \<in> analz (spies evs) |
324 |
WOULD HOLD ONLY IF AN OOPS OCCURRED! ---> Nothing to prove! ****) |
|
325 |
||
326 |
||
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
327 |
text{*Confidentiality for Alice*} |
13926 | 328 |
lemma Confidentiality_A: |
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
329 |
"[| Crypt (shrK A) {|Number T, Agent B, Key K, X|} \<in> parts (spies evs); |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
330 |
~ Expired T evs; |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
331 |
A \<notin> bad; B \<notin> bad; evs \<in> kerberos_ban |
13926 | 332 |
|] ==> Key K \<notin> analz (spies evs)" |
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
333 |
by (blast dest!: A_trusts_K_by_Kb2 Confidentiality_S) |
13926 | 334 |
|
335 |
||
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
336 |
text{*Confidentiality for Bob*} |
13926 | 337 |
lemma Confidentiality_B: |
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
338 |
"[| Crypt (shrK B) {|Number Tk, Agent A, Key K|} |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
339 |
\<in> parts (spies evs); |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
340 |
~ Expired Tk evs; |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
341 |
A \<notin> bad; B \<notin> bad; evs \<in> kerberos_ban |
13926 | 342 |
|] ==> Key K \<notin> analz (spies evs)" |
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
343 |
by (blast dest!: B_trusts_K_by_Kb3 Confidentiality_S) |
13926 | 344 |
|
5053 | 345 |
|
13926 | 346 |
lemma lemma_B [rule_format]: |
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
347 |
"[| B \<notin> bad; evs \<in> kerberos_ban |] |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
348 |
==> Key K \<notin> analz (spies evs) --> |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
349 |
Says Server A (Crypt (shrK A) {|Number Ts, Agent B, Key K, X|}) |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
350 |
\<in> set evs --> |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
351 |
Crypt K (Number Ta) \<in> parts (spies evs) --> |
13926 | 352 |
Says B A (Crypt K (Number Ta)) \<in> set evs" |
353 |
apply (erule kerberos_ban.induct) |
|
354 |
apply (frule_tac [7] Oops_parts_spies) |
|
355 |
apply (frule_tac [5] Says_S_message_form) |
|
356 |
apply (drule_tac [6] Kb3_msg_in_parts_spies, analz_mono_contra) |
|
357 |
apply (simp_all (no_asm_simp) add: all_conj_distrib) |
|
358 |
txt{*Fake*} |
|
359 |
apply blast |
|
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
360 |
txt{*Kb2*} |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
361 |
apply (force dest: Crypt_imp_invKey_keysFor) |
13926 | 362 |
txt{*Kb4*} |
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
363 |
apply (blast dest: B_trusts_K_by_Kb3 unique_session_keys |
13926 | 364 |
Says_imp_spies [THEN analz.Inj] Crypt_Spy_analz_bad) |
365 |
done |
|
366 |
||
367 |
||
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
368 |
text{*Authentication of B to A*} |
13926 | 369 |
lemma Authentication_B: |
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
370 |
"[| Crypt K (Number Ta) \<in> parts (spies evs); |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
371 |
Crypt (shrK A) {|Number Ts, Agent B, Key K, X|} |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
372 |
\<in> parts (spies evs); |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
373 |
~ Expired Ts evs; |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
374 |
A \<notin> bad; B \<notin> bad; evs \<in> kerberos_ban |] |
13926 | 375 |
==> Says B A (Crypt K (Number Ta)) \<in> set evs" |
376 |
by (blast dest!: A_trusts_K_by_Kb2 |
|
377 |
intro!: lemma_B elim!: Confidentiality_S [THEN [2] rev_notE]) |
|
378 |
||
379 |
lemma lemma_A [rule_format]: |
|
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
380 |
"[| A \<notin> bad; B \<notin> bad; evs \<in> kerberos_ban |] |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
381 |
==> |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
382 |
Key K \<notin> analz (spies evs) --> |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
383 |
Says Server A (Crypt (shrK A) {|Number Ts, Agent B, Key K, X|}) |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
384 |
\<in> set evs --> |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
385 |
Crypt K {|Agent A, Number Ta|} \<in> parts (spies evs) --> |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
386 |
Says A B {|X, Crypt K {|Agent A, Number Ta|}|} |
13926 | 387 |
\<in> set evs" |
388 |
apply (erule kerberos_ban.induct) |
|
389 |
apply (frule_tac [7] Oops_parts_spies) |
|
390 |
apply (frule_tac [5] Says_S_message_form) |
|
391 |
apply (frule_tac [6] Kb3_msg_in_parts_spies, analz_mono_contra) |
|
392 |
apply (simp_all (no_asm_simp) add: all_conj_distrib) |
|
393 |
txt{*Fake*} |
|
394 |
apply blast |
|
395 |
txt{*Kb2*} |
|
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
396 |
apply (force dest: Crypt_imp_invKey_keysFor) |
13926 | 397 |
txt{*Kb3*} |
398 |
apply (blast dest: A_trusts_K_by_Kb2 unique_session_keys) |
|
399 |
done |
|
400 |
||
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
401 |
text{*Authentication of A to B*} |
13926 | 402 |
lemma Authentication_A: |
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
403 |
"[| Crypt K {|Agent A, Number Ta|} \<in> parts (spies evs); |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
404 |
Crypt (shrK B) {|Number Ts, Agent A, Key K|} |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
405 |
\<in> parts (spies evs); |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
406 |
~ Expired Ts evs; |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
407 |
A \<notin> bad; B \<notin> bad; evs \<in> kerberos_ban |] |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
408 |
==> Says A B {|Crypt (shrK B) {|Number Ts, Agent A, Key K|}, |
13926 | 409 |
Crypt K {|Agent A, Number Ta|}|} \<in> set evs" |
410 |
by (blast dest!: B_trusts_K_by_Kb3 |
|
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
411 |
intro!: lemma_A |
13926 | 412 |
elim!: Confidentiality_S [THEN [2] rev_notE]) |
5053 | 413 |
|
414 |
end |