author  paulson 
Thu, 26 Jun 1997 11:58:05 +0200  
changeset 3464  315694e22856 
parent 3450  cd73bc206d87 
child 3465  e85c24717cad 
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 ] \ 

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

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

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

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

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

34 

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

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

36 

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

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

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

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

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

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

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

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

45 

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

46 

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

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

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

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

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

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

54 

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

55 

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

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

57 

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

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

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

63 

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

66 

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

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

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

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

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

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

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

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

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

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

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

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

82 

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

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

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

85 

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

86 

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

89 

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

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

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

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

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

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

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

99 

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

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

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

104 
qed "Spy_analz_shrK"; 

105 
Addsimps [Spy_analz_shrK]; 

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

106 

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

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

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

111 

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

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

114 

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

115 

3432  116 
(*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

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

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

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

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

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

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

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

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

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

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

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

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

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

131 

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

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

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

135 

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

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

137 

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

138 

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

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

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

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

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

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

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

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

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

152 

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

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

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

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

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

158 

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

159 

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

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

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

162 

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

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

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

165 

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

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

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

168 

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

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

170 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

186 

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

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

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

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

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

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

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

193 

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

194 

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

197 
goal thy 

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

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

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

201 
\ {Crypt (shrK A) {Agent B, Key K, na, nb}, X} \ 
cd73bc206d87
Proof tidying and variable renaming (NA>na, NB>nb when of type msg)
paulson
parents:
3444
diff
changeset

202 
\ : set_of_list evs > A=A' & B=B' & na=na' & nb=nb' & X=X'"; 
2110  203 
by (etac yahalom.induct 1); 
204 
by (ALLGOALS (asm_simp_tac (!simpset addsimps [all_conj_distrib]))); 

205 
by (Step_tac 1); 

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

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

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

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

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

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

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

216 
goal thy 

217 
"!!evs. [ Says Server A \ 

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

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

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

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

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

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

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

228 

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

2013  230 

231 
goal thy 

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

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

235 
\ Crypt (shrK B) {Agent A, Key K}} \ 
2110  236 
\ : set_of_list evs > \ 
3450
cd73bc206d87
Proof tidying and variable renaming (NA>na, NB>nb when of type msg)
paulson
parents:
3444
diff
changeset

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

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

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

243 
(!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

244 
analz_insert_freshK] 
2013  245 
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

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

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

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

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

251 
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

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

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

256 

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

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

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

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

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

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

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

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

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

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

270 

3432  271 
(*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

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

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

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

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

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

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

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

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

280 
\ ==> 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

281 
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

282 
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

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

284 
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

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

286 

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

287 

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

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

289 
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

290 
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

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

292 
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

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

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

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

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

297 
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

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

299 
THEN parts_sees_tac; 
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 

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

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

303 

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

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

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

306 
"!!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

307 
\ : 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

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

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

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

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

312 
\ : set_of_list evs"; 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

313 
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

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

315 
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

316 
qed "A_trusts_YM3"; 
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 

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

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

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

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

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

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

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

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

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

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

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

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

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

339 
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

340 
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

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

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

343 
\ ==> 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

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

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

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

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

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

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

350 
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

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

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

353 
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

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

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

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

357 
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

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

359 
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

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

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

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

363 

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

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

365 

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

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

367 

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

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

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

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

371 
\ : set_of_list 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

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

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

374 

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

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

376 
"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

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

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

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

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

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

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

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

384 

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

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

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

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

388 
"!!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

389 
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

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

391 

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

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

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

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

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

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

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

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

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

400 
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

401 
qed "Says_Server_KeyWithNonce"; 
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 

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

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

405 
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

406 
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

407 

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

408 

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

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

410 
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

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

412 
"!!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

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

414 
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

415 
val lemma = result(); 
2133  416 

417 
goal thy 

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

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

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

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

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

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

423 
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

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

425 
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

426 
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

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

428 
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

429 
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

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

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

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

433 
([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

434 
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

435 
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

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

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

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

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

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

441 
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

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

443 
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

444 
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

445 
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

446 
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

447 
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

448 

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

449 

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

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

451 
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

452 
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

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

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

455 
\ {Crypt (shrK A) {Agent B, Key KAB, na, Nonce NB'}, X} \ 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

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

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

458 
\ ==> (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

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

460 
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

461 
[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

462 
qed "single_Nonce_secrecy"; 
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 

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

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

466 

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

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

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

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

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

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

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

474 
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

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

476 
by (asm_simp_tac (!simpset addsimps [all_conj_distrib]) 1); 
2133  477 
(*YM2: creation of new Nonce. Move assertion into global context*) 
478 
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

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

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

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

484 
"!!evs.[ 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

485 
\ : 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

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

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

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

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

493 

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

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

495 
not_lost_tac to remove the assumption B' ~: lost.*) 
2133  496 
goal thy 
3444
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

497 
"!!evs.[ Says C D {X, 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

498 
\ : set_of_list evs; B ~: lost; \ 
2284
80ebd1a213fd
Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents:
2269
diff
changeset

499 
\ Says C' D' {X', 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

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

501 
\ NB ~: analz (sees lost Spy evs); evs : yahalom lost ] \ 
2133  502 
\ ==> 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

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

504 
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

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

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

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

509 
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

510 

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

511 

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

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

513 

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

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

516 
\ ==> Nonce NB ~: analz (sees lost Spy evs) > \ 
315694e22856
Trivial changes in connection with the Yahalom paper.
paulson
parents:
3450
diff
changeset

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

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

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

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

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

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

523 
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

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

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

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

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

528 
(*The Server sends YM3 only in response to YM2.*) 
2133  529 
goal thy 
530 
"!!evs. [ Says Server A \ 

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

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

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

534 
\ { Agent B, Crypt (shrK B) {Agent A, na, nb} } \ 
2133  535 
\ : set_of_list evs"; 
536 
by (etac rev_mp 1); 

537 
by (etac yahalom.induct 1); 

538 
by (ALLGOALS Asm_simp_tac); 

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

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

542 

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

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

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

547 
\ ==> Says B Server \ 

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

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

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

552 
by (etac yahalom.induct 1); 

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

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

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

556 
(!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

557 
analz_insert_freshK] @ pushes) 
2133  558 
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

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

560 
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

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

562 
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

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

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

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

566 
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

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

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

569 
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

570 
addSEs sees_Spy_partsEs) 2); 
2377  571 
(*Fake*) 
572 
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

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

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

575 
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

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

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

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

580 
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

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

582 
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

583 
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

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

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

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

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

590 
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

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

592 
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

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

594 
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

595 
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

596 
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

597 
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

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

2001  600 

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

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

602 
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

603 
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

604 
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

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

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

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

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

610 
\ Says A' B {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

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

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

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

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

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

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

618 
\ : set_of_list evs"; 
2133  619 
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

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

626 
by (blast_tac (!claset addDs [Says_unique_NB']) 1); 
2322  627 
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

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 

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

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

632 

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

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

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

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

636 
\ ==> 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

637 
\ : 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

638 
\ B ~: lost > \ 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

639 
\ Says B Server {Agent B, \ 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

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

641 
\ : set_of_list evs"; 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

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

643 
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

644 
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

645 

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

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

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

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

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

650 
\ : set_of_list evs > \ 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

651 
\ B ~: lost > \ 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

652 
\ Says B Server {Agent B, \ 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

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

654 
\ : set_of_list evs"; 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

655 
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

656 
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

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

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

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

660 
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

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

662 
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

663 

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

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

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

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

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

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

669 
\ ==> Says B Server {Agent B, 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

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

671 
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

672 
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

673 
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

674 

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

675 

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

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

677 

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

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

679 
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

680 
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

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

682 
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

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

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

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

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

687 
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

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

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

690 

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

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

692 
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

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

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

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

696 
\ ==> 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

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

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

699 
\ : 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

700 
\ B ~: lost > \ 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

701 
\ (EX X. Says A B {X, Crypt K (Nonce NB)} : set_of_list evs)"; 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

702 
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

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

704 
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

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

706 
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

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

708 
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

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

710 
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

711 
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

712 
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

713 
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

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

715 
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

716 

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

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

718 
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

719 
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

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

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

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

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

724 
\ Says A' B {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

725 
\ Crypt K (Nonce NB)} : set_of_list evs; \ 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

726 
\ (ALL NA k. Says A Spy {Nonce NA, Nonce NB, k} \ 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

727 
\ ~: set_of_list evs); \ 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

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

729 
\ ==> EX X. Says A B {X, Crypt K (Nonce NB)} : set_of_list evs"; 
919de2cb3487
Streamlined proofs of the secrecy of NB and added authentication of A and B
paulson
parents:
3432
diff
changeset

730 
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

731 
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

732 
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

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

734 
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

735 
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

736 
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

737 
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

738 
qed_spec_mp "YM4_imp_A_Said_YM3"; 