author | paulson |
Thu, 05 Dec 1996 19:03:08 +0100 | |
changeset 2326 | 6df4488339e4 |
parent 2321 | 083912bc5775 |
child 2451 | ce85a2aafc7a |
permissions | -rw-r--r-- |
2274 | 1 |
(* Title: HOL/Auth/WooLam |
2 |
ID: $Id$ |
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 |
Copyright 1996 University of Cambridge |
|
5 |
||
6 |
Inductive relation "woolam" for the Woo-Lam protocol. |
|
7 |
||
8 |
Simplified version from page 11 of |
|
9 |
Abadi and Needham. Prudent Engineering Practice for Cryptographic Protocols. |
|
10 |
IEEE Trans. S.E. 22(1), 1996, pages 6-15. |
|
11 |
*) |
|
12 |
||
13 |
open WooLam; |
|
14 |
||
15 |
proof_timing:=true; |
|
16 |
HOL_quantifiers := false; |
|
17 |
Pretty.setdepth 20; |
|
18 |
||
19 |
||
2321 | 20 |
(*A "possibility property": there are traces that reach the end*) |
2274 | 21 |
goal thy |
22 |
"!!A B. [| A ~= B; A ~= Server; B ~= Server |] \ |
|
2283
68829cf138fc
Swapping arguments of Crypt; removing argument lost
paulson
parents:
2274
diff
changeset
|
23 |
\ ==> EX NB. EX evs: woolam. \ |
68829cf138fc
Swapping arguments of Crypt; removing argument lost
paulson
parents:
2274
diff
changeset
|
24 |
\ Says Server B (Crypt (shrK B) {|Agent A, Nonce NB|}) \ |
2274 | 25 |
\ : set_of_list evs"; |
26 |
by (REPEAT (resolve_tac [exI,bexI] 1)); |
|
27 |
by (rtac (woolam.Nil RS woolam.WL1 RS woolam.WL2 RS woolam.WL3 RS |
|
28 |
woolam.WL4 RS woolam.WL5) 2); |
|
29 |
by (ALLGOALS (simp_tac (!simpset setsolver safe_solver))); |
|
30 |
by (REPEAT_FIRST (resolve_tac [refl, conjI])); |
|
31 |
by (REPEAT_FIRST (fast_tac (!claset addss (!simpset setsolver safe_solver)))); |
|
32 |
result(); |
|
33 |
||
34 |
||
35 |
(**** Inductive proofs about woolam ****) |
|
36 |
||
37 |
(*Nobody sends themselves messages*) |
|
2283
68829cf138fc
Swapping arguments of Crypt; removing argument lost
paulson
parents:
2274
diff
changeset
|
38 |
goal thy "!!evs. evs : woolam ==> ALL A X. Says A A X ~: set_of_list evs"; |
2274 | 39 |
by (etac woolam.induct 1); |
40 |
by (Auto_tac()); |
|
41 |
qed_spec_mp "not_Says_to_self"; |
|
42 |
Addsimps [not_Says_to_self]; |
|
43 |
AddSEs [not_Says_to_self RSN (2, rev_notE)]; |
|
44 |
||
45 |
||
46 |
(** For reasoning about the encrypted portion of messages **) |
|
47 |
||
48 |
goal thy "!!evs. Says A' B X : set_of_list evs \ |
|
49 |
\ ==> X : analz (sees lost Spy evs)"; |
|
50 |
by (etac (Says_imp_sees_Spy RS analz.Inj) 1); |
|
51 |
qed "WL4_analz_sees_Spy"; |
|
52 |
||
53 |
bind_thm ("WL4_parts_sees_Spy", |
|
54 |
WL4_analz_sees_Spy RS (impOfSubs analz_subset_parts)); |
|
55 |
||
2283
68829cf138fc
Swapping arguments of Crypt; removing argument lost
paulson
parents:
2274
diff
changeset
|
56 |
val parts_Fake_tac = forward_tac [WL4_parts_sees_Spy] 6; |
2274 | 57 |
|
58 |
(*For proving the easier theorems about X ~: parts (sees lost Spy evs) *) |
|
59 |
fun parts_induct_tac i = SELECT_GOAL |
|
60 |
(DETERM (etac woolam.induct 1 THEN parts_Fake_tac THEN |
|
61 |
(*Fake message*) |
|
62 |
TRY (best_tac (!claset addDs [impOfSubs analz_subset_parts, |
|
63 |
impOfSubs Fake_parts_insert] |
|
64 |
addss (!simpset)) 2)) THEN |
|
65 |
(*Base case*) |
|
66 |
fast_tac (!claset addss (!simpset)) 1 THEN |
|
67 |
ALLGOALS Asm_simp_tac) i; |
|
68 |
||
69 |
(** Theorems of the form X ~: parts (sees lost Spy evs) imply that NOBODY |
|
70 |
sends messages containing X! **) |
|
71 |
||
72 |
(*Spy never sees another agent's shared key! (unless it's lost at start)*) |
|
73 |
goal thy |
|
2283
68829cf138fc
Swapping arguments of Crypt; removing argument lost
paulson
parents:
2274
diff
changeset
|
74 |
"!!evs. evs : woolam \ |
2274 | 75 |
\ ==> (Key (shrK A) : parts (sees lost Spy evs)) = (A : lost)"; |
76 |
by (parts_induct_tac 1); |
|
77 |
by (Auto_tac()); |
|
78 |
qed "Spy_see_shrK"; |
|
79 |
Addsimps [Spy_see_shrK]; |
|
80 |
||
81 |
goal thy |
|
2283
68829cf138fc
Swapping arguments of Crypt; removing argument lost
paulson
parents:
2274
diff
changeset
|
82 |
"!!evs. evs : woolam \ |
2274 | 83 |
\ ==> (Key (shrK A) : analz (sees lost Spy evs)) = (A : lost)"; |
84 |
by (auto_tac(!claset addDs [impOfSubs analz_subset_parts], !simpset)); |
|
85 |
qed "Spy_analz_shrK"; |
|
86 |
Addsimps [Spy_analz_shrK]; |
|
87 |
||
88 |
goal thy "!!A. [| Key (shrK A) : parts (sees lost Spy evs); \ |
|
2283
68829cf138fc
Swapping arguments of Crypt; removing argument lost
paulson
parents:
2274
diff
changeset
|
89 |
\ evs : woolam |] ==> A:lost"; |
2274 | 90 |
by (fast_tac (!claset addDs [Spy_see_shrK]) 1); |
91 |
qed "Spy_see_shrK_D"; |
|
92 |
||
93 |
bind_thm ("Spy_analz_shrK_D", analz_subset_parts RS subsetD RS Spy_see_shrK_D); |
|
94 |
AddSDs [Spy_see_shrK_D, Spy_analz_shrK_D]; |
|
95 |
||
96 |
||
97 |
(*** Future nonces can't be seen or used! ***) |
|
98 |
||
2283
68829cf138fc
Swapping arguments of Crypt; removing argument lost
paulson
parents:
2274
diff
changeset
|
99 |
goal thy "!!evs. evs : woolam ==> \ |
2274 | 100 |
\ length evs <= length evt --> \ |
101 |
\ Nonce (newN evt) ~: parts (sees lost Spy evs)"; |
|
102 |
by (parts_induct_tac 1); |
|
103 |
by (REPEAT_FIRST (fast_tac (!claset |
|
104 |
addSEs partsEs |
|
105 |
addSDs [Says_imp_sees_Spy RS parts.Inj] |
|
106 |
addEs [leD RS notE] |
|
107 |
addDs [impOfSubs analz_subset_parts, |
|
108 |
impOfSubs parts_insert_subset_Un, |
|
109 |
Suc_leD] |
|
110 |
addss (!simpset)))); |
|
111 |
qed_spec_mp "new_nonces_not_seen"; |
|
112 |
Addsimps [new_nonces_not_seen]; |
|
113 |
||
114 |
||
115 |
(**** Autheticity properties for Woo-Lam ****) |
|
116 |
||
117 |
||
118 |
(*** WL4 ***) |
|
119 |
||
120 |
(*If the encrypted message appears then it originated with Alice*) |
|
121 |
goal thy |
|
2283
68829cf138fc
Swapping arguments of Crypt; removing argument lost
paulson
parents:
2274
diff
changeset
|
122 |
"!!evs. [| A ~: lost; evs : woolam |] \ |
68829cf138fc
Swapping arguments of Crypt; removing argument lost
paulson
parents:
2274
diff
changeset
|
123 |
\ ==> Crypt (shrK A) (Nonce NB) : parts (sees lost Spy evs) \ |
68829cf138fc
Swapping arguments of Crypt; removing argument lost
paulson
parents:
2274
diff
changeset
|
124 |
\ --> (EX B. Says A B (Crypt (shrK A) (Nonce NB)) : set_of_list evs)"; |
2274 | 125 |
by (parts_induct_tac 1); |
126 |
by (Fast_tac 1); |
|
127 |
qed_spec_mp "NB_Crypt_imp_Alice_msg"; |
|
128 |
||
129 |
(*Guarantee for Server: if it gets a message containing a certificate from |
|
130 |
Alice, then she originated that certificate. But we DO NOT know that B |
|
131 |
ever saw it: the Spy may have rerouted the message to the Server.*) |
|
132 |
goal thy |
|
2283
68829cf138fc
Swapping arguments of Crypt; removing argument lost
paulson
parents:
2274
diff
changeset
|
133 |
"!!evs. [| A ~: lost; evs : woolam; \ |
68829cf138fc
Swapping arguments of Crypt; removing argument lost
paulson
parents:
2274
diff
changeset
|
134 |
\ Says B' Server {|Agent A, Agent B, Crypt (shrK A) (Nonce NB)|} \ |
2274 | 135 |
\ : set_of_list evs |] \ |
2283
68829cf138fc
Swapping arguments of Crypt; removing argument lost
paulson
parents:
2274
diff
changeset
|
136 |
\ ==> EX B. Says A B (Crypt (shrK A) (Nonce NB)) : set_of_list evs"; |
2274 | 137 |
by (fast_tac (!claset addSIs [NB_Crypt_imp_Alice_msg] |
138 |
addSEs [MPair_parts] |
|
139 |
addDs [Says_imp_sees_Spy RS parts.Inj]) 1); |
|
2321 | 140 |
qed "Server_trusts_WL4"; |
2274 | 141 |
|
142 |
||
143 |
(*** WL5 ***) |
|
144 |
||
145 |
(*Server sent WL5 only if it received the right sort of message*) |
|
146 |
goal thy |
|
2283
68829cf138fc
Swapping arguments of Crypt; removing argument lost
paulson
parents:
2274
diff
changeset
|
147 |
"!!evs. evs : woolam ==> \ |
68829cf138fc
Swapping arguments of Crypt; removing argument lost
paulson
parents:
2274
diff
changeset
|
148 |
\ Says Server B (Crypt (shrK B) {|Agent A, NB|}) : set_of_list evs \ |
68829cf138fc
Swapping arguments of Crypt; removing argument lost
paulson
parents:
2274
diff
changeset
|
149 |
\ --> (EX B'. Says B' Server {|Agent A, Agent B, Crypt (shrK A) NB|} \ |
2274 | 150 |
\ : set_of_list evs)"; |
151 |
by (parts_induct_tac 1); |
|
152 |
by (ALLGOALS Fast_tac); |
|
153 |
bind_thm ("Server_sent_WL5", result() RSN (2, rev_mp)); |
|
154 |
||
155 |
||
156 |
(*If the encrypted message appears then it originated with the Server!*) |
|
157 |
goal thy |
|
2283
68829cf138fc
Swapping arguments of Crypt; removing argument lost
paulson
parents:
2274
diff
changeset
|
158 |
"!!evs. [| B ~: lost; evs : woolam |] \ |
68829cf138fc
Swapping arguments of Crypt; removing argument lost
paulson
parents:
2274
diff
changeset
|
159 |
\ ==> Crypt (shrK B) {|Agent A, NB|} : parts (sees lost Spy evs) \ |
68829cf138fc
Swapping arguments of Crypt; removing argument lost
paulson
parents:
2274
diff
changeset
|
160 |
\ --> Says Server B (Crypt (shrK B) {|Agent A, NB|}) : set_of_list evs"; |
2274 | 161 |
by (parts_induct_tac 1); |
162 |
qed_spec_mp "NB_Crypt_imp_Server_msg"; |
|
163 |
||
164 |
(*Partial guarantee for B: if it gets a message of correct form then the Server |
|
165 |
sent the same message.*) |
|
166 |
goal thy |
|
2283
68829cf138fc
Swapping arguments of Crypt; removing argument lost
paulson
parents:
2274
diff
changeset
|
167 |
"!!evs. [| Says S B (Crypt (shrK B) {|Agent A, NB|}) : set_of_list evs; \ |
68829cf138fc
Swapping arguments of Crypt; removing argument lost
paulson
parents:
2274
diff
changeset
|
168 |
\ B ~: lost; evs : woolam |] \ |
68829cf138fc
Swapping arguments of Crypt; removing argument lost
paulson
parents:
2274
diff
changeset
|
169 |
\ ==> Says Server B (Crypt (shrK B) {|Agent A, NB|}) : set_of_list evs"; |
2274 | 170 |
by (fast_tac (!claset addSIs [NB_Crypt_imp_Server_msg] |
171 |
addDs [Says_imp_sees_Spy RS parts.Inj]) 1); |
|
172 |
qed "B_got_WL5"; |
|
173 |
||
174 |
(*Guarantee for B. If B gets the Server's certificate then A has encrypted |
|
175 |
the nonce using her key. This event can be no older than the nonce itself. |
|
176 |
But A may have sent the nonce to some other agent and it could have reached |
|
177 |
the Server via the Spy.*) |
|
178 |
goal thy |
|
2283
68829cf138fc
Swapping arguments of Crypt; removing argument lost
paulson
parents:
2274
diff
changeset
|
179 |
"!!evs. [| Says S B (Crypt (shrK B) {|Agent A, Nonce NB|}): set_of_list evs; \ |
68829cf138fc
Swapping arguments of Crypt; removing argument lost
paulson
parents:
2274
diff
changeset
|
180 |
\ A ~: lost; B ~: lost; evs : woolam |] \ |
68829cf138fc
Swapping arguments of Crypt; removing argument lost
paulson
parents:
2274
diff
changeset
|
181 |
\ ==> EX B. Says A B (Crypt (shrK A) (Nonce NB)) : set_of_list evs"; |
2321 | 182 |
by (fast_tac (!claset addIs [Server_trusts_WL4] |
2274 | 183 |
addSDs [B_got_WL5 RS Server_sent_WL5]) 1); |
2321 | 184 |
qed "B_trusts_WL5"; |
2274 | 185 |
|
186 |
||
187 |
(*B only issues challenges in response to WL1. Useful??*) |
|
188 |
goal thy |
|
2283
68829cf138fc
Swapping arguments of Crypt; removing argument lost
paulson
parents:
2274
diff
changeset
|
189 |
"!!evs. [| B ~= Spy; evs : woolam |] \ |
2274 | 190 |
\ ==> Says B A (Nonce NB) : set_of_list evs \ |
191 |
\ --> (EX A'. Says A' B (Agent A) : set_of_list evs)"; |
|
192 |
by (parts_induct_tac 1); |
|
193 |
by (ALLGOALS Fast_tac); |
|
194 |
bind_thm ("B_said_WL2", result() RSN (2, rev_mp)); |
|
195 |
||
196 |
||
197 |
(**CANNOT be proved because A doesn't know where challenges come from... |
|
198 |
goal thy |
|
2283
68829cf138fc
Swapping arguments of Crypt; removing argument lost
paulson
parents:
2274
diff
changeset
|
199 |
"!!evs. [| A ~: lost; B ~= Spy; evs : woolam |] \ |
68829cf138fc
Swapping arguments of Crypt; removing argument lost
paulson
parents:
2274
diff
changeset
|
200 |
\ ==> Crypt (shrK A) (Nonce NB) : parts (sees lost Spy evs) & \ |
2274 | 201 |
\ Says B A (Nonce NB) : set_of_list evs \ |
2283
68829cf138fc
Swapping arguments of Crypt; removing argument lost
paulson
parents:
2274
diff
changeset
|
202 |
\ --> Says A B (Crypt (shrK A) (Nonce NB)) : set_of_list evs"; |
2274 | 203 |
by (parts_induct_tac 1); |
204 |
by (Step_tac 1); |
|
205 |
by (best_tac (!claset addSEs partsEs |
|
206 |
addEs [new_nonces_not_seen RSN(2,rev_notE)]) 1); |
|
207 |
**) |