author  paulson 
Wed, 07 May 1997 13:01:43 +0200  
changeset 3121  cbb6c0c1c58a 
parent 2637  e9b203f854ae 
child 3432  04412cfe6861 
permissions  rwrr 
1995  1 
(* Title: HOL/Auth/Yahalom 
1985
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

2 
ID: $Id$ 
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

4 
Copyright 1996 University of Cambridge 
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

5 

84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

6 
Inductive relation "otway" for the Yahalom protocol. 
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

7 

84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

8 
From page 257 of 
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

9 
Burrows, Abadi and Needham. A Logic of Authentication. 
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

10 
Proc. Royal Soc. 426 (1989) 
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

11 
*) 
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

12 

1995  13 
open Yahalom; 
1985
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

14 

84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

15 
proof_timing:=true; 
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

16 
HOL_quantifiers := false; 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2454
diff
changeset

17 
Pretty.setdepth 25; 
1985
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

18 

3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

19 
(*Replacing the variable by a constant improves speed*) 
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

20 
val Says_imp_sees_Spy' = read_instantiate [("lost","lost")] Says_imp_sees_Spy; 
2637
e9b203f854ae
reflecting my recent changes of the simplifier and classical reasoner
oheimb
parents:
2516
diff
changeset

21 

1995  22 

2322  23 
(*A "possibility property": there are traces that reach the end*) 
1995  24 
goal thy 
25 
"!!A B. [ A ~= B; A ~= Server; B ~= Server ] \ 

2032  26 
\ ==> EX X NB K. EX evs: yahalom lost. \ 
2284
80ebd1a213fd
Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents:
2269
diff
changeset

27 
\ Says A B {X, Crypt K (Nonce NB)} : set_of_list evs"; 
1995  28 
by (REPEAT (resolve_tac [exI,bexI] 1)); 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2454
diff
changeset

29 
by (rtac (yahalom.Nil RS yahalom.YM1 RS yahalom.YM2 RS yahalom.YM3 RS 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2454
diff
changeset

30 
yahalom.YM4) 2); 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2454
diff
changeset

31 
by possibility_tac; 
2013  32 
result(); 
1995  33 

34 

1985
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

35 
(**** Inductive proofs about yahalom ****) 
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

36 

2110  37 
(*Monotonicity*) 
2045
ae1030e66745
Removed some dead wood. Transferred lemmas used to prove analz_image_newK
paulson
parents:
2032
diff
changeset

38 
goal thy "!!evs. lost' <= lost ==> yahalom lost' <= yahalom lost"; 
ae1030e66745
Removed some dead wood. Transferred lemmas used to prove analz_image_newK
paulson
parents:
2032
diff
changeset

39 
by (rtac subsetI 1); 
ae1030e66745
Removed some dead wood. Transferred lemmas used to prove analz_image_newK
paulson
parents:
2032
diff
changeset

40 
by (etac yahalom.induct 1); 
ae1030e66745
Removed some dead wood. Transferred lemmas used to prove analz_image_newK
paulson
parents:
2032
diff
changeset

41 
by (REPEAT_FIRST 
3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

42 
(blast_tac (!claset addIs (impOfSubs (sees_mono RS analz_mono RS synth_mono) 
2045
ae1030e66745
Removed some dead wood. Transferred lemmas used to prove analz_image_newK
paulson
parents:
2032
diff
changeset

43 
:: yahalom.intrs)))); 
ae1030e66745
Removed some dead wood. Transferred lemmas used to prove analz_image_newK
paulson
parents:
2032
diff
changeset

44 
qed "yahalom_mono"; 
ae1030e66745
Removed some dead wood. Transferred lemmas used to prove analz_image_newK
paulson
parents:
2032
diff
changeset

45 

1985
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

46 

84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

47 
(*Nobody sends themselves messages*) 
2051  48 
goal thy "!!evs. evs: yahalom lost ==> ALL A X. Says A A X ~: set_of_list evs"; 
2032  49 
by (etac yahalom.induct 1); 
1985
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

50 
by (Auto_tac()); 
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

51 
qed_spec_mp "not_Says_to_self"; 
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

52 
Addsimps [not_Says_to_self]; 
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

53 
AddSEs [not_Says_to_self RSN (2, rev_notE)]; 
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

54 

84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

55 

84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

56 
(** For reasoning about the encrypted portion of messages **) 
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

57 

1995  58 
(*Lets us treat YM4 using a similar argument as for the Fake case.*) 
2284
80ebd1a213fd
Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents:
2269
diff
changeset

59 
goal thy "!!evs. Says S A {Crypt (shrK A) Y, X} : set_of_list evs ==> \ 
2032  60 
\ X : analz (sees lost Spy evs)"; 
3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

61 
by (blast_tac (!claset addSDs [Says_imp_sees_Spy' RS analz.Inj]) 1); 
2032  62 
qed "YM4_analz_sees_Spy"; 
1985
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

63 

2110  64 
bind_thm ("YM4_parts_sees_Spy", 
65 
YM4_analz_sees_Spy RS (impOfSubs analz_subset_parts)); 

66 

2133  67 
(*Relates to both YM4 and Oops*) 
2284
80ebd1a213fd
Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents:
2269
diff
changeset

68 
goal thy "!!evs. Says S A {Crypt (shrK A) {B, K, NA, NB}, X} \ 
1995  69 
\ : set_of_list evs ==> \ 
2032  70 
\ K : parts (sees lost Spy evs)"; 
3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

71 
by (blast_tac (!claset addSEs partsEs 
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

72 
addSDs [Says_imp_sees_Spy' RS parts.Inj]) 1); 
2110  73 
qed "YM4_Key_parts_sees_Spy"; 
74 

3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

75 
(*For proving the easier theorems about X ~: parts (sees lost Spy evs). 
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

76 
We instantiate the variable to "lost" since leaving it as a Var would 
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

77 
interfere with simplification.*) 
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

78 
val parts_sees_tac = 
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

79 
forw_inst_tac [("lost","lost")] YM4_parts_sees_Spy 6 THEN 
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

80 
forw_inst_tac [("lost","lost")] YM4_Key_parts_sees_Spy 7 THEN 
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

81 
prove_simple_subgoals_tac 1; 
1985
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

82 

3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

83 
val parts_induct_tac = 
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

84 
etac yahalom.induct 1 THEN parts_sees_tac; 
1985
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

85 

84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

86 

2032  87 
(** Theorems of the form X ~: parts (sees lost Spy evs) imply that NOBODY 
2013  88 
sends messages containing X! **) 
1985
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

89 

2133  90 
(*Spy never sees another agent's shared key! (unless it's lost at start)*) 
1985
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

91 
goal thy 
2133  92 
"!!evs. evs : yahalom lost \ 
93 
\ ==> (Key (shrK A) : parts (sees lost Spy evs)) = (A : lost)"; 

3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

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

95 
by (Fake_parts_insert_tac 1); 
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

96 
by (Blast_tac 1); 
2133  97 
qed "Spy_see_shrK"; 
98 
Addsimps [Spy_see_shrK]; 

1985
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

99 

2133  100 
goal thy 
101 
"!!evs. evs : yahalom lost \ 

102 
\ ==> (Key (shrK A) : analz (sees lost Spy evs)) = (A : lost)"; 

103 
by (auto_tac(!claset addDs [impOfSubs analz_subset_parts], !simpset)); 

104 
qed "Spy_analz_shrK"; 

105 
Addsimps [Spy_analz_shrK]; 

1985
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

106 

2133  107 
goal thy "!!A. [ Key (shrK A) : parts (sees lost Spy evs); \ 
108 
\ evs : yahalom lost ] ==> A:lost"; 

3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

109 
by (blast_tac (!claset addDs [Spy_see_shrK]) 1); 
2133  110 
qed "Spy_see_shrK_D"; 
1985
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

111 

2133  112 
bind_thm ("Spy_analz_shrK_D", analz_subset_parts RS subsetD RS Spy_see_shrK_D); 
113 
AddSDs [Spy_see_shrK_D, Spy_analz_shrK_D]; 

1985
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

114 

84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

115 

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

116 
(*Nobody can have used nonexistent keys!*) 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2454
diff
changeset

117 
goal thy "!!evs. evs : yahalom lost ==> \ 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2454
diff
changeset

118 
\ Key K ~: used evs > K ~: keysFor (parts (sees lost Spy evs))"; 
3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

119 
by parts_induct_tac; 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2454
diff
changeset

120 
(*YM4: Key K is not fresh!*) 
3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

121 
by (blast_tac (!claset addSEs sees_Spy_partsEs) 3); 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2454
diff
changeset

122 
(*YM3*) 
3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

123 
by (Blast_tac 2); 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2454
diff
changeset

124 
(*Fake*) 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2454
diff
changeset

125 
by (best_tac 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2454
diff
changeset

126 
(!claset addIs [impOfSubs analz_subset_parts] 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2454
diff
changeset

127 
addDs [impOfSubs (analz_subset_parts RS keysFor_mono), 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2454
diff
changeset

128 
impOfSubs (parts_insert_subset_Un RS keysFor_mono)] 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2454
diff
changeset

129 
addss (!simpset)) 1); 
2160  130 
qed_spec_mp "new_keys_not_used"; 
1985
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

131 

84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

132 
bind_thm ("new_keys_not_analzd", 
2032  133 
[analz_subset_parts RS keysFor_mono, 
134 
new_keys_not_used] MRS contra_subsetD); 

1985
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

135 

84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

136 
Addsimps [new_keys_not_used, new_keys_not_analzd]; 
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

137 

84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

138 

2133  139 
(*Describes the form of K when the Server sends this message. Useful for 
140 
Oops as well as main secrecy property.*) 

2110  141 
goal thy 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2454
diff
changeset

142 
"!!evs. [ Says Server A {Crypt (shrK A) {Agent B, Key K, NA, NB}, X} \ 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2454
diff
changeset

143 
\ : set_of_list evs; \ 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2454
diff
changeset

144 
\ evs : yahalom lost ] \ 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2454
diff
changeset

145 
\ ==> K ~: range shrK"; 
2133  146 
by (etac rev_mp 1); 
147 
by (etac yahalom.induct 1); 

3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

148 
by (ALLGOALS Asm_simp_tac); 
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

149 
by (Blast_tac 1); 
2133  150 
qed "Says_Server_message_form"; 
2110  151 

152 

153 
(*For proofs involving analz. We again instantiate the variable to "lost".*) 

3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

154 
val analz_sees_tac = 
2133  155 
forw_inst_tac [("lost","lost")] YM4_analz_sees_Spy 6 THEN 
156 
forw_inst_tac [("lost","lost")] Says_Server_message_form 7 THEN 

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

157 
assume_tac 7 THEN REPEAT ((etac exE ORELSE' hyp_subst_tac) 7); 
1985
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

158 

84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

159 

84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

160 
(**** 
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

161 
The following is to prove theorems of the form 
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

162 

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

163 
Key K : analz (insert (Key KAB) (sees lost Spy evs)) ==> 
2451
ce85a2aafc7a
Extensive tidying and simplification, largely stemming from
paulson
parents:
2377
diff
changeset

164 
Key K : analz (sees lost Spy evs) 
1985
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

165 

84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

166 
A more general formula must be proved inductively. 
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

167 
****) 
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

168 

84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

169 
(** Session keys are not used to encrypt other session keys **) 
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

170 

84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

171 
goal thy 
2032  172 
"!!evs. evs : yahalom lost ==> \ 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2454
diff
changeset

173 
\ ALL K KK. KK <= Compl (range shrK) > \ 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2454
diff
changeset

174 
\ (Key K : analz (Key``KK Un (sees lost Spy evs))) = \ 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2454
diff
changeset

175 
\ (K : KK  Key K : analz (sees lost Spy evs))"; 
2032  176 
by (etac yahalom.induct 1); 
3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

177 
by analz_sees_tac; 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2454
diff
changeset

178 
by (REPEAT_FIRST (resolve_tac [allI, impI])); 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2454
diff
changeset

179 
by (REPEAT_FIRST (rtac analz_image_freshK_lemma )); 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2454
diff
changeset

180 
by (ALLGOALS (asm_simp_tac analz_image_freshK_ss)); 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2454
diff
changeset

181 
(*Base*) 
3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

182 
by (Blast_tac 1); 
2133  183 
(*YM4, Fake*) 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2454
diff
changeset

184 
by (REPEAT (spy_analz_tac 1)); 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2454
diff
changeset

185 
qed_spec_mp "analz_image_freshK"; 
1985
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

186 

84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

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

188 
"!!evs. [ evs : yahalom lost; KAB ~: range shrK ] ==> \ 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2454
diff
changeset

189 
\ Key K : analz (insert (Key KAB) (sees lost Spy evs)) = \ 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2454
diff
changeset

190 
\ (K = KAB  Key K : analz (sees lost Spy evs))"; 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2454
diff
changeset

191 
by (asm_simp_tac (analz_image_freshK_ss addsimps [analz_image_freshK]) 1); 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2454
diff
changeset

192 
qed "analz_insert_freshK"; 
1985
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

193 

84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

194 

2110  195 
(*** The Key K uniquely identifies the Server's message. **) 
196 

197 
goal thy 

198 
"!!evs. evs : yahalom lost ==> \ 

2133  199 
\ EX A' B' NA' NB' X'. ALL A B NA NB X. \ 
2110  200 
\ Says Server A \ 
2284
80ebd1a213fd
Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents:
2269
diff
changeset

201 
\ {Crypt (shrK A) {Agent B, Key K, NA, NB}, X} \ 
2133  202 
\ : set_of_list evs > A=A' & B=B' & NA=NA' & NB=NB' & X=X'"; 
2110  203 
by (etac yahalom.induct 1); 
204 
by (ALLGOALS (asm_simp_tac (!simpset addsimps [all_conj_distrib]))); 

205 
by (Step_tac 1); 

2133  206 
by (ex_strip_tac 2); 
3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

207 
by (Blast_tac 2); 
2110  208 
(*Remaining case: YM3*) 
209 
by (expand_case_tac "K = ?y" 1); 

210 
by (REPEAT (ares_tac [refl,exI,impI,conjI] 2)); 

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

211 
(*...we assume X is a recent message and handle this case by contradiction*) 
3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

212 
by (blast_tac (!claset addSEs sees_Spy_partsEs 
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

213 
delrules [conjI] (*no splitup to 4 subgoals*)) 1); 
2110  214 
val lemma = result(); 
215 

216 
goal thy 

217 
"!!evs. [ Says Server A \ 

2284
80ebd1a213fd
Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents:
2269
diff
changeset

218 
\ {Crypt (shrK A) {Agent B, Key K, NA, NB}, X} \ 
2110  219 
\ : set_of_list evs; \ 
220 
\ Says Server A' \ 

2284
80ebd1a213fd
Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents:
2269
diff
changeset

221 
\ {Crypt (shrK A') {Agent B', Key K, NA', NB'}, X'} \ 
2110  222 
\ : set_of_list evs; \ 
223 
\ evs : yahalom lost ] \ 

224 
\ ==> A=A' & B=B' & NA=NA' & NB=NB'"; 

2451
ce85a2aafc7a
Extensive tidying and simplification, largely stemming from
paulson
parents:
2377
diff
changeset

225 
by (prove_unique_tac lemma 1); 
2110  226 
qed "unique_session_keys"; 
227 

228 

229 
(*If the encrypted message appears then it originated with the Server*) 

230 
goal thy 

2284
80ebd1a213fd
Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents:
2269
diff
changeset

231 
"!!evs. [ Crypt (shrK A) {Agent B, Key K, NA, NB} \ 
2110  232 
\ : parts (sees lost Spy evs); \ 
233 
\ A ~: lost; evs : yahalom lost ] \ 

234 
\ ==> Says Server A \ 

2284
80ebd1a213fd
Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents:
2269
diff
changeset

235 
\ {Crypt (shrK A) {Agent B, Key K, NA, NB}, \ 
80ebd1a213fd
Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents:
2269
diff
changeset

236 
\ Crypt (shrK B) {Agent A, Key K}} \ 
2110  237 
\ : set_of_list evs"; 
238 
by (etac rev_mp 1); 

3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

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

240 
by (Fake_parts_insert_tac 1); 
2322  241 
qed "A_trusts_YM3"; 
2110  242 

243 

244 
(** Crucial secrecy property: Spy does not see the keys sent in msg YM3 **) 

2013  245 

246 
goal thy 

2133  247 
"!!evs. [ A ~: lost; B ~: lost; evs : yahalom lost ] \ 
2051  248 
\ ==> Says Server A \ 
2284
80ebd1a213fd
Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents:
2269
diff
changeset

249 
\ {Crypt (shrK A) {Agent B, Key K, NA, NB}, \ 
80ebd1a213fd
Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents:
2269
diff
changeset

250 
\ Crypt (shrK B) {Agent A, Key K}} \ 
2110  251 
\ : set_of_list evs > \ 
252 
\ Says A Spy {NA, NB, Key K} ~: set_of_list evs > \ 

2051  253 
\ Key K ~: analz (sees lost Spy evs)"; 
2032  254 
by (etac yahalom.induct 1); 
3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

255 
by analz_sees_tac; 
2013  256 
by (ALLGOALS 
257 
(asm_simp_tac 

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

258 
(!simpset addsimps [not_parts_not_analz, analz_insert_freshK] 
2013  259 
setloop split_tac [expand_if]))); 
260 
(*YM3*) 

3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

261 
by (blast_tac (!claset delrules [impCE] 
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

262 
addSEs sees_Spy_partsEs 
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

263 
addIs [impOfSubs analz_subset_parts]) 2); 
2133  264 
(*OR4, Fake*) 
2377  265 
by (REPEAT_FIRST spy_analz_tac); 
2451
ce85a2aafc7a
Extensive tidying and simplification, largely stemming from
paulson
parents:
2377
diff
changeset

266 
(*Oops*) 
3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

267 
by (blast_tac (!claset addDs [unique_session_keys]) 1); 
2110  268 
val lemma = result() RS mp RS mp RSN(2,rev_notE); 
2013  269 

270 

271 
(*Final version: Server's message in the most abstract form*) 

1985
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

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

273 
"!!evs. [ Says Server A \ 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2454
diff
changeset

274 
\ {Crypt (shrK A) {Agent B, Key K, NA, NB}, \ 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2454
diff
changeset

275 
\ Crypt (shrK B) {Agent A, Key K}} \ 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2454
diff
changeset

276 
\ : set_of_list evs; \ 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2454
diff
changeset

277 
\ Says A Spy {NA, NB, Key K} ~: set_of_list evs; \ 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2454
diff
changeset

278 
\ A ~: lost; B ~: lost; evs : yahalom lost ] \ 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2454
diff
changeset

279 
\ ==> Key K ~: analz (sees lost Spy evs)"; 
2013  280 
by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1); 
3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

281 
by (blast_tac (!claset addSEs [lemma]) 1); 
2032  282 
qed "Spy_not_see_encrypted_key"; 
2001  283 

284 

2045
ae1030e66745
Removed some dead wood. Transferred lemmas used to prove analz_image_newK
paulson
parents:
2032
diff
changeset

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

286 
"!!evs. [ C ~: {A,B,Server}; \ 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2454
diff
changeset

287 
\ Says Server A \ 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2454
diff
changeset

288 
\ {Crypt (shrK A) {Agent B, Key K, NA, NB}, \ 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2454
diff
changeset

289 
\ Crypt (shrK B) {Agent A, Key K}} \ 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2454
diff
changeset

290 
\ : set_of_list evs; \ 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2454
diff
changeset

291 
\ Says A Spy {NA, NB, Key K} ~: set_of_list evs; \ 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2454
diff
changeset

292 
\ A ~: lost; B ~: lost; evs : yahalom lost ] \ 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2454
diff
changeset

293 
\ ==> Key K ~: analz (sees lost C evs)"; 
2045
ae1030e66745
Removed some dead wood. Transferred lemmas used to prove analz_image_newK
paulson
parents:
2032
diff
changeset

294 
by (rtac (subset_insertI RS sees_mono RS analz_mono RS contra_subsetD) 1); 
ae1030e66745
Removed some dead wood. Transferred lemmas used to prove analz_image_newK
paulson
parents:
2032
diff
changeset

295 
by (rtac (sees_lost_agent_subset_sees_Spy RS analz_mono RS contra_subsetD) 1); 
ae1030e66745
Removed some dead wood. Transferred lemmas used to prove analz_image_newK
paulson
parents:
2032
diff
changeset

296 
by (FIRSTGOAL (rtac Spy_not_see_encrypted_key)); 
3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

297 
by (REPEAT_FIRST (blast_tac (!claset addIs [yahalom_mono RS subsetD]))); 
2045
ae1030e66745
Removed some dead wood. Transferred lemmas used to prove analz_image_newK
paulson
parents:
2032
diff
changeset

298 
qed "Agent_not_see_encrypted_key"; 
ae1030e66745
Removed some dead wood. Transferred lemmas used to prove analz_image_newK
paulson
parents:
2032
diff
changeset

299 

ae1030e66745
Removed some dead wood. Transferred lemmas used to prove analz_image_newK
paulson
parents:
2032
diff
changeset

300 

2110  301 
(*** Security Guarantee for B upon receiving YM4 ***) 
2013  302 

2110  303 
(*B knows, by the first part of A's message, that the Server distributed 
304 
the key for A and B. But this part says nothing about nonces.*) 

2001  305 
goal thy 
2284
80ebd1a213fd
Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents:
2269
diff
changeset

306 
"!!evs. [ Crypt (shrK B) {Agent A, Key K} : parts (sees lost Spy evs); \ 
2051  307 
\ B ~: lost; evs : yahalom lost ] \ 
2001  308 
\ ==> EX NA NB. Says Server A \ 
2451
ce85a2aafc7a
Extensive tidying and simplification, largely stemming from
paulson
parents:
2377
diff
changeset

309 
\ {Crypt (shrK A) {Agent B, Key K, \ 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2454
diff
changeset

310 
\ Nonce NA, Nonce NB}, \ 
2284
80ebd1a213fd
Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents:
2269
diff
changeset

311 
\ Crypt (shrK B) {Agent A, Key K}} \ 
2013  312 
\ : set_of_list evs"; 
2032  313 
by (etac rev_mp 1); 
3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

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

315 
by (Fake_parts_insert_tac 1); 
2110  316 
(*YM3*) 
3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

317 
by (Blast_tac 1); 
2110  318 
qed "B_trusts_YM4_shrK"; 
319 

2133  320 

321 
(** The Nonce NB uniquely identifies B's message. **) 

322 

323 
goal thy 

2451
ce85a2aafc7a
Extensive tidying and simplification, largely stemming from
paulson
parents:
2377
diff
changeset

324 
"!!evs. evs : yahalom lost ==> \ 
ce85a2aafc7a
Extensive tidying and simplification, largely stemming from
paulson
parents:
2377
diff
changeset

325 
\ EX NA' A' B'. ALL NA A B. \ 
2284
80ebd1a213fd
Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents:
2269
diff
changeset

326 
\ Crypt (shrK B) {Agent A, Nonce NA, NB} : parts(sees lost Spy evs) \ 
2133  327 
\ > B ~: lost > NA = NA' & A = A' & B = B'"; 
3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

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

329 
(*Fake*) 
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

330 
by (REPEAT (etac (exI RSN (2,exE)) 1) (*stripping EXs makes proof faster*) 
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

331 
THEN Fake_parts_insert_tac 1); 
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

332 
by (asm_simp_tac (!simpset addsimps [all_conj_distrib]) 1); 
2133  333 
(*YM2: creation of new Nonce. Move assertion into global context*) 
334 
by (expand_case_tac "NB = ?y" 1); 

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

335 
by (REPEAT (resolve_tac [exI, conjI, impI, refl] 1)); 
3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

336 
by (blast_tac (!claset addSEs sees_Spy_partsEs) 1); 
2133  337 
val lemma = result(); 
338 

2110  339 
goal thy 
2284
80ebd1a213fd
Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents:
2269
diff
changeset

340 
"!!evs.[ Crypt (shrK B) {Agent A, Nonce NA, NB} \ 
2133  341 
\ : parts (sees lost Spy evs); \ 
2284
80ebd1a213fd
Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents:
2269
diff
changeset

342 
\ Crypt (shrK B') {Agent A', Nonce NA', NB} \ 
2133  343 
\ : parts (sees lost Spy evs); \ 
344 
\ evs : yahalom lost; B ~: lost; B' ~: lost ] \ 

345 
\ ==> NA' = NA & A' = A & B' = B"; 

2451
ce85a2aafc7a
Extensive tidying and simplification, largely stemming from
paulson
parents:
2377
diff
changeset

346 
by (prove_unique_tac lemma 1); 
2133  347 
qed "unique_NB"; 
348 

349 
fun lost_tac s = 

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

351 
SELECT_GOAL 

3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

352 
(REPEAT_DETERM (dtac (Says_imp_sees_Spy' RS analz.Inj) 1) THEN 
2133  353 
REPEAT_DETERM (etac MPair_analz 1) THEN 
354 
THEN_BEST_FIRST 

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

2170  356 
(has_fewer_prems 1, size_of_thm) 
357 
(Step_tac 1)); 

2133  358 

359 

360 
(*Variant useful for proving secrecy of NB*) 

361 
goal thy 

2284
80ebd1a213fd
Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents:
2269
diff
changeset

362 
"!!evs.[ Says C D {X, Crypt (shrK B) {Agent A, Nonce NA, NB}} \ 
2133  363 
\ : set_of_list evs; B ~: lost; \ 
2284
80ebd1a213fd
Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents:
2269
diff
changeset

364 
\ Says C' D' {X', Crypt (shrK B') {Agent A', Nonce NA', NB}} \ 
2133  365 
\ : set_of_list evs; \ 
366 
\ NB ~: analz (sees lost Spy evs); \ 

367 
\ evs : yahalom lost ] \ 

368 
\ ==> NA' = NA & A' = A & B' = B"; 

369 
by (lost_tac "B'" 1); 

3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

370 
by (blast_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj] 
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

371 
addSEs [MPair_parts] 
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

372 
addDs [unique_NB]) 1); 
2133  373 
qed "Says_unique_NB"; 
374 

3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

375 
(*Induction for theorems of the form X ~: analz (sees lost Spy evs) > ... 
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

376 
It simplifies the proof by discarding needless information about 
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

377 
analz (insert X (sees lost Spy evs)) 
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

378 
*) 
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

379 
val analz_mono_parts_induct_tac = 
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

380 
etac yahalom.induct 1 
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

381 
THEN 
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

382 
REPEAT_FIRST 
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

383 
(rtac impI THEN' 
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

384 
dtac (sees_subset_sees_Says RS analz_mono RS contra_subsetD) THEN' 
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

385 
mp_tac) 
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

386 
THEN parts_sees_tac; 
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

387 

2133  388 
goal thy 
389 
"!!evs. [ B ~: lost; evs : yahalom lost ] \ 

3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

390 
\ ==> Nonce NB ~: analz (sees lost Spy evs) > \ 
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

391 
\ Crypt (shrK B) {Agent A, Nonce NA, Nonce NB}: parts(sees lost Spy evs)\ 
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

392 
\ > Crypt (shrK B') {Agent A', Nonce NB, NB'} ~: parts(sees lost Spy evs)"; 
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

393 
by analz_mono_parts_induct_tac; 
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

394 
by (Fake_parts_insert_tac 1); 
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

395 
by (blast_tac (!claset addDs [Says_imp_sees_Spy' RS analz.Inj] 
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

396 
addSIs [parts_insertI] 
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

397 
addSEs partsEs) 1); 
2133  398 
val no_nonce_YM1_YM2 = standard (result() RS mp RSN (2, rev_mp) RS notE); 
399 

400 

401 

402 
(**** Towards proving secrecy of Nonce NB ****) 

403 

404 
(*B knows, by the second part of A's message, that the Server distributed 

405 
the key quoting nonce NB. This part says nothing about agent names. 

406 
Secrecy of NB is crucial.*) 

407 
goal thy 

408 
"!!evs. evs : yahalom lost \ 

409 
\ ==> Nonce NB ~: analz (sees lost Spy evs) > \ 

2284
80ebd1a213fd
Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents:
2269
diff
changeset

410 
\ Crypt K (Nonce NB) : parts (sees lost Spy evs) > \ 
2133  411 
\ (EX A B NA. Says Server A \ 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2454
diff
changeset

412 
\ {Crypt (shrK A) {Agent B, Key K, \ 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2454
diff
changeset

413 
\ Nonce NA, Nonce NB}, \ 
2284
80ebd1a213fd
Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents:
2269
diff
changeset

414 
\ Crypt (shrK B) {Agent A, Key K}} \ 
2133  415 
\ : set_of_list evs)"; 
3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

416 
by analz_mono_parts_induct_tac; 
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

417 
(*YM4 & Fake*) 
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

418 
by (Blast_tac 2); 
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

419 
by (Fake_parts_insert_tac 1); 
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

420 
(*YM3*) 
2133  421 
by (Step_tac 1); 
422 
by (lost_tac "A" 1); 

3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

423 
by (blast_tac (!claset addDs [Says_imp_sees_Spy' RS parts.Inj RS parts.Fst RS 
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

424 
A_trusts_YM3]) 1); 
2133  425 
val B_trusts_YM4_newK = result() RS mp RSN (2, rev_mp); 
426 

427 

428 
(*This is the original version of the result above. But it is of little 

429 
value because it assumes secrecy of K, which we cannot be assured of 

430 
until we know that K is fresh  which we do not know at the point this 

431 
result is applied.*) 

432 
goal thy 

433 
"!!evs. evs : yahalom lost \ 

434 
\ ==> Key K ~: analz (sees lost Spy evs) > \ 

2284
80ebd1a213fd
Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents:
2269
diff
changeset

435 
\ Crypt K (Nonce NB) : parts (sees lost Spy evs) > \ 
2110  436 
\ (EX A B NA. Says Server A \ 
3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

437 
\ {Crypt (shrK A) {Agent B, Key K, \ 
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

438 
\ Nonce NA, Nonce NB}, \ 
2284
80ebd1a213fd
Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents:
2269
diff
changeset

439 
\ Crypt (shrK B) {Agent A, Key K}} \ 
2110  440 
\ : set_of_list evs)"; 
3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

441 
by analz_mono_parts_induct_tac; 
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

442 
(*YM4 & Fake*) 
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

443 
by (Blast_tac 2); 
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

444 
by (Fake_parts_insert_tac 1); 
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

445 
(*YM3*) 
2110  446 
by (Step_tac 1); 
2133  447 
by (lost_tac "A" 1); 
3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

448 
by (blast_tac (!claset addDs [Says_imp_sees_Spy' RS parts.Inj RS parts.Fst RS 
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

449 
A_trusts_YM3]) 1); 
2133  450 
result() RS mp RSN (2, rev_mp); 
451 

452 

453 
(*YM3 can only be triggered by YM2*) 

454 
goal thy 

455 
"!!evs. [ Says Server A \ 

2284
80ebd1a213fd
Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents:
2269
diff
changeset

456 
\ {Crypt (shrK A) {Agent B, k, na, nb}, X} : set_of_list evs; \ 
2133  457 
\ evs : yahalom lost ] \ 
458 
\ ==> EX B'. Says B' Server \ 

2284
80ebd1a213fd
Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents:
2269
diff
changeset

459 
\ { Agent B, Crypt (shrK B) {Agent A, na, nb} } \ 
2133  460 
\ : set_of_list evs"; 
461 
by (etac rev_mp 1); 

462 
by (etac yahalom.induct 1); 

463 
by (ALLGOALS Asm_simp_tac); 

3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

464 
by (ALLGOALS Blast_tac); 
2133  465 
qed "Says_Server_imp_YM2"; 
466 

467 

468 
(** Dedicated tactics for the nonce secrecy proofs **) 

469 

470 
val no_nonce_tac = SELECT_GOAL 

471 
(REPEAT (resolve_tac [impI, notI] 1) THEN 

472 
REPEAT (hyp_subst_tac 1) THEN 

3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

473 
etac (Says_imp_sees_Spy' RS parts.Inj RS parts.Snd RS no_nonce_YM1_YM2) 1 
2133  474 
THEN 
3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

475 
etac (Says_imp_sees_Spy' RS parts.Inj RS parts.Snd) 4 
2133  476 
THEN 
477 
REPEAT_FIRST assume_tac); 

478 

479 
val not_analz_insert = subset_insertI RS analz_mono RS contra_subsetD; 

480 

481 

482 
(*The only nonces that can be found with the help of session keys are 

483 
those distributed as nonce NB by the Server. The form of the theorem 

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

484 
recalls analz_image_freshK, but it is much more complicated.*) 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2454
diff
changeset

485 

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

486 
(*As with analz_image_freshK, we take some pains to express the property 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2454
diff
changeset

487 
as a logical equivalence so that the simplifier can apply it.*) 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2454
diff
changeset

488 
goal thy 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2454
diff
changeset

489 
"!!evs. P > (X : analz (G Un H)) > (X : analz H) ==> \ 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2454
diff
changeset

490 
\ P > (X : analz (G Un H)) = (X : analz H)"; 
3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

491 
by (blast_tac (!claset addIs [impOfSubs analz_mono]) 1); 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2454
diff
changeset

492 
qed "Nonce_secrecy_lemma"; 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2454
diff
changeset

493 

2133  494 
goal thy 
3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

495 
"!!evs. evs : yahalom lost ==> \ 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2454
diff
changeset

496 
\ (ALL KK. KK <= Compl (range shrK) > \ 
3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

497 
\ (ALL K: KK. ALL A B na X. \ 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2454
diff
changeset

498 
\ Says Server A \ 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2454
diff
changeset

499 
\ {Crypt (shrK A) {Agent B, Key K, na, Nonce NB}, X} \ 
3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

500 
\ ~: set_of_list evs) > \ 
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

501 
\ (Nonce NB : analz (Key``KK Un (sees lost Spy evs))) = \ 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2454
diff
changeset

502 
\ (Nonce NB : analz (sees lost Spy evs)))"; 
2133  503 
by (etac yahalom.induct 1); 
3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

504 
by analz_sees_tac; 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2454
diff
changeset

505 
by (REPEAT_FIRST (resolve_tac [impI RS allI])); 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2454
diff
changeset

506 
by (REPEAT_FIRST (rtac Nonce_secrecy_lemma )); 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2454
diff
changeset

507 
by (rtac ccontr 7); 
3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

508 
by (subgoal_tac "ALL A B na X. \ 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2454
diff
changeset

509 
\ Says Server A \ 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2454
diff
changeset

510 
\ {Crypt (shrK A) {Agent B, Key K, na, Nonce NB}, X} \ 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2454
diff
changeset

511 
\ ~: set_of_list evsa" 7); 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2454
diff
changeset

512 
by (eres_inst_tac [("P","?PP>?QQ")] notE 7); 
3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

513 
by (subgoal_tac "ALL A B na X. \ 
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

514 
\ Says Server A \ 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2454
diff
changeset

515 
\ {Crypt (shrK A) {Agent B, Key KAB, na, Nonce NB}, X} \ 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2454
diff
changeset

516 
\ ~: set_of_list evsa" 5); 
2451
ce85a2aafc7a
Extensive tidying and simplification, largely stemming from
paulson
parents:
2377
diff
changeset

517 
by (ALLGOALS (*22 seconds*) 
2133  518 
(asm_simp_tac 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2454
diff
changeset

519 
(analz_image_freshK_ss addsimps 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2454
diff
changeset

520 
([all_conj_distrib, 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2454
diff
changeset

521 
not_parts_not_analz, analz_image_freshK] 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2454
diff
changeset

522 
@ pushes @ ball_simps)))); 
2133  523 
(*Base*) 
3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

524 
by (Blast_tac 1); 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2454
diff
changeset

525 
(*Fake*) (** LEVEL 10 **) 
2133  526 
by (spy_analz_tac 1); 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2454
diff
changeset

527 
(*YM3*) 
3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

528 
by (blast_tac (!claset addSEs sees_Spy_partsEs) 1); 
2133  529 
(*Oops*) 
3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

530 
by (Asm_full_simp_tac 2); 
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

531 
by (blast_tac (!claset addDs [unique_session_keys]) 2); 
2133  532 
(*YM4*) 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2454
diff
changeset

533 
(** LEVEL 13 **) 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2454
diff
changeset

534 
by (REPEAT (resolve_tac [impI, allI] 1)); 
2377  535 
by (dtac (impOfSubs Fake_analz_insert) 1 THEN etac synth.Inj 1); 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2454
diff
changeset

536 
by (stac insert_commute 1); 
2133  537 
by (eres_inst_tac [("P","Nonce NB : ?HH")] rev_mp 1); 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2454
diff
changeset

538 
by (asm_simp_tac (analz_image_freshK_ss 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2454
diff
changeset

539 
addsimps [analz_insertI, analz_image_freshK]) 1); 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2454
diff
changeset

540 
by (step_tac (!claset addSDs [not_analz_insert]) 1); 
2133  541 
by (lost_tac "A" 1); 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2454
diff
changeset

542 
(** LEVEL 20 **) 
3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

543 
by (dtac (Says_imp_sees_Spy' RS parts.Inj RS parts.Fst RS A_trusts_YM3) 1 
2133  544 
THEN REPEAT (assume_tac 1)); 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2454
diff
changeset

545 
by (thin_tac "All ?PP" 1); 
3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

546 
by (Blast_tac 1); 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2454
diff
changeset

547 
qed_spec_mp "Nonce_secrecy"; 
2133  548 

549 

550 
(*Version required below: if NB can be decrypted using a session key then it 

551 
was distributed with that key. The more general form above is required 

552 
for the induction to carry through.*) 

553 
goal thy 

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

554 
"!!evs. [ Says Server A \ 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2454
diff
changeset

555 
\ {Crypt (shrK A) {Agent B, Key KAB, na, Nonce NB'}, X} \ 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2454
diff
changeset

556 
\ : set_of_list evs; \ 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2454
diff
changeset

557 
\ Nonce NB : analz (insert (Key KAB) (sees lost Spy evs)); \ 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2454
diff
changeset

558 
\ Nonce NB ~: analz (sees lost Spy evs); \ 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2454
diff
changeset

559 
\ KAB ~: range shrK; evs : yahalom lost ] \ 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2454
diff
changeset

560 
\ ==> NB = NB'"; 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2454
diff
changeset

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

562 
by (subgoal_tac "ALL A B na X. \ 
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

563 
\ Says Server A \ 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2454
diff
changeset

564 
\ {Crypt (shrK A) {Agent B, Key KAB, na, Nonce NB}, X} \ 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2454
diff
changeset

565 
\ ~: set_of_list evs" 1); 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2454
diff
changeset

566 
by (eres_inst_tac [("P","Nonce NB : ?HH")] rev_mp 1); 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2454
diff
changeset

567 
by (asm_simp_tac (analz_image_freshK_ss 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2454
diff
changeset

568 
addsimps ([Nonce_secrecy] @ ball_simps)) 1); 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2454
diff
changeset

569 
by (auto_tac (!claset addDs [unique_session_keys], (!simpset))); 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2454
diff
changeset

570 
qed "single_Nonce_secrecy"; 
2133  571 

572 

3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

573 
val Says_unique_NB' = read_instantiate [("lost","lost")] Says_unique_NB; 
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

574 

2133  575 
goal thy 
576 
"!!evs. [ A ~: lost; B ~: lost; Spy: lost; evs : yahalom lost ] \ 

577 
\ ==> Says B Server \ 

2284
80ebd1a213fd
Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents:
2269
diff
changeset

578 
\ {Agent B, Crypt (shrK B) {Agent A, Nonce NA, Nonce NB}} \ 
2133  579 
\ : set_of_list evs > \ 
580 
\ (ALL k. Says A Spy {Nonce NA, Nonce NB, k} ~: set_of_list evs) > \ 

581 
\ Nonce NB ~: analz (sees lost Spy evs)"; 

582 
by (etac yahalom.induct 1); 

3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

583 
by analz_sees_tac; 
2133  584 
by (ALLGOALS 
585 
(asm_simp_tac 

2377  586 
(!simpset addsimps ([not_parts_not_analz, 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2454
diff
changeset

587 
analz_insert_freshK] @ pushes) 
2133  588 
setloop split_tac [expand_if]))); 
3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

589 
by (blast_tac (!claset addSIs [parts_insertI] 
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

590 
addSEs sees_Spy_partsEs) 2); 
2377  591 
(*Proof of YM2*) (** LEVEL 4 **) 
3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

592 
by (blast_tac (!claset addSEs partsEs 
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

593 
addDs [Says_imp_sees_Spy' RS analz.Inj, 
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

594 
impOfSubs analz_subset_parts]) 2); 
2133  595 
(*Prove YM3 by showing that no NB can also be an NA*) 
596 
by (REPEAT (Safe_step_tac 2 ORELSE no_nonce_tac 2)); 

3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

597 
by (blast_tac (!claset addDs [Says_unique_NB']) 2 THEN flexflex_tac); 
2377  598 
(*Fake*) 
599 
by (spy_analz_tac 1); 

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

600 
(*YM4*) (** LEVEL 8 **) 
2133  601 
by (res_inst_tac [("x1","X")] (insert_commute RS ssubst) 1); 
602 
by (simp_tac (!simpset setloop split_tac [expand_if]) 1); 

3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

603 
(* SLOW: 13s*) 
2377  604 
by (SELECT_GOAL (REPEAT_FIRST (spy_analz_tac ORELSE' Safe_step_tac)) 1); 
2133  605 
by (lost_tac "Aa" 1); 
3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

606 
by (dtac (Says_imp_sees_Spy' RS parts.Inj RS parts.Fst RS A_trusts_YM3) 1); 
2133  607 
by (forward_tac [Says_Server_message_form] 3); 
608 
by (forward_tac [Says_Server_imp_YM2] 4); 

3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

609 
by (REPEAT_FIRST (eresolve_tac [asm_rl, bexE, exE, disjE])); 
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

610 
(** LEVEL 16 **) 
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

611 
(* use unique_NB to identify message components *) 
2133  612 
by (lost_tac "Ba" 1); 
3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

613 
by (subgoal_tac "Aa=A & Ba=B & NAa=NA" 1); 
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

614 
by (blast_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj] 
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

615 
addSEs [MPair_parts] addDs [unique_NB]) 2); 
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

616 
by (blast_tac (!claset addDs [Spy_not_see_encrypted_key, 
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

617 
impOfSubs Fake_analz_insert] 
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

618 
addIs [impOfSubs analz_mono]) 1); 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2454
diff
changeset

619 
(** LEVEL 20 **) 
3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

620 
(*Oops case*) 
2133  621 
by (full_simp_tac (!simpset addsimps [all_conj_distrib]) 1); 
622 
by (step_tac (!claset delrules [disjE, conjI]) 1); 

623 
by (forward_tac [Says_Server_imp_YM2] 1 THEN assume_tac 1 THEN etac exE 1); 

624 
by (expand_case_tac "NB = NBa" 1); 

3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

625 
by (blast_tac (!claset addDs [Says_unique_NB']) 1); 
2170  626 
by (rtac conjI 1); 
2133  627 
by (no_nonce_tac 1); 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2454
diff
changeset

628 
(** LEVEL 30 **) 
3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

629 
by (blast_tac (!claset addSDs [single_Nonce_secrecy]) 1); 
2133  630 
val Spy_not_see_NB = result() RSN(2,rev_mp) RSN(2,rev_mp) > standard; 
631 

2001  632 

2110  633 
(*What can B deduce from receipt of YM4? Note how the two components of 
634 
the message contribute to a single conclusion about the Server's message. 

635 
It's annoying that the "Says A Spy" assumption must quantify over 

2133  636 
ALL POSSIBLE keys instead of our particular K (though at least the 
637 
nonces are forced to agree with NA and NB). *) 

2001  638 
goal thy 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2454
diff
changeset

639 
"!!evs. [ Says B Server \ 
2284
80ebd1a213fd
Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents:
2269
diff
changeset

640 
\ {Agent B, Crypt (shrK B) {Agent A, Nonce NA, Nonce NB}} \ 
2133  641 
\ : set_of_list evs; \ 
2284
80ebd1a213fd
Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents:
2269
diff
changeset

642 
\ Says A' B {Crypt (shrK B) {Agent A, Key K}, \ 
80ebd1a213fd
Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents:
2269
diff
changeset

643 
\ Crypt K (Nonce NB)} : set_of_list evs; \ 
2133  644 
\ ALL k. Says A Spy {Nonce NA, Nonce NB, k} ~: set_of_list evs; \ 
645 
\ A ~: lost; B ~: lost; Spy: lost; evs : yahalom lost ] \ 

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

646 
\ ==> Says Server A \ 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2454
diff
changeset

647 
\ {Crypt (shrK A) {Agent B, Key K, \ 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2454
diff
changeset

648 
\ Nonce NA, Nonce NB}, \ 
2284
80ebd1a213fd
Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents:
2269
diff
changeset

649 
\ Crypt (shrK B) {Agent A, Key K}} \ 
2001  650 
\ : set_of_list evs"; 
2133  651 
by (forward_tac [Spy_not_see_NB] 1 THEN REPEAT (assume_tac 1)); 
3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

652 
by (etac (Says_imp_sees_Spy' RS parts.Inj RS MPair_parts) 1 THEN 
2133  653 
dtac B_trusts_YM4_shrK 1); 
2170  654 
by (dtac B_trusts_YM4_newK 3); 
2110  655 
by (REPEAT_FIRST (eresolve_tac [asm_rl, exE])); 
2133  656 
by (forward_tac [Says_Server_imp_YM2] 1 THEN assume_tac 1); 
2170  657 
by (dtac unique_session_keys 1 THEN REPEAT (assume_tac 1)); 
3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

658 
by (blast_tac (!claset addDs [Says_unique_NB']) 1); 
2322  659 
qed "B_trusts_YM4"; 