author  paulson 
Thu, 02 Jul 1998 17:48:11 +0200  
changeset 5114  c729d4c299c1 
parent 5076  fbc9d95b62ba 
child 5223  4cb05273f764 
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*) 
5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

24 
Goal "[ A ~= B; A ~= Server; B ~= Server ] \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

25 
\ ==> EX NB. EX evs: woolam. \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

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

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

30 
by possibility_tac; 
2274  31 
result(); 
32 

33 

34 
(**** Inductive proofs about woolam ****) 

35 

36 
(*Nobody sends themselves messages*) 

5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

37 
Goal "evs : woolam ==> ALL A X. Says A A X ~: set evs"; 
2274  38 
by (etac woolam.induct 1); 
4477
b3e5857d8d99
New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
paulson
parents:
4470
diff
changeset

39 
by Auto_tac; 
2274  40 
qed_spec_mp "not_Says_to_self"; 
41 
Addsimps [not_Says_to_self]; 

42 
AddSEs [not_Says_to_self RSN (2, rev_notE)]; 

43 

44 

45 
(** For reasoning about the encrypted portion of messages **) 

46 

5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

47 
Goal "Says A' B X : set evs ==> X : analz (spies evs)"; 
3683  48 
by (etac (Says_imp_spies RS analz.Inj) 1); 
49 
qed "WL4_analz_spies"; 

2274  50 

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

2274  53 

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

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

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

58 
prove_simple_subgoals_tac 1; 
2274  59 

60 

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

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

65 
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

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

70 

5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

71 
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

72 
by Auto_tac; 
2274  73 
qed "Spy_analz_shrK"; 
74 
Addsimps [Spy_analz_shrK]; 

75 

4470  76 
AddSDs [Spy_see_shrK RSN (2, rev_iffD1), 
77 
Spy_analz_shrK RSN (2, rev_iffD1)]; 

2274  78 

79 

80 
(**** Autheticity properties for WooLam ****) 

81 

82 

83 
(*** WL4 ***) 

84 

85 
(*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

86 
Goal "[ Crypt (shrK A) (Nonce NB) : parts (spies evs); \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

87 
\ A ~: bad; evs : woolam ] \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

88 
\ ==> EX B. Says A B (Crypt (shrK A) (Nonce NB)) : set evs"; 
4470  89 
by (etac rev_mp 1); 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3471
diff
changeset

90 
by (parts_induct_tac 1); 
4470  91 
by (ALLGOALS Blast_tac); 
92 
qed "NB_Crypt_imp_Alice_msg"; 

2274  93 

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

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

96 
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

97 
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

98 
\ : set evs; \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

99 
\ A ~: bad; evs : woolam ] \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

100 
\ ==> EX B. Says A B (Crypt (shrK A) (Nonce NB)) : set evs"; 
4470  101 
by (blast_tac (claset() addSIs [NB_Crypt_imp_Alice_msg]) 1); 
2321  102 
qed "Server_trusts_WL4"; 
2274  103 

4470  104 
AddDs [Server_trusts_WL4]; 
105 

2274  106 

107 
(*** WL5 ***) 

108 

109 
(*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

110 
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

111 
\ evs : woolam ] \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

112 
\ ==> 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

113 
\ : set evs"; 
4470  114 
by (etac rev_mp 1); 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3471
diff
changeset

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

116 
by (ALLGOALS Blast_tac); 
4470  117 
qed "Server_sent_WL5"; 
2274  118 

4470  119 
AddDs [Server_sent_WL5]; 
2274  120 

121 
(*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

122 
Goal "[ Crypt (shrK B) {Agent A, NB} : parts (spies evs); \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

123 
\ B ~: bad; evs : woolam ] \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

124 
\ ==> Says Server B (Crypt (shrK B) {Agent A, NB}) : set evs"; 
4470  125 
by (etac rev_mp 1); 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3471
diff
changeset

126 
by (parts_induct_tac 1); 
4470  127 
by (Blast_tac 1); 
2274  128 
qed_spec_mp "NB_Crypt_imp_Server_msg"; 
129 

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

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

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

133 
the Server via the Spy.*) 

5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

134 
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

135 
\ A ~: bad; B ~: bad; evs : woolam ] \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

136 
\ ==> EX B. Says A B (Crypt (shrK A) (Nonce NB)) : set evs"; 
4470  137 
by (blast_tac (claset() addSDs [NB_Crypt_imp_Server_msg]) 1); 
2321  138 
qed "B_trusts_WL5"; 
2274  139 

140 

4470  141 
(*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

142 
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

143 
\ ==> EX A'. Says A' B (Agent A) : set evs"; 
4470  144 
by (etac rev_mp 1); 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3471
diff
changeset

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

146 
by (ALLGOALS Blast_tac); 
4470  147 
qed "B_said_WL2"; 
2274  148 

149 

150 
(**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

151 
Goal "[ A ~: bad; B ~= Spy; evs : woolam ] \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

152 
\ ==> Crypt (shrK A) (Nonce NB) : parts (spies evs) & \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

153 
\ Says B A (Nonce NB) : set evs \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

154 
\ > 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

155 
by (parts_induct_tac 1); 
4470  156 
by (Blast_tac 1); 
3730  157 
by Safe_tac; 
2274  158 
**) 