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

3432  20 
(*Replacing the variable by a constant improves speed*) 
21 
val Says_imp_sees_Spy' = read_instantiate [("lost","lost")] Says_imp_sees_Spy; 

22 

23 

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

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

26 
"!!A B. [ A ~= B; A ~= Server; B ~= Server ] \ 
2111
81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

27 
\ ==> EX X NB K. EX evs: yahalom lost. \ 
3465  28 
\ 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

29 
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

30 
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

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

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

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

34 

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

35 

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

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

37 

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

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

39 
goal thy "!!evs. lost' <= lost ==> yahalom lost' <= yahalom lost"; 
81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

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

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

42 
by (REPEAT_FIRST 
3432  43 
(blast_tac (!claset addIs (impOfSubs(sees_mono RS analz_mono RS synth_mono) 
44 
:: yahalom.intrs)))); 

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

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

46 

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

47 

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

48 
(*Nobody sends themselves messages*) 
3465  49 
goal thy "!!evs. evs: yahalom lost ==> 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

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

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

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

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

54 
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

55 

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

56 

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

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

58 

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

59 
(*Lets us treat YM4 using a similar argument as for the Fake case.*) 
3465  60 
goal thy "!!evs. Says S A {NB, Crypt (shrK A) Y, X} : set evs ==> \ 
2111
81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

61 
\ X : analz (sees lost Spy evs)"; 
3432  62 
by (blast_tac (!claset addSDs [Says_imp_sees_Spy' RS analz.Inj]) 1); 
2111
81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

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

64 

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

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

66 
YM4_analz_sees_Spy RS (impOfSubs analz_subset_parts)); 
81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

67 

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

69 
goal thy "!!evs. Says S A {NB, Crypt (shrK A) {B,K,NA}, X} : set evs ==> \ 
2111
81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

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

71 
by (blast_tac (!claset addSEs partsEs 
3466
30791e5a69c4
Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents:
3465
diff
changeset

72 
addSDs [Says_imp_sees_Spy' RS parts.Inj]) 1); 
2111
81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

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

74 

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

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

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

77 
interfere with simplification.*) 
3432  78 
val parts_sees_tac = 
3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

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

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

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

82 

3432  83 
val parts_induct_tac = 
84 
etac yahalom.induct 1 THEN parts_sees_tac; 

85 

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

86 

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

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

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

89 

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

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

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

92 
"!!evs. evs : yahalom lost \ 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

93 
\ ==> (Key (shrK A) : parts (sees lost Spy evs)) = (A : lost)"; 
3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

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

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

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

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

98 
Addsimps [Spy_see_shrK]; 
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 
goal thy 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

101 
"!!evs. evs : yahalom lost \ 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

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

103 
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

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

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

106 

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

107 
goal thy "!!A. [ Key (shrK A) : parts (sees lost Spy evs); \ 
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

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

109 
by (blast_tac (!claset addDs [Spy_see_shrK]) 1); 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

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

111 

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

112 
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

113 
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

114 

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

115 

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

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

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

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

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

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

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

123 
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

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

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

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

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

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

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

131 

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

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

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

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

135 

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

136 
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

137 

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

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

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

142 
\ : set evs; \ 
2155  143 
\ evs : yahalom lost ] \ 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

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

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

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

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

151 
(*For proofs involving analz. We again instantiate the variable to "lost".*) 
3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

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

153 
dres_inst_tac [("lost","lost")] YM4_analz_sees_Spy 6 THEN 
2155  154 
forw_inst_tac [("lost","lost")] Says_Server_message_form 7 THEN 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

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

156 
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

157 

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

160 
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

161 

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

162 
Key K : analz (insert (Key KAB) (sees lost Spy evs)) ==> 
2111
81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

163 
Key K : analz (sees lost Spy evs) 
81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

164 

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

165 
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

166 

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

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

168 

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

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

170 

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

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

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

173 
\ ALL K KK. KK <= Compl (range shrK) > \ 
30791e5a69c4
Corrected indentations and margins after the renaming of "set_of_list"
paulson
parents:
3465
diff
changeset

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

175 
\ (K : KK  Key K : analz (sees lost Spy evs))"; 
2111
81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

176 
by (etac yahalom.induct 1); 
3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

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

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

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

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

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

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

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

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

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

186 

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

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

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

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

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

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

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

193 

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

194 

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

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

196 

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

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

198 
"!!evs. evs : yahalom lost ==> \ 
3450
cd73bc206d87
Proof tidying and variable renaming (NA>na, NB>nb when of type msg)
paulson
parents:
3432
diff
changeset

199 
\ EX A' B' na' nb' X'. ALL A B na nb X. \ 
2111
81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

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

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

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

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

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

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

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

208 
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

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

210 
by (blast_tac (!claset addSEs sees_Spy_partsEs 
2111
81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

211 
delrules [conjI] (*prevent splitup into 4 subgoals*) 
81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

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

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

214 

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

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

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

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

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

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

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

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

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

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

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

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

226 

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

227 

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

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

229 

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

230 
goal thy 
2155  231 
"!!evs. [ A ~: lost; B ~: lost; A ~= B; \ 
3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

232 
\ evs : yahalom lost ] \ 
2111
81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

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

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

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

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

237 
\ Says A Spy {na, nb, Key K} ~: set evs > \ 
2111
81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

238 
\ Key K ~: analz (sees lost Spy evs)"; 
81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

239 
by (etac yahalom.induct 1); 
3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

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

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

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

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

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

245 
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

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

247 
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

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

249 
by (blast_tac (!claset delrules [impCE] 
3432  250 
addSEs sees_Spy_partsEs 
251 
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

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

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

254 
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

255 

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

256 

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

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

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

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

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

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

263 
\ Says A Spy {na, nb, Key K} ~: set evs; \ 
2155  264 
\ A ~: lost; B ~: lost; evs : yahalom lost ] \ 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

265 
\ ==> Key K ~: analz (sees lost Spy evs)"; 
2111
81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

266 
by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1); 
3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

267 
by (blast_tac (!claset addSEs [lemma]) 1); 
2111
81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

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

269 

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

270 

3432  271 
(*And other agents don't see the key either.*) 
2111
81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

272 
goal thy 
2155  273 
"!!evs. [ C ~: {A,B,Server}; \ 
2111
81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

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

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

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

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

278 
\ Says A Spy {na, nb, Key K} ~: set evs; \ 
2155  279 
\ A ~: lost; B ~: lost; evs : yahalom lost ] \ 
2516
4d68fbe6378b
Now with Andy Gordon's treatment of freshness to replace newN/K
paulson
parents:
2451
diff
changeset

280 
\ ==> Key K ~: analz (sees lost C evs)"; 
2111
81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

281 
by (rtac (subset_insertI RS sees_mono RS analz_mono RS contra_subsetD) 1); 
81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

282 
by (rtac (sees_lost_agent_subset_sees_Spy RS analz_mono RS contra_subsetD) 1); 
81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

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

284 
by (REPEAT_FIRST (blast_tac (!claset addIs [yahalom_mono RS subsetD]))); 
2111
81c8d46edfa3
New version of Yahalom, as recommended on p 259 of BAN paper
paulson
parents:
diff
changeset

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

286 

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

287 

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

288 
(** Security Guarantee for A upon receiving YM3 **) 
2155  289 

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

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

293 
"!!evs. [ Crypt (shrK A) {Agent B, Key K, na} \ 
2155  294 
\ : parts (sees lost Spy evs); \ 
295 
\ A ~: lost; evs : yahalom lost ] \ 

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

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

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

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

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

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

303 
by (Blast_tac 1); 
2323  304 
qed "A_trusts_YM3"; 
2155  305 

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

306 

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

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

308 

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

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

310 
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

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

312 
"!!evs. [ Crypt (shrK B) {Nonce NB, Key K, Agent A} \ 
2155  313 
\ : parts (sees lost Spy evs); \ 
314 
\ B ~: lost; evs : yahalom lost ] \ 

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

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

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

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

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

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

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

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

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

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

326 

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

327 

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

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

329 
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

330 

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

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

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

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

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

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

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

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

340 
\ Crypt (shrK B) {Nonce NB, Key K, Agent A}} \ 
3465  341 
\ : set evs"; 
3432  342 
by (etac (Says_imp_sees_Spy' RS parts.Inj RS MPair_parts) 1); 
3121
cbb6c0c1c58a
Conversion to use blast_tac (with other improvements)
paulson
parents:
2637
diff
changeset

343 
by (blast_tac (!claset addSDs [B_trusts_YM4_shrK]) 1); 
2323  344 
qed "B_trusts_YM4"; 
3432  345 

346 

347 

348 
(*** Authenticating B to A ***) 

349 

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

351 
goal thy 

352 
"!!evs. evs : yahalom lost \ 

353 
\ ==> Crypt (shrK B) {Agent A, Nonce NA} : parts (sees lost Spy evs) > \ 

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

354 
\ B ~: lost > \ 
3432  355 
\ (EX NB. Says B Server {Agent B, Nonce NB, \ 
356 
\ Crypt (shrK B) {Agent A, Nonce NA}} \ 

3465  357 
\ : set evs)"; 
3432  358 
by parts_induct_tac; 
359 
by (Fake_parts_insert_tac 1); 

360 
(*YM2*) 

361 
by (Blast_tac 1); 

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

363 

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

365 
goal thy 

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

366 
"!!evs. evs : yahalom lost \ 
3432  367 
\ ==> 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

368 
\ : set evs > \ 
3432  369 
\ B ~: lost > \ 
370 
\ (EX nb'. Says B Server {Agent B, nb', \ 

371 
\ Crypt (shrK B) {Agent A, Nonce NA}} \ 

3465  372 
\ : set evs)"; 
3432  373 
by (etac yahalom.induct 1); 
374 
by (ALLGOALS Asm_simp_tac); 

375 
(*YM3*) 

376 
by (blast_tac (!claset addSDs [B_Said_YM2] 

377 
addSEs [MPair_parts] 

378 
addDs [Says_imp_sees_Spy' RS parts.Inj]) 3); 

379 
(*Fake, YM2*) 

380 
by (ALLGOALS Blast_tac); 

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

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

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

384 
goal thy 

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

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

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

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

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

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

391 
by (blast_tac (!claset addSDs [A_trusts_YM3, lemma] 
3432  392 
addEs sees_Spy_partsEs) 1); 
393 
qed "YM3_auth_B_to_A"; 

394 

395 

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

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

397 

3432  398 
(*Induction for theorems of the form X ~: analz (sees lost Spy evs) > ... 
399 
It simplifies the proof by discarding needless information about 

400 
analz (insert X (sees lost Spy evs)) 

401 
*) 

402 
val analz_mono_parts_induct_tac = 

403 
etac yahalom.induct 1 

404 
THEN 

405 
REPEAT_FIRST 

406 
(rtac impI THEN' 

407 
dtac (sees_subset_sees_Says RS analz_mono RS contra_subsetD) THEN' 

408 
mp_tac) 

409 
THEN parts_sees_tac; 

410 

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

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

414 
goal thy 

415 
"!!evs. evs : yahalom lost \ 

416 
\ ==> Key K ~: analz (sees lost Spy evs) > \ 

417 
\ Crypt K (Nonce NB) : parts (sees lost Spy evs) > \ 

418 
\ Crypt (shrK B) {Nonce NB, Key K, Agent A} \ 

419 
\ : parts (sees lost Spy evs) > \ 

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

420 
\ B ~: lost > \ 
3465  421 
\ (EX X. Says A B {X, Crypt K (Nonce NB)} : set evs)"; 
3432  422 
by analz_mono_parts_induct_tac; 
423 
(*Fake*) 

424 
by (Fake_parts_insert_tac 1); 

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

426 
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

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

428 
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

429 
(*yes: apply unicity of session keys*) 
cd73bc206d87
Proof tidying and variable renaming (NA>na, NB>nb when of type msg)
paulson
parents:
3432
diff
changeset

430 
by (not_lost_tac "Aa" 1); 
3432  431 
by (blast_tac (!claset addSEs [MPair_parts] 
432 
addSDs [A_trusts_YM3, B_trusts_YM4_shrK] 

433 
addDs [Says_imp_sees_Spy' RS parts.Inj, 

434 
unique_session_keys]) 1); 

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

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

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

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

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

442 
\ Crypt K (Nonce NB)} : set evs; \ 
3465  443 
\ (ALL NA. Says A Spy {Nonce NA, Nonce NB, Key K} ~: set evs); \ 
3432  444 
\ A ~: lost; B ~: lost; evs : yahalom lost ] \ 
3465  445 
\ ==> EX X. Says A B {X, Crypt K (Nonce NB)} : set evs"; 
3450
cd73bc206d87
Proof tidying and variable renaming (NA>na, NB>nb when of type msg)
paulson
parents:
3432
diff
changeset

446 
by (etac (Says_imp_sees_Spy' RS parts.Inj RS MPair_parts) 1); 
cd73bc206d87
Proof tidying and variable renaming (NA>na, NB>nb when of type msg)
paulson
parents:
3432
diff
changeset

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

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

450 
by (rtac Spy_not_see_encrypted_key 2); 
3432  451 
by (REPEAT_FIRST assume_tac); 
452 
by (ALLGOALS (blast_tac (!claset addSEs [MPair_parts] 

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

453 
addDs [Says_imp_sees_Spy' RS parts.Inj]))); 
3432  454 
qed_spec_mp "YM4_imp_A_Said_YM3"; 