author | paulson |
Wed, 07 May 1997 13:01:43 +0200 | |
changeset 3121 | cbb6c0c1c58a |
parent 2637 | e9b203f854ae |
child 3465 | e85c24717cad |
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 |
|
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset
|
28 |
woolam.WL4 RS woolam.WL5) 2); |
2637
e9b203f854ae
reflecting my recent changes of the simplifier and classical reasoner
oheimb
parents:
2516
diff
changeset
|
29 |
by (ALLGOALS (simp_tac (!simpset setSolver safe_solver))); |
2274 | 30 |
by (REPEAT_FIRST (resolve_tac [refl, conjI])); |
3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset
|
31 |
by (REPEAT_FIRST (blast_tac (!claset addSEs [Nonce_supply RS notE]))); |
2274 | 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 |
||
3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset
|
56 |
(*For proving the easier theorems about X ~: parts (sees lost Spy evs) *) |
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset
|
57 |
val parts_induct_tac = |
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset
|
58 |
etac woolam.induct 1 THEN |
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset
|
59 |
forward_tac [WL4_parts_sees_Spy] 6 THEN |
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset
|
60 |
prove_simple_subgoals_tac 1; |
2274 | 61 |
|
62 |
||
63 |
(** Theorems of the form X ~: parts (sees lost Spy evs) imply that NOBODY |
|
64 |
sends messages containing X! **) |
|
65 |
||
66 |
(*Spy never sees another agent's shared key! (unless it's lost at start)*) |
|
67 |
goal thy |
|
2283
68829cf138fc
Swapping arguments of Crypt; removing argument lost
paulson
parents:
2274
diff
changeset
|
68 |
"!!evs. evs : woolam \ |
2274 | 69 |
\ ==> (Key (shrK A) : parts (sees lost Spy evs)) = (A : lost)"; |
3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset
|
70 |
by parts_induct_tac; |
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset
|
71 |
by (Fake_parts_insert_tac 1); |
2274 | 72 |
qed "Spy_see_shrK"; |
73 |
Addsimps [Spy_see_shrK]; |
|
74 |
||
75 |
goal thy |
|
2283
68829cf138fc
Swapping arguments of Crypt; removing argument lost
paulson
parents:
2274
diff
changeset
|
76 |
"!!evs. evs : woolam \ |
2274 | 77 |
\ ==> (Key (shrK A) : analz (sees lost Spy evs)) = (A : lost)"; |
78 |
by (auto_tac(!claset addDs [impOfSubs analz_subset_parts], !simpset)); |
|
79 |
qed "Spy_analz_shrK"; |
|
80 |
Addsimps [Spy_analz_shrK]; |
|
81 |
||
82 |
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
|
83 |
\ evs : woolam |] ==> A:lost"; |
3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset
|
84 |
by (blast_tac (!claset addDs [Spy_see_shrK]) 1); |
2274 | 85 |
qed "Spy_see_shrK_D"; |
86 |
||
87 |
bind_thm ("Spy_analz_shrK_D", analz_subset_parts RS subsetD RS Spy_see_shrK_D); |
|
88 |
AddSDs [Spy_see_shrK_D, Spy_analz_shrK_D]; |
|
89 |
||
90 |
||
91 |
(**** Autheticity properties for Woo-Lam ****) |
|
92 |
||
93 |
||
94 |
(*** WL4 ***) |
|
95 |
||
96 |
(*If the encrypted message appears then it originated with Alice*) |
|
97 |
goal thy |
|
2283
68829cf138fc
Swapping arguments of Crypt; removing argument lost
paulson
parents:
2274
diff
changeset
|
98 |
"!!evs. [| A ~: lost; evs : woolam |] \ |
68829cf138fc
Swapping arguments of Crypt; removing argument lost
paulson
parents:
2274
diff
changeset
|
99 |
\ ==> Crypt (shrK A) (Nonce NB) : parts (sees lost Spy evs) \ |
68829cf138fc
Swapping arguments of Crypt; removing argument lost
paulson
parents:
2274
diff
changeset
|
100 |
\ --> (EX B. Says A B (Crypt (shrK A) (Nonce NB)) : set_of_list evs)"; |
3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset
|
101 |
by parts_induct_tac; |
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset
|
102 |
by (Fake_parts_insert_tac 1); |
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset
|
103 |
by (Blast_tac 1); |
2274 | 104 |
qed_spec_mp "NB_Crypt_imp_Alice_msg"; |
105 |
||
106 |
(*Guarantee for Server: if it gets a message containing a certificate from |
|
107 |
Alice, then she originated that certificate. But we DO NOT know that B |
|
108 |
ever saw it: the Spy may have rerouted the message to the Server.*) |
|
109 |
goal thy |
|
2283
68829cf138fc
Swapping arguments of Crypt; removing argument lost
paulson
parents:
2274
diff
changeset
|
110 |
"!!evs. [| A ~: lost; evs : woolam; \ |
68829cf138fc
Swapping arguments of Crypt; removing argument lost
paulson
parents:
2274
diff
changeset
|
111 |
\ Says B' Server {|Agent A, Agent B, Crypt (shrK A) (Nonce NB)|} \ |
2274 | 112 |
\ : set_of_list evs |] \ |
2283
68829cf138fc
Swapping arguments of Crypt; removing argument lost
paulson
parents:
2274
diff
changeset
|
113 |
\ ==> EX B. Says A B (Crypt (shrK A) (Nonce NB)) : set_of_list evs"; |
3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset
|
114 |
by (blast_tac (!claset addSIs [NB_Crypt_imp_Alice_msg] |
2274 | 115 |
addSEs [MPair_parts] |
116 |
addDs [Says_imp_sees_Spy RS parts.Inj]) 1); |
|
2321 | 117 |
qed "Server_trusts_WL4"; |
2274 | 118 |
|
119 |
||
120 |
(*** WL5 ***) |
|
121 |
||
122 |
(*Server sent WL5 only if it received the right sort of message*) |
|
123 |
goal thy |
|
2283
68829cf138fc
Swapping arguments of Crypt; removing argument lost
paulson
parents:
2274
diff
changeset
|
124 |
"!!evs. evs : woolam ==> \ |
68829cf138fc
Swapping arguments of Crypt; removing argument lost
paulson
parents:
2274
diff
changeset
|
125 |
\ 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
|
126 |
\ --> (EX B'. Says B' Server {|Agent A, Agent B, Crypt (shrK A) NB|} \ |
2274 | 127 |
\ : set_of_list evs)"; |
3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset
|
128 |
by parts_induct_tac; |
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset
|
129 |
by (Fake_parts_insert_tac 1); |
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset
|
130 |
by (ALLGOALS Blast_tac); |
2274 | 131 |
bind_thm ("Server_sent_WL5", result() RSN (2, rev_mp)); |
132 |
||
133 |
||
134 |
(*If the encrypted message appears then it originated with the Server!*) |
|
135 |
goal thy |
|
2283
68829cf138fc
Swapping arguments of Crypt; removing argument lost
paulson
parents:
2274
diff
changeset
|
136 |
"!!evs. [| B ~: lost; evs : woolam |] \ |
68829cf138fc
Swapping arguments of Crypt; removing argument lost
paulson
parents:
2274
diff
changeset
|
137 |
\ ==> Crypt (shrK B) {|Agent A, NB|} : parts (sees lost Spy evs) \ |
68829cf138fc
Swapping arguments of Crypt; removing argument lost
paulson
parents:
2274
diff
changeset
|
138 |
\ --> Says Server B (Crypt (shrK B) {|Agent A, NB|}) : set_of_list evs"; |
3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset
|
139 |
by parts_induct_tac; |
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset
|
140 |
by (Fake_parts_insert_tac 1); |
2274 | 141 |
qed_spec_mp "NB_Crypt_imp_Server_msg"; |
142 |
||
143 |
(*Partial guarantee for B: if it gets a message of correct form then the Server |
|
144 |
sent the same message.*) |
|
145 |
goal thy |
|
2283
68829cf138fc
Swapping arguments of Crypt; removing argument lost
paulson
parents:
2274
diff
changeset
|
146 |
"!!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
|
147 |
\ B ~: lost; 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"; |
3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset
|
149 |
by (blast_tac (!claset addSIs [NB_Crypt_imp_Server_msg] |
2274 | 150 |
addDs [Says_imp_sees_Spy RS parts.Inj]) 1); |
151 |
qed "B_got_WL5"; |
|
152 |
||
153 |
(*Guarantee for B. If B gets the Server's certificate then A has encrypted |
|
154 |
the nonce using her key. This event can be no older than the nonce itself. |
|
155 |
But A may have sent the nonce to some other agent and it could have reached |
|
156 |
the Server via the Spy.*) |
|
157 |
goal thy |
|
2283
68829cf138fc
Swapping arguments of Crypt; removing argument lost
paulson
parents:
2274
diff
changeset
|
158 |
"!!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
|
159 |
\ A ~: lost; B ~: lost; evs : woolam |] \ |
68829cf138fc
Swapping arguments of Crypt; removing argument lost
paulson
parents:
2274
diff
changeset
|
160 |
\ ==> EX B. Says A B (Crypt (shrK A) (Nonce NB)) : set_of_list evs"; |
3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset
|
161 |
by (blast_tac (!claset addIs [Server_trusts_WL4] |
2274 | 162 |
addSDs [B_got_WL5 RS Server_sent_WL5]) 1); |
2321 | 163 |
qed "B_trusts_WL5"; |
2274 | 164 |
|
165 |
||
166 |
(*B only issues challenges in response to WL1. Useful??*) |
|
167 |
goal thy |
|
2283
68829cf138fc
Swapping arguments of Crypt; removing argument lost
paulson
parents:
2274
diff
changeset
|
168 |
"!!evs. [| B ~= Spy; evs : woolam |] \ |
2274 | 169 |
\ ==> Says B A (Nonce NB) : set_of_list evs \ |
170 |
\ --> (EX A'. Says A' B (Agent A) : set_of_list evs)"; |
|
3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset
|
171 |
by parts_induct_tac; |
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset
|
172 |
by (Fake_parts_insert_tac 1); |
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset
|
173 |
by (ALLGOALS Blast_tac); |
2274 | 174 |
bind_thm ("B_said_WL2", result() RSN (2, rev_mp)); |
175 |
||
176 |
||
177 |
(**CANNOT be proved because A doesn't know where challenges come from... |
|
178 |
goal thy |
|
2283
68829cf138fc
Swapping arguments of Crypt; removing argument lost
paulson
parents:
2274
diff
changeset
|
179 |
"!!evs. [| A ~: lost; B ~= Spy; evs : woolam |] \ |
68829cf138fc
Swapping arguments of Crypt; removing argument lost
paulson
parents:
2274
diff
changeset
|
180 |
\ ==> Crypt (shrK A) (Nonce NB) : parts (sees lost Spy evs) & \ |
2274 | 181 |
\ Says B A (Nonce NB) : set_of_list evs \ |
2283
68829cf138fc
Swapping arguments of Crypt; removing argument lost
paulson
parents:
2274
diff
changeset
|
182 |
\ --> Says A B (Crypt (shrK A) (Nonce NB)) : set_of_list evs"; |
3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset
|
183 |
by parts_induct_tac; |
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset
|
184 |
by (Fake_parts_insert_tac 1); |
2274 | 185 |
by (Step_tac 1); |
3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset
|
186 |
by (blast_tac (!claset addSEs partsEs) 1); |
2274 | 187 |
**) |