author | paulson |
Tue, 27 Feb 2001 16:13:23 +0100 | |
changeset 11185 | 1b737b4c2108 |
parent 11150 | 67387142225e |
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 |
||
11150 | 13 |
AddDs [Says_imp_knows_Spy RS parts.Inj, parts.Body]; |
14 |
AddDs [impOfSubs analz_subset_parts, impOfSubs Fake_parts_insert]; |
|
4470 | 15 |
|
2274 | 16 |
|
2321 | 17 |
(*A "possibility property": there are traces that reach the end*) |
11185
1b737b4c2108
Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11150
diff
changeset
|
18 |
Goal "\\<exists>NB. \\<exists>evs \\<in> woolam. \ |
1b737b4c2108
Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11150
diff
changeset
|
19 |
\ Says Server B (Crypt (shrK B) {|Agent A, Nonce NB|}) \\<in> set evs"; |
2274 | 20 |
by (REPEAT (resolve_tac [exI,bexI] 1)); |
21 |
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
|
22 |
woolam.WL4 RS woolam.WL5) 2); |
3471
cd37ec057028
Now the possibility proof calls the appropriate tactic
paulson
parents:
3466
diff
changeset
|
23 |
by possibility_tac; |
2274 | 24 |
result(); |
25 |
||
26 |
||
27 |
(**** Inductive proofs about woolam ****) |
|
28 |
||
29 |
(** For reasoning about the encrypted portion of messages **) |
|
30 |
||
11185
1b737b4c2108
Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11150
diff
changeset
|
31 |
Goal "Says A' B X \\<in> set evs ==> X \\<in> analz (spies evs)"; |
3683 | 32 |
by (etac (Says_imp_spies RS analz.Inj) 1); |
33 |
qed "WL4_analz_spies"; |
|
2274 | 34 |
|
3683 | 35 |
bind_thm ("WL4_parts_spies", |
36 |
WL4_analz_spies RS (impOfSubs analz_subset_parts)); |
|
2274 | 37 |
|
11185
1b737b4c2108
Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11150
diff
changeset
|
38 |
(*For proving the easier theorems about X \\<notin> parts (spies evs) *) |
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3471
diff
changeset
|
39 |
fun parts_induct_tac i = |
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3471
diff
changeset
|
40 |
etac woolam.induct i THEN |
7499 | 41 |
ftac WL4_parts_spies (i+5) THEN |
3471
cd37ec057028
Now the possibility proof calls the appropriate tactic
paulson
parents:
3466
diff
changeset
|
42 |
prove_simple_subgoals_tac 1; |
2274 | 43 |
|
44 |
||
11185
1b737b4c2108
Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11150
diff
changeset
|
45 |
(** Theorems of the form X \\<notin> parts (spies evs) imply that NOBODY |
2274 | 46 |
sends messages containing X! **) |
47 |
||
3683 | 48 |
(*Spy never sees another agent's shared key! (unless it's bad at start)*) |
11185
1b737b4c2108
Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11150
diff
changeset
|
49 |
Goal "evs \\<in> woolam ==> (Key (shrK A) \\<in> parts (spies evs)) = (A \\<in> bad)"; |
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3471
diff
changeset
|
50 |
by (parts_induct_tac 1); |
4470 | 51 |
by (Blast_tac 1); |
2274 | 52 |
qed "Spy_see_shrK"; |
53 |
Addsimps [Spy_see_shrK]; |
|
54 |
||
11185
1b737b4c2108
Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11150
diff
changeset
|
55 |
Goal "evs \\<in> woolam ==> (Key (shrK A) \\<in> analz (spies evs)) = (A \\<in> bad)"; |
4477
b3e5857d8d99
New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
paulson
parents:
4470
diff
changeset
|
56 |
by Auto_tac; |
2274 | 57 |
qed "Spy_analz_shrK"; |
58 |
Addsimps [Spy_analz_shrK]; |
|
59 |
||
4470 | 60 |
AddSDs [Spy_see_shrK RSN (2, rev_iffD1), |
61 |
Spy_analz_shrK RSN (2, rev_iffD1)]; |
|
2274 | 62 |
|
63 |
||
64 |
(**** Autheticity properties for Woo-Lam ****) |
|
65 |
||
66 |
||
67 |
(*** WL4 ***) |
|
68 |
||
69 |
(*If the encrypted message appears then it originated with Alice*) |
|
11185
1b737b4c2108
Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11150
diff
changeset
|
70 |
Goal "[| Crypt (shrK A) (Nonce NB) \\<in> parts (spies evs); \ |
1b737b4c2108
Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11150
diff
changeset
|
71 |
\ A \\<notin> bad; evs \\<in> woolam |] \ |
1b737b4c2108
Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11150
diff
changeset
|
72 |
\ ==> \\<exists>B. Says A B (Crypt (shrK A) (Nonce NB)) \\<in> set evs"; |
4470 | 73 |
by (etac rev_mp 1); |
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3471
diff
changeset
|
74 |
by (parts_induct_tac 1); |
4470 | 75 |
by (ALLGOALS Blast_tac); |
76 |
qed "NB_Crypt_imp_Alice_msg"; |
|
2274 | 77 |
|
78 |
(*Guarantee for Server: if it gets a message containing a certificate from |
|
79 |
Alice, then she originated that certificate. But we DO NOT know that B |
|
80 |
ever saw it: the Spy may have rerouted the message to the Server.*) |
|
5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
81 |
Goal "[| Says B' Server {|Agent A, Agent B, Crypt (shrK A) (Nonce NB)|} \ |
11185
1b737b4c2108
Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11150
diff
changeset
|
82 |
\ \\<in> set evs; \ |
1b737b4c2108
Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11150
diff
changeset
|
83 |
\ A \\<notin> bad; evs \\<in> woolam |] \ |
1b737b4c2108
Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11150
diff
changeset
|
84 |
\ ==> \\<exists>B. Says A B (Crypt (shrK A) (Nonce NB)) \\<in> set evs"; |
4470 | 85 |
by (blast_tac (claset() addSIs [NB_Crypt_imp_Alice_msg]) 1); |
2321 | 86 |
qed "Server_trusts_WL4"; |
2274 | 87 |
|
4470 | 88 |
AddDs [Server_trusts_WL4]; |
89 |
||
2274 | 90 |
|
91 |
(*** WL5 ***) |
|
92 |
||
93 |
(*Server sent WL5 only if it received the right sort of message*) |
|
11185
1b737b4c2108
Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11150
diff
changeset
|
94 |
Goal "[| Says Server B (Crypt (shrK B) {|Agent A, NB|}) \\<in> set evs; \ |
1b737b4c2108
Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11150
diff
changeset
|
95 |
\ evs \\<in> woolam |] \ |
1b737b4c2108
Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11150
diff
changeset
|
96 |
\ ==> \\<exists>B'. Says B' Server {|Agent A, Agent B, Crypt (shrK A) NB|} \ |
1b737b4c2108
Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11150
diff
changeset
|
97 |
\ \\<in> set evs"; |
4470 | 98 |
by (etac rev_mp 1); |
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3471
diff
changeset
|
99 |
by (parts_induct_tac 1); |
3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset
|
100 |
by (ALLGOALS Blast_tac); |
4470 | 101 |
qed "Server_sent_WL5"; |
2274 | 102 |
|
4470 | 103 |
AddDs [Server_sent_WL5]; |
2274 | 104 |
|
105 |
(*If the encrypted message appears then it originated with the Server!*) |
|
11185
1b737b4c2108
Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11150
diff
changeset
|
106 |
Goal "[| Crypt (shrK B) {|Agent A, NB|} \\<in> parts (spies evs); \ |
1b737b4c2108
Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11150
diff
changeset
|
107 |
\ B \\<notin> bad; evs \\<in> woolam |] \ |
1b737b4c2108
Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11150
diff
changeset
|
108 |
\ ==> Says Server B (Crypt (shrK B) {|Agent A, NB|}) \\<in> set evs"; |
4470 | 109 |
by (etac rev_mp 1); |
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3471
diff
changeset
|
110 |
by (parts_induct_tac 1); |
4470 | 111 |
by (Blast_tac 1); |
2274 | 112 |
qed_spec_mp "NB_Crypt_imp_Server_msg"; |
113 |
||
114 |
(*Guarantee for B. If B gets the Server's certificate then A has encrypted |
|
115 |
the nonce using her key. This event can be no older than the nonce itself. |
|
116 |
But A may have sent the nonce to some other agent and it could have reached |
|
117 |
the Server via the Spy.*) |
|
5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset
|
118 |
Goal "[| Says S B (Crypt (shrK B) {|Agent A, Nonce NB|}): set evs; \ |
11185
1b737b4c2108
Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11150
diff
changeset
|
119 |
\ A \\<notin> bad; B \\<notin> bad; evs \\<in> woolam |] \ |
1b737b4c2108
Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11150
diff
changeset
|
120 |
\ ==> \\<exists>B. Says A B (Crypt (shrK A) (Nonce NB)) \\<in> set evs"; |
4470 | 121 |
by (blast_tac (claset() addSDs [NB_Crypt_imp_Server_msg]) 1); |
2321 | 122 |
qed "B_trusts_WL5"; |
2274 | 123 |
|
124 |
||
4470 | 125 |
(*B only issues challenges in response to WL1. Not used.*) |
11185
1b737b4c2108
Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11150
diff
changeset
|
126 |
Goal "[| Says B A (Nonce NB) \\<in> set evs; B \\<noteq> Spy; evs \\<in> woolam |] \ |
1b737b4c2108
Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11150
diff
changeset
|
127 |
\ ==> \\<exists>A'. Says A' B (Agent A) \\<in> set evs"; |
4470 | 128 |
by (etac rev_mp 1); |
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3471
diff
changeset
|
129 |
by (parts_induct_tac 1); |
3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset
|
130 |
by (ALLGOALS Blast_tac); |
4470 | 131 |
qed "B_said_WL2"; |
2274 | 132 |
|
133 |
||
134 |
(**CANNOT be proved because A doesn't know where challenges come from... |
|
11185
1b737b4c2108
Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11150
diff
changeset
|
135 |
Goal "[| A \\<notin> bad; B \\<noteq> Spy; evs \\<in> woolam |] \ |
1b737b4c2108
Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11150
diff
changeset
|
136 |
\ ==> Crypt (shrK A) (Nonce NB) \\<in> parts (spies evs) & \ |
1b737b4c2108
Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11150
diff
changeset
|
137 |
\ Says B A (Nonce NB) \\<in> set evs \ |
1b737b4c2108
Some X-symbols for <notin>, <noteq>, <forall>, <exists>
paulson
parents:
11150
diff
changeset
|
138 |
\ --> Says A B (Crypt (shrK A) (Nonce NB)) \\<in> set evs"; |
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3471
diff
changeset
|
139 |
by (parts_induct_tac 1); |
4470 | 140 |
by (Blast_tac 1); |
3730 | 141 |
by Safe_tac; |
2274 | 142 |
**) |