author  paulson 
Mon, 29 Sep 1997 11:47:01 +0200  
changeset 3730  6933d20f335f 
parent 3683  aafe719dff14 
child 3919  c036caebfc75 
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 

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

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

37 
by (Auto_tac()); 
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)"; 
48 
by (blast_tac (!claset addSDs [Says_imp_spies RS analz.Inj]) 1); 

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)"; 
3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

57 
by (blast_tac (!claset addSEs partsEs 
3683  58 
addSDs [Says_imp_spies RS parts.Inj]) 1); 
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)"; 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

91 
by (auto_tac(!claset addDs [impOfSubs analz_subset_parts], !simpset)); 
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 

3683  95 
goal thy "!!A. [ Key (shrK A) : parts (spies evs); \ 
96 
\ evs : yahalom ] ==> A:bad"; 

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); 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

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

99 

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

100 
bind_thm ("Spy_analz_shrK_D", analz_subset_parts RS subsetD RS Spy_see_shrK_D); 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

101 
AddSDs [Spy_see_shrK_D, Spy_analz_shrK_D]; 
2111
81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

102 

81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
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 ==> \ 
3683  106 
\ 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

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

108 
(*YM4: Key K is not fresh!*) 
3683  109 
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

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

111 
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

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

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

114 
(!claset addIs [impOfSubs analz_subset_parts] 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
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:
2451
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:
2451
diff
changeset

117 
addss (!simpset)) 1); 
2160  118 
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

119 

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

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

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

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

123 

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

124 
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

125 

2155  126 
(*Describes the form of K when the Server sends this message. Useful for 
127 
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

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

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

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

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

132 
\ ==> K ~: range shrK & A ~= B"; 
2155  133 
by (etac rev_mp 1); 
134 
by (etac yahalom.induct 1); 

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

135 
by (ALLGOALS Asm_simp_tac); 
2155  136 
qed "Says_Server_message_form"; 
2111
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 

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

139 
(*For proofs involving analz.*) 
3683  140 
val analz_spies_tac = 
141 
dtac YM4_analz_spies 6 THEN 

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

142 
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

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

144 
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

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

149 

3683  150 
Key K : analz (insert (Key KAB) (spies evs)) ==> 
151 
Key K : analz (spies evs) 

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

152 

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

153 
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

154 

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

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

156 

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

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

158 

81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
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 ==> \ 
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

161 
\ ALL K KK. KK <= Compl (range shrK) > \ 
3683  162 
\ (Key K : analz (Key``KK Un (spies evs))) = \ 
163 
\ (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

164 
by (etac yahalom.induct 1); 
3683  165 
by analz_spies_tac; 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
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:
2451
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:
2451
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:
3432
diff
changeset

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

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

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

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

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

174 

81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
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 ] ==> \ 
3683  177 
\ Key K : analz (insert (Key KAB) (spies evs)) = \ 
178 
\ (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

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

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

181 

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

182 

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

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

184 

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

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 ==> \ 
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

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

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

189 
\ {nb, Crypt (shrK A) {Agent B, Key K, na}, X} \ 
3465  190 
\ : 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

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

192 
by (ALLGOALS (asm_simp_tac (!simpset addsimps [all_conj_distrib]))); 
3730  193 
by (Clarify_tac 1); 
2111
81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

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

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

196 
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

197 
(*...we assume X is a recent message and handle this case by contradiction*) 
3683  198 
by (blast_tac (!claset addSEs spies_partsEs 
3519
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

199 
delrules [conjI] (*prevent splitup into 4 subgoals*) 
ab0a9fbed4c0
Changing "lost" from a parameter of protocol definitions to a constant.
paulson
parents:
3516
diff
changeset

200 
addss (!simpset addsimps [parts_insertI])) 1); 
2111
81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

201 
val lemma = result(); 
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 
goal thy 
81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

204 
"!!evs. [ Says Server A \ 
3683  205 
\ {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

206 
\ Says Server A' \ 
3683  207 
\ {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

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

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

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

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

212 

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

213 

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

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

215 

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

216 
goal thy 
3683  217 
"!!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

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

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

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

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

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

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

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

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

228 
(asm_simp_tac 
3674
65ec38fbb265
Deleted the redundant simprule not_parts_not_analz
paulson
parents:
3519
diff
changeset

229 
(!simpset addsimps [analz_insert_eq, analz_insert_freshK] 
2111
81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

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

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

232 
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

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

234 
by (blast_tac (!claset delrules [impCE] 
3683  235 
addSEs spies_partsEs 
3432  236 
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

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

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

239 
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

240 

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

241 

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

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

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

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

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

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

248 
\ Says A Spy {na, nb, Key K} ~: set evs; \ 
3683  249 
\ A ~: bad; B ~: bad; evs : yahalom ] \ 
250 
\ ==> Key K ~: analz (spies evs)"; 

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

251 
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

252 
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

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

254 

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

255 

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

256 
(** Security Guarantee for A upon receiving YM3 **) 
2155  257 

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

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

261 
"!!evs. [ Crypt (shrK A) {Agent B, Key K, na} \ 
3683  262 
\ : parts (spies evs); \ 
263 
\ A ~: bad; evs : yahalom ] \ 

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

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

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

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

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

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

271 
by (Blast_tac 1); 
2323  272 
qed "A_trusts_YM3"; 
2155  273 

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

274 

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

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

276 

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

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

278 
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

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

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

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

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

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

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

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

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

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

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

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

293 

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

294 

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

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

296 
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

297 

2155  298 
(*What can B deduce from receipt of YM4? Stronger and simpler than Yahalom 
299 
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

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

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

302 
\ : set evs; \ 
3683  303 
\ 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

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

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

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

307 
\ Crypt (shrK B) {Nonce NB, Key K, Agent A}} \ 
3465  308 
\ : set evs"; 
3683  309 
by (etac (Says_imp_spies RS parts.Inj RS MPair_parts) 1); 
3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

310 
by (blast_tac (!claset addSDs [B_trusts_YM4_shrK]) 1); 
2323  311 
qed "B_trusts_YM4"; 
3432  312 

313 

314 

315 
(*** Authenticating B to A ***) 

316 

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

318 
goal thy 

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

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

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

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

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

325 
by (parts_induct_tac 1); 
3432  326 
by (Fake_parts_insert_tac 1); 
327 
(*YM2*) 

328 
by (Blast_tac 1); 

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

330 

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

332 
goal thy 

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

333 
"!!evs. evs : yahalom \ 
3432  334 
\ ==> 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

335 
\ : set evs > \ 
3683  336 
\ B ~: bad > \ 
3432  337 
\ (EX nb'. Says B Server {Agent B, nb', \ 
338 
\ Crypt (shrK B) {Agent A, Nonce NA}} \ 

3465  339 
\ : set evs)"; 
3432  340 
by (etac yahalom.induct 1); 
341 
by (ALLGOALS Asm_simp_tac); 

342 
(*YM3*) 

343 
by (blast_tac (!claset addSDs [B_Said_YM2] 

344 
addSEs [MPair_parts] 

3683  345 
addDs [Says_imp_spies RS parts.Inj]) 3); 
3432  346 
(*Fake, YM2*) 
347 
by (ALLGOALS Blast_tac); 

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

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

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

351 
goal thy 

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

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

353 
\ : set evs; \ 
3683  354 
\ 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

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

356 
\ {Agent B, nb', Crypt (shrK B) {Agent A, Nonce NA}} \ 
3465  357 
\ : set evs"; 
3450
cd73bc206d87
Proof tidying and variable renaming (NA>na, NB>nb when of type msg)
paulson
parents:
3432
diff
changeset

358 
by (blast_tac (!claset addSDs [A_trusts_YM3, lemma] 
3683  359 
addEs spies_partsEs) 1); 
3432  360 
qed "YM3_auth_B_to_A"; 
361 

362 

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

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

364 

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

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

368 
goal thy 

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

369 
"!!evs. evs : yahalom \ 
3683  370 
\ ==> Key K ~: analz (spies evs) > \ 
371 
\ 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

372 
\ Crypt (shrK B) {Nonce NB, Key K, Agent A} \ 
3683  373 
\ : parts (spies evs) > \ 
374 
\ B ~: bad > \ 

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

376 
by (parts_induct_tac 1); 
3432  377 
(*Fake*) 
378 
by (Fake_parts_insert_tac 1); 

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

380 
by (fast_tac (!claset addSDs [Crypt_imp_invKey_keysFor] addss (!simpset)) 1); 

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

381 
(*YM4: was Crypt K (Nonce NB) the very last message? If not, use ind. hyp.*) 
cd73bc206d87
Proof tidying and variable renaming (NA>na, NB>nb when of type msg)
paulson
parents:
3432
diff
changeset

382 
by (asm_simp_tac (!simpset addsimps [ex_disj_distrib]) 1); 
cd73bc206d87
Proof tidying and variable renaming (NA>na, NB>nb when of type msg)
paulson
parents:
3432
diff
changeset

383 
(*yes: apply unicity of session keys*) 
3683  384 
by (not_bad_tac "Aa" 1); 
3432  385 
by (blast_tac (!claset addSEs [MPair_parts] 
386 
addSDs [A_trusts_YM3, B_trusts_YM4_shrK] 

3683  387 
addDs [Says_imp_spies RS parts.Inj, 
3432  388 
unique_session_keys]) 1); 
3450
cd73bc206d87
Proof tidying and variable renaming (NA>na, NB>nb when of type msg)
paulson
parents:
3432
diff
changeset

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

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

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

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

396 
\ Crypt K (Nonce NB)} : set evs; \ 
3465  397 
\ (ALL NA. Says A Spy {Nonce NA, Nonce NB, Key K} ~: set evs); \ 
3683  398 
\ A ~: bad; B ~: bad; evs : yahalom ] \ 
3465  399 
\ ==> EX X. Says A B {X, Crypt K (Nonce NB)} : set evs"; 
3683  400 
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

401 
by (dtac B_trusts_YM4_shrK 1); 
3432  402 
by (safe_tac (!claset)); 
3450
cd73bc206d87
Proof tidying and variable renaming (NA>na, NB>nb when of type msg)
paulson
parents:
3432
diff
changeset

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

404 
by (rtac Spy_not_see_encrypted_key 2); 
3432  405 
by (REPEAT_FIRST assume_tac); 
406 
by (ALLGOALS (blast_tac (!claset addSEs [MPair_parts] 

3683  407 
addDs [Says_imp_spies RS parts.Inj]))); 
3432  408 
qed_spec_mp "YM4_imp_A_Said_YM3"; 