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