author  nipkow 
Fri, 24 Nov 2000 16:49:27 +0100  
changeset 10519  ade64af4c57c 
parent 9970  dfe4747c8318 
child 10833  c0844a30ea4e 
permissions  rwrr 
2318  1 
(* Title: HOL/Auth/Public 
2 
ID: $Id$ 

3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 

4 
Copyright 1996 University of Cambridge 

5 

6 
Theory of Public Keys (common to all symmetrickey protocols) 

7 

8 
Server keys; initial states of agents; new nonces and keys; function "sees" 

9 
*) 

10 

2497  11 
(*** Basic properties of pubK & priK ***) 
12 

13 
AddIffs [inj_pubK RS inj_eq]; 

3477  14 

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

15 
Goal "(priK A = priK B) = (A=B)"; 
3730  16 
by Safe_tac; 
3477  17 
by (dres_inst_tac [("f","invKey")] arg_cong 1); 
18 
by (Full_simp_tac 1); 

19 
qed "priK_inj_eq"; 

20 

21 
AddIffs [priK_inj_eq]; 

3473
c2334f9532ab
New and stronger lemmas; more default simp/cla rules
paulson
parents:
3465
diff
changeset

22 
AddIffs [priK_neq_pubK, priK_neq_pubK RS not_sym]; 
c2334f9532ab
New and stronger lemmas; more default simp/cla rules
paulson
parents:
3465
diff
changeset

23 

5076  24 
Goalw [isSymKey_def] "~ isSymKey (pubK A)"; 
3473
c2334f9532ab
New and stronger lemmas; more default simp/cla rules
paulson
parents:
3465
diff
changeset

25 
by (Simp_tac 1); 
c2334f9532ab
New and stronger lemmas; more default simp/cla rules
paulson
parents:
3465
diff
changeset

26 
qed "not_isSymKey_pubK"; 
c2334f9532ab
New and stronger lemmas; more default simp/cla rules
paulson
parents:
3465
diff
changeset

27 

5076  28 
Goalw [isSymKey_def] "~ isSymKey (priK A)"; 
3473
c2334f9532ab
New and stronger lemmas; more default simp/cla rules
paulson
parents:
3465
diff
changeset

29 
by (Simp_tac 1); 
c2334f9532ab
New and stronger lemmas; more default simp/cla rules
paulson
parents:
3465
diff
changeset

30 
qed "not_isSymKey_priK"; 
c2334f9532ab
New and stronger lemmas; more default simp/cla rules
paulson
parents:
3465
diff
changeset

31 

c2334f9532ab
New and stronger lemmas; more default simp/cla rules
paulson
parents:
3465
diff
changeset

32 
AddIffs [not_isSymKey_pubK, not_isSymKey_priK]; 
c2334f9532ab
New and stronger lemmas; more default simp/cla rules
paulson
parents:
3465
diff
changeset

33 

4422
21238c9d363e
Simplified proofs using rewrites for f``A where f is injective
paulson
parents:
4091
diff
changeset

34 

21238c9d363e
Simplified proofs using rewrites for f``A where f is injective
paulson
parents:
4091
diff
changeset

35 
(** "Image" equations that hold for injective functions **) 
21238c9d363e
Simplified proofs using rewrites for f``A where f is injective
paulson
parents:
4091
diff
changeset

36 

5076  37 
Goal "(invKey x : invKey``A) = (x:A)"; 
4477
b3e5857d8d99
New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
paulson
parents:
4422
diff
changeset

38 
by Auto_tac; 
4422
21238c9d363e
Simplified proofs using rewrites for f``A where f is injective
paulson
parents:
4091
diff
changeset

39 
qed "invKey_image_eq"; 
21238c9d363e
Simplified proofs using rewrites for f``A where f is injective
paulson
parents:
4091
diff
changeset

40 

21238c9d363e
Simplified proofs using rewrites for f``A where f is injective
paulson
parents:
4091
diff
changeset

41 
(*holds because invKey is injective*) 
5076  42 
Goal "(pubK x : pubK``A) = (x:A)"; 
4477
b3e5857d8d99
New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
paulson
parents:
4422
diff
changeset

43 
by Auto_tac; 
4422
21238c9d363e
Simplified proofs using rewrites for f``A where f is injective
paulson
parents:
4091
diff
changeset

44 
qed "pubK_image_eq"; 
21238c9d363e
Simplified proofs using rewrites for f``A where f is injective
paulson
parents:
4091
diff
changeset

45 

5076  46 
Goal "(priK x ~: pubK``A)"; 
4477
b3e5857d8d99
New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
paulson
parents:
4422
diff
changeset

47 
by Auto_tac; 
4422
21238c9d363e
Simplified proofs using rewrites for f``A where f is injective
paulson
parents:
4091
diff
changeset

48 
qed "priK_pubK_image_eq"; 
21238c9d363e
Simplified proofs using rewrites for f``A where f is injective
paulson
parents:
4091
diff
changeset

49 
Addsimps [invKey_image_eq, pubK_image_eq, priK_pubK_image_eq]; 
21238c9d363e
Simplified proofs using rewrites for f``A where f is injective
paulson
parents:
4091
diff
changeset

50 

21238c9d363e
Simplified proofs using rewrites for f``A where f is injective
paulson
parents:
4091
diff
changeset

51 

3512
9dcb4daa15e8
Moving common declarations and proofs from theories "Shared"
paulson
parents:
3477
diff
changeset

52 
(** Rewrites should not refer to initState(Friend i) 
9dcb4daa15e8
Moving common declarations and proofs from theories "Shared"
paulson
parents:
3477
diff
changeset

53 
 not in normal form! **) 
9dcb4daa15e8
Moving common declarations and proofs from theories "Shared"
paulson
parents:
3477
diff
changeset

54 

5076  55 
Goalw [keysFor_def] "keysFor (parts (initState C)) = {}"; 
3667  56 
by (induct_tac "C" 1); 
4091  57 
by (auto_tac (claset() addIs [range_eqI], simpset())); 
3512
9dcb4daa15e8
Moving common declarations and proofs from theories "Shared"
paulson
parents:
3477
diff
changeset

58 
qed "keysFor_parts_initState"; 
9dcb4daa15e8
Moving common declarations and proofs from theories "Shared"
paulson
parents:
3477
diff
changeset

59 
Addsimps [keysFor_parts_initState]; 
9dcb4daa15e8
Moving common declarations and proofs from theories "Shared"
paulson
parents:
3477
diff
changeset

60 

9dcb4daa15e8
Moving common declarations and proofs from theories "Shared"
paulson
parents:
3477
diff
changeset

61 

3683  62 
(*** Function "spies" ***) 
2497  63 

2318  64 
(*Agents see their own private keys!*) 
5076  65 
Goal "Key (priK A) : initState A"; 
3667  66 
by (induct_tac "A" 1); 
4477
b3e5857d8d99
New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
paulson
parents:
4422
diff
changeset

67 
by Auto_tac; 
3683  68 
qed "priK_in_initState"; 
69 
AddIffs [priK_in_initState]; 

2318  70 

3683  71 
(*All public keys are visible*) 
5076  72 
Goal "Key (pubK A) : spies evs"; 
3667  73 
by (induct_tac "evs" 1); 
3683  74 
by (ALLGOALS (asm_simp_tac 
6308
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5223
diff
changeset

75 
(simpset() addsimps [imageI, knows_Cons] 
4686  76 
addsplits [expand_event_case]))); 
3683  77 
qed_spec_mp "spies_pubK"; 
2318  78 

3683  79 
(*Spy sees private keys of bad agents!*) 
5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

80 
Goal "A: bad ==> Key (priK A) : spies evs"; 
3667  81 
by (induct_tac "evs" 1); 
3683  82 
by (ALLGOALS (asm_simp_tac 
6308
76f3865a2b1d
Added Bella's "Gets" model for Otway_Rees. Also affects some other theories.
paulson
parents:
5223
diff
changeset

83 
(simpset() addsimps [imageI, knows_Cons] 
4686  84 
addsplits [expand_event_case]))); 
3683  85 
qed "Spy_spies_bad"; 
2318  86 

3683  87 
AddIffs [spies_pubK, spies_pubK RS analz.Inj]; 
88 
AddSIs [Spy_spies_bad]; 

2318  89 

90 

3683  91 
(*For not_bad_tac*) 
5114
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

92 
Goal "[ Crypt (pubK A) X : analz (spies evs); A: bad ] \ 
c729d4c299c1
Deleted leading parameters thanks to new Goal command
paulson
parents:
5076
diff
changeset

93 
\ ==> X : analz (spies evs)"; 
4091  94 
by (blast_tac (claset() addSDs [analz.Decrypt]) 1); 
3683  95 
qed "Crypt_Spy_analz_bad"; 
2318  96 

3442  97 
(*Prove that the agent is uncompromised by the confidentiality of 
98 
a component of a message she's said.*) 

3683  99 
fun not_bad_tac s = 
100 
case_tac ("(" ^ s ^ ") : bad") THEN' 

3442  101 
SELECT_GOAL 
3683  102 
(REPEAT_DETERM (dtac (Says_imp_spies RS analz.Inj) 1) THEN 
3442  103 
REPEAT_DETERM (etac MPair_analz 1) THEN 
104 
THEN_BEST_FIRST 

3683  105 
(dres_inst_tac [("A", s)] Crypt_Spy_analz_bad 1 THEN assume_tac 1) 
3442  106 
(has_fewer_prems 1, size_of_thm) 
3730  107 
Safe_tac); 
2318  108 

109 

2497  110 
(*** Fresh nonces ***) 
111 

5076  112 
Goal "Nonce N ~: parts (initState B)"; 
3667  113 
by (induct_tac "B" 1); 
4477
b3e5857d8d99
New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
paulson
parents:
4422
diff
changeset

114 
by Auto_tac; 
2497  115 
qed "Nonce_notin_initState"; 
116 
AddIffs [Nonce_notin_initState]; 

117 

5076  118 
Goal "Nonce N ~: used []"; 
4091  119 
by (simp_tac (simpset() addsimps [used_Nil]) 1); 
3512
9dcb4daa15e8
Moving common declarations and proofs from theories "Shared"
paulson
parents:
3477
diff
changeset

120 
qed "Nonce_notin_used_empty"; 
9dcb4daa15e8
Moving common declarations and proofs from theories "Shared"
paulson
parents:
3477
diff
changeset

121 
Addsimps [Nonce_notin_used_empty]; 
2497  122 

123 

3512
9dcb4daa15e8
Moving common declarations and proofs from theories "Shared"
paulson
parents:
3477
diff
changeset

124 
(*** Supply fresh nonces for possibility theorems. ***) 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2497
diff
changeset

125 

3683  126 
(*In any trace, there is an upper bound N on the greatest nonce in use.*) 
5076  127 
Goal "EX N. ALL n. N<=n > Nonce n ~: used evs"; 
3667  128 
by (induct_tac "evs" 1); 
2497  129 
by (res_inst_tac [("x","0")] exI 1); 
3683  130 
by (ALLGOALS (asm_simp_tac 
4091  131 
(simpset() addsimps [used_Cons] 
4686  132 
addsplits [expand_event_case]))); 
3730  133 
by Safe_tac; 
3512
9dcb4daa15e8
Moving common declarations and proofs from theories "Shared"
paulson
parents:
3477
diff
changeset

134 
by (ALLGOALS (rtac (msg_Nonce_supply RS exE))); 
4091  135 
by (ALLGOALS (blast_tac (claset() addSEs [add_leE]))); 
2497  136 
val lemma = result(); 
137 

5076  138 
Goal "EX N. Nonce N ~: used evs"; 
3683  139 
by (rtac (lemma RS exE) 1); 
140 
by (Blast_tac 1); 

141 
qed "Nonce_supply1"; 

142 

5076  143 
Goal "Nonce (@ N. Nonce N ~: used evs) ~: used evs"; 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2497
diff
changeset

144 
by (rtac (lemma RS exE) 1); 
9970  145 
by (rtac someI 1); 
2497  146 
by (Fast_tac 1); 
147 
qed "Nonce_supply"; 

148 

2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2497
diff
changeset

149 
(*Tactic for possibility theorems*) 
3544
6ae62d55a620
Now possibility_tac is an explicit function, in order to delay
paulson
parents:
3519
diff
changeset

150 
fun possibility_tac st = st > 
3673
3b06747c3f37
Having "addcongs [if_weak_cong]" in analz_image_..._ss makes simplification
paulson
parents:
3667
diff
changeset

151 
REPEAT (*omit used_Says so that Nonces start from different traces!*) 
8054
2ce57ef2a4aa
used image_eq_UN to speed up slow proofs of base cases
paulson
parents:
6915
diff
changeset

152 
(ALLGOALS (simp_tac (simpset() delsimps [used_Says])) 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2497
diff
changeset

153 
THEN 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2497
diff
changeset

154 
REPEAT_FIRST (eq_assume_tac ORELSE' 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2497
diff
changeset

155 
resolve_tac [refl, conjI, Nonce_supply])); 
2497  156 

3512
9dcb4daa15e8
Moving common declarations and proofs from theories "Shared"
paulson
parents:
3477
diff
changeset

157 

9dcb4daa15e8
Moving common declarations and proofs from theories "Shared"
paulson
parents:
3477
diff
changeset

158 
(*** Specialized rewriting for the analz_image_... theorems ***) 
2318  159 

5076  160 
Goal "insert (Key K) H = Key `` {K} Un H"; 
3512
9dcb4daa15e8
Moving common declarations and proofs from theories "Shared"
paulson
parents:
3477
diff
changeset

161 
by (Blast_tac 1); 
9dcb4daa15e8
Moving common declarations and proofs from theories "Shared"
paulson
parents:
3477
diff
changeset

162 
qed "insert_Key_singleton"; 
9dcb4daa15e8
Moving common declarations and proofs from theories "Shared"
paulson
parents:
3477
diff
changeset

163 

5076  164 
Goal "insert (Key K) (Key``KK Un C) = Key `` (insert K KK) Un C"; 
3512
9dcb4daa15e8
Moving common declarations and proofs from theories "Shared"
paulson
parents:
3477
diff
changeset

165 
by (Blast_tac 1); 
9dcb4daa15e8
Moving common declarations and proofs from theories "Shared"
paulson
parents:
3477
diff
changeset

166 
qed "insert_Key_image"; 
2318  167 

3512
9dcb4daa15e8
Moving common declarations and proofs from theories "Shared"
paulson
parents:
3477
diff
changeset

168 
(*Reverse the normal simplification of "image" to build up (not break down) 
9dcb4daa15e8
Moving common declarations and proofs from theories "Shared"
paulson
parents:
3477
diff
changeset

169 
the set of keys. Based on analz_image_freshK_ss, but simpler.*) 
9dcb4daa15e8
Moving common declarations and proofs from theories "Shared"
paulson
parents:
3477
diff
changeset

170 
val analz_image_keys_ss = 
6915  171 
simpset() delsimps [image_insert, image_Un] 
172 
delsimps [imp_disjL] (*reduces blowup*) 

173 
addsimps [image_insert RS sym, image_Un RS sym, 

174 
rangeI, 

175 
insert_Key_singleton, 

176 
insert_Key_image, Un_assoc RS sym]; 

2318  177 