author  paulson 
Fri, 11 Jul 1997 13:26:15 +0200  
changeset 3512  9dcb4daa15e8 
parent 3477  3aced7fa7d8b 
child 3519  ab0a9fbed4c0 
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)"; 

19 
by (Step_tac 1); 

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 

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

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

41 
by (agent.induct_tac "C" 1); 
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 

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

47 
(*** Function "sees" ***) 
2497  48 

2318  49 
(*Agents see their own private keys!*) 
50 
goal thy "A ~= Spy > Key (priK A) : sees lost A evs"; 

51 
by (list.induct_tac "evs" 1); 

52 
by (agent.induct_tac "A" 1); 

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

53 
by (ALLGOALS (asm_simp_tac (!simpset addsimps [sees_Cons]))); 
2318  54 
qed_spec_mp "sees_own_priK"; 
55 

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

56 
(*All public keys are visible to all*) 
c2334f9532ab
New and stronger lemmas; more default simp/cla rules
paulson
parents:
3465
diff
changeset

57 
goal thy "Key (pubK A) : sees lost B evs"; 
2318  58 
by (list.induct_tac "evs" 1); 
3473
c2334f9532ab
New and stronger lemmas; more default simp/cla rules
paulson
parents:
3465
diff
changeset

59 
by (agent.induct_tac "B" 1); 
3512
9dcb4daa15e8
Moving common declarations and proofs from theories "Shared"
paulson
parents:
3477
diff
changeset

60 
by (ALLGOALS (asm_simp_tac (!simpset addsimps [sees_Cons]))); 
2318  61 
by (Auto_tac ()); 
62 
qed_spec_mp "sees_pubK"; 

63 

64 
(*Spy sees private keys of lost agents!*) 

65 
goal thy "!!A. A: lost ==> Key (priK A) : sees lost Spy evs"; 

66 
by (list.induct_tac "evs" 1); 

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

67 
by (ALLGOALS (asm_simp_tac (!simpset addsimps [sees_Cons]))); 
9dcb4daa15e8
Moving common declarations and proofs from theories "Shared"
paulson
parents:
3477
diff
changeset

68 
by (Blast_tac 1); 
2318  69 
qed "Spy_sees_lost"; 
70 

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

71 
AddIffs [sees_pubK, sees_pubK RS analz.Inj]; 
2318  72 
AddSIs [sees_own_priK, Spy_sees_lost]; 
73 

74 

3442  75 
(*For not_lost_tac*) 
76 
goal thy "!!A. [ Crypt (pubK A) X : analz (sees lost Spy evs); A: lost ] \ 

77 
\ ==> X : analz (sees lost Spy evs)"; 

78 
by (blast_tac (!claset addSDs [analz.Decrypt]) 1); 

79 
qed "Crypt_Spy_analz_lost"; 

2318  80 

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

83 
fun not_lost_tac s = 

84 
case_tac ("(" ^ s ^ ") : lost") THEN' 

85 
SELECT_GOAL 

86 
(REPEAT_DETERM (dtac (Says_imp_sees_Spy RS analz.Inj) 1) THEN 

87 
REPEAT_DETERM (etac MPair_analz 1) THEN 

88 
THEN_BEST_FIRST 

89 
(dres_inst_tac [("A", s)] Crypt_Spy_analz_lost 1 THEN assume_tac 1) 

90 
(has_fewer_prems 1, size_of_thm) 

91 
(Step_tac 1)); 

2318  92 

93 

2497  94 
(*** Fresh nonces ***) 
95 

96 
goal thy "Nonce N ~: parts (initState lost B)"; 

97 
by (agent.induct_tac "B" 1); 

98 
by (Auto_tac ()); 

99 
qed "Nonce_notin_initState"; 

100 
AddIffs [Nonce_notin_initState]; 

101 

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

102 
goal thy "Nonce N ~: used []"; 
9dcb4daa15e8
Moving common declarations and proofs from theories "Shared"
paulson
parents:
3477
diff
changeset

103 
by (simp_tac (!simpset addsimps [used_def]) 1); 
9dcb4daa15e8
Moving common declarations and proofs from theories "Shared"
paulson
parents:
3477
diff
changeset

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

105 
Addsimps [Nonce_notin_used_empty]; 
2497  106 

107 

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

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

109 

2497  110 
goalw thy [used_def] "EX N. ALL n. N<=n > Nonce n ~: used evs"; 
111 
by (list.induct_tac "evs" 1); 

112 
by (res_inst_tac [("x","0")] exI 1); 

113 
by (Step_tac 1); 

114 
by (Full_simp_tac 1); 

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

115 
(*Inductive step*) 
2497  116 
by (event.induct_tac "a" 1); 
3512
9dcb4daa15e8
Moving common declarations and proofs from theories "Shared"
paulson
parents:
3477
diff
changeset

117 
by (ALLGOALS (full_simp_tac 
9dcb4daa15e8
Moving common declarations and proofs from theories "Shared"
paulson
parents:
3477
diff
changeset

118 
(!simpset delsimps [sees_Notes] 
9dcb4daa15e8
Moving common declarations and proofs from theories "Shared"
paulson
parents:
3477
diff
changeset

119 
addsimps [UN_parts_sees_Says, 
9dcb4daa15e8
Moving common declarations and proofs from theories "Shared"
paulson
parents:
3477
diff
changeset

120 
UN_parts_sees_Notes]))); 
9dcb4daa15e8
Moving common declarations and proofs from theories "Shared"
paulson
parents:
3477
diff
changeset

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

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

125 
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

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

127 
by (rtac selectI 1); 
2497  128 
by (Fast_tac 1); 
129 
qed "Nonce_supply"; 

130 

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

131 
(*Tactic for possibility theorems*) 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2497
diff
changeset

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

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

134 
(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

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

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

137 
resolve_tac [refl, conjI, Nonce_supply])); 
2497  138 

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

139 

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

140 
(*** Specialized rewriting for the analz_image_... theorems ***) 
2318  141 

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

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

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

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

145 

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

146 
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

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

148 
qed "insert_Key_image"; 
2318  149 

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

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

151 
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

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

153 
!simpset delsimps [image_insert, image_Un] 
9dcb4daa15e8
Moving common declarations and proofs from theories "Shared"
paulson
parents:
3477
diff
changeset

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

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

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

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

158 
setloop split_tac [expand_if]; 
2318  159 