author | haftmann |
Fri, 11 Jun 2010 17:14:02 +0200 | |
changeset 37407 | 61dd8c145da7 |
parent 36866 | 426d5781bb25 |
child 37936 | 1e4c5015a72e |
permissions | -rw-r--r-- |
1934 | 1 |
(* Title: HOL/Auth/NS_Shared |
2 |
ID: $Id$ |
|
18886 | 3 |
Author: Lawrence C Paulson and Giampaolo Bella |
1934 | 4 |
Copyright 1996 University of Cambridge |
5 |
*) |
|
6 |
||
18886 | 7 |
header{*Needham-Schroeder Shared-Key Protocol and the Issues Property*} |
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
8 |
|
16417 | 9 |
theory NS_Shared imports Public begin |
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
10 |
|
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
11 |
text{* |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
12 |
From page 247 of |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
13 |
Burrows, Abadi and Needham (1989). A Logic of Authentication. |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
14 |
Proc. Royal Soc. 426 |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
15 |
*} |
1934 | 16 |
|
36866 | 17 |
definition |
18886 | 18 |
(* A is the true creator of X if she has sent X and X never appeared on |
19 |
the trace before this event. Recall that traces grow from head. *) |
|
20 |
Issues :: "[agent, agent, msg, event list] => bool" |
|
36866 | 21 |
("_ Issues _ with _ on _") where |
22 |
"A Issues B with X on evs = |
|
23 |
(\<exists>Y. Says A B Y \<in> set evs & X \<in> parts {Y} & |
|
24 |
X \<notin> parts (spies (takeWhile (% z. z \<noteq> Says A B Y) (rev evs))))" |
|
18886 | 25 |
|
26 |
||
23746 | 27 |
inductive_set ns_shared :: "event list set" |
28 |
where |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32527
diff
changeset
|
29 |
(*Initial trace is empty*) |
13926 | 30 |
Nil: "[] \<in> ns_shared" |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32527
diff
changeset
|
31 |
(*The spy MAY say anything he CAN say. We do not expect him to |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32527
diff
changeset
|
32 |
invent new nonces here, but he can also use NS1. Common to |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32527
diff
changeset
|
33 |
all similar protocols.*) |
23746 | 34 |
| Fake: "\<lbrakk>evsf \<in> ns_shared; X \<in> synth (analz (spies evsf))\<rbrakk> |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32527
diff
changeset
|
35 |
\<Longrightarrow> Says Spy B X # evsf \<in> ns_shared" |
11104 | 36 |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32527
diff
changeset
|
37 |
(*Alice initiates a protocol run, requesting to talk to any B*) |
23746 | 38 |
| NS1: "\<lbrakk>evs1 \<in> ns_shared; Nonce NA \<notin> used evs1\<rbrakk> |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32527
diff
changeset
|
39 |
\<Longrightarrow> Says A Server \<lbrace>Agent A, Agent B, Nonce NA\<rbrace> # evs1 \<in> ns_shared" |
11104 | 40 |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32527
diff
changeset
|
41 |
(*Server's response to Alice's message. |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32527
diff
changeset
|
42 |
!! It may respond more than once to A's request !! |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32527
diff
changeset
|
43 |
Server doesn't know who the true sender is, hence the A' in |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32527
diff
changeset
|
44 |
the sender field.*) |
23746 | 45 |
| NS2: "\<lbrakk>evs2 \<in> ns_shared; Key KAB \<notin> used evs2; KAB \<in> symKeys; |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32527
diff
changeset
|
46 |
Says A' Server \<lbrace>Agent A, Agent B, Nonce NA\<rbrace> \<in> set evs2\<rbrakk> |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32527
diff
changeset
|
47 |
\<Longrightarrow> Says Server A |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32527
diff
changeset
|
48 |
(Crypt (shrK A) |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32527
diff
changeset
|
49 |
\<lbrace>Nonce NA, Agent B, Key KAB, |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32527
diff
changeset
|
50 |
(Crypt (shrK B) \<lbrace>Key KAB, Agent A\<rbrace>)\<rbrace>) |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32527
diff
changeset
|
51 |
# evs2 \<in> ns_shared" |
11104 | 52 |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32527
diff
changeset
|
53 |
(*We can't assume S=Server. Agent A "remembers" her nonce. |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32527
diff
changeset
|
54 |
Need A \<noteq> Server because we allow messages to self.*) |
23746 | 55 |
| NS3: "\<lbrakk>evs3 \<in> ns_shared; A \<noteq> Server; |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32527
diff
changeset
|
56 |
Says S A (Crypt (shrK A) \<lbrace>Nonce NA, Agent B, Key K, X\<rbrace>) \<in> set evs3; |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32527
diff
changeset
|
57 |
Says A Server \<lbrace>Agent A, Agent B, Nonce NA\<rbrace> \<in> set evs3\<rbrakk> |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32527
diff
changeset
|
58 |
\<Longrightarrow> Says A B X # evs3 \<in> ns_shared" |
11104 | 59 |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32527
diff
changeset
|
60 |
(*Bob's nonce exchange. He does not know who the message came |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32527
diff
changeset
|
61 |
from, but responds to A because she is mentioned inside.*) |
23746 | 62 |
| NS4: "\<lbrakk>evs4 \<in> ns_shared; Nonce NB \<notin> used evs4; K \<in> symKeys; |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32527
diff
changeset
|
63 |
Says A' B (Crypt (shrK B) \<lbrace>Key K, Agent A\<rbrace>) \<in> set evs4\<rbrakk> |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32527
diff
changeset
|
64 |
\<Longrightarrow> Says B A (Crypt K (Nonce NB)) # evs4 \<in> ns_shared" |
1934 | 65 |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32527
diff
changeset
|
66 |
(*Alice responds with Nonce NB if she has seen the key before. |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32527
diff
changeset
|
67 |
Maybe should somehow check Nonce NA again. |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32527
diff
changeset
|
68 |
We do NOT send NB-1 or similar as the Spy cannot spoof such things. |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32527
diff
changeset
|
69 |
Letting the Spy add or subtract 1 lets him send all nonces. |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32527
diff
changeset
|
70 |
Instead we distinguish the messages by sending the nonce twice.*) |
23746 | 71 |
| NS5: "\<lbrakk>evs5 \<in> ns_shared; K \<in> symKeys; |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32527
diff
changeset
|
72 |
Says B' A (Crypt K (Nonce NB)) \<in> set evs5; |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32527
diff
changeset
|
73 |
Says S A (Crypt (shrK A) \<lbrace>Nonce NA, Agent B, Key K, X\<rbrace>) |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32527
diff
changeset
|
74 |
\<in> set evs5\<rbrakk> |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32527
diff
changeset
|
75 |
\<Longrightarrow> Says A B (Crypt K \<lbrace>Nonce NB, Nonce NB\<rbrace>) # evs5 \<in> ns_shared" |
11104 | 76 |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32527
diff
changeset
|
77 |
(*This message models possible leaks of session keys. |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32527
diff
changeset
|
78 |
The two Nonces identify the protocol run: the rule insists upon |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32527
diff
changeset
|
79 |
the true senders in order to make them accurate.*) |
23746 | 80 |
| Oops: "\<lbrakk>evso \<in> ns_shared; Says B A (Crypt K (Nonce NB)) \<in> set evso; |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32527
diff
changeset
|
81 |
Says Server A (Crypt (shrK A) \<lbrace>Nonce NA, Agent B, Key K, X\<rbrace>) |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32527
diff
changeset
|
82 |
\<in> set evso\<rbrakk> |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32527
diff
changeset
|
83 |
\<Longrightarrow> Notes Spy \<lbrace>Nonce NA, Nonce NB, Key K\<rbrace> # evso \<in> ns_shared" |
11104 | 84 |
|
11150 | 85 |
|
86 |
declare Says_imp_knows_Spy [THEN parts.Inj, dest] |
|
87 |
declare parts.Body [dest] |
|
11251 | 88 |
declare Fake_parts_insert_in_Un [dest] |
89 |
declare analz_into_parts [dest] |
|
11104 | 90 |
declare image_eq_UN [simp] (*accelerates proofs involving nested images*) |
91 |
||
92 |
||
13926 | 93 |
text{*A "possibility property": there are traces that reach the end*} |
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
94 |
lemma "[| A \<noteq> Server; Key K \<notin> used []; K \<in> symKeys |] |
14200
d8598e24f8fa
Removal of the Key_supply axiom (affects many possbility proofs) and minor
paulson
parents:
13956
diff
changeset
|
95 |
==> \<exists>N. \<exists>evs \<in> ns_shared. |
d8598e24f8fa
Removal of the Key_supply axiom (affects many possbility proofs) and minor
paulson
parents:
13956
diff
changeset
|
96 |
Says A B (Crypt K \<lbrace>Nonce N, Nonce N\<rbrace>) \<in> set evs" |
11104 | 97 |
apply (intro exI bexI) |
98 |
apply (rule_tac [2] ns_shared.Nil |
|
99 |
[THEN ns_shared.NS1, THEN ns_shared.NS2, THEN ns_shared.NS3, |
|
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32527
diff
changeset
|
100 |
THEN ns_shared.NS4, THEN ns_shared.NS5]) |
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
101 |
apply (possibility, simp add: used_Cons) |
11104 | 102 |
done |
103 |
||
104 |
(*This version is similar, while instantiating ?K and ?N to epsilon-terms |
|
13926 | 105 |
lemma "A \<noteq> Server \<Longrightarrow> \<exists>evs \<in> ns_shared. |
106 |
Says A B (Crypt ?K \<lbrace>Nonce ?N, Nonce ?N\<rbrace>) \<in> set evs" |
|
11104 | 107 |
*) |
108 |
||
109 |
||
13926 | 110 |
subsection{*Inductive proofs about @{term ns_shared}*} |
11104 | 111 |
|
13926 | 112 |
subsubsection{*Forwarding lemmas, to aid simplification*} |
1934 | 113 |
|
13926 | 114 |
text{*For reasoning about the encrypted portion of message NS3*} |
11104 | 115 |
lemma NS3_msg_in_parts_spies: |
13926 | 116 |
"Says S A (Crypt KA \<lbrace>N, B, K, X\<rbrace>) \<in> set evs \<Longrightarrow> X \<in> parts (spies evs)" |
11104 | 117 |
by blast |
11280 | 118 |
|
13926 | 119 |
text{*For reasoning about the Oops message*} |
11104 | 120 |
lemma Oops_parts_spies: |
13926 | 121 |
"Says Server A (Crypt (shrK A) \<lbrace>NA, B, K, X\<rbrace>) \<in> set evs |
122 |
\<Longrightarrow> K \<in> parts (spies evs)" |
|
11104 | 123 |
by blast |
124 |
||
13926 | 125 |
text{*Theorems of the form @{term "X \<notin> parts (spies evs)"} imply that NOBODY |
126 |
sends messages containing @{term X}*} |
|
11104 | 127 |
|
13926 | 128 |
text{*Spy never sees another agent's shared key! (unless it's bad at start)*} |
11104 | 129 |
lemma Spy_see_shrK [simp]: |
13926 | 130 |
"evs \<in> ns_shared \<Longrightarrow> (Key (shrK A) \<in> parts (spies evs)) = (A \<in> bad)" |
13507 | 131 |
apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies, simp_all, blast+) |
11104 | 132 |
done |
133 |
||
134 |
lemma Spy_analz_shrK [simp]: |
|
13926 | 135 |
"evs \<in> ns_shared \<Longrightarrow> (Key (shrK A) \<in> analz (spies evs)) = (A \<in> bad)" |
11104 | 136 |
by auto |
137 |
||
138 |
||
13926 | 139 |
text{*Nobody can have used non-existent keys!*} |
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
140 |
lemma new_keys_not_used [simp]: |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
141 |
"[|Key K \<notin> used evs; K \<in> symKeys; evs \<in> ns_shared|] |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
142 |
==> K \<notin> keysFor (parts (spies evs))" |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
143 |
apply (erule rev_mp) |
13507 | 144 |
apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies, simp_all) |
13926 | 145 |
txt{*Fake, NS2, NS4, NS5*} |
146 |
apply (force dest!: keysFor_parts_insert, blast+) |
|
11104 | 147 |
done |
148 |
||
149 |
||
13926 | 150 |
subsubsection{*Lemmas concerning the form of items passed in messages*} |
11104 | 151 |
|
13926 | 152 |
text{*Describes the form of K, X and K' when the Server sends this message.*} |
11104 | 153 |
lemma Says_Server_message_form: |
13926 | 154 |
"\<lbrakk>Says Server A (Crypt K' \<lbrace>N, Agent B, Key K, X\<rbrace>) \<in> set evs; |
155 |
evs \<in> ns_shared\<rbrakk> |
|
156 |
\<Longrightarrow> K \<notin> range shrK \<and> |
|
157 |
X = (Crypt (shrK B) \<lbrace>Key K, Agent A\<rbrace>) \<and> |
|
11104 | 158 |
K' = shrK A" |
159 |
by (erule rev_mp, erule ns_shared.induct, auto) |
|
160 |
||
1934 | 161 |
|
13926 | 162 |
text{*If the encrypted message appears then it originated with the Server*} |
11104 | 163 |
lemma A_trusts_NS2: |
13926 | 164 |
"\<lbrakk>Crypt (shrK A) \<lbrace>NA, Agent B, Key K, X\<rbrace> \<in> parts (spies evs); |
165 |
A \<notin> bad; evs \<in> ns_shared\<rbrakk> |
|
166 |
\<Longrightarrow> Says Server A (Crypt (shrK A) \<lbrace>NA, Agent B, Key K, X\<rbrace>) \<in> set evs" |
|
11104 | 167 |
apply (erule rev_mp) |
13507 | 168 |
apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies, auto) |
11104 | 169 |
done |
170 |
||
171 |
lemma cert_A_form: |
|
13926 | 172 |
"\<lbrakk>Crypt (shrK A) \<lbrace>NA, Agent B, Key K, X\<rbrace> \<in> parts (spies evs); |
173 |
A \<notin> bad; evs \<in> ns_shared\<rbrakk> |
|
174 |
\<Longrightarrow> K \<notin> range shrK \<and> X = (Crypt (shrK B) \<lbrace>Key K, Agent A\<rbrace>)" |
|
11104 | 175 |
by (blast dest!: A_trusts_NS2 Says_Server_message_form) |
176 |
||
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
177 |
text{*EITHER describes the form of X when the following message is sent, |
11104 | 178 |
OR reduces it to the Fake case. |
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
179 |
Use @{text Says_Server_message_form} if applicable.*} |
11104 | 180 |
lemma Says_S_message_form: |
13926 | 181 |
"\<lbrakk>Says S A (Crypt (shrK A) \<lbrace>Nonce NA, Agent B, Key K, X\<rbrace>) \<in> set evs; |
182 |
evs \<in> ns_shared\<rbrakk> |
|
183 |
\<Longrightarrow> (K \<notin> range shrK \<and> X = (Crypt (shrK B) \<lbrace>Key K, Agent A\<rbrace>)) |
|
184 |
\<or> X \<in> analz (spies evs)" |
|
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
185 |
by (blast dest: Says_imp_knows_Spy analz_shrK_Decrypt cert_A_form analz.Inj) |
11150 | 186 |
|
11104 | 187 |
|
188 |
(*Alternative version also provable |
|
189 |
lemma Says_S_message_form2: |
|
13926 | 190 |
"\<lbrakk>Says S A (Crypt (shrK A) \<lbrace>Nonce NA, Agent B, Key K, X\<rbrace>) \<in> set evs; |
191 |
evs \<in> ns_shared\<rbrakk> |
|
192 |
\<Longrightarrow> Says Server A (Crypt (shrK A) \<lbrace>Nonce NA, Agent B, Key K, X\<rbrace>) \<in> set evs |
|
193 |
\<or> X \<in> analz (spies evs)" |
|
194 |
apply (case_tac "A \<in> bad") |
|
13507 | 195 |
apply (force dest!: Says_imp_knows_Spy [THEN analz.Inj]) |
11104 | 196 |
by (blast dest!: A_trusts_NS2 Says_Server_message_form) |
197 |
*) |
|
198 |
||
199 |
||
200 |
(**** |
|
201 |
SESSION KEY COMPROMISE THEOREM. To prove theorems of the form |
|
202 |
||
13926 | 203 |
Key K \<in> analz (insert (Key KAB) (spies evs)) \<Longrightarrow> |
204 |
Key K \<in> analz (spies evs) |
|
11104 | 205 |
|
206 |
A more general formula must be proved inductively. |
|
207 |
****) |
|
1934 | 208 |
|
13926 | 209 |
text{*NOT useful in this form, but it says that session keys are not used |
11104 | 210 |
to encrypt messages containing other keys, in the actual protocol. |
13926 | 211 |
We require that agents should behave like this subsequently also.*} |
212 |
lemma "\<lbrakk>evs \<in> ns_shared; Kab \<notin> range shrK\<rbrakk> \<Longrightarrow> |
|
213 |
(Crypt KAB X) \<in> parts (spies evs) \<and> |
|
214 |
Key K \<in> parts {X} \<longrightarrow> Key K \<in> parts (spies evs)" |
|
13507 | 215 |
apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies, simp_all) |
13926 | 216 |
txt{*Fake*} |
11104 | 217 |
apply (blast dest: parts_insert_subset_Un) |
13926 | 218 |
txt{*Base, NS4 and NS5*} |
11104 | 219 |
apply auto |
220 |
done |
|
221 |
||
222 |
||
13926 | 223 |
subsubsection{*Session keys are not used to encrypt other session keys*} |
11104 | 224 |
|
13926 | 225 |
text{*The equality makes the induction hypothesis easier to apply*} |
11104 | 226 |
|
227 |
lemma analz_image_freshK [rule_format]: |
|
13926 | 228 |
"evs \<in> ns_shared \<Longrightarrow> |
229 |
\<forall>K KK. KK \<subseteq> - (range shrK) \<longrightarrow> |
|
230 |
(Key K \<in> analz (Key`KK \<union> (spies evs))) = |
|
231 |
(K \<in> KK \<or> Key K \<in> analz (spies evs))" |
|
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
232 |
apply (erule ns_shared.induct) |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
233 |
apply (drule_tac [8] Says_Server_message_form) |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
234 |
apply (erule_tac [5] Says_S_message_form [THEN disjE], analz_freshK, spy_analz) |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
235 |
txt{*NS2, NS3*} |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
236 |
apply blast+; |
11104 | 237 |
done |
238 |
||
239 |
||
240 |
lemma analz_insert_freshK: |
|
13926 | 241 |
"\<lbrakk>evs \<in> ns_shared; KAB \<notin> range shrK\<rbrakk> \<Longrightarrow> |
242 |
(Key K \<in> analz (insert (Key KAB) (spies evs))) = |
|
243 |
(K = KAB \<or> Key K \<in> analz (spies evs))" |
|
11104 | 244 |
by (simp only: analz_image_freshK analz_image_freshK_simps) |
245 |
||
246 |
||
13926 | 247 |
subsubsection{*The session key K uniquely identifies the message*} |
1934 | 248 |
|
13926 | 249 |
text{*In messages of this form, the session key uniquely identifies the rest*} |
11104 | 250 |
lemma unique_session_keys: |
13926 | 251 |
"\<lbrakk>Says Server A (Crypt (shrK A) \<lbrace>NA, Agent B, Key K, X\<rbrace>) \<in> set evs; |
252 |
Says Server A' (Crypt (shrK A') \<lbrace>NA', Agent B', Key K, X'\<rbrace>) \<in> set evs; |
|
253 |
evs \<in> ns_shared\<rbrakk> \<Longrightarrow> A=A' \<and> NA=NA' \<and> B=B' \<and> X = X'" |
|
18886 | 254 |
by (erule rev_mp, erule rev_mp, erule ns_shared.induct, simp_all, blast+) |
11104 | 255 |
|
256 |
||
18886 | 257 |
subsubsection{*Crucial secrecy property: Spy doesn't see the keys sent in NS2*} |
11104 | 258 |
|
13956 | 259 |
text{*Beware of @{text "[rule_format]"} and the universal quantifier!*} |
11150 | 260 |
lemma secrecy_lemma: |
13926 | 261 |
"\<lbrakk>Says Server A (Crypt (shrK A) \<lbrace>NA, Agent B, Key K, |
262 |
Crypt (shrK B) \<lbrace>Key K, Agent A\<rbrace>\<rbrace>) |
|
263 |
\<in> set evs; |
|
264 |
A \<notin> bad; B \<notin> bad; evs \<in> ns_shared\<rbrakk> |
|
265 |
\<Longrightarrow> (\<forall>NB. Notes Spy \<lbrace>NA, NB, Key K\<rbrace> \<notin> set evs) \<longrightarrow> |
|
266 |
Key K \<notin> analz (spies evs)" |
|
11104 | 267 |
apply (erule rev_mp) |
268 |
apply (erule ns_shared.induct, force) |
|
269 |
apply (frule_tac [7] Says_Server_message_form) |
|
270 |
apply (frule_tac [4] Says_S_message_form) |
|
271 |
apply (erule_tac [5] disjE) |
|
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
272 |
apply (simp_all add: analz_insert_eq analz_insert_freshK pushes split_ifs, spy_analz) |
13926 | 273 |
txt{*NS2*} |
274 |
apply blast |
|
32404 | 275 |
txt{*NS3*} |
11188 | 276 |
apply (blast dest!: Crypt_Spy_analz_bad A_trusts_NS2 |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32527
diff
changeset
|
277 |
dest: Says_imp_knows_Spy analz.Inj unique_session_keys) |
32404 | 278 |
txt{*Oops*} |
279 |
apply (blast dest: unique_session_keys) |
|
11104 | 280 |
done |
281 |
||
282 |
||
11188 | 283 |
|
13926 | 284 |
text{*Final version: Server's message in the most abstract form*} |
11104 | 285 |
lemma Spy_not_see_encrypted_key: |
13926 | 286 |
"\<lbrakk>Says Server A (Crypt K' \<lbrace>NA, Agent B, Key K, X\<rbrace>) \<in> set evs; |
287 |
\<forall>NB. Notes Spy \<lbrace>NA, NB, Key K\<rbrace> \<notin> set evs; |
|
288 |
A \<notin> bad; B \<notin> bad; evs \<in> ns_shared\<rbrakk> |
|
289 |
\<Longrightarrow> Key K \<notin> analz (spies evs)" |
|
11150 | 290 |
by (blast dest: Says_Server_message_form secrecy_lemma) |
11104 | 291 |
|
292 |
||
13926 | 293 |
subsection{*Guarantees available at various stages of protocol*} |
1934 | 294 |
|
13926 | 295 |
text{*If the encrypted message appears then it originated with the Server*} |
11104 | 296 |
lemma B_trusts_NS3: |
13926 | 297 |
"\<lbrakk>Crypt (shrK B) \<lbrace>Key K, Agent A\<rbrace> \<in> parts (spies evs); |
298 |
B \<notin> bad; evs \<in> ns_shared\<rbrakk> |
|
299 |
\<Longrightarrow> \<exists>NA. Says Server A |
|
300 |
(Crypt (shrK A) \<lbrace>NA, Agent B, Key K, |
|
301 |
Crypt (shrK B) \<lbrace>Key K, Agent A\<rbrace>\<rbrace>) |
|
302 |
\<in> set evs" |
|
11104 | 303 |
apply (erule rev_mp) |
13507 | 304 |
apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies, auto) |
11104 | 305 |
done |
306 |
||
307 |
||
308 |
lemma A_trusts_NS4_lemma [rule_format]: |
|
13926 | 309 |
"evs \<in> ns_shared \<Longrightarrow> |
310 |
Key K \<notin> analz (spies evs) \<longrightarrow> |
|
311 |
Says Server A (Crypt (shrK A) \<lbrace>NA, Agent B, Key K, X\<rbrace>) \<in> set evs \<longrightarrow> |
|
312 |
Crypt K (Nonce NB) \<in> parts (spies evs) \<longrightarrow> |
|
313 |
Says B A (Crypt K (Nonce NB)) \<in> set evs" |
|
11104 | 314 |
apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies) |
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
315 |
apply (analz_mono_contra, simp_all, blast) |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
316 |
txt{*NS2: contradiction from the assumptions @{term "Key K \<notin> used evs2"} and |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
317 |
@{term "Crypt K (Nonce NB) \<in> parts (spies evs2)"} *} |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
318 |
apply (force dest!: Crypt_imp_keysFor) |
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
319 |
txt{*NS4*} |
32527 | 320 |
apply (metis B_trusts_NS3 Crypt_Spy_analz_bad Says_imp_analz_Spy Says_imp_parts_knows_Spy analz.Fst unique_session_keys) |
11104 | 321 |
done |
322 |
||
13926 | 323 |
text{*This version no longer assumes that K is secure*} |
11104 | 324 |
lemma A_trusts_NS4: |
13926 | 325 |
"\<lbrakk>Crypt K (Nonce NB) \<in> parts (spies evs); |
326 |
Crypt (shrK A) \<lbrace>NA, Agent B, Key K, X\<rbrace> \<in> parts (spies evs); |
|
327 |
\<forall>NB. Notes Spy \<lbrace>NA, NB, Key K\<rbrace> \<notin> set evs; |
|
328 |
A \<notin> bad; B \<notin> bad; evs \<in> ns_shared\<rbrakk> |
|
329 |
\<Longrightarrow> Says B A (Crypt K (Nonce NB)) \<in> set evs" |
|
11280 | 330 |
by (blast intro: A_trusts_NS4_lemma |
11104 | 331 |
dest: A_trusts_NS2 Spy_not_see_encrypted_key) |
332 |
||
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
333 |
text{*If the session key has been used in NS4 then somebody has forwarded |
11280 | 334 |
component X in some instance of NS4. Perhaps an interesting property, |
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
335 |
but not needed (after all) for the proofs below.*} |
11104 | 336 |
theorem NS4_implies_NS3 [rule_format]: |
13926 | 337 |
"evs \<in> ns_shared \<Longrightarrow> |
338 |
Key K \<notin> analz (spies evs) \<longrightarrow> |
|
339 |
Says Server A (Crypt (shrK A) \<lbrace>NA, Agent B, Key K, X\<rbrace>) \<in> set evs \<longrightarrow> |
|
340 |
Crypt K (Nonce NB) \<in> parts (spies evs) \<longrightarrow> |
|
341 |
(\<exists>A'. Says A' B X \<in> set evs)" |
|
18886 | 342 |
apply (erule ns_shared.induct, force) |
343 |
apply (drule_tac [4] NS3_msg_in_parts_spies) |
|
344 |
apply analz_mono_contra |
|
13926 | 345 |
apply (simp_all add: ex_disj_distrib, blast) |
346 |
txt{*NS2*} |
|
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
347 |
apply (blast dest!: new_keys_not_used Crypt_imp_keysFor) |
13926 | 348 |
txt{*NS4*} |
32527 | 349 |
apply (metis B_trusts_NS3 Crypt_Spy_analz_bad Says_imp_analz_Spy Says_imp_parts_knows_Spy analz.Fst unique_session_keys) |
11104 | 350 |
done |
351 |
||
352 |
||
353 |
lemma B_trusts_NS5_lemma [rule_format]: |
|
13926 | 354 |
"\<lbrakk>B \<notin> bad; evs \<in> ns_shared\<rbrakk> \<Longrightarrow> |
355 |
Key K \<notin> analz (spies evs) \<longrightarrow> |
|
11104 | 356 |
Says Server A |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32527
diff
changeset
|
357 |
(Crypt (shrK A) \<lbrace>NA, Agent B, Key K, |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32527
diff
changeset
|
358 |
Crypt (shrK B) \<lbrace>Key K, Agent A\<rbrace>\<rbrace>) \<in> set evs \<longrightarrow> |
13926 | 359 |
Crypt K \<lbrace>Nonce NB, Nonce NB\<rbrace> \<in> parts (spies evs) \<longrightarrow> |
360 |
Says A B (Crypt K \<lbrace>Nonce NB, Nonce NB\<rbrace>) \<in> set evs" |
|
18886 | 361 |
apply (erule ns_shared.induct, force) |
362 |
apply (drule_tac [4] NS3_msg_in_parts_spies) |
|
363 |
apply (analz_mono_contra, simp_all, blast) |
|
13926 | 364 |
txt{*NS2*} |
14207
f20fbb141673
Conversion of all main protocols from "Shared" to "Public".
paulson
parents:
14200
diff
changeset
|
365 |
apply (blast dest!: new_keys_not_used Crypt_imp_keysFor) |
13926 | 366 |
txt{*NS5*} |
11150 | 367 |
apply (blast dest!: A_trusts_NS2 |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32527
diff
changeset
|
368 |
dest: Says_imp_knows_Spy [THEN analz.Inj] |
11150 | 369 |
unique_session_keys Crypt_Spy_analz_bad) |
11104 | 370 |
done |
371 |
||
372 |
||
13926 | 373 |
text{*Very strong Oops condition reveals protocol's weakness*} |
11104 | 374 |
lemma B_trusts_NS5: |
13926 | 375 |
"\<lbrakk>Crypt K \<lbrace>Nonce NB, Nonce NB\<rbrace> \<in> parts (spies evs); |
376 |
Crypt (shrK B) \<lbrace>Key K, Agent A\<rbrace> \<in> parts (spies evs); |
|
377 |
\<forall>NA NB. Notes Spy \<lbrace>NA, NB, Key K\<rbrace> \<notin> set evs; |
|
378 |
A \<notin> bad; B \<notin> bad; evs \<in> ns_shared\<rbrakk> |
|
379 |
\<Longrightarrow> Says A B (Crypt K \<lbrace>Nonce NB, Nonce NB\<rbrace>) \<in> set evs" |
|
11280 | 380 |
by (blast intro: B_trusts_NS5_lemma |
11150 | 381 |
dest: B_trusts_NS3 Spy_not_see_encrypted_key) |
1934 | 382 |
|
18886 | 383 |
text{*Unaltered so far wrt original version*} |
384 |
||
385 |
subsection{*Lemmas for reasoning about predicate "Issues"*} |
|
386 |
||
387 |
lemma spies_Says_rev: "spies (evs @ [Says A B X]) = insert X (spies evs)" |
|
388 |
apply (induct_tac "evs") |
|
389 |
apply (induct_tac [2] "a", auto) |
|
390 |
done |
|
391 |
||
392 |
lemma spies_Gets_rev: "spies (evs @ [Gets A X]) = spies evs" |
|
393 |
apply (induct_tac "evs") |
|
394 |
apply (induct_tac [2] "a", auto) |
|
395 |
done |
|
396 |
||
397 |
lemma spies_Notes_rev: "spies (evs @ [Notes A X]) = |
|
398 |
(if A:bad then insert X (spies evs) else spies evs)" |
|
399 |
apply (induct_tac "evs") |
|
400 |
apply (induct_tac [2] "a", auto) |
|
401 |
done |
|
402 |
||
403 |
lemma spies_evs_rev: "spies evs = spies (rev evs)" |
|
404 |
apply (induct_tac "evs") |
|
405 |
apply (induct_tac [2] "a") |
|
406 |
apply (simp_all (no_asm_simp) add: spies_Says_rev spies_Gets_rev spies_Notes_rev) |
|
407 |
done |
|
408 |
||
409 |
lemmas parts_spies_evs_revD2 = spies_evs_rev [THEN equalityD2, THEN parts_mono] |
|
410 |
||
411 |
lemma spies_takeWhile: "spies (takeWhile P evs) <= spies evs" |
|
412 |
apply (induct_tac "evs") |
|
413 |
apply (induct_tac [2] "a", auto) |
|
414 |
txt{* Resembles @{text"used_subset_append"} in theory Event.*} |
|
415 |
done |
|
416 |
||
417 |
lemmas parts_spies_takeWhile_mono = spies_takeWhile [THEN parts_mono] |
|
418 |
||
419 |
||
420 |
subsection{*Guarantees of non-injective agreement on the session key, and |
|
421 |
of key distribution. They also express forms of freshness of certain messages, |
|
422 |
namely that agents were alive after something happened.*} |
|
423 |
||
424 |
lemma B_Issues_A: |
|
425 |
"\<lbrakk> Says B A (Crypt K (Nonce Nb)) \<in> set evs; |
|
426 |
Key K \<notin> analz (spies evs); |
|
427 |
A \<notin> bad; B \<notin> bad; evs \<in> ns_shared \<rbrakk> |
|
428 |
\<Longrightarrow> B Issues A with (Crypt K (Nonce Nb)) on evs" |
|
429 |
apply (simp (no_asm) add: Issues_def) |
|
430 |
apply (rule exI) |
|
431 |
apply (rule conjI, assumption) |
|
432 |
apply (simp (no_asm)) |
|
433 |
apply (erule rev_mp) |
|
434 |
apply (erule rev_mp) |
|
435 |
apply (erule ns_shared.induct, analz_mono_contra) |
|
436 |
apply (simp_all) |
|
437 |
txt{*fake*} |
|
438 |
apply blast |
|
439 |
apply (simp_all add: takeWhile_tail) |
|
440 |
txt{*NS3 remains by pure coincidence!*} |
|
441 |
apply (force dest!: A_trusts_NS2 Says_Server_message_form) |
|
442 |
txt{*NS4 would be the non-trivial case can be solved by Nb being used*} |
|
443 |
apply (blast dest: parts_spies_takeWhile_mono [THEN subsetD] |
|
444 |
parts_spies_evs_revD2 [THEN subsetD]) |
|
445 |
done |
|
446 |
||
447 |
text{*Tells A that B was alive after she sent him the session key. The |
|
448 |
session key must be assumed confidential for this deduction to be meaningful, |
|
449 |
but that assumption can be relaxed by the appropriate argument. |
|
450 |
||
451 |
Precisely, the theorem guarantees (to A) key distribution of the session key |
|
452 |
to B. It also guarantees (to A) non-injective agreement of B with A on the |
|
453 |
session key. Both goals are available to A in the sense of Goal Availability. |
|
454 |
*} |
|
455 |
lemma A_authenticates_and_keydist_to_B: |
|
456 |
"\<lbrakk>Crypt K (Nonce NB) \<in> parts (spies evs); |
|
457 |
Crypt (shrK A) \<lbrace>NA, Agent B, Key K, X\<rbrace> \<in> parts (spies evs); |
|
458 |
Key K \<notin> analz(knows Spy evs); |
|
459 |
A \<notin> bad; B \<notin> bad; evs \<in> ns_shared\<rbrakk> |
|
460 |
\<Longrightarrow> B Issues A with (Crypt K (Nonce NB)) on evs" |
|
461 |
by (blast intro: A_trusts_NS4_lemma B_Issues_A dest: A_trusts_NS2) |
|
462 |
||
463 |
lemma A_trusts_NS5: |
|
464 |
"\<lbrakk> Crypt K \<lbrace>Nonce NB, Nonce NB\<rbrace> \<in> parts(spies evs); |
|
465 |
Crypt (shrK A) \<lbrace>Nonce NA, Agent B, Key K, X\<rbrace> \<in> parts(spies evs); |
|
466 |
Key K \<notin> analz (spies evs); |
|
467 |
A \<notin> bad; B \<notin> bad; evs \<in> ns_shared \<rbrakk> |
|
468 |
\<Longrightarrow> Says A B (Crypt K \<lbrace>Nonce NB, Nonce NB\<rbrace>) \<in> set evs"; |
|
469 |
apply (erule rev_mp) |
|
470 |
apply (erule rev_mp) |
|
471 |
apply (erule rev_mp) |
|
472 |
apply (erule ns_shared.induct, analz_mono_contra) |
|
473 |
apply (simp_all) |
|
474 |
txt{*Fake*} |
|
475 |
apply blast |
|
476 |
txt{*NS2*} |
|
477 |
apply (force dest!: Crypt_imp_keysFor) |
|
32527 | 478 |
txt{*NS3*} |
479 |
apply (metis NS3_msg_in_parts_spies parts_cut_eq) |
|
18886 | 480 |
txt{*NS5, the most important case, can be solved by unicity*} |
32527 | 481 |
apply (metis A_trusts_NS2 Crypt_Spy_analz_bad Says_imp_analz_Spy Says_imp_parts_knows_Spy analz.Fst analz.Snd unique_session_keys) |
18886 | 482 |
done |
483 |
||
484 |
lemma A_Issues_B: |
|
485 |
"\<lbrakk> Says A B (Crypt K \<lbrace>Nonce NB, Nonce NB\<rbrace>) \<in> set evs; |
|
486 |
Key K \<notin> analz (spies evs); |
|
487 |
A \<notin> bad; B \<notin> bad; evs \<in> ns_shared \<rbrakk> |
|
488 |
\<Longrightarrow> A Issues B with (Crypt K \<lbrace>Nonce NB, Nonce NB\<rbrace>) on evs" |
|
489 |
apply (simp (no_asm) add: Issues_def) |
|
490 |
apply (rule exI) |
|
491 |
apply (rule conjI, assumption) |
|
492 |
apply (simp (no_asm)) |
|
493 |
apply (erule rev_mp) |
|
494 |
apply (erule rev_mp) |
|
495 |
apply (erule ns_shared.induct, analz_mono_contra) |
|
496 |
apply (simp_all) |
|
497 |
txt{*fake*} |
|
498 |
apply blast |
|
499 |
apply (simp_all add: takeWhile_tail) |
|
500 |
txt{*NS3 remains by pure coincidence!*} |
|
501 |
apply (force dest!: A_trusts_NS2 Says_Server_message_form) |
|
502 |
txt{*NS5 is the non-trivial case and cannot be solved as in @{term B_Issues_A}! because NB is not fresh. We need @{term A_trusts_NS5}, proved for this very purpose*} |
|
503 |
apply (blast dest: A_trusts_NS5 parts_spies_takeWhile_mono [THEN subsetD] |
|
504 |
parts_spies_evs_revD2 [THEN subsetD]) |
|
505 |
done |
|
506 |
||
507 |
text{*Tells B that A was alive after B issued NB. |
|
508 |
||
509 |
Precisely, the theorem guarantees (to B) key distribution of the session key to A. It also guarantees (to B) non-injective agreement of A with B on the session key. Both goals are available to B in the sense of Goal Availability. |
|
510 |
*} |
|
511 |
lemma B_authenticates_and_keydist_to_A: |
|
512 |
"\<lbrakk>Crypt K \<lbrace>Nonce NB, Nonce NB\<rbrace> \<in> parts (spies evs); |
|
513 |
Crypt (shrK B) \<lbrace>Key K, Agent A\<rbrace> \<in> parts (spies evs); |
|
514 |
Key K \<notin> analz (spies evs); |
|
515 |
A \<notin> bad; B \<notin> bad; evs \<in> ns_shared\<rbrakk> |
|
516 |
\<Longrightarrow> A Issues B with (Crypt K \<lbrace>Nonce NB, Nonce NB\<rbrace>) on evs" |
|
517 |
by (blast intro: A_Issues_B B_trusts_NS5_lemma dest: B_trusts_NS3) |
|
518 |
||
1934 | 519 |
end |