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 M M"
  45       | "constructed_from M (Signature _ m) \<Longrightarrow> constructed_from M m"
  46       | "constructed_from M (Encrypted _ _ m) \<Longrightarrow> constructed_from M m"
  47       | "m \<in> set ms \<Longrightarrow> constructed_from M (MessageList ms)
  48           \<Longrightarrow> constructed_from M m"
  49
  50 lemma actor_name_constructed_from:
  51   "constructed_from (ActorName a) m \<Longrightarrow> m = ActorName a"
  52   by (induction rule: constructed_from.induct) simp_all
  53
  54 text {* What can a particular actor learn from a particular message? *}
  55 inductive learnable :: "actor \<Rightarrow> message \<Rightarrow> message \<Rightarrow> bool" for a M
  56   where identity_learnable: "learnable a M M"
  57           -- {* the message itself *}
  58       | encrypted1_learnable: "learnable a M (Encrypted a _ m) \<Longrightarrow> learnable a M m"
  59       | encrypted2_learnable: "learnable a M (Encrypted _ a m) \<Longrightarrow> learnable a M m"
  60           -- {* the body of a learnable message encrypted for the actor *}
  61       | listed_learnable:
  62           "m \<in> set l \<Longrightarrow> learnable a M (MessageList l) \<Longrightarrow> learnable a M m"
  63           -- {* any element of a learnable list of messages *}
  64
  65 lemma learnable_implies_constructed_from:
  66   "learnable a M m \<Longrightarrow> constructed_from M m"
  67 proof (induction rule: learnable.induct)
  68   show "constructed_from M M" by rule
  69   fix b m
  70   { assume "constructed_from M (Encrypted a b m)"
  71     thus "constructed_from M m" by rule
  72   next
  73     assume "constructed_from M (Encrypted b a m)"
  74     thus "constructed_from M m" by rule
  75   }
  76 next
  77   fix m ms
  78   assume "m \<in> set ms" and "constructed_from M (MessageList ms)"
  79   thus "constructed_from M m" by rule
  80 qed
  81
  82 text {* What messages can a particular actor construct from a particular set of
  83         messages? *}
  84 inductive constructible :: "actor \<Rightarrow> message set \<Rightarrow> message \<Rightarrow> bool" for a Ms
  85   where learnable_constructible:
  86           "M \<in> Ms \<Longrightarrow> learnable a M m \<Longrightarrow> constructible a Ms m"
  87           -- {* any message learnable from any message in the set *}
  88       | actorName_constructible: "constructible a Ms (ActorName _)"
  89           -- {* any actor's name *}
  90       | number_constructible: "constructible a Ms (Number _)"
  91           -- {* any number *}
  92       | signed_constructible:
  93           "constructible a Ms m \<Longrightarrow> constructible a Ms (Signature a m)"
  94           -- {* an otherwise constructible message, signed by this actor *}
  95       | encrypted_constructible:
  96           "constructible a Ms m \<Longrightarrow> constructible a Ms (Encrypted _ _ m)"
  97           -- {* an otherwise constructible message, encrypted to any pair of actors *}
  98       | listed_constructible:
  99           "(\<forall> m \<in> set l. constructible a Ms m)
 100             \<Longrightarrow> constructible a Ms (MessageList l)"
 101           -- {* a list of otherwise constructible messages *}
 102
 103 subsubsection {* Indistinguishability of messages *}
 104 datatype_new agent = CommunicationLayer | Actor actor
 105
 106 text {* What pairs of messages should we not expect a particular agent to be able
 107         to distinguish between, given a particular set of messages to work from?
 108         This definition isn't intended to express a limit on what an attacker might
 109         be able to do; rather, it's meant to limit what we might reasonably expect
 110         an honest agent to be able to do without resorting to sophisticated
 111         cryptanalysis or anything similarly difficult. *}
 112 inductive indistinguishable :: "agent \<Rightarrow> message set \<Rightarrow> message \<Rightarrow> message \<Rightarrow> bool"
 113   where "indistinguishable CommunicationLayer _ _ _"
 114       | "indistinguishable _ _ m m"
 115       | "\<not> constructible a Ms m \<Longrightarrow> \<not> constructible a Ms m'
 116           \<Longrightarrow> indistinguishable (Actor a) Ms (Signature _ m) (Signature _ m')"
 117       | "indistinguishable A Ms m m'
 118           \<Longrightarrow> indistinguishable A Ms (Signature a m) (Signature a m')"
 119       | "A \<noteq> Actor a \<Longrightarrow> A \<noteq> Actor b \<Longrightarrow> A \<noteq> Actor c \<Longrightarrow> A \<noteq> Actor d
 120           \<Longrightarrow> indistinguishable A _ (Encrypted a b _) (Encrypted c d _)"
 121       | "indistinguishable A Ms m m'
 122           \<Longrightarrow> indistinguishable A Ms (Encrypted a b m) (Encrypted a b m')"
 123       | "indistinguishable A Ms m m'
 124           \<Longrightarrow> indistinguishable A Ms (MessageList ms) (MessageList ms')
 125           \<Longrightarrow> indistinguishable A Ms
 126                 (MessageList (m # ms))
 127                 (MessageList (m' # ms'))"
 128
 129 lemma indistinguishable_symmetric:
 130   "indistinguishable A Ms m m' \<Longrightarrow> indistinguishable A Ms m' m"
 131 proof (induction rule: indistinguishable.induct)
 132   fix Ms m m'
 133   show "indistinguishable CommunicationLayer Ms m m'" by rule
 134   fix A
 135   show "indistinguishable A Ms m m" by rule
 136   fix a b c
 137   assume "\<not> constructible a Ms m'" and "\<not> constructible a Ms m"
 138   thus "indistinguishable (Actor a) Ms (Signature c m') (Signature b m)" by rule
 139 next
 140   fix A Ms m m' a
 141   assume "indistinguishable A Ms m' m"
 142   thus "indistinguishable A Ms (Signature a m') (Signature a m)" by rule
 143 next
 144   fix A Ms m m' a b c d
 145   assume "A \<noteq> Actor c" and "A \<noteq> Actor d" and "A \<noteq> Actor a" and "A \<noteq> Actor b"
 146   thus "indistinguishable A Ms (Encrypted c d m') (Encrypted a b m)" by rule
 147 next
 148   fix A Ms m m' a b
 149   assume "indistinguishable A Ms m' m"
 150   thus "indistinguishable A Ms (Encrypted a b m') (Encrypted a b m)" by rule
 151 next
 152   fix A Ms m m' ms ms'
 153   assume  "indistinguishable A Ms m' m"
 154     and   "indistinguishable A Ms (MessageList ms') (MessageList ms)"
 155   thus "indistinguishable A Ms (MessageList (m' # ms')) (MessageList (m # ms))"
 156     by rule
 157 qed
 158
 159 definition indistinguishability_map ::
 160   "agent \<Rightarrow> message set \<Rightarrow> (message \<Rightarrow> message) \<Rightarrow> bool" where
 161     "indistinguishability_map A Ms f
 162       \<longleftrightarrow> bij f
 163         \<and> (\<forall> m. indistinguishable A Ms m (f m)
 164               \<and> (\<forall> a b. (A = Actor a \<and> constructible a Ms m
 165                           \<longrightarrow> f (Signature b m) = Signature b (f m)
 166                         )
 167                       \<and> (A = Actor a \<or> A = Actor b
 168                           \<longrightarrow> f (Encrypted a b m) = Encrypted a b (f m)
 169                         )
 170                 )
 171           )
 172         \<and> (A \<noteq> CommunicationLayer
 173             \<longrightarrow> (\<forall> ms. f (MessageList ms) = MessageList (map f ms))
 174           )"
 175
 176 lemma learnable_indistinguishability_map:
 177   assumes im: "indistinguishability_map (Actor a) Ms f"
 178   shows "learnable a M m \<Longrightarrow> learnable a (f M) (f m)"
 179 proof (induction rule: learnable.induct)
 180   show "learnable a (f M) (f M)" by rule
 181   fix b m
 182   assume "learnable a (f M) (f (Encrypted a b m))"
 183   moreover
 184     from im have "f (Encrypted a b m) = Encrypted a b (f m)"
 185       by (unfold indistinguishability_map_def) simp
 186   ultimately show "learnable a (f M) (f m)" by (metis encrypted1_learnable)
 187 next
 188   fix b m
 189   assume "learnable a (f M) (f (Encrypted b a m))"
 190   moreover
 191     from im have "f (Encrypted b a m) = Encrypted b a (f m)"
 192       by (unfold indistinguishability_map_def) simp
 193   ultimately show "learnable a (f M) (f m)" by (metis encrypted2_learnable)
 194 next
 195   fix m ms
 196   assume  minms: "m \<in> set ms"
 197     and   learnablefms: "learnable a (f M) (f (MessageList ms))"
 198   from minms have fminfms: "f m \<in> set (map f ms)" by simp
 199   from im have "f (MessageList ms) = MessageList (map f ms)"
 200     by (unfold indistinguishability_map_def) simp
 201   with fminfms and learnablefms show "learnable a (f M) (f m)"
 202     by (metis listed_learnable)
 203 qed
 204
 205 lemma indistinguishable_message_type:
 206   "indistinguishable (Actor a) Ms m m' \<Longrightarrow> type_of_message m = type_of_message m'"
 207 proof (induction rule: indistinguishable.cases)
 208   assume "Actor a = CommunicationLayer"
 209   thus "type_of_message m = type_of_message m'" ..
 210 next
 211   fix n
 212   assume "m = n" and "m' = n"
 213   thus "type_of_message m = type_of_message m'" by simp
 214 next
 215   fix b c n n'
 216   assume "m = Signature b n" and "m' = Signature c n'"
 217   thus "type_of_message m = type_of_message m'" by simp
 218   thus "type_of_message m = type_of_message m'" .
 219 next
 220   fix b c d e n n'
 221   assume "m = Encrypted b c n" and "m' = Encrypted d e n'"
 222   thus "type_of_message m = type_of_message m'" by simp
 223   thus "type_of_message m = type_of_message m'" .
 224 next
 225   fix n ns n' ns'
 226   assume "m = MessageList (n # ns)" and "m' = MessageList (n' # ns')"
 227   thus "type_of_message m = type_of_message m'" by simp
 228 qed
 229
 230 lemma learnable_inverse_indistinguishability_map:
 231   assumes im: "indistinguishability_map (Actor a) Ms f"
 232   shows "learnable a M m \<Longrightarrow> learnable a (inv f M) (inv f m)"
 233 proof (induction rule: learnable.induct)
 234   from im have bij: "bij f" unfolding indistinguishability_map_def ..
 235   { show "learnable a (inv f M) (inv f M)" by rule
 236     fix b m
 237     assume "learnable a (inv f M) (inv f (Encrypted a b m))"
 238     moreover
 239       { from im have "f (Encrypted a b (inv f m)) = Encrypted a b (f (inv f m))"
 240           by (unfold indistinguishability_map_def) simp
 241         also from bij have "\<dots> = Encrypted a b m" by simp
 242         finally have "inv f (Encrypted a b m) = Encrypted a b (inv f m)"
 243           by (simp add: bij)
 244       }
 245     ultimately have "learnable a (inv f M) (Encrypted a b (inv f m))" by simp
 246     thus "learnable a (inv f M) (inv f m)" by rule
 247   next
 248     fix b m
 249     assume "learnable a (inv f M) (inv f (Encrypted b a m))"
 250     moreover
 251       { from im have "f (Encrypted b a (inv f m)) = Encrypted b a (f (inv f m))"
 252           by (unfold indistinguishability_map_def) simp
 253         also from bij have "\<dots> = Encrypted b a m" by simp
 254         finally have "inv f (Encrypted b a m) = Encrypted b a (inv f m)"
 255           by (simp add: bij)
 256       }
 257     ultimately have "learnable a (inv f M) (Encrypted b a (inv f m))" by simp
 258     thus "learnable a (inv f M) (inv f m)" by rule
 259   next
 260     fix m ms
 261     assume  minms: "m \<in> set ms"
 262       and   learnableinvfms: "learnable a (inv f M) (inv f (MessageList ms))"
 263     from minms have invfmininvfms: "inv f m \<in> set (map (inv f) ms)" by simp
 264     from im have
 265         "f (MessageList (map (inv f) ms)) = MessageList (map f (map (inv f) ms))"
 266       by (unfold indistinguishability_map_def) simp
 267     also from bij have "\<dots> = MessageList ms"
 268       by (subst bij_map_f_map_inv_f) simp_all
 269     finally have "inv f (MessageList ms) = MessageList (map (inv f) ms)"
 270       by (simp add: bij)
 271     with invfmininvfms and learnableinvfms show "learnable a (inv f M) (inv f m)"
 272       by (metis listed_learnable)
 273   }
 274 qed
 275
 276 type_synonym encrypted_message_data = "actor \<times> actor \<times> message"
 277 type_synonym
 278   encrypted_message_map = "encrypted_message_data \<Rightarrow> encrypted_message_data"
 279
 280 subsection {* Events *}
 281 type_synonym payment = nat
 282
 283 datatype_new event
 284   = Construct actor message   -- {* an actor constructs a message *}
 285   | Send actor actor message  -- {* send a message from one actor to another *}
 286   | Receive actor message     -- {* an actor receives a message *}
 287   | Pay
 288       actor         -- {* payer *}
 289       actor         -- {* payee *}
 290       payment       -- {* specifies amount and manner of payment *}
 291       nat           -- {* payment id, intended to be unique to payer/payee pair*}
 292
 293 text {* Given a set of past events, which messages has a particular actor received? *}
 294 definition messages_received :: "actor \<Rightarrow> event set \<Rightarrow> message set"
 295   where "messages_received a es = {m. Receive a m \<in> es}"
 296
 297 text {* What can a particular agent do, given a set of past events and a set of
 298         concurrent events? *}
 299 inductive doable :: "agent \<Rightarrow> event set \<Rightarrow> event set \<Rightarrow> event \<Rightarrow> bool"
 300   where communicationLayer_transmit_doable:
 301           "(Send _ _ m) \<in> es \<Longrightarrow> doable CommunicationLayer es _ (Receive _ m)"
 302           -- {* the communication layer can cause anyone to receive any message
 303                 previously sent by anyone to anyone *}
 304       | construct_actor_name: "doable (Actor a) _ _ (Construct a (ActorName _))"
 305           -- {* an actor can construct any actor's name *}
 306       | construct_number: "doable (Actor a) _ _ (Construct a (Number _))"
 307           -- {* an actor can construct any number *}
 308       | construct_signature:
 309           "Construct a m \<in> es \<union> es'
 310             \<Longrightarrow> doable (Actor a) es es' (Construct a (Signature a m))"
 311           -- {* an actor can construct their own signature for a message they've
 312                 constructed *}
 313       | construct_encrypted:
 314           "Construct a m \<in> es \<union> es'
 315             \<Longrightarrow> doable (Actor a) es es' (Construct a (Encrypted _ _ m))"
 316           -- {* an actor can construct an encrypted version of a message they've
 317                 constructed *}
 318       | construct_list:
 319           "\<forall> m \<in> set ms. Construct a m \<in> es \<union> es'
 320             \<Longrightarrow> doable (Actor a) es es' (Construct a (MessageList ms))"
 321           -- {* an actor can construct a list of messages they've constructed *}
 322       | construct_received:
 323           "Receive a M \<in> es \<Longrightarrow> learnable a M m
 324           \<Longrightarrow> doable (Actor a) es _ (Construct a m)"
 325           -- {* an actor can construct a message they can learn from one they've
 326                 previously received *}
 327       | constructed_sendable:
 328           "Construct a m \<in> es \<union> es' \<Longrightarrow> doable (Actor a) es es' (Send a _ m)"
 329           -- {* an actor can send any message they've constructed *}
 330       | pay_doable: "doable (Actor a) _ _ (Pay a _ _ _)"
 331           -- {* an actor can always pay anyone any amount with any payment id *}
 332
 333 text {* Which agent must have caused a particular event? *}
 334 fun causal_agent :: "event \<Rightarrow> agent"
 335   where construct_cause: "causal_agent (Construct a _) = Actor a"
 336       | send_cause: "causal_agent (Send a _ _) = Actor a"
 337       | receive_cause: "causal_agent (Receive _ _) = CommunicationLayer"
 338       | pay_cause: "causal_agent (Pay a _ _ _) = Actor a"
 339
 340 text {* If an event is doable by an agent, then that agent must be the causal one *}
 341 lemma doable_implies_causal:
 342   assumes "doable a es es' e"
 343   shows "causal_agent e = a"
 344   using assms by (cases rule: doable.cases) simp_all
 345
 346 text {* Which events affect a particular agent? *}
 347 inductive affected_agent :: "agent \<Rightarrow> event \<Rightarrow> bool"
 348   where constructor_affected: "affected_agent (Actor a) (Construct a _)"
 349       | sender_affected: "affected_agent (Actor a) (Send a _ _)"
 350       | send_affects_communication:
 351           "affected_agent CommunicationLayer (Send _ _ _)"
 352       | receiver_affected: "affected_agent (Actor a) (Receive a _)"
 353       | receive_affects_communication:
 354           "affected_agent CommunicationLayer (Receive _ _)"
 355       | payer_affected: "affected_agent (Actor a) (Pay a _ _ _)"
 356       | payee_affected: "affected_agent (Actor a) (Pay _ a _ _)"
 357
 358 text {* The causal agent is always affected *}
 359 lemma causal_affected: "affected_agent (causal_agent e) e"
 360   by (cases rule: causal_agent.induct) (simp_all add: affected_agent.simps)
 361
 362 fun lift_message_map_event
 363   :: "(message \<Rightarrow> message) \<Rightarrow> event \<Rightarrow> event"
 364   where "lift_message_map_event f (Construct a m) = Construct a (f m)"
 365       | "lift_message_map_event f (Send a b m) = Send a b (f m)"
 366       | "lift_message_map_event f (Receive a m) = Receive a (f m)"
 367       | "lift_message_map_event _ e = e"
 368
 369 lemma sendable'_implies_sendable:
 370   assumes sendable': "Send a b M' \<in> image (lift_message_map_event f) es"
 371   shows "\<exists> M. f M = M' \<and> Send a b M \<in> es"
 372 proof -
 373   from sendable' obtain e
 374     where ein: "e \<in> es" and mape: "lift_message_map_event f e = Send a b M'"
 375       by auto
 376   from mape
 377     obtain M where esend: "e = Send a b M" and mapM: "f M = M'"
 378       by (cases e) simp_all
 379   from esend and ein have sendable: "Send a b M \<in> es" by simp
 380   from mapM and sendable show "\<exists> M. f M = M' \<and> Send a b M \<in> es" by auto
 381 qed
 382
 383 subsection {* Histories *}
 384 type_synonym time = nat
 385 type_synonym history = "(event \<times> time) set"
 386
 387 text {* What events occurred before a given time? *}
 388 definition events_before :: "history \<Rightarrow> time \<Rightarrow> event set" where
 389   "events_before h t = {e. \<exists> u < t. (e, u) \<in> h}"
 390
 391 text {* What events occurred at a given time? *}
 392 definition events_at :: "history \<Rightarrow> time \<Rightarrow> event set" where
 393   "events_at h t = {e. (e, t) \<in> h}"
 394
 395 abbreviation events_not_after :: "history \<Rightarrow> time \<Rightarrow> event set" where
 396   "events_not_after h t == events_before h t \<union> events_at h t"
 397
 398 text {* Which histories could possibly occur? *}
 399 definition possible_history :: "history \<Rightarrow> bool" where
 400   "possible_history h \<longleftrightarrow>
 401     (\<forall> (e, t) \<in> h. doable (causal_agent e) (events_before h t) (events_at h t) e)"
 402
 403 text {* What messages did a given agent receive before a given time? *}
 404 fun messages_received_before :: "agent \<Rightarrow> history \<Rightarrow> time \<Rightarrow> message set"
 405   where "messages_received_before CommunicationLayer _ _ = {}"
 406       | "messages_received_before (Actor a) h t
 407           = {m. Receive a m \<in> events_before h t}"
 408
 409 text {* What subhistory is relevant to a given agent before a given time? *}
 410 definition relevant_subhistory :: "agent \<Rightarrow> time \<Rightarrow> history \<Rightarrow> history" where
 411   "relevant_subhistory A t h = {(e, t') \<in> h. affected_agent A e \<and> t' < t}"
 412
 413 end