author  paulson 
Tue, 23 Dec 1997 11:43:48 +0100  
changeset 4470  af3239def3d4 
parent 4449  df30e75f670f 
child 4477  b3e5857d8d99 
permissions  rwrr 
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 WooLam 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 615. 

11 
*) 

12 

13 
open WooLam; 

14 

4449  15 
set proof_timing; 
2274  16 
HOL_quantifiers := false; 
17 

4470  18 
AddEs spies_partsEs; 
19 
AddDs [impOfSubs analz_subset_parts]; 

20 
AddDs [impOfSubs Fake_parts_insert]; 

21 

2274  22 

2321  23 
(*A "possibility property": there are traces that reach the end*) 
2274  24 
goal thy 
25 
"!!A B. [ A ~= B; A ~= Server; B ~= Server ] \ 

2283
68829cf138fc
Swapping arguments of Crypt; removing argument lost
paulson
parents:
2274
diff
changeset

26 
\ ==> EX NB. EX evs: woolam. \ 
3466
30791e5a69c4
Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents:
3465
diff
changeset

27 
\ Says Server B (Crypt (shrK B) {Agent A, Nonce NB}) : set evs"; 
2274  28 
by (REPEAT (resolve_tac [exI,bexI] 1)); 
29 
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

30 
woolam.WL4 RS woolam.WL5) 2); 
3471
cd37ec057028
Now the possibility proof calls the appropriate tactic
paulson
parents:
3466
diff
changeset

31 
by possibility_tac; 
2274  32 
result(); 
33 

34 

35 
(**** Inductive proofs about woolam ****) 

36 

37 
(*Nobody sends themselves messages*) 

3465  38 
goal thy "!!evs. evs : woolam ==> ALL A X. Says A A X ~: set 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 

3683  48 
goal thy "!!evs. Says A' B X : set evs ==> X : analz (spies evs)"; 
49 
by (etac (Says_imp_spies RS analz.Inj) 1); 

50 
qed "WL4_analz_spies"; 

2274  51 

3683  52 
bind_thm ("WL4_parts_spies", 
53 
WL4_analz_spies RS (impOfSubs analz_subset_parts)); 

2274  54 

3683  55 
(*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

56 
fun parts_induct_tac i = 
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3471
diff
changeset

57 
etac woolam.induct i THEN 
3683  58 
forward_tac [WL4_parts_spies] (i+5) THEN 
3471
cd37ec057028
Now the possibility proof calls the appropriate tactic
paulson
parents:
3466
diff
changeset

59 
prove_simple_subgoals_tac 1; 
2274  60 

61 

3683  62 
(** Theorems of the form X ~: parts (spies evs) imply that NOBODY 
2274  63 
sends messages containing X! **) 
64 

3683  65 
(*Spy never sees another agent's shared key! (unless it's bad at start)*) 
2274  66 
goal thy 
3683  67 
"!!evs. 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

68 
by (parts_induct_tac 1); 
4470  69 
by (Blast_tac 1); 
2274  70 
qed "Spy_see_shrK"; 
71 
Addsimps [Spy_see_shrK]; 

72 

73 
goal thy 

3683  74 
"!!evs. evs : woolam ==> (Key (shrK A) : analz (spies evs)) = (A : bad)"; 
4470  75 
by (Auto_tac()); 
2274  76 
qed "Spy_analz_shrK"; 
77 
Addsimps [Spy_analz_shrK]; 

78 

4470  79 
AddSDs [Spy_see_shrK RSN (2, rev_iffD1), 
80 
Spy_analz_shrK RSN (2, rev_iffD1)]; 

2274  81 

82 

83 
(**** Autheticity properties for WooLam ****) 

84 

85 

86 
(*** WL4 ***) 

87 

88 
(*If the encrypted message appears then it originated with Alice*) 

89 
goal thy 

4470  90 
"!!evs. [ Crypt (shrK A) (Nonce NB) : parts (spies evs); \ 
91 
\ A ~: bad; evs : woolam ] \ 

92 
\ ==> EX B. Says A B (Crypt (shrK A) (Nonce NB)) : set evs"; 

93 
by (etac rev_mp 1); 

3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3471
diff
changeset

94 
by (parts_induct_tac 1); 
4470  95 
by (ALLGOALS Blast_tac); 
96 
qed "NB_Crypt_imp_Alice_msg"; 

2274  97 

98 
(*Guarantee for Server: if it gets a message containing a certificate from 

99 
Alice, then she originated that certificate. But we DO NOT know that B 

100 
ever saw it: the Spy may have rerouted the message to the Server.*) 

101 
goal thy 

4470  102 
"!!evs. [ Says B' Server {Agent A, Agent B, Crypt (shrK A) (Nonce NB)} \ 
103 
\ : set evs; \ 

104 
\ A ~: bad; evs : woolam ] \ 

3465  105 
\ ==> EX B. Says A B (Crypt (shrK A) (Nonce NB)) : set evs"; 
4470  106 
by (blast_tac (claset() addSIs [NB_Crypt_imp_Alice_msg]) 1); 
2321  107 
qed "Server_trusts_WL4"; 
2274  108 

4470  109 
AddDs [Server_trusts_WL4]; 
110 

2274  111 

112 
(*** WL5 ***) 

113 

114 
(*Server sent WL5 only if it received the right sort of message*) 

115 
goal thy 

4470  116 
"!!evs. [ Says Server B (Crypt (shrK B) {Agent A, NB}) : set evs; \ 
117 
\ evs : woolam ] \ 

118 
\ ==> EX B'. Says B' Server {Agent A, Agent B, Crypt (shrK A) NB} \ 

119 
\ : set evs"; 

120 
by (etac rev_mp 1); 

3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3471
diff
changeset

121 
by (parts_induct_tac 1); 
3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

122 
by (ALLGOALS Blast_tac); 
4470  123 
qed "Server_sent_WL5"; 
2274  124 

4470  125 
AddDs [Server_sent_WL5]; 
2274  126 

127 
(*If the encrypted message appears then it originated with the Server!*) 

128 
goal thy 

4470  129 
"!!evs. [ Crypt (shrK B) {Agent A, NB} : parts (spies evs); \ 
130 
\ B ~: bad; evs : woolam ] \ 

131 
\ ==> Says Server B (Crypt (shrK B) {Agent A, NB}) : set evs"; 

132 
by (etac rev_mp 1); 

3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3471
diff
changeset

133 
by (parts_induct_tac 1); 
4470  134 
by (Blast_tac 1); 
2274  135 
qed_spec_mp "NB_Crypt_imp_Server_msg"; 
136 

137 
(*Guarantee for B. If B gets the Server's certificate then A has encrypted 

138 
the nonce using her key. This event can be no older than the nonce itself. 

139 
But A may have sent the nonce to some other agent and it could have reached 

140 
the Server via the Spy.*) 

141 
goal thy 

3465  142 
"!!evs. [ Says S B (Crypt (shrK B) {Agent A, Nonce NB}): set evs; \ 
3683  143 
\ A ~: bad; B ~: bad; evs : woolam ] \ 
3465  144 
\ ==> EX B. Says A B (Crypt (shrK A) (Nonce NB)) : set evs"; 
4470  145 
by (blast_tac (claset() addSDs [NB_Crypt_imp_Server_msg]) 1); 
2321  146 
qed "B_trusts_WL5"; 
2274  147 

148 

4470  149 
(*B only issues challenges in response to WL1. Not used.*) 
2274  150 
goal thy 
4470  151 
"!!evs. [ Says B A (Nonce NB) : set evs; B ~= Spy; evs : woolam ] \ 
152 
\ ==> EX A'. Says A' B (Agent A) : set evs"; 

153 
by (etac rev_mp 1); 

3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3471
diff
changeset

154 
by (parts_induct_tac 1); 
3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

155 
by (ALLGOALS Blast_tac); 
4470  156 
qed "B_said_WL2"; 
2274  157 

158 

159 
(**CANNOT be proved because A doesn't know where challenges come from... 

160 
goal thy 

3683  161 
"!!evs. [ A ~: bad; B ~= Spy; evs : woolam ] \ 
162 
\ ==> Crypt (shrK A) (Nonce NB) : parts (spies evs) & \ 

3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3471
diff
changeset

163 
\ Says B A (Nonce NB) : set evs \ 
3465  164 
\ > 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

165 
by (parts_induct_tac 1); 
4470  166 
by (Blast_tac 1); 
3730  167 
by Safe_tac; 
2274  168 
**) 