author  paulson 
Mon, 14 Jul 1997 12:47:21 +0200  
changeset 3519  ab0a9fbed4c0 
parent 3516  470626799511 
child 3543  82f33248d89d 
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 

1995  19 

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

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

23 
\ ==> EX X NB K. EX evs: yahalom. \ 
3465  24 
\ Says A B {X, Crypt K (Nonce NB)} : set evs"; 
1995  25 
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

26 
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

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

28 
by possibility_tac; 
2013  29 
result(); 
1995  30 

31 

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

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

33 

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

34 
(*Nobody sends themselves messages*) 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

35 
goal thy "!!evs. evs: yahalom ==> ALL A X. Says A A X ~: set evs"; 
2032  36 
by (etac yahalom.induct 1); 
1985
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

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

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

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

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

41 

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

42 

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

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

44 

1995  45 
(*Lets us treat YM4 using a similar argument as for the Fake case.*) 
3465  46 
goal thy "!!evs. Says S A {Crypt (shrK A) Y, X} : set evs ==> \ 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

47 
\ X : analz (sees Spy evs)"; 
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

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

50 

2110  51 
bind_thm ("YM4_parts_sees_Spy", 
52 
YM4_analz_sees_Spy RS (impOfSubs analz_subset_parts)); 

53 

2133  54 
(*Relates to both YM4 and Oops*) 
3466
30791e5a69c4
Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents:
3465
diff
changeset

55 
goal thy "!!evs. Says S A {Crypt (shrK A) {B,K,NA,NB}, X} : set evs ==> \ 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

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

57 
by (blast_tac (!claset addSEs partsEs 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

58 
addSDs [Says_imp_sees_Spy RS parts.Inj]) 1); 
2110  59 
qed "YM4_Key_parts_sees_Spy"; 
60 

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

61 
(*For proving the easier theorems about X ~: parts (sees Spy evs).*) 
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

62 
fun parts_sees_tac i = 
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

63 
forward_tac [YM4_Key_parts_sees_Spy] (i+6) THEN 
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

64 
forward_tac [YM4_parts_sees_Spy] (i+5) THEN 
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

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

66 

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

67 
(*Induction for regularity theorems. If induction formula has the form 
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

68 
X ~: analz (sees Spy evs) > ... then it shortens the proof by discarding 
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

69 
needless information about analz (insert X (sees Spy evs)) *) 
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

70 
fun parts_induct_tac i = 
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

71 
etac yahalom.induct i 
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

72 
THEN 
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

73 
REPEAT (FIRSTGOAL analz_mono_contra_tac) 
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

74 
THEN parts_sees_tac i; 
1985
84cf16192e03
Tidied many proofs, using AddIffs to let equivalences take
paulson
parents:
diff
changeset

75 

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

76 

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

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

79 

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

81 
goal thy 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

82 
"!!evs. evs : yahalom ==> (Key (shrK A) : parts (sees Spy evs)) = (A : lost)"; 
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

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

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

85 
by (Blast_tac 1); 
2133  86 
qed "Spy_see_shrK"; 
87 
Addsimps [Spy_see_shrK]; 

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

88 

2133  89 
goal thy 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

90 
"!!evs. evs : yahalom ==> (Key (shrK A) : analz (sees Spy evs)) = (A : lost)"; 
2133  91 
by (auto_tac(!claset addDs [impOfSubs analz_subset_parts], !simpset)); 
92 
qed "Spy_analz_shrK"; 

93 
Addsimps [Spy_analz_shrK]; 

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

94 

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

95 
goal thy "!!A. [ Key (shrK A) : parts (sees Spy evs); \ 
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

96 
\ evs : yahalom ] ==> A:lost"; 
3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

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

99 

2133  100 
bind_thm ("Spy_analz_shrK_D", analz_subset_parts RS subsetD RS Spy_see_shrK_D); 
101 
AddSDs [Spy_see_shrK_D, Spy_analz_shrK_D]; 

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

102 

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

103 

3432  104 
(*Nobody can have used nonexistent keys! Needed to apply analz_insert_Key*) 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

105 
goal thy "!!evs. evs : yahalom ==> \ 
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

106 
\ Key K ~: used evs > K ~: keysFor (parts (sees Spy evs))"; 
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

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

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

109 
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

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

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

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

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

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

115 
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

116 
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

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

119 

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

120 
bind_thm ("new_keys_not_analzd", 
2032  121 
[analz_subset_parts RS keysFor_mono, 
122 
new_keys_not_used] MRS contra_subsetD); 

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

123 

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

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

125 

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

126 

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

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

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

131 
\ : set evs; \ 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

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

133 
\ ==> K ~: range shrK"; 
2133  134 
by (etac rev_mp 1); 
135 
by (etac yahalom.induct 1); 

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

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

137 
by (Blast_tac 1); 
2133  138 
qed "Says_Server_message_form"; 
2110  139 

140 

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

141 
(*For proofs involving analz.*) 
3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

142 
val analz_sees_tac = 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

143 
forward_tac [YM4_analz_sees_Spy] 6 THEN 
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

144 
forward_tac [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

145 
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

146 

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

147 

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

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

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

150 

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

151 
Key K : analz (insert (Key KAB) (sees Spy evs)) ==> 
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

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

153 

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

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

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

156 

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

157 
(** Session keys are not used to encrypt other session keys **) 
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 
goal thy 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

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

161 
\ ALL K KK. KK <= Compl (range shrK) > \ 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

162 
\ (Key K : analz (Key``KK Un (sees Spy evs))) = \ 
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

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

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

166 
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

167 
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

168 
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

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

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

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

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

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

174 

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

175 
goal thy 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

176 
"!!evs. [ evs : yahalom; KAB ~: range shrK ] ==> \ 
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

177 
\ Key K : analz (insert (Key KAB) (sees Spy evs)) = \ 
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

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

179 
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

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

181 

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

182 

2110  183 
(*** The Key K uniquely identifies the Server's message. **) 
184 

185 
goal thy 

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

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

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

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

193 
by (Step_tac 1); 

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

195 
by (Blast_tac 2); 
2110  196 
(*Remaining case: YM3*) 
197 
by (expand_case_tac "K = ?y" 1); 

198 
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

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

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

201 
delrules [conjI] (*no splitup to 4 subgoals*)) 1); 
2110  202 
val lemma = result(); 
203 

204 
goal thy 

205 
"!!evs. [ Says Server A \ 

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

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

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

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

210 
\ : set evs; \ 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

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

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

213 
by (prove_unique_tac lemma 1); 
2110  214 
qed "unique_session_keys"; 
215 

216 

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

2013  218 

219 
goal thy 

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

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

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

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

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

225 
\ Says A Spy {na, nb, Key K} ~: set evs > \ 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

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

228 
by analz_sees_tac; 
2013  229 
by (ALLGOALS 
230 
(asm_simp_tac 

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

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

232 
analz_insert_freshK] 
2013  233 
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

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

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

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

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

239 
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

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

241 
by (spy_analz_tac 1); 
2110  242 
val lemma = result() RS mp RS mp RSN(2,rev_notE); 
2013  243 

244 

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

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

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

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

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

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

251 
\ Says A Spy {na, nb, Key K} ~: set evs; \ 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

252 
\ A ~: lost; B ~: lost; evs : yahalom ] \ 
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

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

255 
by (blast_tac (!claset addSEs [lemma]) 1); 
2032  256 
qed "Spy_not_see_encrypted_key"; 
2001  257 

258 

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

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

260 

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

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

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

263 
"!!evs. [ Crypt (shrK A) {Agent B, Key K, na, nb} \ 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

264 
\ : parts (sees Spy evs); \ 
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

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

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

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

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

270 
by (etac rev_mp 1); 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

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

272 
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

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

274 

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

275 

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

276 
(** Security Guarantees for B upon receiving YM4 **) 
2013  277 

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

2001  280 
goal thy 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

281 
"!!evs. [ Crypt (shrK B) {Agent A, Key K} : parts (sees Spy evs); \ 
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

282 
\ B ~: lost; evs : yahalom ] \ 
2001  283 
\ ==> EX NA NB. Says Server A \ 
2451
ce85a2aafc7a
Extensive tidying and simplification, largely stemming from
paulson
parents:
2377
diff
changeset

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

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

286 
\ Crypt (shrK B) {Agent A, Key K}} \ 
3465  287 
\ : set evs"; 
2032  288 
by (etac rev_mp 1); 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

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

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

292 
by (Blast_tac 1); 
2110  293 
qed "B_trusts_YM4_shrK"; 
294 

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

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

296 
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

297 
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

298 
goal thy 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

299 
"!!evs. evs : yahalom \ 
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

300 
\ ==> Nonce NB ~: analz (sees Spy evs) > \ 
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

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

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

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

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

305 
\ Crypt (shrK B) {Agent A, Key K}} \ 
3465  306 
\ : set evs)"; 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

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

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

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

310 
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

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

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

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

314 
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

315 
(*A's certificate guarantees the existence of the Server message*) 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

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

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

318 
bind_thm ("B_trusts_YM4_newK", result() RS mp RSN (2, rev_mp)); 
2133  319 

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

320 

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

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

322 

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

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

324 

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

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

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

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

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

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

331 

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

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

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

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

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

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

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

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

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

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

341 

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

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

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

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

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

346 
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

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

348 

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

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

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

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

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

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

354 
\ : set evs; \ 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

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

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

357 
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

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

359 

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

360 

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

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

362 
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

363 
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

364 

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

367 
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

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

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

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

371 
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

372 
val lemma = result(); 
2133  373 

374 
goal thy 

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

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

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

377 
\ (ALL K: KK. ~ KeyWithNonce K NB evs) > \ 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

378 
\ (Nonce NB : analz (Key``KK Un (sees Spy evs))) = \ 
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

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

380 
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

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

382 
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

383 
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

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

385 
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

386 
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

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

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

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

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

391 
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

392 
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

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

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

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

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

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

398 
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

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

400 
by (not_lost_tac "A" 1); 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

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

402 
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

403 
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

404 
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

405 

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

406 

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

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

408 
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

409 
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

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

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

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

413 
\ : set evs; \ 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

414 
\ NB ~= NB'; KAB ~: range shrK; evs : yahalom ] \ 
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

415 
\ ==> (Nonce NB : analz (insert (Key KAB) (sees Spy evs))) = \ 
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

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

417 
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

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

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

420 

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

421 

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

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

423 

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

424 
goal thy 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

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

426 
\ EX NA' A' B'. ALL NA A B. \ 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

427 
\ Crypt (shrK B) {Agent A, Nonce NA, nb} : parts(sees Spy evs) \ 
2133  428 
\ > B ~: lost > NA = NA' & A = A' & B = B'"; 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

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

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

431 
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

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

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

435 
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

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

437 
by (blast_tac (!claset addSEs sees_Spy_partsEs) 1); 
2133  438 
val lemma = result(); 
439 

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

441 
"!!evs.[ Crypt (shrK B) {Agent A, Nonce NA, nb} \ 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

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

443 
\ Crypt (shrK B') {Agent A', Nonce NA', nb} \ 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

444 
\ : parts (sees Spy evs); \ 
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

445 
\ evs : yahalom; B ~: lost; B' ~: lost ] \ 
2133  446 
\ ==> NA' = NA & A' = A & B' = B"; 
2451
ce85a2aafc7a
Extensive tidying and simplification, largely stemming from
paulson
parents:
2377
diff
changeset

447 
by (prove_unique_tac lemma 1); 
2133  448 
qed "unique_NB"; 
449 

450 

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

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

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

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

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

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

457 
\ : set evs; \ 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

458 
\ nb ~: analz (sees Spy evs); evs : yahalom ] \ 
2133  459 
\ ==> 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

460 
by (not_lost_tac "B'" 1); 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

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

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

463 
addDs [unique_NB]) 1); 
2133  464 
qed "Says_unique_NB"; 
465 

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

468 

2133  469 
goal thy 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

470 
"!!evs. [ B ~: lost; evs : yahalom ] \ 
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

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

472 
\ Crypt (shrK B') {Agent A', Nonce NB, nb'} \ 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

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

474 
\ > Crypt (shrK B) {Agent A, Nonce NA, Nonce NB} \ 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

475 
\ ~: parts(sees Spy evs)"; 
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

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

477 
by (Fake_parts_insert_tac 1); 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

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

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

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

481 
bind_thm ("no_nonce_YM1_YM2", result() RS mp RSN (2,rev_mp) RSN (2,rev_notE)); 
2133  482 

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

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

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

486 
\ {Crypt (shrK A) {Agent B, k, na, nb}, X} : set evs; \ 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

487 
\ evs : yahalom ] \ 
2133  488 
\ ==> EX B'. Says B' Server \ 
2284
80ebd1a213fd
Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents:
2269
diff
changeset

489 
\ { Agent B, Crypt (shrK B) {Agent A, na, nb} } \ 
3465  490 
\ : set evs"; 
2133  491 
by (etac rev_mp 1); 
492 
by (etac yahalom.induct 1); 

493 
by (ALLGOALS Asm_simp_tac); 

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

494 
by (ALLGOALS Blast_tac); 
2133  495 
qed "Says_Server_imp_YM2"; 
496 

497 

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

498 
(*A vital theorem for B, that nonce NB remains secure from the Spy.*) 
2133  499 
goal thy 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

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

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

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

504 
\ (ALL k. Says A Spy {Nonce NA, Nonce NB, k} ~: set evs) > \ 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

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

507 
by analz_sees_tac; 
2133  508 
by (ALLGOALS 
509 
(asm_simp_tac 

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

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

511 
analz_insert_freshK] @ pushes) 
2133  512 
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

513 
(*Prove YM3 by showing that no NB can also be an NA*) 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

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

515 
addSEs [MPair_parts] 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

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

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

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

519 
by (blast_tac (!claset addSEs partsEs 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

520 
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

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

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

523 
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

524 
addSEs sees_Spy_partsEs) 2); 
2377  525 
(*Fake*) 
526 
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

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

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

529 
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

530 
by (not_lost_tac "Aa" 1); 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

531 
by (dtac (Says_imp_sees_Spy RS parts.Inj RS parts.Fst RS A_trusts_YM3) 1); 
2133  532 
by (forward_tac [Says_Server_message_form] 3); 
533 
by (forward_tac [Says_Server_imp_YM2] 4); 

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

534 
by (REPEAT_FIRST (eresolve_tac [asm_rl, bexE, exE, disjE])); 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

535 
(* use Says_unique_NB to identify message components: Aa=A, Ba=B, NAa=NA *) 
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

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

537 
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

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

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

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

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

544 
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

545 
(*If NB=NBa then all other components of the Oops message agree*) 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

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

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

548 
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

549 
by (blast_tac (!claset addSEs [MPair_parts] 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

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

551 
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

552 
bind_thm ("Spy_not_see_NB", result() RSN(2,rev_mp) RSN(2,rev_mp)); 
2133  553 

2001  554 

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

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

556 
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

557 
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

558 
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

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

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

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

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

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

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

566 
\ ALL k. Says A Spy {Nonce NA, Nonce NB, k} ~: set evs; \ 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

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

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

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

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

571 
\ Crypt (shrK B) {Agent A, Key K}} \ 
3465  572 
\ : set evs"; 
2133  573 
by (forward_tac [Spy_not_see_NB] 1 THEN REPEAT (assume_tac 1)); 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

574 
by (etac (Says_imp_sees_Spy RS parts.Inj RS MPair_parts) 1 THEN 
2133  575 
dtac B_trusts_YM4_shrK 1); 
2170  576 
by (dtac B_trusts_YM4_newK 3); 
2110  577 
by (REPEAT_FIRST (eresolve_tac [asm_rl, exE])); 
2133  578 
by (forward_tac [Says_Server_imp_YM2] 1 THEN assume_tac 1); 
2170  579 
by (dtac unique_session_keys 1 THEN REPEAT (assume_tac 1)); 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

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

582 

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

583 

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

584 

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

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

586 

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

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

588 
goal thy 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

589 
"!!evs. evs : yahalom \ 
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

590 
\ ==> Crypt (shrK B) {Agent A, Nonce NA, nb} \ 
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

591 
\ : parts (sees Spy evs) > \ 
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

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

593 
\ Says B Server {Agent B, Crypt (shrK B) {Agent A, Nonce NA, nb}} \ 
3465  594 
\ : set evs"; 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

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

596 
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

597 
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

598 

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

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

600 
goal thy 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

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

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

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

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

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

607 
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

608 
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

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

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

611 
(*YM3*) 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

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

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

614 
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

615 

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

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

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

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

619 
\ : set evs; \ 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

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

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

623 
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

624 
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

625 
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

626 

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

627 

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

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

629 

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

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

631 
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

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

633 
goal thy 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

634 
"!!evs. evs : yahalom \ 
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

635 
\ ==> Key K ~: analz (sees Spy evs) > \ 
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

636 
\ Crypt K (Nonce NB) : parts (sees Spy evs) > \ 
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

637 
\ Crypt (shrK B) {Agent A, Key K} \ 
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

638 
\ : parts (sees Spy evs) > \ 
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

639 
\ B ~: lost > \ 
3465  640 
\ (EX X. Says A B {X, Crypt K (Nonce NB)} : set evs)"; 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

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

642 
(*Fake*) 
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 
(*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

645 
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

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

647 
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

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

649 
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

650 
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

651 
addSDs [A_trusts_YM3, B_trusts_YM4_shrK] 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

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

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

654 
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

655 

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

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

657 
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

658 
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

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

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

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

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

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

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

665 
\ (ALL NA k. Says A Spy {Nonce NA, Nonce NB, k} ~: set evs); \ 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

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

668 
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

669 
by (REPEAT_FIRST (eresolve_tac [asm_rl, spec])); 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

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

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

672 
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

673 
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

674 
by (blast_tac (!claset addSEs [MPair_parts] 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

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

676 
qed_spec_mp "YM4_imp_A_Said_YM3"; 