Communication.thy

   1 header {* Communication layer *}
   2 theory Communication
   3 imports
   4   Main
   5   Miscellany
   6 begin
   7
   8 subsection {* Messages *}
   9 type_synonym actor = nat
  10
  11 datatype_new message
  12   = ActorName actor               -- {* specify an actor *}
  13   | Number nat                    -- {* arbitrary data, as a natural number *}
  14   | Signature actor message       -- {* an actor's signature for a message *}
  15   | Encrypted actor actor message -- {* a message encrypted for two actors *}
  16   | MessageList "message list"    -- {* a list of messages *}
  17
  18 datatype_new message_type
  19   = ActorNameType
  20   | NumberType
  21   | SignatureType
  22   | EncryptedType
  23   | MessageListType
  24
  25 fun type_of_message :: "message \<Rightarrow> message_type"
  26   where "type_of_message (ActorName _) = ActorNameType"
  27       | "type_of_message (Number _) = NumberType"
  28       | "type_of_message (Signature _ _) = SignatureType"
  29       | "type_of_message (Encrypted _ _ _) = EncryptedType"
  30       | "type_of_message (MessageList _) = MessageListType"
  31
  32 text {* What are the components of a message, from an omniscient point of view? *}
  33 inductive contains_message :: "message \<Rightarrow> message \<Rightarrow> bool"
  34   where contains_message_self: "contains_message M M"
  35       | contains_message_encrypted:
  36           "contains_message M (Encrypted _ _ m) \<Longrightarrow> contains_message M m"
  37       | contains_message_list:
  38           "m \<in> set ms \<Longrightarrow> contains_message M (MessageList ms)
  39             \<Longrightarrow> contains_message M m"
  40
  41 text {* If a particular message has been constructed, what other messages must also
  42         have been constructed? *}
  43 inductive constructed_from :: "message \<Rightarrow> message \<Rightarrow> bool" for M
  44   where constructed_from_self: "constructed_from M M"
  45       | constructed_from_signature:
  46           "constructed_from M (Signature _ m) \<Longrightarrow> constructed_from M m"
  47       | constructed_from_encrypted:
  48           "constructed_from M (Encrypted _ _ m) \<Longrightarrow> constructed_from M m"
  49       | constructed_from_list:
  50           "m \<in> set ms \<Longrightarrow> constructed_from M (MessageList ms)
  51           \<Longrightarrow> constructed_from M m"
  52
  53 lemma actor_name_constructed_from:
  54   "constructed_from (ActorName a) m \<Longrightarrow> m = ActorName a"
  55   by (induction rule: constructed_from.induct) simp_all
  56
  57 lemma number_constructed_from:
  58   "constructed_from (Number x) m \<Longrightarrow> m = Number x"
  59   by (induction rule: constructed_from.induct) simp_all
  60
  61 lemma signature_constructed_from:
  62   "constructed_from (Signature a M) m
  63   \<Longrightarrow> m = Signature a M \<or> constructed_from M m"
  64 proof (induction rule: constructed_from.induct)
  65   show "Signature a M = Signature a M \<or> constructed_from M (Signature a M)" by simp
  66   fix b m
  67   assume "Signature b m = Signature a M \<or> constructed_from M (Signature b m)"
  68   hence "constructed_from M m"
  69   proof
  70     assume "Signature b m = Signature a M"
  71     hence "m = M" by simp
  72     thus "constructed_from M m" by (simp add: constructed_from_self)
  73   next
  74     assume "constructed_from M (Signature b m)"
  75     thus "constructed_from M m" by rule
  76   qed
  77   thus "m = Signature a M \<or> constructed_from M m" ..
  78 next
  79   fix b c m
  80   assume "Encrypted b c m = Signature a M
  81           \<or> constructed_from M (Encrypted b c m)"
  82   with constructed_from_encrypted
  83     show "m = Signature a M \<or> constructed_from M m"
  84       by blast
  85 next
  86   fix m ms
  87   assume  "m \<in> set ms"
  88     and   "MessageList ms = Signature a M
  89             \<or> constructed_from M (MessageList ms)"
  90   with constructed_from_list show "m = Signature a M \<or> constructed_from M m"
  91     by blast
  92 qed
  93
  94 lemma constructed_from_transitive:
  95   assumes "constructed_from M' M"
  96   shows "constructed_from M m \<Longrightarrow> constructed_from M' m"
  97 proof (induction rule: constructed_from.induct)
  98   case constructed_from_self
  99   from assms show "constructed_from M' M" .
 100 next
 101   case (constructed_from_signature a m)
 102   from constructed_from_signature.IH show "constructed_from M' m" by rule
 103 next
 104   case (constructed_from_encrypted a b m)
 105   from constructed_from_encrypted.IH show "constructed_from M' m" by rule
 106 next
 107   case (constructed_from_list m ms)
 108   from constructed_from_list.hyps(1) and constructed_from_list.IH
 109     show "constructed_from M' m" by rule
 110 qed
 111
 112 text {* What can a particular actor learn from a particular message? *}
 113 inductive learnable :: "actor \<Rightarrow> message \<Rightarrow> message \<Rightarrow> bool" for a M
 114   where identity_learnable: "learnable a M M"
 115           -- {* the message itself *}
 116       | encrypted1_learnable: "learnable a M (Encrypted a _ m) \<Longrightarrow> learnable a M m"
 117       | encrypted2_learnable: "learnable a M (Encrypted _ a m) \<Longrightarrow> learnable a M m"
 118           -- {* the body of a learnable message encrypted for the actor *}
 119       | listed_learnable:
 120           "m \<in> set l \<Longrightarrow> learnable a M (MessageList l) \<Longrightarrow> learnable a M m"
 121           -- {* any element of a learnable list of messages *}
 122
 123 lemma learnable_implies_constructed_from:
 124   "learnable a M m \<Longrightarrow> constructed_from M m"
 125 proof (induction rule: learnable.induct)
 126   show "constructed_from M M" by rule
 127   fix b m
 128   { assume "constructed_from M (Encrypted a b m)"
 129     thus "constructed_from M m" by rule
 130   next
 131     assume "constructed_from M (Encrypted b a m)"
 132     thus "constructed_from M m" by rule
 133   }
 134 next
 135   fix m ms
 136   assume "m \<in> set ms" and "constructed_from M (MessageList ms)"
 137   thus "constructed_from M m" by rule
 138 qed
 139
 140 text {* What messages can a particular actor construct from a particular set of
 141         messages? *}
 142 inductive constructible :: "actor \<Rightarrow> message set \<Rightarrow> message \<Rightarrow> bool" for a Ms
 143   where learnable_constructible:
 144           "M \<in> Ms \<Longrightarrow> learnable a M m \<Longrightarrow> constructible a Ms m"
 145           -- {* any message learnable from any message in the set *}
 146       | actorName_constructible: "constructible a Ms (ActorName _)"
 147           -- {* any actor's name *}
 148       | number_constructible: "constructible a Ms (Number _)"
 149           -- {* any number *}
 150       | signed_constructible:
 151           "constructible a Ms m \<Longrightarrow> constructible a Ms (Signature a m)"
 152           -- {* an otherwise constructible message, signed by this actor *}
 153       | encrypted_constructible:
 154           "constructible a Ms m \<Longrightarrow> constructible a Ms (Encrypted _ _ m)"
 155           -- {* an otherwise constructible message, encrypted to any pair of actors *}
 156       | listed_constructible:
 157           "(\<forall> m \<in> set l. constructible a Ms m)
 158             \<Longrightarrow> constructible a Ms (MessageList l)"
 159           -- {* a list of otherwise constructible messages *}
 160
 161 subsubsection {* Indistinguishability of messages *}
 162 datatype_new agent = CommunicationLayer | Actor actor
 163
 164 text {* What pairs of messages should we not expect a particular agent to be able
 165         to distinguish between, given a particular set of messages to work from?
 166         This definition isn't intended to express a limit on what an attacker might
 167         be able to do; rather, it's meant to limit what we might reasonably expect
 168         an honest agent to be able to do without resorting to sophisticated
 169         cryptanalysis or anything similarly difficult. *}
 170 inductive indistinguishable :: "agent \<Rightarrow> message set \<Rightarrow> message \<Rightarrow> message \<Rightarrow> bool"
 171   where "indistinguishable CommunicationLayer _ _ _"
 172       | "indistinguishable _ _ m m"
 173       | "\<not> constructible a Ms m \<Longrightarrow> \<not> constructible a Ms m'
 174           \<Longrightarrow> indistinguishable (Actor a) Ms (Signature _ m) (Signature _ m')"
 175       | "indistinguishable A Ms m m'
 176           \<Longrightarrow> indistinguishable A Ms (Signature a m) (Signature a m')"
 177       | "A \<noteq> Actor a \<Longrightarrow> A \<noteq> Actor b \<Longrightarrow> A \<noteq> Actor c \<Longrightarrow> A \<noteq> Actor d
 178           \<Longrightarrow> indistinguishable A _ (Encrypted a b _) (Encrypted c d _)"
 179       | "indistinguishable A Ms m m'
 180           \<Longrightarrow> indistinguishable A Ms (Encrypted a b m) (Encrypted a b m')"
 181       | "indistinguishable A Ms m m'
 182           \<Longrightarrow> indistinguishable A Ms (MessageList ms) (MessageList ms')
 183           \<Longrightarrow> indistinguishable A Ms
 184                 (MessageList (m # ms))
 185                 (MessageList (m' # ms'))"
 186
 187 lemma indistinguishable_symmetric:
 188   "indistinguishable A Ms m m' \<Longrightarrow> indistinguishable A Ms m' m"
 189 proof (induction rule: indistinguishable.induct)
 190   fix Ms m m'
 191   show "indistinguishable CommunicationLayer Ms m m'" by rule
 192   fix A
 193   show "indistinguishable A Ms m m" by rule
 194   fix a b c
 195   assume "\<not> constructible a Ms m'" and "\<not> constructible a Ms m"
 196   thus "indistinguishable (Actor a) Ms (Signature c m') (Signature b m)" by rule
 197 next
 198   fix A Ms m m' a
 199   assume "indistinguishable A Ms m' m"
 200   thus "indistinguishable A Ms (Signature a m') (Signature a m)" by rule
 201 next
 202   fix A Ms m m' a b c d
 203   assume "A \<noteq> Actor c" and "A \<noteq> Actor d" and "A \<noteq> Actor a" and "A \<noteq> Actor b"
 204   thus "indistinguishable A Ms (Encrypted c d m') (Encrypted a b m)" by rule
 205 next
 206   fix A Ms m m' a b
 207   assume "indistinguishable A Ms m' m"
 208   thus "indistinguishable A Ms (Encrypted a b m') (Encrypted a b m)" by rule
 209 next
 210   fix A Ms m m' ms ms'
 211   assume  "indistinguishable A Ms m' m"
 212     and   "indistinguishable A Ms (MessageList ms') (MessageList ms)"
 213   thus "indistinguishable A Ms (MessageList (m' # ms')) (MessageList (m # ms))"
 214     by rule
 215 qed
 216
 217 definition indistinguishability_map ::
 218   "agent \<Rightarrow> message set \<Rightarrow> (message \<Rightarrow> message) \<Rightarrow> bool" where
 219     "indistinguishability_map A Ms f
 220       \<longleftrightarrow> bij f
 221         \<and> (\<forall> m. indistinguishable A Ms m (f m)
 222               \<and> (\<forall> a b. (A = Actor a \<and> constructible a Ms m
 223                           \<longrightarrow> f (Signature b m) = Signature b (f m)
 224                         )
 225                       \<and> (A = Actor a \<or> A = Actor b
 226                           \<longrightarrow> f (Encrypted a b m) = Encrypted a b (f m)
 227                         )
 228                 )
 229           )
 230         \<and> (A \<noteq> CommunicationLayer
 231             \<longrightarrow> (\<forall> ms. f (MessageList ms) = MessageList (map f ms))
 232           )"
 233
 234 lemma learnable_indistinguishability_map:
 235   assumes im: "indistinguishability_map (Actor a) Ms f"
 236   shows "learnable a M m \<Longrightarrow> learnable a (f M) (f m)"
 237 proof (induction rule: learnable.induct)
 238   show "learnable a (f M) (f M)" by rule
 239   fix b m
 240   assume "learnable a (f M) (f (Encrypted a b m))"
 241   moreover
 242     from im have "f (Encrypted a b m) = Encrypted a b (f m)"
 243       by (unfold indistinguishability_map_def) simp
 244   ultimately show "learnable a (f M) (f m)" by (metis encrypted1_learnable)
 245 next
 246   fix b m
 247   assume "learnable a (f M) (f (Encrypted b a m))"
 248   moreover
 249     from im have "f (Encrypted b a m) = Encrypted b a (f m)"
 250       by (unfold indistinguishability_map_def) simp
 251   ultimately show "learnable a (f M) (f m)" by (metis encrypted2_learnable)
 252 next
 253   fix m ms
 254   assume  minms: "m \<in> set ms"
 255     and   learnablefms: "learnable a (f M) (f (MessageList ms))"
 256   from minms have fminfms: "f m \<in> set (map f ms)" by simp
 257   from im have "f (MessageList ms) = MessageList (map f ms)"
 258     by (unfold indistinguishability_map_def) simp
 259   with fminfms and learnablefms show "learnable a (f M) (f m)"
 260     by (metis listed_learnable)
 261 qed
 262
 263 lemma indistinguishable_message_type:
 264   "indistinguishable (Actor a) Ms m m' \<Longrightarrow> type_of_message m = type_of_message m'"
 265 proof (induction rule: indistinguishable.cases)
 266   assume "Actor a = CommunicationLayer"
 267   thus "type_of_message m = type_of_message m'" ..
 268 next
 269   fix n
 270   assume "m = n" and "m' = n"
 271   thus "type_of_message m = type_of_message m'" by simp
 272 next
 273   fix b c n n'
 274   assume "m = Signature b n" and "m' = Signature c n'"
 275   thus "type_of_message m = type_of_message m'" by simp
 276   thus "type_of_message m = type_of_message m'" .
 277 next
 278   fix b c d e n n'
 279   assume "m = Encrypted b c n" and "m' = Encrypted d e n'"
 280   thus "type_of_message m = type_of_message m'" by simp
 281   thus "type_of_message m = type_of_message m'" .
 282 next
 283   fix n ns n' ns'
 284   assume "m = MessageList (n # ns)" and "m' = MessageList (n' # ns')"
 285   thus "type_of_message m = type_of_message m'" by simp
 286 qed
 287
 288 lemma learnable_inverse_indistinguishability_map:
 289   assumes im: "indistinguishability_map (Actor a) Ms f"
 290   shows "learnable a M m \<Longrightarrow> learnable a (inv f M) (inv f m)"
 291 proof (induction rule: learnable.induct)
 292   from im have bij: "bij f" unfolding indistinguishability_map_def ..
 293   { show "learnable a (inv f M) (inv f M)" by rule
 294     fix b m
 295     assume "learnable a (inv f M) (inv f (Encrypted a b m))"
 296     moreover
 297       { from im have "f (Encrypted a b (inv f m)) = Encrypted a b (f (inv f m))"
 298           by (unfold indistinguishability_map_def) simp
 299         also from bij have "\<dots> = Encrypted a b m" by simp
 300         finally have "inv f (Encrypted a b m) = Encrypted a b (inv f m)"
 301           by (simp add: bij)
 302       }
 303     ultimately have "learnable a (inv f M) (Encrypted a b (inv f m))" by simp
 304     thus "learnable a (inv f M) (inv f m)" by rule
 305   next
 306     fix b m
 307     assume "learnable a (inv f M) (inv f (Encrypted b a m))"
 308     moreover
 309       { from im have "f (Encrypted b a (inv f m)) = Encrypted b a (f (inv f m))"
 310           by (unfold indistinguishability_map_def) simp
 311         also from bij have "\<dots> = Encrypted b a m" by simp
 312         finally have "inv f (Encrypted b a m) = Encrypted b a (inv f m)"
 313           by (simp add: bij)
 314       }
 315     ultimately have "learnable a (inv f M) (Encrypted b a (inv f m))" by simp
 316     thus "learnable a (inv f M) (inv f m)" by rule
 317   next
 318     fix m ms
 319     assume  minms: "m \<in> set ms"
 320       and   learnableinvfms: "learnable a (inv f M) (inv f (MessageList ms))"
 321     from minms have invfmininvfms: "inv f m \<in> set (map (inv f) ms)" by simp
 322     from im have
 323         "f (MessageList (map (inv f) ms)) = MessageList (map f (map (inv f) ms))"
 324       by (unfold indistinguishability_map_def) simp
 325     also from bij have "\<dots> = MessageList ms"
 326       by (subst bij_map_f_map_inv_f) simp_all
 327     finally have "inv f (MessageList ms) = MessageList (map (inv f) ms)"
 328       by (simp add: bij)
 329     with invfmininvfms and learnableinvfms show "learnable a (inv f M) (inv f m)"
 330       by (metis listed_learnable)
 331   }
 332 qed
 333
 334 type_synonym encrypted_message_data = "actor \<times> actor \<times> message"
 335 type_synonym
 336   encrypted_message_map = "encrypted_message_data \<Rightarrow> encrypted_message_data"
 337
 338 subsection {* Events *}
 339 type_synonym payment = nat
 340
 341 datatype_new event
 342   = Construct actor message   -- {* an actor constructs a message *}
 343   | Send actor actor message  -- {* send a message from one actor to another *}
 344   | Receive actor message     -- {* an actor receives a message *}
 345   | Pay
 346       actor         -- {* payer *}
 347       actor         -- {* payee *}
 348       payment       -- {* specifies amount and manner of payment *}
 349       nat           -- {* payment id, intended to be unique to payer/payee pair*}
 350
 351 text {* Given a set of past events, which messages has a particular actor received? *}
 352 definition messages_received :: "actor \<Rightarrow> event set \<Rightarrow> message set"
 353   where "messages_received a es = {m. Receive a m \<in> es}"
 354
 355 text {* What can a particular agent do, given a set of past events and a set of
 356         concurrent events? *}
 357 inductive doable :: "agent \<Rightarrow> event set \<Rightarrow> event set \<Rightarrow> event \<Rightarrow> bool"
 358   where communicationLayer_transmit_doable:
 359           "(Send _ _ m) \<in> es \<Longrightarrow> doable CommunicationLayer es _ (Receive _ m)"
 360           -- {* the communication layer can cause anyone to receive any message
 361                 previously sent by anyone to anyone *}
 362       | construct_actor_name: "doable (Actor a) _ _ (Construct a (ActorName _))"
 363           -- {* an actor can construct any actor's name *}
 364       | construct_number: "doable (Actor a) _ _ (Construct a (Number _))"
 365           -- {* an actor can construct any number *}
 366       | construct_signature:
 367           "Construct a m \<in> es \<union> es'
 368             \<Longrightarrow> doable (Actor a) es es' (Construct a (Signature a m))"
 369           -- {* an actor can construct their own signature for a message they've
 370                 constructed *}
 371       | construct_encrypted:
 372           "Construct a m \<in> es \<union> es'
 373             \<Longrightarrow> doable (Actor a) es es' (Construct a (Encrypted _ _ m))"
 374           -- {* an actor can construct an encrypted version of a message they've
 375                 constructed *}
 376       | construct_list:
 377           "\<forall> m \<in> set ms. Construct a m \<in> es \<union> es'
 378             \<Longrightarrow> doable (Actor a) es es' (Construct a (MessageList ms))"
 379           -- {* an actor can construct a list of messages they've constructed *}
 380       | construct_received:
 381           "Receive a M \<in> es \<Longrightarrow> learnable a M m
 382           \<Longrightarrow> doable (Actor a) es _ (Construct a m)"
 383           -- {* an actor can construct a message they can learn from one they've
 384                 previously received *}
 385       | constructed_sendable:
 386           "Construct a m \<in> es \<union> es' \<Longrightarrow> doable (Actor a) es es' (Send a _ m)"
 387           -- {* an actor can send any message they've constructed *}
 388       | pay_doable: "doable (Actor a) _ _ (Pay a _ _ _)"
 389           -- {* an actor can always pay anyone any amount with any payment id *}
 390
 391 text {* Which agent must have caused a particular event? *}
 392 fun causal_agent :: "event \<Rightarrow> agent"
 393   where construct_cause: "causal_agent (Construct a _) = Actor a"
 394       | send_cause: "causal_agent (Send a _ _) = Actor a"
 395       | receive_cause: "causal_agent (Receive _ _) = CommunicationLayer"
 396       | pay_cause: "causal_agent (Pay a _ _ _) = Actor a"
 397
 398 text {* If an event is doable by an agent, then that agent must be the causal one *}
 399 lemma doable_implies_causal:
 400   assumes "doable a es es' e"
 401   shows "causal_agent e = a"
 402   using assms by (cases rule: doable.cases) simp_all
 403
 404 text {* Which events affect a particular agent? *}
 405 inductive affected_agent :: "agent \<Rightarrow> event \<Rightarrow> bool"
 406   where constructor_affected: "affected_agent (Actor a) (Construct a _)"
 407       | sender_affected: "affected_agent (Actor a) (Send a _ _)"
 408       | send_affects_communication:
 409           "affected_agent CommunicationLayer (Send _ _ _)"
 410       | receiver_affected: "affected_agent (Actor a) (Receive a _)"
 411       | receive_affects_communication:
 412           "affected_agent CommunicationLayer (Receive _ _)"
 413       | payer_affected: "affected_agent (Actor a) (Pay a _ _ _)"
 414       | payee_affected: "affected_agent (Actor a) (Pay _ a _ _)"
 415
 416 text {* The causal agent is always affected *}
 417 lemma causal_affected: "affected_agent (causal_agent e) e"
 418   by (cases rule: causal_agent.induct) (simp_all add: affected_agent.simps)
 419
 420 fun lift_message_map_event
 421   :: "(message \<Rightarrow> message) \<Rightarrow> event \<Rightarrow> event"
 422   where "lift_message_map_event f (Construct a m) = Construct a (f m)"
 423       | "lift_message_map_event f (Send a b m) = Send a b (f m)"
 424       | "lift_message_map_event f (Receive a m) = Receive a (f m)"
 425       | "lift_message_map_event _ e = e"
 426
 427 lemma sendable'_implies_sendable:
 428   assumes sendable': "Send a b M' \<in> image (lift_message_map_event f) es"
 429   shows "\<exists> M. f M = M' \<and> Send a b M \<in> es"
 430 proof -
 431   from sendable' obtain e
 432     where ein: "e \<in> es" and mape: "lift_message_map_event f e = Send a b M'"
 433       by auto
 434   from mape
 435     obtain M where esend: "e = Send a b M" and mapM: "f M = M'"
 436       by (cases e) simp_all
 437   from esend and ein have sendable: "Send a b M \<in> es" by simp
 438   from mapM and sendable show "\<exists> M. f M = M' \<and> Send a b M \<in> es" by auto
 439 qed
 440
 441 subsection {* Histories *}
 442 type_synonym time = nat
 443 type_synonym history = "(event \<times> time) set"
 444
 445 text {* What events occurred before a given time? *}
 446 definition events_before :: "history \<Rightarrow> time \<Rightarrow> event set" where
 447   "events_before h t = {e. \<exists> u < t. (e, u) \<in> h}"
 448
 449 lemma events_before_monotonic:
 450   assumes "t' \<le> t"
 451   shows "events_before h t' \<subseteq> events_before h t"
 452 proof
 453   fix e
 454   assume "e \<in> events_before h t'"
 455   then obtain t'' where t''t': "t'' < t'" and inh: "(e, t'') \<in> h"
 456     by (unfold events_before_def) auto
 457   from t''t' and assms have "t'' < t" by simp
 458   with inh show "e \<in> events_before h t" by (unfold events_before_def) auto
 459 qed
 460
 461 text {* What events occurred at a given time? *}
 462 definition events_at :: "history \<Rightarrow> time \<Rightarrow> event set" where
 463   "events_at h t = {e. (e, t) \<in> h}"
 464
 465 abbreviation events_not_after :: "history \<Rightarrow> time \<Rightarrow> event set" where
 466   "events_not_after h t == events_before h t \<union> events_at h t"
 467
 468 lemma events_not_after: "e \<in> events_not_after h t \<longleftrightarrow> (\<exists> t' \<le> t. (e, t') \<in> h)"
 469 proof
 470   assume "e \<in> events_not_after h t"
 471   hence "e \<in> events_before h t \<or> e \<in> events_at h t" by simp
 472   thus "\<exists> t' \<le> t. (e, t') \<in> h"
 473   proof
 474     assume "e \<in> events_before h t"
 475     then obtain t' where "t' < t" and "(e, t') \<in> h"
 476       by (unfold events_before_def) auto
 477     thus "\<exists> t' \<le> t. (e, t') \<in> h" by (simp add: exI[of _ t'])
 478   next
 479     assume "e \<in> events_at h t"
 480     thus "\<exists> t' \<le> t. (e, t') \<in> h" by (unfold events_at_def) (simp add: exI[of _ t])
 481   qed
 482 next
 483   assume "\<exists> t' \<le> t. (e, t') \<in> h"
 484   then obtain t' where t't: "t' \<le> t" and inh: "(e, t') \<in> h" by auto
 485   show "e \<in> events_not_after h t"
 486   proof cases
 487     assume "t' = t"
 488     with inh show "e \<in> events_not_after h t" by (unfold events_at_def) simp
 489   next
 490     assume "t' \<noteq> t"
 491     with t't have "t' < t" by simp
 492     with inh show "e \<in> events_not_after h t" by (unfold events_before_def) auto
 493   qed
 494 qed
 495
 496 lemma events_not_after_monotonic:
 497   assumes "t' \<le> t"
 498   shows "events_not_after h t' \<subseteq> events_not_after h t"
 499 proof
 500   fix e
 501   assume "e \<in> events_not_after h t'"
 502   with events_not_after obtain t'' where t''t': "t'' \<le> t'" and inh: "(e, t'') \<in> h"
 503     by auto
 504   from t''t' and assms have "t'' \<le> t" by simp
 505   with inh and events_not_after show "e \<in> events_not_after h t" by auto
 506 qed
 507
 508 text {* Which histories could possibly occur? *}
 509 definition possible_history :: "history \<Rightarrow> bool" where
 510   "possible_history h \<longleftrightarrow>
 511     (\<forall> (e, t) \<in> h. doable (causal_agent e) (events_before h t) (events_at h t) e)"
 512
 513 text {* What messages did a given agent receive before a given time? *}
 514 fun messages_received_before :: "agent \<Rightarrow> history \<Rightarrow> time \<Rightarrow> message set"
 515   where "messages_received_before CommunicationLayer _ _ = {}"
 516       | "messages_received_before (Actor a) h t
 517           = {m. Receive a m \<in> events_before h t}"
 518
 519 text {* What subhistory is relevant to a given agent before a given time? *}
 520 definition relevant_subhistory :: "agent \<Rightarrow> time \<Rightarrow> history \<Rightarrow> history" where
 521   "relevant_subhistory A t h = {(e, t') \<in> h. affected_agent A e \<and> t' < t}"
 522
 523 end