author  wenzelm 
Sat, 07 Apr 2012 16:41:59 +0200  
changeset 47389  e8552cba702d 
parent 46471  2289a3869c88 
child 55417  01fbfb60c33e 
permissions  rwrr 
33028  1 
(* Title: HOL/SET_Protocol/Event_SET.thy 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30549
diff
changeset

2 
Author: Giampaolo Bella 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30549
diff
changeset

3 
Author: Fabio Massacci 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30549
diff
changeset

4 
Author: Lawrence C Paulson 
14199  5 
*) 
6 

7 
header{*Theory of Events for SET*} 

8 

33028  9 
theory Event_SET 
10 
imports Message_SET 

11 
begin 

14199  12 

13 
text{*The Root Certification Authority*} 

35101  14 
abbreviation "RCA == CA 0" 
14199  15 

16 

17 
text{*Message events*} 

18 
datatype 

19 
event = Says agent agent msg 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30549
diff
changeset

20 
 Gets agent msg 
14199  21 
 Notes agent msg 
22 

23 

24 
text{*compromised agents: keys known, Notes visible*} 

25 
consts bad :: "agent set" 

26 

27 
text{*Spy has access to his own key for spoof messages, but RCA is secure*} 

28 
specification (bad) 

29 
Spy_in_bad [iff]: "Spy \<in> bad" 

30 
RCA_not_bad [iff]: "RCA \<notin> bad" 

31 
by (rule exI [of _ "{Spy}"], simp) 

32 

33 

34 
subsection{*Agents' Knowledge*} 

35 

36 
consts (*Initial states of agents  parameter of the construction*) 

37 
initState :: "agent => msg set" 

38 

39 
(* Message reception does not extend spy's knowledge because of 

40 
reception invariant enforced by Reception rule in protocol definition*) 

39758  41 
primrec knows :: "[agent, event list] => msg set" 
42 
where 

43 
knows_Nil: 

44 
"knows A [] = initState A" 

45 
 knows_Cons: 

14199  46 
"knows A (ev # evs) = 
47 
(if A = Spy then 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30549
diff
changeset

48 
(case ev of 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30549
diff
changeset

49 
Says A' B X => insert X (knows Spy evs) 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30549
diff
changeset

50 
 Gets A' X => knows Spy evs 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30549
diff
changeset

51 
 Notes A' X => 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30549
diff
changeset

52 
if A' \<in> bad then insert X (knows Spy evs) else knows Spy evs) 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30549
diff
changeset

53 
else 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30549
diff
changeset

54 
(case ev of 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30549
diff
changeset

55 
Says A' B X => 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30549
diff
changeset

56 
if A'=A then insert X (knows A evs) else knows A evs 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30549
diff
changeset

57 
 Gets A' X => 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30549
diff
changeset

58 
if A'=A then insert X (knows A evs) else knows A evs 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30549
diff
changeset

59 
 Notes A' X => 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30549
diff
changeset

60 
if A'=A then insert X (knows A evs) else knows A evs))" 
14199  61 

62 

63 
subsection{*Used Messages*} 

64 

39758  65 
primrec used :: "event list => msg set" 
66 
where 

14199  67 
(*Set of items that might be visible to somebody: 
39758  68 
complement of the set of fresh items. 
69 
As above, message reception does extend used items *) 

14199  70 
used_Nil: "used [] = (UN B. parts (initState B))" 
39758  71 
 used_Cons: "used (ev # evs) = 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30549
diff
changeset

72 
(case ev of 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30549
diff
changeset

73 
Says A B X => parts {X} Un (used evs) 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30549
diff
changeset

74 
 Gets A X => used evs 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
30549
diff
changeset

75 
 Notes A X => parts {X} Un (used evs))" 
14199  76 

77 

78 

79 
(* Inserted by default but later removed. This declaration lets the file 

80 
be reloaded. Addsimps [knows_Cons, used_Nil, *) 

81 

82 
(** Simplifying parts (insert X (knows Spy evs)) 

83 
= parts {X} Un parts (knows Spy evs)  since general case loops*) 

84 

45605  85 
lemmas parts_insert_knows_A = parts_insert [of _ "knows A evs"] for A evs 
14199  86 

87 
lemma knows_Spy_Says [simp]: 

88 
"knows Spy (Says A B X # evs) = insert X (knows Spy evs)" 

89 
by auto 

90 

91 
text{*Letting the Spy see "bad" agents' notes avoids redundant casesplits 

92 
on whether @{term "A=Spy"} and whether @{term "A\<in>bad"}*} 

93 
lemma knows_Spy_Notes [simp]: 

94 
"knows Spy (Notes A X # evs) = 

95 
(if A:bad then insert X (knows Spy evs) else knows Spy evs)" 

96 
apply auto 

97 
done 

98 

99 
lemma knows_Spy_Gets [simp]: "knows Spy (Gets A X # evs) = knows Spy evs" 

100 
by auto 

101 

102 
lemma initState_subset_knows: "initState A <= knows A evs" 

103 
apply (induct_tac "evs") 

104 
apply (auto split: event.split) 

105 
done 

106 

107 
lemma knows_Spy_subset_knows_Spy_Says: 

108 
"knows Spy evs <= knows Spy (Says A B X # evs)" 

109 
by auto 

110 

111 
lemma knows_Spy_subset_knows_Spy_Notes: 

112 
"knows Spy evs <= knows Spy (Notes A X # evs)" 

113 
by auto 

114 

115 
lemma knows_Spy_subset_knows_Spy_Gets: 

116 
"knows Spy evs <= knows Spy (Gets A X # evs)" 

117 
by auto 

118 

119 
(*Spy sees what is sent on the traffic*) 

120 
lemma Says_imp_knows_Spy [rule_format]: 

121 
"Says A B X \<in> set evs > X \<in> knows Spy evs" 

122 
apply (induct_tac "evs") 

123 
apply (auto split: event.split) 

124 
done 

125 

126 
(*Use with addSEs to derive contradictions from old Says events containing 

127 
items known to be fresh*) 

128 
lemmas knows_Spy_partsEs = 

46471  129 
Says_imp_knows_Spy [THEN parts.Inj, elim_format] 
130 
parts.Body [elim_format] 

14199  131 

132 

133 
subsection{*The Function @{term used}*} 

134 

135 
lemma parts_knows_Spy_subset_used: "parts (knows Spy evs) <= used evs" 

136 
apply (induct_tac "evs") 

137 
apply (auto simp add: parts_insert_knows_A split: event.split) 

138 
done 

139 

140 
lemmas usedI = parts_knows_Spy_subset_used [THEN subsetD, intro] 

141 

142 
lemma initState_subset_used: "parts (initState B) <= used evs" 

143 
apply (induct_tac "evs") 

144 
apply (auto split: event.split) 

145 
done 

146 

147 
lemmas initState_into_used = initState_subset_used [THEN subsetD] 

148 

149 
lemma used_Says [simp]: "used (Says A B X # evs) = parts{X} Un used evs" 

150 
by auto 

151 

152 
lemma used_Notes [simp]: "used (Notes A X # evs) = parts{X} Un used evs" 

153 
by auto 

154 

155 
lemma used_Gets [simp]: "used (Gets A X # evs) = used evs" 

156 
by auto 

157 

158 

159 
lemma Notes_imp_parts_subset_used [rule_format]: 

160 
"Notes A X \<in> set evs > parts {X} <= used evs" 

161 
apply (induct_tac "evs") 

162 
apply (induct_tac [2] "a", auto) 

163 
done 

164 

165 
text{*NOTE REMOVALlaws above are cleaner, as they don't involve "case"*} 

166 
declare knows_Cons [simp del] 

167 
used_Nil [simp del] used_Cons [simp del] 

168 

169 

170 
text{*For proving theorems of the form @{term "X \<notin> analz (knows Spy evs) > P"} 

171 
New events added by induction to "evs" are discarded. Provided 

172 
this information isn't needed, the proof will be much shorter, since 

173 
it will omit complicated reasoning about @{term analz}.*} 

174 

175 
lemmas analz_mono_contra = 

176 
knows_Spy_subset_knows_Spy_Says [THEN analz_mono, THEN contra_subsetD] 

177 
knows_Spy_subset_knows_Spy_Notes [THEN analz_mono, THEN contra_subsetD] 

178 
knows_Spy_subset_knows_Spy_Gets [THEN analz_mono, THEN contra_subsetD] 

27225  179 

45605  180 
lemmas analz_impI = impI [where P = "Y \<notin> analz (knows Spy evs)"] for Y evs 
27225  181 

14199  182 
ML 
183 
{* 

184 
val analz_mono_contra_tac = 

27225  185 
rtac @{thm analz_impI} THEN' 
186 
REPEAT1 o (dresolve_tac @{thms analz_mono_contra}) 

187 
THEN' mp_tac 

14199  188 
*} 
189 

190 
method_setup analz_mono_contra = {* 

30549  191 
Scan.succeed (K (SIMPLE_METHOD (REPEAT_FIRST analz_mono_contra_tac))) *} 
14199  192 
"for proving theorems of the form X \<notin> analz (knows Spy evs) > P" 
193 

194 
end 