author  nipkow 
Fri, 24 Nov 2000 16:49:27 +0100  
changeset 10519  ade64af4c57c 
parent 7499  23e090051cb8 
child 11150  67387142225e 
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 

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 
7499  42 
ftac 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 WooLam ****) 

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 
**) 