author  paulson 
Thu, 08 Jan 1998 18:10:34 +0100  
changeset 4537  4e835bd9fada 
parent 4509  828148415197 
child 4598  649bf14debe7 
permissions  rwrr 
2111
81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

1 
(* Title: HOL/Auth/Yahalom2 
81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

2 
ID: $Id$ 
81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 
81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

4 
Copyright 1996 University of Cambridge 
81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

5 

81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

6 
Inductive relation "yahalom" for the Yahalom protocol, Variant 2. 
81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

7 

81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

8 
This version trades encryption of NB for additional explicitness in YM3. 
81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

9 

81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

10 
From page 259 of 
81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

11 
Burrows, Abadi and Needham. A Logic of Authentication. 
81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

12 
Proc. Royal Soc. 426 (1989) 
81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

13 
*) 
81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

14 

81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

15 
open Yahalom2; 
81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

16 

4449  17 
set proof_timing; 
2111
81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

18 
HOL_quantifiers := false; 
81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

19 

2323  20 
(*A "possibility property": there are traces that reach the end*) 
2111
81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

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

22 
"!!A B. [ A ~= B; A ~= Server; B ~= Server ] \ 
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"; 
2111
81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

25 
by (REPEAT (resolve_tac [exI,bexI] 1)); 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
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:
2451
diff
changeset

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

28 
by possibility_tac; 
2111
81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

29 
result(); 
81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

30 

81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

31 

81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

32 
(**** Inductive proofs about yahalom ****) 
81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

33 

81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
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"; 
2111
81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

36 
by (etac yahalom.induct 1); 
4477
b3e5857d8d99
New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
paulson
parents:
4471
diff
changeset

37 
by Auto_tac; 
2111
81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

38 
qed_spec_mp "not_Says_to_self"; 
81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

39 
Addsimps [not_Says_to_self]; 
81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

40 
AddSEs [not_Says_to_self RSN (2, rev_notE)]; 
81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

41 

81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

42 

81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

43 
(** For reasoning about the encrypted portion of messages **) 
81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

44 

81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

45 
(*Lets us treat YM4 using a similar argument as for the Fake case.*) 
3465  46 
goal thy "!!evs. Says S A {NB, Crypt (shrK A) Y, X} : set evs ==> \ 
3683  47 
\ X : analz (spies evs)"; 
4091  48 
by (blast_tac (claset() addSDs [Says_imp_spies RS analz.Inj]) 1); 
3683  49 
qed "YM4_analz_spies"; 
2111
81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

50 

3683  51 
bind_thm ("YM4_parts_spies", 
52 
YM4_analz_spies RS (impOfSubs analz_subset_parts)); 

2111
81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

53 

2155  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 {NB, Crypt (shrK A) {B,K,NA}, X} : set evs ==> \ 
3683  56 
\ K : parts (spies evs)"; 
4091  57 
by (blast_tac (claset() addSEs partsEs 
4238
679a233fb206
Crypt_imp_keysFor: version of Crypt_imp_invKey_keysFor for shared keys
paulson
parents:
4199
diff
changeset

58 
addSDs [Says_imp_spies RS parts.Inj]) 1); 
3683  59 
qed "YM4_Key_parts_spies"; 
2111
81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

60 

3683  61 
(*For proving the easier theorems about X ~: parts (spies evs).*) 
62 
fun parts_spies_tac i = 

63 
forward_tac [YM4_Key_parts_spies] (i+6) THEN 

64 
forward_tac [YM4_parts_spies] (i+5) THEN 

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

65 
prove_simple_subgoals_tac i; 
2111
81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
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 
3683  68 
X ~: analz (spies evs) > ... then it shortens the proof by discarding 
69 
needless information about analz (insert X (spies evs)) *) 

3519
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) 
3683  74 
THEN parts_spies_tac i; 
3432  75 

2111
81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

76 

3683  77 
(** Theorems of the form X ~: parts (spies evs) imply that NOBODY 
2111
81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

78 
sends messages containing X! **) 
81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

79 

3683  80 
(*Spy never sees another agent's shared key! (unless it's bad at start)*) 
2111
81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

81 
goal thy 
3683  82 
"!!evs. evs : yahalom ==> (Key (shrK A) : parts (spies evs)) = (A : bad)"; 
3519
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); 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

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

87 
Addsimps [Spy_see_shrK]; 
2111
81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

88 

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

89 
goal thy 
3683  90 
"!!evs. evs : yahalom ==> (Key (shrK A) : analz (spies evs)) = (A : bad)"; 
4091  91 
by (auto_tac(claset() addDs [impOfSubs analz_subset_parts], simpset())); 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

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

93 
Addsimps [Spy_analz_shrK]; 
2111
81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

94 

4471  95 
AddSDs [Spy_see_shrK RSN (2, rev_iffD1), 
96 
Spy_analz_shrK RSN (2, rev_iffD1)]; 

2111
81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

97 

81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

98 

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

100 
goal thy "!!evs. evs : yahalom ==> \ 
3683  101 
\ Key K ~: used evs > K ~: keysFor (parts (spies evs))"; 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

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

103 
(*YM4: Key K is not fresh!*) 
4091  104 
by (blast_tac (claset() addSEs spies_partsEs) 3); 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

105 
(*YM3*) 
4091  106 
by (blast_tac (claset() addss (simpset())) 2); 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

107 
(*Fake*) 
4509
828148415197
Making proofs faster, especially using keysFor_parts_insert
paulson
parents:
4477
diff
changeset

108 
by (blast_tac (claset() addSDs [keysFor_parts_insert]) 1); 
2160  109 
qed_spec_mp "new_keys_not_used"; 
2111
81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

110 

81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

111 
bind_thm ("new_keys_not_analzd", 
81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

112 
[analz_subset_parts RS keysFor_mono, 
81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

113 
new_keys_not_used] MRS contra_subsetD); 
81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

114 

81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

115 
Addsimps [new_keys_not_used, new_keys_not_analzd]; 
81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

116 

2155  117 
(*Describes the form of K when the Server sends this message. Useful for 
118 
Oops as well as main secrecy property.*) 

2111
81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

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

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

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

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

123 
\ ==> K ~: range shrK & A ~= B"; 
2155  124 
by (etac rev_mp 1); 
125 
by (etac yahalom.induct 1); 

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

126 
by (ALLGOALS Asm_simp_tac); 
2155  127 
qed "Says_Server_message_form"; 
2111
81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

128 

81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

129 

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

130 
(*For proofs involving analz.*) 
3683  131 
val analz_spies_tac = 
132 
dtac YM4_analz_spies 6 THEN 

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

133 
forward_tac [Says_Server_message_form] 7 THEN 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

134 
assume_tac 7 THEN 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

135 
REPEAT ((etac conjE ORELSE' hyp_subst_tac) 7); 
2111
81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

136 

81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

137 

81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

138 
(**** 
81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

139 
The following is to prove theorems of the form 
81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

140 

3683  141 
Key K : analz (insert (Key KAB) (spies evs)) ==> 
142 
Key K : analz (spies evs) 

2111
81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

143 

81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

144 
A more general formula must be proved inductively. 
81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

145 

81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

146 
****) 
81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

147 

81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

148 
(** Session keys are not used to encrypt other session keys **) 
81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

149 

81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

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

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

152 
\ ALL K KK. KK <= Compl (range shrK) > \ 
3683  153 
\ (Key K : analz (Key``KK Un (spies evs))) = \ 
154 
\ (K : KK  Key K : analz (spies evs))"; 

2111
81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

155 
by (etac yahalom.induct 1); 
3683  156 
by analz_spies_tac; 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

157 
by (REPEAT_FIRST (resolve_tac [allI, impI])); 
3961  158 
by (REPEAT_FIRST (rtac analz_image_freshK_lemma)); 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

159 
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:
3432
diff
changeset

160 
(*Fake*) 
4422
21238c9d363e
Simplified proofs using rewrites for f``A where f is injective
paulson
parents:
4238
diff
changeset

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

162 
qed_spec_mp "analz_image_freshK"; 
2111
81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

163 

81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

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

165 
"!!evs. [ evs : yahalom; KAB ~: range shrK ] ==> \ 
3683  166 
\ Key K : analz (insert (Key KAB) (spies evs)) = \ 
167 
\ (K = KAB  Key K : analz (spies evs))"; 

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

168 
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:
2451
diff
changeset

169 
qed "analz_insert_freshK"; 
2111
81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

170 

81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

171 

81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

172 
(*** The Key K uniquely identifies the Server's message. **) 
81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

173 

81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

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

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

176 
\ EX A' B' na' nb' X'. ALL A B na nb X. \ 
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

177 
\ Says Server A \ 
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

178 
\ {nb, Crypt (shrK A) {Agent B, Key K, na}, X} \ 
3465  179 
\ : set evs > A=A' & B=B' & na=na' & nb=nb' & X=X'"; 
2111
81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

180 
by (etac yahalom.induct 1); 
4091  181 
by (ALLGOALS (asm_simp_tac (simpset() addsimps [all_conj_distrib]))); 
3730  182 
by (Clarify_tac 1); 
2111
81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

183 
(*Remaining case: YM3*) 
81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

184 
by (expand_case_tac "K = ?y" 1); 
81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

185 
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:
2451
diff
changeset

186 
(*...we assume X is a recent message and handle this case by contradiction*) 
4091  187 
by (blast_tac (claset() addSEs spies_partsEs 
4199  188 
delrules [conjI] (*prevent splitup into 4 subgoals*) 
189 
addss (simpset() addsimps [parts_insertI])) 1); 

2111
81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

190 
val lemma = result(); 
81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

191 

81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

192 
goal thy 
81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

193 
"!!evs. [ Says Server A \ 
3683  194 
\ {nb, Crypt (shrK A) {Agent B, Key K, na}, X} : set evs; \ 
2111
81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

195 
\ Says Server A' \ 
3683  196 
\ {nb', Crypt (shrK A') {Agent B', Key K, na'}, X'} : set evs; \ 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

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

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

199 
by (prove_unique_tac lemma 1); 
2111
81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

200 
qed "unique_session_keys"; 
81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

201 

81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

202 

81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

203 
(** Crucial secrecy property: Spy does not see the keys sent in msg YM3 **) 
81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

204 

81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

205 
goal thy 
3683  206 
"!!evs. [ A ~: bad; B ~: bad; A ~= B; \ 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

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

208 
\ ==> Says Server A \ 
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

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

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

211 
\ : set evs > \ 
4537
4e835bd9fada
Expressed most Oops rules using Notes instead of Says, and other tidying
paulson
parents:
4509
diff
changeset

212 
\ Notes Spy {na, nb, Key K} ~: set evs > \ 
3683  213 
\ Key K ~: analz (spies evs)"; 
2111
81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

214 
by (etac yahalom.induct 1); 
3683  215 
by analz_spies_tac; 
2111
81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

216 
by (ALLGOALS 
81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

217 
(asm_simp_tac 
4091  218 
(simpset() addsimps expand_ifs 
4199  219 
addsimps [analz_insert_eq, analz_insert_freshK] 
220 
addsplits [expand_if]))); 

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

221 
(*Oops*) 
4091  222 
by (blast_tac (claset() addDs [unique_session_keys]) 3); 
2111
81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

223 
(*YM3*) 
4091  224 
by (blast_tac (claset() delrules [impCE] 
4199  225 
addSEs spies_partsEs 
226 
addIs [impOfSubs analz_subset_parts]) 2); 

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

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

228 
by (spy_analz_tac 1); 
2111
81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

229 
val lemma = result() RS mp RS mp RSN(2,rev_notE); 
81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

230 

81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

231 

3432  232 
(*Final version*) 
2111
81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

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

234 
"!!evs. [ Says Server A \ 
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

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

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

237 
\ : set evs; \ 
4537
4e835bd9fada
Expressed most Oops rules using Notes instead of Says, and other tidying
paulson
parents:
4509
diff
changeset

238 
\ Notes Spy {na, nb, Key K} ~: set evs; \ 
4e835bd9fada
Expressed most Oops rules using Notes instead of Says, and other tidying
paulson
parents:
4509
diff
changeset

239 
\ A ~: bad; B ~: bad; evs : yahalom ] \ 
3683  240 
\ ==> Key K ~: analz (spies evs)"; 
2111
81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

241 
by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1); 
4091  242 
by (blast_tac (claset() addSEs [lemma]) 1); 
2111
81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

243 
qed "Spy_not_see_encrypted_key"; 
81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

244 

81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

245 

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

246 
(** Security Guarantee for A upon receiving YM3 **) 
2155  247 

3432  248 
(*If the encrypted message appears then it originated with the Server. 
249 
May now apply Spy_not_see_encrypted_key, subject to its conditions.*) 

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

251 
"!!evs. [ Crypt (shrK A) {Agent B, Key K, na} \ 
4537
4e835bd9fada
Expressed most Oops rules using Notes instead of Says, and other tidying
paulson
parents:
4509
diff
changeset

252 
\ : parts (spies evs); \ 
4e835bd9fada
Expressed most Oops rules using Notes instead of Says, and other tidying
paulson
parents:
4509
diff
changeset

253 
\ A ~: bad; evs : yahalom ] \ 
3450
cd73bc206d87
Proof tidying and variable renaming (NA>na, NB>nb when of type msg)
paulson
parents:
3432
diff
changeset

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

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

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

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

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

261 
by (Blast_tac 1); 
2323  262 
qed "A_trusts_YM3"; 
2155  263 

2111
81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

264 

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

265 
(** Security Guarantee for B upon receiving YM4 **) 
cd73bc206d87
Proof tidying and variable renaming (NA>na, NB>nb when of type msg)
paulson
parents:
3432
diff
changeset

266 

2111
81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

267 
(*B knows, by the first part of A's message, that the Server distributed 
3450
cd73bc206d87
Proof tidying and variable renaming (NA>na, NB>nb when of type msg)
paulson
parents:
3432
diff
changeset

268 
the key for A and B, and has associated it with NB. *) 
2111
81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

269 
goal thy 
3683  270 
"!!evs. [ Crypt (shrK B) {Nonce NB, Key K, Agent A} : parts (spies evs); \ 
271 
\ B ~: bad; evs : yahalom ] \ 

2111
81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

272 
\ ==> EX NA. Says Server A \ 
2155  273 
\ {Nonce NB, \ 
2284
80ebd1a213fd
Swapped arguments of Crypt (for clarity and because it is conventional)
paulson
parents:
2264
diff
changeset

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

275 
\ Crypt (shrK B) {Nonce NB, Key K, Agent A}} \ 
3465  276 
\ : set evs"; 
2111
81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

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

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

279 
by (Fake_parts_insert_tac 1); 
2111
81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

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

281 
by (Blast_tac 1); 
2111
81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

282 
qed "B_trusts_YM4_shrK"; 
81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

283 

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

284 

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

285 
(*With this protocol variant, we don't need the 2nd part of YM4 at all: 
cd73bc206d87
Proof tidying and variable renaming (NA>na, NB>nb when of type msg)
paulson
parents:
3432
diff
changeset

286 
Nonce NB is available in the first part.*) 
2111
81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

287 

2155  288 
(*What can B deduce from receipt of YM4? Stronger and simpler than Yahalom 
289 
because we do not have to show that NB is secret. *) 

2111
81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

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

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

292 
\ : set evs; \ 
3683  293 
\ A ~: bad; B ~: bad; evs : yahalom ] \ 
3450
cd73bc206d87
Proof tidying and variable renaming (NA>na, NB>nb when of type msg)
paulson
parents:
3432
diff
changeset

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

295 
\ {Nonce NB, \ 
cd73bc206d87
Proof tidying and variable renaming (NA>na, NB>nb when of type msg)
paulson
parents:
3432
diff
changeset

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

297 
\ Crypt (shrK B) {Nonce NB, Key K, Agent A}} \ 
3465  298 
\ : set evs"; 
3683  299 
by (etac (Says_imp_spies RS parts.Inj RS MPair_parts) 1); 
4091  300 
by (blast_tac (claset() addSDs [B_trusts_YM4_shrK]) 1); 
2323  301 
qed "B_trusts_YM4"; 
3432  302 

303 

304 

305 
(*** Authenticating B to A ***) 

306 

307 
(*The encryption in message YM2 tells us it cannot be faked.*) 

308 
goal thy 

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

309 
"!!evs. evs : yahalom \ 
3683  310 
\ ==> Crypt (shrK B) {Agent A, Nonce NA} : parts (spies evs) > \ 
311 
\ B ~: bad > \ 

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

312 
\ (EX NB. Says B Server {Agent B, Nonce NB, \ 
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

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

315 
by (parts_induct_tac 1); 
3432  316 
by (Fake_parts_insert_tac 1); 
317 
(*YM2*) 

318 
by (Blast_tac 1); 

319 
bind_thm ("B_Said_YM2", result() RSN (2, rev_mp) RS mp); 

320 

321 
(*If the server sends YM3 then B sent YM2, perhaps with a different NB*) 

322 
goal thy 

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

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

325 
\ : set evs > \ 
3683  326 
\ B ~: bad > \ 
3432  327 
\ (EX nb'. Says B Server {Agent B, nb', \ 
328 
\ Crypt (shrK B) {Agent A, Nonce NA}} \ 

3465  329 
\ : set evs)"; 
3432  330 
by (etac yahalom.induct 1); 
331 
by (ALLGOALS Asm_simp_tac); 

332 
(*YM3*) 

4091  333 
by (blast_tac (claset() addSDs [B_Said_YM2] 
4199  334 
addSEs [MPair_parts] 
335 
addDs [Says_imp_spies RS parts.Inj]) 3); 

3432  336 
(*Fake, YM2*) 
337 
by (ALLGOALS Blast_tac); 

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

338 
val lemma = result() RSN (2, rev_mp) RS mp > standard; 
3432  339 

340 
(*If A receives YM3 then B has used nonce NA (and therefore is alive)*) 

341 
goal thy 

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

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

343 
\ : set evs; \ 
3683  344 
\ A ~: bad; B ~: bad; evs : yahalom ] \ 
3450
cd73bc206d87
Proof tidying and variable renaming (NA>na, NB>nb when of type msg)
paulson
parents:
3432
diff
changeset

345 
\ ==> EX nb'. Says B Server \ 
cd73bc206d87
Proof tidying and variable renaming (NA>na, NB>nb when of type msg)
paulson
parents:
3432
diff
changeset

346 
\ {Agent B, nb', Crypt (shrK B) {Agent A, Nonce NA}} \ 
3465  347 
\ : set evs"; 
4091  348 
by (blast_tac (claset() addSDs [A_trusts_YM3, lemma] 
4199  349 
addEs spies_partsEs) 1); 
3432  350 
qed "YM3_auth_B_to_A"; 
351 

352 

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

353 
(*** Authenticating A to B using the certificate Crypt K (Nonce NB) ***) 
cd73bc206d87
Proof tidying and variable renaming (NA>na, NB>nb when of type msg)
paulson
parents:
3432
diff
changeset

354 

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

355 
(*Assuming the session key is secure, if both certificates are present then 
3432  356 
A has said NB. We can't be sure about the rest of A's message, but only 
357 
NB matters for freshness.*) 

358 
goal thy 

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

359 
"!!evs. evs : yahalom \ 
3683  360 
\ ==> Key K ~: analz (spies evs) > \ 
361 
\ Crypt K (Nonce NB) : parts (spies evs) > \ 

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

362 
\ Crypt (shrK B) {Nonce NB, Key K, Agent A} \ 
3683  363 
\ : parts (spies evs) > \ 
364 
\ B ~: bad > \ 

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

366 
by (parts_induct_tac 1); 
3432  367 
(*Fake*) 
368 
by (Fake_parts_insert_tac 1); 

369 
(*YM3: by new_keys_not_used we note that Crypt K (Nonce NB) could not exist*) 

4238
679a233fb206
Crypt_imp_keysFor: version of Crypt_imp_invKey_keysFor for shared keys
paulson
parents:
4199
diff
changeset

370 
by (fast_tac (claset() addSDs [Crypt_imp_keysFor] addss (simpset())) 1); 
3450
cd73bc206d87
Proof tidying and variable renaming (NA>na, NB>nb when of type msg)
paulson
parents:
3432
diff
changeset

371 
(*YM4: was Crypt K (Nonce NB) the very last message? If not, use ind. hyp.*) 
4091  372 
by (asm_simp_tac (simpset() addsimps [ex_disj_distrib]) 1); 
3450
cd73bc206d87
Proof tidying and variable renaming (NA>na, NB>nb when of type msg)
paulson
parents:
3432
diff
changeset

373 
(*yes: apply unicity of session keys*) 
3683  374 
by (not_bad_tac "Aa" 1); 
4091  375 
by (blast_tac (claset() addSEs [MPair_parts] 
4199  376 
addSDs [A_trusts_YM3, B_trusts_YM4_shrK] 
377 
addDs [Says_imp_spies RS parts.Inj, 

378 
unique_session_keys]) 1); 

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

379 
val lemma = normalize_thm [RSspec, RSmp] (result()) > standard; 
3432  380 

381 
(*If B receives YM4 then A has used nonce NB (and therefore is alive). 

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

382 
Moreover, A associates K with NB (thus is talking about the same run). 
3432  383 
Other premises guarantee secrecy of K.*) 
384 
goal thy 

385 
"!!evs. [ Says A' B {Crypt (shrK B) {Nonce NB, Key K, Agent A}, \ 

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

386 
\ Crypt K (Nonce NB)} : set evs; \ 
4537
4e835bd9fada
Expressed most Oops rules using Notes instead of Says, and other tidying
paulson
parents:
4509
diff
changeset

387 
\ (ALL NA. Notes Spy {Nonce NA, Nonce NB, Key K} ~: set evs); \ 
3683  388 
\ A ~: bad; B ~: bad; evs : yahalom ] \ 
3465  389 
\ ==> EX X. Says A B {X, Crypt K (Nonce NB)} : set evs"; 
3683  390 
by (etac (Says_imp_spies RS parts.Inj RS MPair_parts) 1); 
3450
cd73bc206d87
Proof tidying and variable renaming (NA>na, NB>nb when of type msg)
paulson
parents:
3432
diff
changeset

391 
by (dtac B_trusts_YM4_shrK 1); 
4153  392 
by Safe_tac; 
3450
cd73bc206d87
Proof tidying and variable renaming (NA>na, NB>nb when of type msg)
paulson
parents:
3432
diff
changeset

393 
by (rtac lemma 1); 
cd73bc206d87
Proof tidying and variable renaming (NA>na, NB>nb when of type msg)
paulson
parents:
3432
diff
changeset

394 
by (rtac Spy_not_see_encrypted_key 2); 
3432  395 
by (REPEAT_FIRST assume_tac); 
4091  396 
by (ALLGOALS (blast_tac (claset() addSEs [MPair_parts] 
4199  397 
addDs [Says_imp_spies RS parts.Inj]))); 
3432  398 
qed_spec_mp "YM4_imp_A_Said_YM3"; 