author  paulson 
Fri, 11 Jul 1997 13:26:15 +0200  
changeset 3512  9dcb4daa15e8 
parent 3501  4ab477ffb4c6 
child 3516  470626799511 
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 

3432  6 
Inductive relation "yahalom" for the Yahalom protocol. 
1985
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 ] \ 

3466
30791e5a69c4
Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents:
3465
diff
changeset

26 
\ ==> EX X NB K. EX evs: yahalom lost. \ 
3465  27 
\ Says A B {X, Crypt K (Nonce NB)} : set 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 
3466
30791e5a69c4
Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents:
3465
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*) 
3465  48 
goal thy "!!evs. evs: yahalom lost ==> ALL A X. Says A A X ~: set 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.*) 
3465  59 
goal thy "!!evs. Says S A {Crypt (shrK A) Y, X} : set 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*) 
3466
30791e5a69c4
Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents:
3465
diff
changeset

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

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

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

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

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

75 
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

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

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

78 
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

79 
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

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

81 

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

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

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

84 

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

85 

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

88 

2133  89 
(*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

90 
goal thy 
2133  91 
"!!evs. evs : yahalom lost \ 
92 
\ ==> (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

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

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

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

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

98 

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

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

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

103 
qed "Spy_analz_shrK"; 

104 
Addsimps [Spy_analz_shrK]; 

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

105 

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

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

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

110 

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

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

113 

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

114 

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

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

117 
\ 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

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

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

120 
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

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

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

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

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

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

126 
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

127 
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

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

130 

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

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

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

134 

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

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

136 

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

137 

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

2110  140 
goal thy 
3501
4ab477ffb4c6
Changed some variables of type msg to lower case (e.g. from NB to nb
paulson
parents:
3466
diff
changeset

141 
"!!evs. [ Says Server A {Crypt (shrK A) {Agent B, Key K, na, nb}, X} \ 
3466
30791e5a69c4
Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents:
3465
diff
changeset

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

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

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

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

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

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

151 

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

153 
val analz_sees_tac = 
2133  154 
forw_inst_tac [("lost","lost")] YM4_analz_sees_Spy 6 THEN 
155 
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

156 
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

157 

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 
The following is to prove theorems of the form 
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

161 

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

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

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

164 

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

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

166 
****) 
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 
(** Session keys are not used to encrypt other session keys **) 
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

169 

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

170 
goal thy 
3466
30791e5a69c4
Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents:
3465
diff
changeset

171 
"!!evs. evs : yahalom lost ==> \ 
30791e5a69c4
Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents:
3465
diff
changeset

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

173 
\ (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

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

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

177 
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

178 
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

179 
by (ALLGOALS (asm_simp_tac analz_image_freshK_ss)); 
3450
cd73bc206d87
Proof tidying and variable renaming (NA>na, NB>nb when of type msg)
paulson
parents:
3444
diff
changeset

180 
(*Fake*) 
cd73bc206d87
Proof tidying and variable renaming (NA>na, NB>nb when of type msg)
paulson
parents:
3444
diff
changeset

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

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

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

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

185 

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

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

187 
"!!evs. [ evs : yahalom lost; KAB ~: range shrK ] ==> \ 
3466
30791e5a69c4
Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents:
3465
diff
changeset

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

189 
\ (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

190 
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

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

192 

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

193 

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

196 
goal thy 

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

3466
30791e5a69c4
Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents:
3465
diff
changeset

198 
\ EX A' B' na' nb' X'. ALL A B na nb X. \ 
2110  199 
\ Says Server A \ 
3450
cd73bc206d87
Proof tidying and variable renaming (NA>na, NB>nb when of type msg)
paulson
parents:
3444
diff
changeset

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

204 
by (Step_tac 1); 

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

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

209 
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

210 
(*...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

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

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

215 
goal thy 

216 
"!!evs. [ Says Server A \ 

3450
cd73bc206d87
Proof tidying and variable renaming (NA>na, NB>nb when of type msg)
paulson
parents:
3444
diff
changeset

217 
\ {Crypt (shrK A) {Agent B, Key K, na, nb}, X} \ 
3466
30791e5a69c4
Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents:
3465
diff
changeset

218 
\ : set evs; \ 
2110  219 
\ Says Server A' \ 
3450
cd73bc206d87
Proof tidying and variable renaming (NA>na, NB>nb when of type msg)
paulson
parents:
3444
diff
changeset

220 
\ {Crypt (shrK A') {Agent B', Key K, na', nb'}, X'} \ 
3466
30791e5a69c4
Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents:
3465
diff
changeset

221 
\ : set evs; \ 
2110  222 
\ evs : yahalom lost ] \ 
3450
cd73bc206d87
Proof tidying and variable renaming (NA>na, NB>nb when of type msg)
paulson
parents:
3444
diff
changeset

223 
\ ==> A=A' & B=B' & na=na' & nb=nb'"; 
2451
ce85a2aafc7a
Extensive tidying and simplification, largely stemming from
paulson
parents:
2377
diff
changeset

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

227 

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

2013  229 

230 
goal thy 

2133  231 
"!!evs. [ A ~: lost; B ~: lost; evs : yahalom lost ] \ 
2051  232 
\ ==> Says Server A \ 
3450
cd73bc206d87
Proof tidying and variable renaming (NA>na, NB>nb when of type msg)
paulson
parents:
3444
diff
changeset

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

234 
\ Crypt (shrK B) {Agent A, Key K}} \ 
3466
30791e5a69c4
Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents:
3465
diff
changeset

235 
\ : set evs > \ 
30791e5a69c4
Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents:
3465
diff
changeset

236 
\ Says A Spy {na, nb, Key K} ~: set evs > \ 
2051  237 
\ Key K ~: analz (sees lost Spy evs)"; 
2032  238 
by (etac yahalom.induct 1); 
3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

239 
by analz_sees_tac; 
2013  240 
by (ALLGOALS 
241 
(asm_simp_tac 

3450
cd73bc206d87
Proof tidying and variable renaming (NA>na, NB>nb when of type msg)
paulson
parents:
3444
diff
changeset

242 
(!simpset addsimps [analz_insert_eq, not_parts_not_analz, 
cd73bc206d87
Proof tidying and variable renaming (NA>na, NB>nb when of type msg)
paulson
parents:
3444
diff
changeset

243 
analz_insert_freshK] 
2013  244 
setloop split_tac [expand_if]))); 
3450
cd73bc206d87
Proof tidying and variable renaming (NA>na, NB>nb when of type msg)
paulson
parents:
3444
diff
changeset

245 
(*Oops*) 
cd73bc206d87
Proof tidying and variable renaming (NA>na, NB>nb when of type msg)
paulson
parents:
3444
diff
changeset

246 
by (blast_tac (!claset addDs [unique_session_keys]) 3); 
2013  247 
(*YM3*) 
3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

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

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

250 
addIs [impOfSubs analz_subset_parts]) 2); 
3450
cd73bc206d87
Proof tidying and variable renaming (NA>na, NB>nb when of type msg)
paulson
parents:
3444
diff
changeset

251 
(*Fake*) 
cd73bc206d87
Proof tidying and variable renaming (NA>na, NB>nb when of type msg)
paulson
parents:
3444
diff
changeset

252 
by (spy_analz_tac 1); 
2110  253 
val lemma = result() RS mp RS mp RSN(2,rev_notE); 
2013  254 

255 

3432  256 
(*Final version*) 
1985
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

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

258 
"!!evs. [ Says Server A \ 
3450
cd73bc206d87
Proof tidying and variable renaming (NA>na, NB>nb when of type msg)
paulson
parents:
3444
diff
changeset

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

260 
\ Crypt (shrK B) {Agent A, Key K}} \ 
3466
30791e5a69c4
Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents:
3465
diff
changeset

261 
\ : set evs; \ 
30791e5a69c4
Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents:
3465
diff
changeset

262 
\ Says A Spy {na, nb, Key K} ~: set evs; \ 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2454
diff
changeset

263 
\ 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

264 
\ ==> Key K ~: analz (sees lost Spy evs)"; 
2013  265 
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

266 
by (blast_tac (!claset addSEs [lemma]) 1); 
2032  267 
qed "Spy_not_see_encrypted_key"; 
2001  268 

269 

3432  270 
(*And other agents don't see the key either.*) 
2045
ae1030e66745
Removed some dead wood. Transferred lemmas used to prove analz_image_newK
paulson
parents:
2032
diff
changeset

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

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

273 
\ Says Server A \ 
3450
cd73bc206d87
Proof tidying and variable renaming (NA>na, NB>nb when of type msg)
paulson
parents:
3444
diff
changeset

274 
\ {Crypt (shrK A) {Agent B, Key K, na, nb}, \ 
2516
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}} \ 
3466
30791e5a69c4
Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents:
3465
diff
changeset

276 
\ : set evs; \ 
30791e5a69c4
Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents:
3465
diff
changeset

277 
\ Says A Spy {na, nb, Key K} ~: set evs; \ 
2516
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 C evs)"; 
2045
ae1030e66745
Removed some dead wood. Transferred lemmas used to prove analz_image_newK
paulson
parents:
2032
diff
changeset

280 
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

281 
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

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

283 
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

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

285 

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

286 

3444
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

287 
(*Induction for theorems of the form X ~: analz (sees lost Spy evs) > ... 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

288 
It simplifies the proof by discarding needless information about 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

289 
analz (insert X (sees lost Spy evs)) 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

290 
*) 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

291 
val analz_mono_parts_induct_tac = 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

292 
etac yahalom.induct 1 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

293 
THEN 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

294 
REPEAT_FIRST 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

295 
(rtac impI THEN' 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

296 
dtac (sees_subset_sees_Says RS analz_mono RS contra_subsetD) THEN' 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

297 
mp_tac) 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

298 
THEN parts_sees_tac; 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

299 

919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

300 

919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

301 
(** Security Guarantee for A upon receiving YM3 **) 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

302 

919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

303 
(*If the encrypted message appears then it originated with the Server*) 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

304 
goal thy 
3450
cd73bc206d87
Proof tidying and variable renaming (NA>na, NB>nb when of type msg)
paulson
parents:
3444
diff
changeset

305 
"!!evs. [ Crypt (shrK A) {Agent B, Key K, na, nb} \ 
3444
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

306 
\ : parts (sees lost Spy evs); \ 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

307 
\ A ~: lost; evs : yahalom lost ] \ 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

308 
\ ==> Says Server A \ 
3450
cd73bc206d87
Proof tidying and variable renaming (NA>na, NB>nb when of type msg)
paulson
parents:
3444
diff
changeset

309 
\ {Crypt (shrK A) {Agent B, Key K, na, nb}, \ 
3444
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

310 
\ Crypt (shrK B) {Agent A, Key K}} \ 
3465  311 
\ : set evs"; 
3444
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

312 
by (etac rev_mp 1); 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

313 
by parts_induct_tac; 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

314 
by (Fake_parts_insert_tac 1); 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

315 
qed "A_trusts_YM3"; 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

316 

919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

317 

919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

318 
(** Security Guarantees for B upon receiving YM4 **) 
2013  319 

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

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

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

326 
\ {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

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

328 
\ Crypt (shrK B) {Agent A, Key K}} \ 
3465  329 
\ : set evs"; 
2032  330 
by (etac rev_mp 1); 
3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

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

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

334 
by (Blast_tac 1); 
2110  335 
qed "B_trusts_YM4_shrK"; 
336 

3444
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

337 
(*B knows, by the second part of A's message, that the Server distributed 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

338 
the key quoting nonce NB. This part says nothing about agent names. 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

339 
Secrecy of NB is crucial.*) 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

340 
goal thy 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

341 
"!!evs. evs : yahalom lost \ 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

342 
\ ==> Nonce NB ~: analz (sees lost Spy evs) > \ 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

343 
\ Crypt K (Nonce NB) : parts (sees lost Spy evs) > \ 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

344 
\ (EX A B NA. Says Server A \ 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

345 
\ {Crypt (shrK A) {Agent B, Key K, \ 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

346 
\ Nonce NA, Nonce NB}, \ 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

347 
\ Crypt (shrK B) {Agent A, Key K}} \ 
3465  348 
\ : set evs)"; 
3444
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

349 
by analz_mono_parts_induct_tac; 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

350 
(*YM3 & Fake*) 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

351 
by (Blast_tac 2); 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

352 
by (Fake_parts_insert_tac 1); 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

353 
(*YM4*) 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

354 
by (Step_tac 1); 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

355 
(*A is uncompromised because NB is secure*) 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

356 
by (not_lost_tac "A" 1); 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

357 
(*A's certificate guarantees the existence of the Server message*) 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

358 
by (blast_tac (!claset addDs [Says_imp_sees_Spy' RS parts.Inj RS parts.Fst RS 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

359 
A_trusts_YM3]) 1); 
3464
315694e22856
Trivial changes in connection with the Yahalom paper.
paulson
parents:
3450
diff
changeset

360 
bind_thm ("B_trusts_YM4_newK", result() RS mp RSN (2, rev_mp)); 
2133  361 

3444
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

362 

919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

363 
(**** Towards proving secrecy of Nonce NB ****) 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

364 

919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

365 
(** Lemmas about the predicate KeyWithNonce **) 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

366 

919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

367 
goalw thy [KeyWithNonce_def] 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

368 
"!!evs. Says Server A \ 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

369 
\ {Crypt (shrK A) {Agent B, Key K, na, Nonce NB}, X} \ 
3465  370 
\ : set evs ==> KeyWithNonce K NB evs"; 
3444
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

371 
by (Blast_tac 1); 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

372 
qed "KeyWithNonceI"; 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

373 

919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

374 
goalw thy [KeyWithNonce_def] 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

375 
"KeyWithNonce K NB (Says S A X # evs) = \ 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

376 
\ (Server = S & \ 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

377 
\ (EX B n X'. X = {Crypt (shrK A) {Agent B, Key K, n, Nonce NB}, X'}) \ 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

378 
\  KeyWithNonce K NB evs)"; 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

379 
by (Simp_tac 1); 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

380 
by (Blast_tac 1); 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

381 
qed "KeyWithNonce_Says"; 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

382 
Addsimps [KeyWithNonce_Says]; 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

383 

3464
315694e22856
Trivial changes in connection with the Yahalom paper.
paulson
parents:
3450
diff
changeset

384 
(*A fresh key cannot be associated with any nonce 
315694e22856
Trivial changes in connection with the Yahalom paper.
paulson
parents:
3450
diff
changeset

385 
(with respect to a given trace). *) 
3444
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

386 
goalw thy [KeyWithNonce_def] 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

387 
"!!evs. Key K ~: used evs ==> ~ KeyWithNonce K NB evs"; 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

388 
by (blast_tac (!claset addSEs sees_Spy_partsEs) 1); 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

389 
qed "fresh_not_KeyWithNonce"; 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

390 

919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

391 
(*The Server message associates K with NB' and therefore not with any 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

392 
other nonce NB.*) 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

393 
goalw thy [KeyWithNonce_def] 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

394 
"!!evs. [ Says Server A \ 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

395 
\ {Crypt (shrK A) {Agent B, Key K, na, Nonce NB'}, X} \ 
3466
30791e5a69c4
Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents:
3465
diff
changeset

396 
\ : set evs; \ 
3444
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

397 
\ NB ~= NB'; evs : yahalom lost ] \ 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

398 
\ ==> ~ KeyWithNonce K NB evs"; 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

399 
by (blast_tac (!claset addDs [unique_session_keys]) 1); 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

400 
qed "Says_Server_KeyWithNonce"; 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

401 

919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

402 

919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

403 
(*The only nonces that can be found with the help of session keys are 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

404 
those distributed as nonce NB by the Server. The form of the theorem 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

405 
recalls analz_image_freshK, but it is much more complicated.*) 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

406 

919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

407 

919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

408 
(*As with analz_image_freshK, we take some pains to express the property 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

409 
as a logical equivalence so that the simplifier can apply it.*) 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

410 
goal thy 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

411 
"!!evs. P > (X : analz (G Un H)) > (X : analz H) ==> \ 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

412 
\ P > (X : analz (G Un H)) = (X : analz H)"; 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

413 
by (blast_tac (!claset addIs [impOfSubs analz_mono]) 1); 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

414 
val lemma = result(); 
2133  415 

416 
goal thy 

3444
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

417 
"!!evs. evs : yahalom lost ==> \ 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

418 
\ (ALL KK. KK <= Compl (range shrK) > \ 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

419 
\ (ALL K: KK. ~ KeyWithNonce K NB evs) > \ 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

420 
\ (Nonce NB : analz (Key``KK Un (sees lost Spy evs))) = \ 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

421 
\ (Nonce NB : analz (sees lost Spy evs)))"; 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

422 
by (etac yahalom.induct 1); 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

423 
by analz_sees_tac; 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

424 
by (REPEAT_FIRST (resolve_tac [impI RS allI])); 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

425 
by (REPEAT_FIRST (rtac lemma)); 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

426 
(*For Oops, simplification proves NBa~=NB. By Says_Server_KeyWithNonce, 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

427 
we get (~ KeyWithNonce K NB evsa); then simplification can apply the 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

428 
induction hypothesis with KK = {K}.*) 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

429 
by (ALLGOALS (*22 seconds*) 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

430 
(asm_simp_tac 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

431 
(analz_image_freshK_ss addsimps 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

432 
([all_conj_distrib, not_parts_not_analz, analz_image_freshK, 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

433 
KeyWithNonce_Says, fresh_not_KeyWithNonce, 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

434 
imp_disj_not1, (*Moves NBa~=NB to the front*) 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

435 
Says_Server_KeyWithNonce] 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

436 
@ pushes)))); 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

437 
(*Base*) 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

438 
by (Blast_tac 1); 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

439 
(*Fake*) 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

440 
by (spy_analz_tac 1); 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

441 
(*YM4*) (** LEVEL 7 **) 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

442 
by (not_lost_tac "A" 1); 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

443 
by (dtac (Says_imp_sees_Spy' RS parts.Inj RS parts.Fst RS A_trusts_YM3) 1 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

444 
THEN REPEAT (assume_tac 1)); 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

445 
by (blast_tac (!claset addIs [KeyWithNonceI]) 1); 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

446 
qed_spec_mp "Nonce_secrecy"; 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

447 

919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

448 

919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

449 
(*Version required below: if NB can be decrypted using a session key then it 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

450 
was distributed with that key. The more general form above is required 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

451 
for the induction to carry through.*) 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

452 
goal thy 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

453 
"!!evs. [ Says Server A \ 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

454 
\ {Crypt (shrK A) {Agent B, Key KAB, na, Nonce NB'}, X} \ 
3466
30791e5a69c4
Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents:
3465
diff
changeset

455 
\ : set evs; \ 
3444
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

456 
\ NB ~= NB'; KAB ~: range shrK; evs : yahalom lost ] \ 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

457 
\ ==> (Nonce NB : analz (insert (Key KAB) (sees lost Spy evs))) = \ 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

458 
\ (Nonce NB : analz (sees lost Spy evs))"; 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

459 
by (asm_simp_tac (analz_image_freshK_ss addsimps 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

460 
[Nonce_secrecy, Says_Server_KeyWithNonce]) 1); 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

461 
qed "single_Nonce_secrecy"; 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

462 

919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

463 

919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

464 
(*** The Nonce NB uniquely identifies B's message. ***) 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

465 

919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

466 
goal thy 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

467 
"!!evs. evs : yahalom lost ==> \ 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

468 
\ EX NA' A' B'. ALL NA A B. \ 
3501
4ab477ffb4c6
Changed some variables of type msg to lower case (e.g. from NB to nb
paulson
parents:
3466
diff
changeset

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

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

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

473 
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

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

475 
by (asm_simp_tac (!simpset addsimps [all_conj_distrib]) 1); 
2133  476 
(*YM2: creation of new Nonce. Move assertion into global context*) 
3501
4ab477ffb4c6
Changed some variables of type msg to lower case (e.g. from NB to nb
paulson
parents:
3466
diff
changeset

477 
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

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

479 
by (blast_tac (!claset addSEs sees_Spy_partsEs) 1); 
2133  480 
val lemma = result(); 
481 

2110  482 
goal thy 
3501
4ab477ffb4c6
Changed some variables of type msg to lower case (e.g. from NB to nb
paulson
parents:
3466
diff
changeset

483 
"!!evs.[ Crypt (shrK B) {Agent A, Nonce NA, nb} \ 
3444
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

484 
\ : parts (sees lost Spy evs); \ 
3501
4ab477ffb4c6
Changed some variables of type msg to lower case (e.g. from NB to nb
paulson
parents:
3466
diff
changeset

485 
\ Crypt (shrK B') {Agent A', Nonce NA', nb} \ 
3444
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

486 
\ : parts (sees lost Spy evs); \ 
2133  487 
\ evs : yahalom lost; B ~: lost; B' ~: lost ] \ 
488 
\ ==> NA' = NA & A' = A & B' = B"; 

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

489 
by (prove_unique_tac lemma 1); 
2133  490 
qed "unique_NB"; 
491 

492 

3444
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

493 
(*Variant useful for proving secrecy of NB: the Says... form allows 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

494 
not_lost_tac to remove the assumption B' ~: lost.*) 
2133  495 
goal thy 
3501
4ab477ffb4c6
Changed some variables of type msg to lower case (e.g. from NB to nb
paulson
parents:
3466
diff
changeset

496 
"!!evs.[ Says C D {X, Crypt (shrK B) {Agent A, Nonce NA, nb}} \ 
3466
30791e5a69c4
Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents:
3465
diff
changeset

497 
\ : set evs; B ~: lost; \ 
3501
4ab477ffb4c6
Changed some variables of type msg to lower case (e.g. from NB to nb
paulson
parents:
3466
diff
changeset

498 
\ Says C' D' {X', Crypt (shrK B') {Agent A', Nonce NA', nb}} \ 
3466
30791e5a69c4
Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents:
3465
diff
changeset

499 
\ : set evs; \ 
3501
4ab477ffb4c6
Changed some variables of type msg to lower case (e.g. from NB to nb
paulson
parents:
3466
diff
changeset

500 
\ nb ~: analz (sees lost Spy evs); evs : yahalom lost ] \ 
2133  501 
\ ==> NA' = NA & A' = A & B' = B"; 
3444
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

502 
by (not_lost_tac "B'" 1); 
3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

503 
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

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

505 
addDs [unique_NB]) 1); 
2133  506 
qed "Says_unique_NB"; 
507 

3444
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

508 
val Says_unique_NB' = read_instantiate [("lost","lost")] Says_unique_NB; 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

509 

919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

510 

919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

511 
(** A nonce value is never used both as NA and as NB **) 
3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

512 

2133  513 
goal thy 
3464
315694e22856
Trivial changes in connection with the Yahalom paper.
paulson
parents:
3450
diff
changeset

514 
"!!evs. [ B ~: lost; evs : yahalom lost ] \ 
315694e22856
Trivial changes in connection with the Yahalom paper.
paulson
parents:
3450
diff
changeset

515 
\ ==> Nonce NB ~: analz (sees lost Spy evs) > \ 
3501
4ab477ffb4c6
Changed some variables of type msg to lower case (e.g. from NB to nb
paulson
parents:
3466
diff
changeset

516 
\ Crypt (shrK B') {Agent A', Nonce NB, nb'} \ 
3464
315694e22856
Trivial changes in connection with the Yahalom paper.
paulson
parents:
3450
diff
changeset

517 
\ : parts(sees lost Spy evs) \ 
315694e22856
Trivial changes in connection with the Yahalom paper.
paulson
parents:
3450
diff
changeset

518 
\ > Crypt (shrK B) {Agent A, Nonce NA, Nonce NB} \ 
315694e22856
Trivial changes in connection with the Yahalom paper.
paulson
parents:
3450
diff
changeset

519 
\ ~: parts(sees lost Spy evs)"; 
3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

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

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

522 
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

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

524 
addSEs partsEs) 1); 
3464
315694e22856
Trivial changes in connection with the Yahalom paper.
paulson
parents:
3450
diff
changeset

525 
bind_thm ("no_nonce_YM1_YM2", result() RS mp RSN (2,rev_mp) RSN (2,rev_notE)); 
2133  526 

3464
315694e22856
Trivial changes in connection with the Yahalom paper.
paulson
parents:
3450
diff
changeset

527 
(*The Server sends YM3 only in response to YM2.*) 
2133  528 
goal thy 
3466
30791e5a69c4
Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents:
3465
diff
changeset

529 
"!!evs. [ Says Server A \ 
30791e5a69c4
Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents:
3465
diff
changeset

530 
\ {Crypt (shrK A) {Agent B, k, na, nb}, X} : set evs; \ 
2133  531 
\ evs : yahalom lost ] \ 
532 
\ ==> EX B'. Says B' Server \ 

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

533 
\ { Agent B, Crypt (shrK B) {Agent A, na, nb} } \ 
3465  534 
\ : set evs"; 
2133  535 
by (etac rev_mp 1); 
536 
by (etac yahalom.induct 1); 

537 
by (ALLGOALS Asm_simp_tac); 

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

538 
by (ALLGOALS Blast_tac); 
2133  539 
qed "Says_Server_imp_YM2"; 
540 

541 

3464
315694e22856
Trivial changes in connection with the Yahalom paper.
paulson
parents:
3450
diff
changeset

542 
(*A vital theorem for B, that nonce NB remains secure from the Spy. 
3444
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

543 
Unusually, the Fake case requires Spy:lost.*) 
2133  544 
goal thy 
545 
"!!evs. [ A ~: lost; B ~: lost; Spy: lost; evs : yahalom lost ] \ 

546 
\ ==> Says B Server \ 

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

547 
\ {Agent B, Crypt (shrK B) {Agent A, Nonce NA, Nonce NB}} \ 
3466
30791e5a69c4
Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents:
3465
diff
changeset

548 
\ : set evs > \ 
30791e5a69c4
Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents:
3465
diff
changeset

549 
\ (ALL k. Says A Spy {Nonce NA, Nonce NB, k} ~: set evs) > \ 
2133  550 
\ Nonce NB ~: analz (sees lost Spy evs)"; 
551 
by (etac yahalom.induct 1); 

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

552 
by analz_sees_tac; 
2133  553 
by (ALLGOALS 
554 
(asm_simp_tac 

3444
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

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

556 
analz_insert_freshK] @ pushes) 
2133  557 
setloop split_tac [expand_if]))); 
3450
cd73bc206d87
Proof tidying and variable renaming (NA>na, NB>nb when of type msg)
paulson
parents:
3444
diff
changeset

558 
(*Prove YM3 by showing that no NB can also be an NA*) 
cd73bc206d87
Proof tidying and variable renaming (NA>na, NB>nb when of type msg)
paulson
parents:
3444
diff
changeset

559 
by (blast_tac (!claset addDs [Says_imp_sees_Spy' RS parts.Inj] 
cd73bc206d87
Proof tidying and variable renaming (NA>na, NB>nb when of type msg)
paulson
parents:
3444
diff
changeset

560 
addSEs [MPair_parts] 
cd73bc206d87
Proof tidying and variable renaming (NA>na, NB>nb when of type msg)
paulson
parents:
3444
diff
changeset

561 
addDs [no_nonce_YM1_YM2, Says_unique_NB']) 4 
cd73bc206d87
Proof tidying and variable renaming (NA>na, NB>nb when of type msg)
paulson
parents:
3444
diff
changeset

562 
THEN flexflex_tac); 
3444
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

563 
(*YM2: similar freshness reasoning*) 
3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

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

565 
addDs [Says_imp_sees_Spy' RS analz.Inj, 
3450
cd73bc206d87
Proof tidying and variable renaming (NA>na, NB>nb when of type msg)
paulson
parents:
3444
diff
changeset

566 
impOfSubs analz_subset_parts]) 3); 
cd73bc206d87
Proof tidying and variable renaming (NA>na, NB>nb when of type msg)
paulson
parents:
3444
diff
changeset

567 
(*YM1: NB=NA is impossible anyway, but NA is secret because it is fresh!*) 
cd73bc206d87
Proof tidying and variable renaming (NA>na, NB>nb when of type msg)
paulson
parents:
3444
diff
changeset

568 
by (blast_tac (!claset addSIs [parts_insertI] 
cd73bc206d87
Proof tidying and variable renaming (NA>na, NB>nb when of type msg)
paulson
parents:
3444
diff
changeset

569 
addSEs sees_Spy_partsEs) 2); 
2377  570 
(*Fake*) 
571 
by (spy_analz_tac 1); 

3444
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

572 
(** LEVEL 7: YM4 and Oops remain **) 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

573 
(*YM4: key K is visible to Spy, contradicting session key secrecy theorem*) 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

574 
by (REPEAT (Safe_step_tac 1)); 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

575 
by (not_lost_tac "Aa" 1); 
3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

576 
by (dtac (Says_imp_sees_Spy' RS parts.Inj RS parts.Fst RS A_trusts_YM3) 1); 
2133  577 
by (forward_tac [Says_Server_message_form] 3); 
578 
by (forward_tac [Says_Server_imp_YM2] 4); 

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

579 
by (REPEAT_FIRST (eresolve_tac [asm_rl, bexE, exE, disjE])); 
3444
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

580 
(* use Says_unique_NB' to identify message components: Aa=A, Ba=B, NAa=NA *) 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

581 
by (blast_tac (!claset addDs [Says_unique_NB', Spy_not_see_encrypted_key, 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

582 
impOfSubs Fake_analz_insert]) 1); 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

583 
(** LEVEL 14 **) 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

584 
(*Oops case: if the nonce is betrayed now, show that the Oops event is 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

585 
covered by the quantified Oops assumption.*) 
2133  586 
by (full_simp_tac (!simpset addsimps [all_conj_distrib]) 1); 
587 
by (step_tac (!claset delrules [disjE, conjI]) 1); 

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

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

3444
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

590 
(*If NB=NBa then all other components of the Oops message agree*) 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

591 
by (blast_tac (!claset addDs [Says_unique_NB']) 1 THEN flexflex_tac); 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

592 
(*case NB ~= NBa*) 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

593 
by (asm_simp_tac (!simpset addsimps [single_Nonce_secrecy]) 1); 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

594 
by (blast_tac (!claset addSEs [MPair_parts] 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

595 
addDs [Says_imp_sees_Spy' RS parts.Inj, 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

596 
no_nonce_YM1_YM2 (*to prove NB~=NAa*) ]) 1); 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

597 
bind_thm ("Spy_not_see_NB", result() RSN(2,rev_mp) RSN(2,rev_mp)); 
2133  598 

2001  599 

3464
315694e22856
Trivial changes in connection with the Yahalom paper.
paulson
parents:
3450
diff
changeset

600 
(*B's session key guarantee from YM4. The two certificates contribute to a 
315694e22856
Trivial changes in connection with the Yahalom paper.
paulson
parents:
3450
diff
changeset

601 
single conclusion about the Server's message. Note that the "Says A Spy" 
315694e22856
Trivial changes in connection with the Yahalom paper.
paulson
parents:
3450
diff
changeset

602 
assumption must quantify over ALL POSSIBLE keys instead of our particular K. 
315694e22856
Trivial changes in connection with the Yahalom paper.
paulson
parents:
3450
diff
changeset

603 
If this run is broken and the spy substitutes a certificate containing an 
315694e22856
Trivial changes in connection with the Yahalom paper.
paulson
parents:
3450
diff
changeset

604 
old key, B has no means of telling.*) 
2001  605 
goal thy 
3444
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

606 
"!!evs. [ Says B Server \ 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

607 
\ {Agent B, Crypt (shrK B) {Agent A, Nonce NA, Nonce NB}} \ 
3466
30791e5a69c4
Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents:
3465
diff
changeset

608 
\ : set evs; \ 
3444
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

609 
\ Says A' B {Crypt (shrK B) {Agent A, Key K}, \ 
3466
30791e5a69c4
Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents:
3465
diff
changeset

610 
\ Crypt K (Nonce NB)} : set evs; \ 
30791e5a69c4
Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents:
3465
diff
changeset

611 
\ ALL k. Says A Spy {Nonce NA, Nonce NB, k} ~: set evs; \ 
3444
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

612 
\ A ~: lost; B ~: lost; Spy: lost; evs : yahalom lost ] \ 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

613 
\ ==> Says Server A \ 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

614 
\ {Crypt (shrK A) {Agent B, Key K, \ 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

615 
\ Nonce NA, Nonce NB}, \ 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

616 
\ Crypt (shrK B) {Agent A, Key K}} \ 
3465  617 
\ : set evs"; 
2133  618 
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

619 
by (etac (Says_imp_sees_Spy' RS parts.Inj RS MPair_parts) 1 THEN 
2133  620 
dtac B_trusts_YM4_shrK 1); 
2170  621 
by (dtac B_trusts_YM4_newK 3); 
2110  622 
by (REPEAT_FIRST (eresolve_tac [asm_rl, exE])); 
2133  623 
by (forward_tac [Says_Server_imp_YM2] 1 THEN assume_tac 1); 
2170  624 
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

625 
by (blast_tac (!claset addDs [Says_unique_NB']) 1); 
2322  626 
qed "B_trusts_YM4"; 
3444
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

627 

919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

628 

919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

629 

919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

630 
(*** Authenticating B to A ***) 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

631 

919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

632 
(*The encryption in message YM2 tells us it cannot be faked.*) 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

633 
goal thy 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

634 
"!!evs. evs : yahalom lost \ 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

635 
\ ==> Crypt (shrK B) {Agent A, Nonce NA, nb} \ 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

636 
\ : parts (sees lost Spy evs) > \ 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

637 
\ B ~: lost > \ 
3466
30791e5a69c4
Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents:
3465
diff
changeset

638 
\ Says B Server {Agent B, Crypt (shrK B) {Agent A, Nonce NA, nb}} \ 
3465  639 
\ : set evs"; 
3444
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

640 
by parts_induct_tac; 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

641 
by (Fake_parts_insert_tac 1); 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

642 
bind_thm ("B_Said_YM2", result() RSN (2, rev_mp) RS mp); 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

643 

919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

644 
(*If the server sends YM3 then B sent YM2*) 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

645 
goal thy 
3466
30791e5a69c4
Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents:
3465
diff
changeset

646 
"!!evs. evs : yahalom lost \ 
3444
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

647 
\ ==> Says Server A {Crypt (shrK A) {Agent B, Key K, Nonce NA, nb}, X} \ 
3466
30791e5a69c4
Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents:
3465
diff
changeset

648 
\ : set evs > \ 
30791e5a69c4
Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents:
3465
diff
changeset

649 
\ B ~: lost > \ 
30791e5a69c4
Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents:
3465
diff
changeset

650 
\ Says B Server {Agent B, Crypt (shrK B) {Agent A, Nonce NA, nb}} \ 
3465  651 
\ : set evs"; 
3444
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

652 
by (etac yahalom.induct 1); 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

653 
by (ALLGOALS Asm_simp_tac); 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

654 
(*YM4*) 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

655 
by (Blast_tac 2); 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

656 
(*YM3*) 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

657 
by (best_tac (!claset addSDs [B_Said_YM2, Says_imp_sees_Spy' RS parts.Inj] 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

658 
addSEs [MPair_parts]) 1); 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

659 
val lemma = result() RSN (2, rev_mp) RS mp > standard; 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

660 

919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

661 
(*If A receives YM3 then B has used nonce NA (and therefore is alive)*) 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

662 
goal thy 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

663 
"!!evs. [ Says S A {Crypt (shrK A) {Agent B, Key K, Nonce NA, nb}, X} \ 
3466
30791e5a69c4
Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents:
3465
diff
changeset

664 
\ : set evs; \ 
3444
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

665 
\ A ~: lost; B ~: lost; evs : yahalom lost ] \ 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

666 
\ ==> Says B Server {Agent B, Crypt (shrK B) {Agent A, Nonce NA, nb}} \ 
3465  667 
\ : set evs"; 
3444
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

668 
by (blast_tac (!claset addSDs [A_trusts_YM3, lemma] 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

669 
addEs sees_Spy_partsEs) 1); 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

670 
qed "YM3_auth_B_to_A"; 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

671 

919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

672 

919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

673 
(*** Authenticating A to B using the certificate Crypt K (Nonce NB) ***) 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

674 

919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

675 
(*Induction for theorems of the form X ~: analz (sees lost Spy evs) > ... 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

676 
It simplifies the proof by discarding needless information about 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

677 
analz (insert X (sees lost Spy evs)) 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

678 
*) 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

679 
val analz_mono_parts_induct_tac = 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

680 
etac yahalom.induct 1 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

681 
THEN 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

682 
REPEAT_FIRST 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

683 
(rtac impI THEN' 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

684 
dtac (sees_subset_sees_Says RS analz_mono RS contra_subsetD) THEN' 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

685 
mp_tac) 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

686 
THEN parts_sees_tac; 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

687 

919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

688 
(*Assuming the session key is secure, if both certificates are present then 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

689 
A has said NB. We can't be sure about the rest of A's message, but only 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

690 
NB matters for freshness.*) 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

691 
goal thy 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

692 
"!!evs. evs : yahalom lost \ 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

693 
\ ==> Key K ~: analz (sees lost Spy evs) > \ 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

694 
\ Crypt K (Nonce NB) : parts (sees lost Spy evs) > \ 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

695 
\ Crypt (shrK B) {Agent A, Key K} \ 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

696 
\ : parts (sees lost Spy evs) > \ 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

697 
\ B ~: lost > \ 
3465  698 
\ (EX X. Says A B {X, Crypt K (Nonce NB)} : set evs)"; 
3444
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

699 
by analz_mono_parts_induct_tac; 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

700 
(*Fake*) 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

701 
by (Fake_parts_insert_tac 1); 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

702 
(*YM3: by new_keys_not_used we note that Crypt K (Nonce NB) could not exist*) 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

703 
by (fast_tac (!claset addSDs [Crypt_imp_invKey_keysFor] addss (!simpset)) 1); 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

704 
(*YM4: was Crypt K (Nonce NB) the very last message? If not, use ind. hyp.*) 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

705 
by (asm_simp_tac (!simpset addsimps [ex_disj_distrib]) 1); 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

706 
(*yes: apply unicity of session keys*) 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

707 
by (not_lost_tac "Aa" 1); 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

708 
by (blast_tac (!claset addSEs [MPair_parts] 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

709 
addSDs [A_trusts_YM3, B_trusts_YM4_shrK] 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

710 
addDs [Says_imp_sees_Spy' RS parts.Inj, 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

711 
unique_session_keys]) 1); 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

712 
val lemma = normalize_thm [RSspec, RSmp] (result()) > standard; 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

713 

919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

714 
(*If B receives YM4 then A has used nonce NB (and therefore is alive). 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

715 
Moreover, A associates K with NB (thus is talking about the same run). 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

716 
Other premises guarantee secrecy of K.*) 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

717 
goal thy 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

718 
"!!evs. [ Says B Server \ 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

719 
\ {Agent B, Crypt (shrK B) {Agent A, Nonce NA, Nonce NB}} \ 
3466
30791e5a69c4
Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents:
3465
diff
changeset

720 
\ : set evs; \ 
30791e5a69c4
Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents:
3465
diff
changeset

721 
\ Says A' B {Crypt (shrK B) {Agent A, Key K}, \ 
30791e5a69c4
Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents:
3465
diff
changeset

722 
\ Crypt K (Nonce NB)} : set evs; \ 
30791e5a69c4
Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents:
3465
diff
changeset

723 
\ (ALL NA k. Says A Spy {Nonce NA, Nonce NB, k} ~: set evs); \ 
3444
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

724 
\ A ~: lost; B ~: lost; Spy: lost; evs : yahalom lost ] \ 
3465  725 
\ ==> EX X. Says A B {X, Crypt K (Nonce NB)} : set evs"; 
3444
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

726 
by (dtac B_trusts_YM4 1); 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

727 
by (REPEAT_FIRST (eresolve_tac [asm_rl, spec])); 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

728 
by (etac (Says_imp_sees_Spy' RS parts.Inj RS MPair_parts) 1); 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

729 
by (rtac lemma 1); 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

730 
by (rtac Spy_not_see_encrypted_key 2); 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

731 
by (REPEAT_FIRST assume_tac); 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

732 
by (blast_tac (!claset addSEs [MPair_parts] 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

733 
addDs [Says_imp_sees_Spy' RS parts.Inj]) 1); 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

734 
qed_spec_mp "YM4_imp_A_Said_YM3"; 