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 encrypted_constructed_from:
  95   "constructed_from (Encrypted a b M) m
  96   \<Longrightarrow> m = Encrypted a b M \<or> constructed_from M m"
  97 proof (induction rule: constructed_from.induct)
  98   case constructed_from_self
  99   show "Encrypted a b M = Encrypted a b M
 100         \<or> constructed_from M (Encrypted a b M)"
 101     by simp
 102 next
 103   case (constructed_from_signature c m)
 104   from constructed_from_signature.IH have "constructed_from M (Signature c m)"
 105     by simp
 106   hence "constructed_from M m" by rule
 107   thus "m = Encrypted a b M \<or> constructed_from M m" ..
 108 next
 109   case (constructed_from_encrypted c d m)
 110   from constructed_from_encrypted.IH have "constructed_from M m"
 111   proof
 112     assume "Encrypted c d m = Encrypted a b M"
 113     thus "constructed_from M m" by (simp add: constructed_from_self)
 114   next
 115     assume "constructed_from M (Encrypted c d m)"
 116     thus "constructed_from M m" by rule
 117   qed
 118   thus "m = Encrypted a b M \<or> constructed_from M m" ..
 119 next
 120   case (constructed_from_list m ms)
 121   from constructed_from_list.IH have "constructed_from M (MessageList ms)"
 122     by simp
 123   with constructed_from_list.hyps(1) have "constructed_from M m" by rule
 124   thus "m = Encrypted a b M \<or> constructed_from M m" ..
 125 qed
 126
 127 lemma list_constructed_from:
 128   "constructed_from (MessageList ms) m
 129   \<Longrightarrow> m = MessageList ms \<or> (\<exists> M \<in> set ms. constructed_from M m)"
 130 proof (induction rule: constructed_from.induct)
 131   case constructed_from_self
 132   show "MessageList ms = MessageList ms
 133         \<or> (\<exists> M \<in> set ms. constructed_from M (MessageList ms))"
 134     by simp
 135 next
 136   case (constructed_from_signature a m)
 137   from constructed_from_signature.IH
 138     have "\<exists> M \<in> set ms. constructed_from M (Signature a m)"
 139       by simp
 140   hence "\<exists> M \<in> set ms. constructed_from M m"
 141     by (metis constructed_from.constructed_from_signature)
 142   thus "m = MessageList ms \<or> (\<exists> M \<in> set ms. constructed_from M m)" ..
 143 next
 144   case (constructed_from_encrypted a b m)
 145   from constructed_from_encrypted.IH
 146     have "\<exists> M \<in> set ms. constructed_from M (Encrypted a b m)"
 147       by simp
 148   hence "\<exists> M \<in> set ms. constructed_from M m"
 149     by (metis constructed_from.constructed_from_encrypted)
 150   thus "m = MessageList ms \<or> (\<exists> M \<in> set ms. constructed_from M m)" ..
 151 next
 152   case (constructed_from_list m ms')
 153   from constructed_from_list.IH have "\<exists> M \<in> set ms. constructed_from M m"
 154   proof
 155     assume "MessageList ms' = MessageList ms"
 156     with `m \<in> set ms'` have "m \<in> set ms" by simp
 157     with constructed_from_self show "\<exists> M \<in> set ms. constructed_from M m"
 158       by blast
 159   next
 160     assume "\<exists> M \<in> set ms. constructed_from M (MessageList ms')"
 161     with `m \<in> set ms'` show "\<exists> M \<in> set ms. constructed_from M m"
 162       by (metis constructed_from.constructed_from_list)
 163   qed
 164   thus "m = MessageList ms \<or> (\<exists> M \<in> set ms. constructed_from M m)" ..
 165 qed
 166
 167 lemma constructed_from_transitive:
 168   assumes "constructed_from M' M"
 169   shows "constructed_from M m \<Longrightarrow> constructed_from M' m"
 170 proof (induction rule: constructed_from.induct)
 171   case constructed_from_self
 172   from assms show "constructed_from M' M" .
 173 next
 174   case (constructed_from_signature a m)
 175   from constructed_from_signature.IH show "constructed_from M' m" by rule
 176 next
 177   case (constructed_from_encrypted a b m)
 178   from constructed_from_encrypted.IH show "constructed_from M' m" by rule
 179 next
 180   case (constructed_from_list m ms)
 181   from constructed_from_list.hyps(1) and constructed_from_list.IH
 182     show "constructed_from M' m" by rule
 183 qed
 184
 185 text {* What can a particular actor learn from a particular message? *}
 186 inductive learnable :: "actor \<Rightarrow> message \<Rightarrow> message \<Rightarrow> bool" for a M
 187   where identity_learnable: "learnable a M M"
 188           -- {* the message itself *}
 189       | encrypted1_learnable: "learnable a M (Encrypted a _ m) \<Longrightarrow> learnable a M m"
 190       | encrypted2_learnable: "learnable a M (Encrypted _ a m) \<Longrightarrow> learnable a M m"
 191           -- {* the body of a learnable message encrypted for the actor *}
 192       | listed_learnable:
 193           "m \<in> set l \<Longrightarrow> learnable a M (MessageList l) \<Longrightarrow> learnable a M m"
 194           -- {* any element of a learnable list of messages *}
 195
 196 lemma learnable_implies_constructed_from:
 197   "learnable a M m \<Longrightarrow> constructed_from M m"
 198 proof (induction rule: learnable.induct)
 199   show "constructed_from M M" by rule
 200   fix b m
 201   { assume "constructed_from M (Encrypted a b m)"
 202     thus "constructed_from M m" by rule
 203   next
 204     assume "constructed_from M (Encrypted b a m)"
 205     thus "constructed_from M m" by rule
 206   }
 207 next
 208   fix m ms
 209   assume "m \<in> set ms" and "constructed_from M (MessageList ms)"
 210   thus "constructed_from M m" by rule
 211 qed
 212
 213 text {* What messages can a particular actor construct from a particular set of
 214         messages? *}
 215 inductive constructible :: "actor \<Rightarrow> message set \<Rightarrow> message \<Rightarrow> bool" for a Ms
 216   where learnable_constructible:
 217           "M \<in> Ms \<Longrightarrow> learnable a M m \<Longrightarrow> constructible a Ms m"
 218           -- {* any message learnable from any message in the set *}
 219       | actorName_constructible: "constructible a Ms (ActorName _)"
 220           -- {* any actor's name *}
 221       | number_constructible: "constructible a Ms (Number _)"
 222           -- {* any number *}
 223       | signed_constructible:
 224           "constructible a Ms m \<Longrightarrow> constructible a Ms (Signature a m)"
 225           -- {* an otherwise constructible message, signed by this actor *}
 226       | encrypted_constructible:
 227           "constructible a Ms m \<Longrightarrow> constructible a Ms (Encrypted _ _ m)"
 228           -- {* an otherwise constructible message, encrypted to any pair of actors *}
 229       | listed_constructible:
 230           "(\<forall> m \<in> set l. constructible a Ms m)
 231             \<Longrightarrow> constructible a Ms (MessageList l)"
 232           -- {* a list of otherwise constructible messages *}
 233
 234 subsubsection {* Indistinguishability of messages *}
 235 datatype_new agent = CommunicationLayer | Actor actor
 236
 237 text {* What pairs of messages should we not expect a particular agent to be able
 238         to distinguish between, given a particular set of messages to work from?
 239         This definition isn't intended to express a limit on what an attacker might
 240         be able to do; rather, it's meant to limit what we might reasonably expect
 241         an honest agent to be able to do without resorting to sophisticated
 242         cryptanalysis or anything similarly difficult. *}
 243 inductive indistinguishable :: "agent \<Rightarrow> message set \<Rightarrow> message \<Rightarrow> message \<Rightarrow> bool"
 244   where "indistinguishable CommunicationLayer _ _ _"
 245       | "indistinguishable _ _ m m"
 246       | "\<not> constructible a Ms m \<Longrightarrow> \<not> constructible a Ms m'
 247           \<Longrightarrow> indistinguishable (Actor a) Ms (Signature _ m) (Signature _ m')"
 248       | "indistinguishable A Ms m m'
 249           \<Longrightarrow> indistinguishable A Ms (Signature a m) (Signature a m')"
 250       | "A \<noteq> Actor a \<Longrightarrow> A \<noteq> Actor b \<Longrightarrow> A \<noteq> Actor c \<Longrightarrow> A \<noteq> Actor d
 251           \<Longrightarrow> indistinguishable A _ (Encrypted a b _) (Encrypted c d _)"
 252       | "indistinguishable A Ms m m'
 253           \<Longrightarrow> indistinguishable A Ms (Encrypted a b m) (Encrypted a b m')"
 254       | "indistinguishable A Ms m m'
 255           \<Longrightarrow> indistinguishable A Ms (MessageList ms) (MessageList ms')
 256           \<Longrightarrow> indistinguishable A Ms
 257                 (MessageList (m # ms))
 258                 (MessageList (m' # ms'))"
 259
 260 lemma indistinguishable_symmetric:
 261   "indistinguishable A Ms m m' \<Longrightarrow> indistinguishable A Ms m' m"
 262 proof (induction rule: indistinguishable.induct)
 263   fix Ms m m'
 264   show "indistinguishable CommunicationLayer Ms m m'" by rule
 265   fix A
 266   show "indistinguishable A Ms m m" by rule
 267   fix a b c
 268   assume "\<not> constructible a Ms m'" and "\<not> constructible a Ms m"
 269   thus "indistinguishable (Actor a) Ms (Signature c m') (Signature b m)" by rule
 270 next
 271   fix A Ms m m' a
 272   assume "indistinguishable A Ms m' m"
 273   thus "indistinguishable A Ms (Signature a m') (Signature a m)" by rule
 274 next
 275   fix A Ms m m' a b c d
 276   assume "A \<noteq> Actor c" and "A \<noteq> Actor d" and "A \<noteq> Actor a" and "A \<noteq> Actor b"
 277   thus "indistinguishable A Ms (Encrypted c d m') (Encrypted a b m)" by rule
 278 next
 279   fix A Ms m m' a b
 280   assume "indistinguishable A Ms m' m"
 281   thus "indistinguishable A Ms (Encrypted a b m') (Encrypted a b m)" by rule
 282 next
 283   fix A Ms m m' ms ms'
 284   assume  "indistinguishable A Ms m' m"
 285     and   "indistinguishable A Ms (MessageList ms') (MessageList ms)"
 286   thus "indistinguishable A Ms (MessageList (m' # ms')) (MessageList (m # ms))"
 287     by rule
 288 qed
 289
 290 definition indistinguishability_map ::
 291   "agent \<Rightarrow> message set \<Rightarrow> (message \<Rightarrow> message) \<Rightarrow> bool" where
 292     "indistinguishability_map A Ms f
 293       \<longleftrightarrow> bij f
 294         \<and> (\<forall> m. indistinguishable A Ms m (f m)
 295               \<and> (\<forall> a b. (A = Actor a \<and> constructible a Ms m
 296                           \<longrightarrow> f (Signature b m) = Signature b (f m)
 297                         )
 298                       \<and> (A = Actor a \<or> A = Actor b
 299                           \<longrightarrow> f (Encrypted a b m) = Encrypted a b (f m)
 300                         )
 301                 )
 302           )
 303         \<and> (A \<noteq> CommunicationLayer
 304             \<longrightarrow> (\<forall> ms. f (MessageList ms) = MessageList (map f ms))
 305           )"
 306
 307 lemma learnable_indistinguishability_map:
 308   assumes im: "indistinguishability_map (Actor a) Ms f"
 309   shows "learnable a M m \<Longrightarrow> learnable a (f M) (f m)"
 310 proof (induction rule: learnable.induct)
 311   show "learnable a (f M) (f M)" by rule
 312   fix b m
 313   assume "learnable a (f M) (f (Encrypted a b m))"
 314   moreover
 315     from im have "f (Encrypted a b m) = Encrypted a b (f m)"
 316       by (unfold indistinguishability_map_def) simp
 317   ultimately show "learnable a (f M) (f m)" by (metis encrypted1_learnable)
 318 next
 319   fix b m
 320   assume "learnable a (f M) (f (Encrypted b a m))"
 321   moreover
 322     from im have "f (Encrypted b a m) = Encrypted b a (f m)"
 323       by (unfold indistinguishability_map_def) simp
 324   ultimately show "learnable a (f M) (f m)" by (metis encrypted2_learnable)
 325 next
 326   fix m ms
 327   assume  minms: "m \<in> set ms"
 328     and   learnablefms: "learnable a (f M) (f (MessageList ms))"
 329   from minms have fminfms: "f m \<in> set (map f ms)" by simp
 330   from im have "f (MessageList ms) = MessageList (map f ms)"
 331     by (unfold indistinguishability_map_def) simp
 332   with fminfms and learnablefms show "learnable a (f M) (f m)"
 333     by (metis listed_learnable)
 334 qed
 335
 336 lemma indistinguishable_message_type:
 337   "indistinguishable (Actor a) Ms m m' \<Longrightarrow> type_of_message m = type_of_message m'"
 338 proof (induction rule: indistinguishable.cases)
 339   assume "Actor a = CommunicationLayer"
 340   thus "type_of_message m = type_of_message m'" ..
 341 next
 342   fix n
 343   assume "m = n" and "m' = n"
 344   thus "type_of_message m = type_of_message m'" by simp
 345 next
 346   fix b c n n'
 347   assume "m = Signature b n" and "m' = Signature c n'"
 348   thus "type_of_message m = type_of_message m'" by simp
 349   thus "type_of_message m = type_of_message m'" .
 350 next
 351   fix b c d e n n'
 352   assume "m = Encrypted b c n" and "m' = Encrypted d e n'"
 353   thus "type_of_message m = type_of_message m'" by simp
 354   thus "type_of_message m = type_of_message m'" .
 355 next
 356   fix n ns n' ns'
 357   assume "m = MessageList (n # ns)" and "m' = MessageList (n' # ns')"
 358   thus "type_of_message m = type_of_message m'" by simp
 359 qed
 360
 361 lemma learnable_inverse_indistinguishability_map:
 362   assumes im: "indistinguishability_map (Actor a) Ms f"
 363   shows "learnable a M m \<Longrightarrow> learnable a (inv f M) (inv f m)"
 364 proof (induction rule: learnable.induct)
 365   from im have bij: "bij f" unfolding indistinguishability_map_def ..
 366   { show "learnable a (inv f M) (inv f M)" by rule
 367     fix b m
 368     assume "learnable a (inv f M) (inv f (Encrypted a b m))"
 369     moreover
 370       { from im have "f (Encrypted a b (inv f m)) = Encrypted a b (f (inv f m))"
 371           by (unfold indistinguishability_map_def) simp
 372         also from bij have "\<dots> = Encrypted a b m" by simp
 373         finally have "inv f (Encrypted a b m) = Encrypted a b (inv f m)"
 374           by (simp add: bij)
 375       }
 376     ultimately have "learnable a (inv f M) (Encrypted a b (inv f m))" by simp
 377     thus "learnable a (inv f M) (inv f m)" by rule
 378   next
 379     fix b m
 380     assume "learnable a (inv f M) (inv f (Encrypted b a m))"
 381     moreover
 382       { from im have "f (Encrypted b a (inv f m)) = Encrypted b a (f (inv f m))"
 383           by (unfold indistinguishability_map_def) simp
 384         also from bij have "\<dots> = Encrypted b a m" by simp
 385         finally have "inv f (Encrypted b a m) = Encrypted b a (inv f m)"
 386           by (simp add: bij)
 387       }
 388     ultimately have "learnable a (inv f M) (Encrypted b a (inv f m))" by simp
 389     thus "learnable a (inv f M) (inv f m)" by rule
 390   next
 391     fix m ms
 392     assume  minms: "m \<in> set ms"
 393       and   learnableinvfms: "learnable a (inv f M) (inv f (MessageList ms))"
 394     from minms have invfmininvfms: "inv f m \<in> set (map (inv f) ms)" by simp
 395     from im have
 396         "f (MessageList (map (inv f) ms)) = MessageList (map f (map (inv f) ms))"
 397       by (unfold indistinguishability_map_def) simp
 398     also from bij have "\<dots> = MessageList ms"
 399       by (subst bij_map_f_map_inv_f) simp_all
 400     finally have "inv f (MessageList ms) = MessageList (map (inv f) ms)"
 401       by (simp add: bij)
 402     with invfmininvfms and learnableinvfms show "learnable a (inv f M) (inv f m)"
 403       by (metis listed_learnable)
 404   }
 405 qed
 406
 407 type_synonym encrypted_message_data = "actor \<times> actor \<times> message"
 408 type_synonym
 409   encrypted_message_map = "encrypted_message_data \<Rightarrow> encrypted_message_data"
 410
 411 subsection {* Events *}
 412 type_synonym payment = nat
 413
 414 datatype_new event
 415   = Construct actor message   -- {* an actor constructs a message *}
 416   | Send actor actor message  -- {* send a message from one actor to another *}
 417   | Receive actor message     -- {* an actor receives a message *}
 418   | Pay
 419       actor         -- {* payer *}
 420       actor         -- {* payee *}
 421       payment       -- {* specifies amount and manner of payment *}
 422       nat           -- {* payment id, intended to be unique to payer/payee pair*}
 423
 424 text {* Given a set of past events, which messages has a particular actor received? *}
 425 definition messages_received :: "actor \<Rightarrow> event set \<Rightarrow> message set"
 426   where "messages_received a es = {m. Receive a m \<in> es}"
 427
 428 text {* What can a particular agent do, given a set of past events and a set of
 429         concurrent events? *}
 430 inductive doable :: "agent \<Rightarrow> event set \<Rightarrow> event set \<Rightarrow> event \<Rightarrow> bool"
 431   where communicationLayer_transmit_doable:
 432           "(Send _ _ m) \<in> es \<Longrightarrow> doable CommunicationLayer es _ (Receive _ m)"
 433           -- {* the communication layer can cause anyone to receive any message
 434                 previously sent by anyone to anyone *}
 435       | construct_actor_name: "doable (Actor a) _ _ (Construct a (ActorName _))"
 436           -- {* an actor can construct any actor's name *}
 437       | construct_number: "doable (Actor a) _ _ (Construct a (Number _))"
 438           -- {* an actor can construct any number *}
 439       | construct_signature:
 440           "Construct a m \<in> es \<union> es'
 441             \<Longrightarrow> doable (Actor a) es es' (Construct a (Signature a m))"
 442           -- {* an actor can construct their own signature for a message they've
 443                 constructed *}
 444       | construct_encrypted:
 445           "Construct a m \<in> es \<union> es'
 446             \<Longrightarrow> doable (Actor a) es es' (Construct a (Encrypted _ _ m))"
 447           -- {* an actor can construct an encrypted version of a message they've
 448                 constructed *}
 449       | construct_list:
 450           "\<forall> m \<in> set ms. Construct a m \<in> es \<union> es'
 451             \<Longrightarrow> doable (Actor a) es es' (Construct a (MessageList ms))"
 452           -- {* an actor can construct a list of messages they've constructed *}
 453       | construct_received:
 454           "Receive a M \<in> es \<Longrightarrow> learnable a M m
 455           \<Longrightarrow> doable (Actor a) es _ (Construct a m)"
 456           -- {* an actor can construct a message they can learn from one they've
 457                 previously received *}
 458       | constructed_sendable:
 459           "Construct a m \<in> es \<union> es' \<Longrightarrow> doable (Actor a) es es' (Send a _ m)"
 460           -- {* an actor can send any message they've constructed *}
 461       | pay_doable: "doable (Actor a) _ _ (Pay a _ _ _)"
 462           -- {* an actor can always pay anyone any amount with any payment id *}
 463
 464 text {* Which agent must have caused a particular event? *}
 465 fun causal_agent :: "event \<Rightarrow> agent"
 466   where construct_cause: "causal_agent (Construct a _) = Actor a"
 467       | send_cause: "causal_agent (Send a _ _) = Actor a"
 468       | receive_cause: "causal_agent (Receive _ _) = CommunicationLayer"
 469       | pay_cause: "causal_agent (Pay a _ _ _) = Actor a"
 470
 471 text {* If an event is doable by an agent, then that agent must be the causal one *}
 472 lemma doable_implies_causal:
 473   assumes "doable a es es' e"
 474   shows "causal_agent e = a"
 475   using assms by (cases rule: doable.cases) simp_all
 476
 477 text {* Which events affect a particular agent? *}
 478 inductive affected_agent :: "agent \<Rightarrow> event \<Rightarrow> bool"
 479   where constructor_affected: "affected_agent (Actor a) (Construct a _)"
 480       | sender_affected: "affected_agent (Actor a) (Send a _ _)"
 481       | send_affects_communication:
 482           "affected_agent CommunicationLayer (Send _ _ _)"
 483       | receiver_affected: "affected_agent (Actor a) (Receive a _)"
 484       | receive_affects_communication:
 485           "affected_agent CommunicationLayer (Receive _ _)"
 486       | payer_affected: "affected_agent (Actor a) (Pay a _ _ _)"
 487       | payee_affected: "affected_agent (Actor a) (Pay _ a _ _)"
 488
 489 text {* The causal agent is always affected *}
 490 lemma causal_affected: "affected_agent (causal_agent e) e"
 491   by (cases rule: causal_agent.induct) (simp_all add: affected_agent.simps)
 492
 493 fun lift_message_map_event
 494   :: "(message \<Rightarrow> message) \<Rightarrow> event \<Rightarrow> event"
 495   where "lift_message_map_event f (Construct a m) = Construct a (f m)"
 496       | "lift_message_map_event f (Send a b m) = Send a b (f m)"
 497       | "lift_message_map_event f (Receive a m) = Receive a (f m)"
 498       | "lift_message_map_event _ e = e"
 499
 500 lemma sendable'_implies_sendable:
 501   assumes sendable': "Send a b M' \<in> image (lift_message_map_event f) es"
 502   shows "\<exists> M. f M = M' \<and> Send a b M \<in> es"
 503 proof -
 504   from sendable' obtain e
 505     where ein: "e \<in> es" and mape: "lift_message_map_event f e = Send a b M'"
 506       by auto
 507   from mape
 508     obtain M where esend: "e = Send a b M" and mapM: "f M = M'"
 509       by (cases e) simp_all
 510   from esend and ein have sendable: "Send a b M \<in> es" by simp
 511   from mapM and sendable show "\<exists> M. f M = M' \<and> Send a b M \<in> es" by auto
 512 qed
 513
 514 subsection {* Histories *}
 515 type_synonym time = nat
 516 type_synonym history = "(event \<times> time) set"
 517
 518 text {* What events occurred before a given time? *}
 519 definition events_before :: "history \<Rightarrow> time \<Rightarrow> event set" where
 520   "events_before h t = {e. \<exists> u < t. (e, u) \<in> h}"
 521
 522 lemma events_before_monotonic:
 523   assumes "t' \<le> t"
 524   shows "events_before h t' \<subseteq> events_before h t"
 525 proof
 526   fix e
 527   assume "e \<in> events_before h t'"
 528   then obtain t'' where t''t': "t'' < t'" and inh: "(e, t'') \<in> h"
 529     by (unfold events_before_def) auto
 530   from t''t' and assms have "t'' < t" by simp
 531   with inh show "e \<in> events_before h t" by (unfold events_before_def) auto
 532 qed
 533
 534 text {* What events occurred at a given time? *}
 535 definition events_at :: "history \<Rightarrow> time \<Rightarrow> event set" where
 536   "events_at h t = {e. (e, t) \<in> h}"
 537
 538 abbreviation events_not_after :: "history \<Rightarrow> time \<Rightarrow> event set" where
 539   "events_not_after h t == events_before h t \<union> events_at h t"
 540
 541 lemma events_not_after: "e \<in> events_not_after h t \<longleftrightarrow> (\<exists> t' \<le> t. (e, t') \<in> h)"
 542 proof
 543   assume "e \<in> events_not_after h t"
 544   hence "e \<in> events_before h t \<or> e \<in> events_at h t" by simp
 545   thus "\<exists> t' \<le> t. (e, t') \<in> h"
 546   proof
 547     assume "e \<in> events_before h t"
 548     then obtain t' where "t' < t" and "(e, t') \<in> h"
 549       by (unfold events_before_def) auto
 550     thus "\<exists> t' \<le> t. (e, t') \<in> h" by (simp add: exI[of _ t'])
 551   next
 552     assume "e \<in> events_at h t"
 553     thus "\<exists> t' \<le> t. (e, t') \<in> h" by (unfold events_at_def) (simp add: exI[of _ t])
 554   qed
 555 next
 556   assume "\<exists> t' \<le> t. (e, t') \<in> h"
 557   then obtain t' where t't: "t' \<le> t" and inh: "(e, t') \<in> h" by auto
 558   show "e \<in> events_not_after h t"
 559   proof cases
 560     assume "t' = t"
 561     with inh show "e \<in> events_not_after h t" by (unfold events_at_def) simp
 562   next
 563     assume "t' \<noteq> t"
 564     with t't have "t' < t" by simp
 565     with inh show "e \<in> events_not_after h t" by (unfold events_before_def) auto
 566   qed
 567 qed
 568
 569 lemma events_not_after_monotonic:
 570   assumes "t' \<le> t"
 571   shows "events_not_after h t' \<subseteq> events_not_after h t"
 572 proof
 573   fix e
 574   assume "e \<in> events_not_after h t'"
 575   with events_not_after obtain t'' where t''t': "t'' \<le> t'" and inh: "(e, t'') \<in> h"
 576     by auto
 577   from t''t' and assms have "t'' \<le> t" by simp
 578   with inh and events_not_after show "e \<in> events_not_after h t" by auto
 579 qed
 580
 581 text {* Which histories could possibly occur? *}
 582 definition possible_history :: "history \<Rightarrow> bool" where
 583   "possible_history h \<longleftrightarrow>
 584     (\<forall> (e, t) \<in> h. doable (causal_agent e) (events_before h t) (events_at h t) e)"
 585
 586 text {* What messages did a given agent receive before a given time? *}
 587 fun messages_received_before :: "agent \<Rightarrow> history \<Rightarrow> time \<Rightarrow> message set"
 588   where "messages_received_before CommunicationLayer _ _ = {}"
 589       | "messages_received_before (Actor a) h t
 590           = {m. Receive a m \<in> events_before h t}"
 591
 592 text {* What subhistory is relevant to a given agent before a given time? *}
 593 definition relevant_subhistory :: "agent \<Rightarrow> time \<Rightarrow> history \<Rightarrow> history" where
 594   "relevant_subhistory A t h = {(e, t') \<in> h. affected_agent A e \<and> t' < t}"
 595
 596 end