author  paulson 
Mon, 29 Sep 1997 11:47:01 +0200  
changeset 3730  6933d20f335f 
parent 3683  aafe719dff14 
child 3919  c036caebfc75 
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 

11 

12 
open Public; 

13 

2497  14 
(*** Basic properties of pubK & priK ***) 
15 

16 
AddIffs [inj_pubK RS inj_eq]; 

3477  17 

18 
goal thy "!!A B. (priK A = priK B) = (A=B)"; 

3730  19 
by Safe_tac; 
3477  20 
by (dres_inst_tac [("f","invKey")] arg_cong 1); 
21 
by (Full_simp_tac 1); 

22 
qed "priK_inj_eq"; 

23 

24 
AddIffs [priK_inj_eq]; 

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

25 
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

26 

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

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

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

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

30 

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

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

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

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

34 

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

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

36 

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

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

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

39 

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

40 
goalw thy [keysFor_def] "keysFor (parts (initState C)) = {}"; 
3667  41 
by (induct_tac "C" 1); 
3512
9dcb4daa15e8
Moving common declarations and proofs from theories "Shared"
paulson
parents:
3477
diff
changeset

42 
by (auto_tac (!claset addIs [range_eqI], !simpset)); 
9dcb4daa15e8
Moving common declarations and proofs from theories "Shared"
paulson
parents:
3477
diff
changeset

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

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

45 

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

46 

3683  47 
(*** Function "spies" ***) 
2497  48 

2318  49 
(*Agents see their own private keys!*) 
3683  50 
goal thy "Key (priK A) : initState A"; 
3667  51 
by (induct_tac "A" 1); 
3683  52 
by (Auto_tac()); 
53 
qed "priK_in_initState"; 

54 
AddIffs [priK_in_initState]; 

2318  55 

3683  56 
(*All public keys are visible*) 
57 
goal thy "Key (pubK A) : spies evs"; 

3667  58 
by (induct_tac "evs" 1); 
3683  59 
by (ALLGOALS (asm_simp_tac 
60 
(!simpset addsimps [imageI, spies_Cons] 

61 
setloop split_tac [expand_event_case, expand_if]))); 

62 
qed_spec_mp "spies_pubK"; 

2318  63 

3683  64 
(*Spy sees private keys of bad agents!*) 
65 
goal thy "!!A. A: bad ==> Key (priK A) : spies evs"; 

3667  66 
by (induct_tac "evs" 1); 
3683  67 
by (ALLGOALS (asm_simp_tac 
68 
(!simpset addsimps [imageI, spies_Cons] 

69 
setloop split_tac [expand_event_case, expand_if]))); 

70 
qed "Spy_spies_bad"; 

2318  71 

3683  72 
AddIffs [spies_pubK, spies_pubK RS analz.Inj]; 
73 
AddSIs [Spy_spies_bad]; 

2318  74 

75 

3683  76 
(*For not_bad_tac*) 
77 
goal thy "!!A. [ Crypt (pubK A) X : analz (spies evs); A: bad ] \ 

78 
\ ==> X : analz (spies evs)"; 

3442  79 
by (blast_tac (!claset addSDs [analz.Decrypt]) 1); 
3683  80 
qed "Crypt_Spy_analz_bad"; 
2318  81 

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

3683  84 
fun not_bad_tac s = 
85 
case_tac ("(" ^ s ^ ") : bad") THEN' 

3442  86 
SELECT_GOAL 
3683  87 
(REPEAT_DETERM (dtac (Says_imp_spies RS analz.Inj) 1) THEN 
3442  88 
REPEAT_DETERM (etac MPair_analz 1) THEN 
89 
THEN_BEST_FIRST 

3683  90 
(dres_inst_tac [("A", s)] Crypt_Spy_analz_bad 1 THEN assume_tac 1) 
3442  91 
(has_fewer_prems 1, size_of_thm) 
3730  92 
Safe_tac); 
2318  93 

94 

2497  95 
(*** Fresh nonces ***) 
96 

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

97 
goal thy "Nonce N ~: parts (initState B)"; 
3667  98 
by (induct_tac "B" 1); 
2497  99 
by (Auto_tac ()); 
100 
qed "Nonce_notin_initState"; 

101 
AddIffs [Nonce_notin_initState]; 

102 

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

103 
goal thy "Nonce N ~: used []"; 
3683  104 
by (simp_tac (!simpset addsimps [used_Nil]) 1); 
3512
9dcb4daa15e8
Moving common declarations and proofs from theories "Shared"
paulson
parents:
3477
diff
changeset

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

106 
Addsimps [Nonce_notin_used_empty]; 
2497  107 

108 

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

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

110 

3683  111 
(*In any trace, there is an upper bound N on the greatest nonce in use.*) 
112 
goal thy "EX N. ALL n. N<=n > Nonce n ~: used evs"; 

3667  113 
by (induct_tac "evs" 1); 
2497  114 
by (res_inst_tac [("x","0")] exI 1); 
3683  115 
by (ALLGOALS (asm_simp_tac 
116 
(!simpset addsimps [used_Cons] 

117 
setloop split_tac [expand_event_case, expand_if]))); 

3730  118 
by Safe_tac; 
3512
9dcb4daa15e8
Moving common declarations and proofs from theories "Shared"
paulson
parents:
3477
diff
changeset

119 
by (ALLGOALS (rtac (msg_Nonce_supply RS exE))); 
9dcb4daa15e8
Moving common declarations and proofs from theories "Shared"
paulson
parents:
3477
diff
changeset

120 
by (ALLGOALS (blast_tac (!claset addSEs [add_leE]))); 
2497  121 
val lemma = result(); 
122 

3683  123 
goal thy "EX N. Nonce N ~: used evs"; 
124 
by (rtac (lemma RS exE) 1); 

125 
by (Blast_tac 1); 

126 
qed "Nonce_supply1"; 

127 

2497  128 
goal thy "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

129 
by (rtac (lemma RS exE) 1); 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2497
diff
changeset

130 
by (rtac selectI 1); 
2497  131 
by (Fast_tac 1); 
132 
qed "Nonce_supply"; 

133 

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

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

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

136 
REPEAT (*omit used_Says so that Nonces start from different traces!*) 
3512
9dcb4daa15e8
Moving common declarations and proofs from theories "Shared"
paulson
parents:
3477
diff
changeset

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

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

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

140 
resolve_tac [refl, conjI, Nonce_supply])); 
2497  141 

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

142 

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

143 
(*** Specialized rewriting for the analz_image_... theorems ***) 
2318  144 

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

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

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

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

148 

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

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

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

151 
qed "insert_Key_image"; 
2318  152 

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

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

154 
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

155 
val analz_image_keys_ss = 
3673
3b06747c3f37
Having "addcongs [if_weak_cong]" in analz_image_..._ss makes simplification
paulson
parents:
3667
diff
changeset

156 
!simpset addcongs [if_weak_cong] 
3b06747c3f37
Having "addcongs [if_weak_cong]" in analz_image_..._ss makes simplification
paulson
parents:
3667
diff
changeset

157 
delsimps [image_insert, image_Un] 
3680
7588653475b2
Removed the simprule imp_disjL from the analz_image_..._ss to boost speed
paulson
parents:
3673
diff
changeset

158 
delsimps [imp_disjL] (*reduces blowup*) 
3512
9dcb4daa15e8
Moving common declarations and proofs from theories "Shared"
paulson
parents:
3477
diff
changeset

159 
addsimps [image_insert RS sym, image_Un RS sym, 
9dcb4daa15e8
Moving common declarations and proofs from theories "Shared"
paulson
parents:
3477
diff
changeset

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

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

162 
insert_Key_image, Un_assoc RS sym] 
9dcb4daa15e8
Moving common declarations and proofs from theories "Shared"
paulson
parents:
3477
diff
changeset

163 
setloop split_tac [expand_if]; 
2318  164 