Communication.thy

   1 header {* Communication layer *}
   2 theory Communication
   3 imports Main
   4 begin
   5
   6 subsection {* Messages *}
   7 type_synonym actor = nat
   8
   9 datatype_new message
  10   = ActorName actor               -- {* specify an actor *}
  11   | Number nat                    -- {* arbitrary data, as a natural number *}
  12   | Signature actor message       -- {* an actor's signature for a message *}
  13   | Encrypted actor actor message -- {* a message encrypted for two actors *}
  14   | MessageList "message list"    -- {* a list of messages *}
  15
  16 datatype_new message_type
  17   = ActorNameType
  18   | NumberType
  19   | SignatureType
  20   | EncryptedType
  21   | MessageListType
  22
  23 fun type_of_message :: "message \<Rightarrow> message_type"
  24   where "type_of_message (ActorName _) = ActorNameType"
  25       | "type_of_message (Number _) = NumberType"
  26       | "type_of_message (Signature _ _) = SignatureType"
  27       | "type_of_message (Encrypted _ _ _) = EncryptedType"
  28       | "type_of_message (MessageList _) = MessageListType"
  29
  30 text {* What are the components of a message, from an omniscient point of view? *}
  31 inductive contains_message :: "message \<Rightarrow> message \<Rightarrow> bool"
  32   where contains_message_self: "contains_message M M"
  33       | contains_message_encrypted:
  34           "contains_message M (Encrypted _ _ m) \<Longrightarrow> contains_message M m"
  35       | contains_message_list:
  36           "m \<in> set ms \<Longrightarrow> contains_message M (MessageList ms)
  37             \<Longrightarrow> contains_message M m"
  38
  39 text {* What can a particular actor learn from a particular message? *}
  40 inductive learnable :: "actor \<Rightarrow> message \<Rightarrow> message \<Rightarrow> bool" for a M
  41   where identity_learnable: "learnable a M M"
  42           -- {* the message itself *}
  43       | encrypted1_learnable: "learnable a M (Encrypted a _ m) \<Longrightarrow> learnable a M m"
  44       | encrypted2_learnable: "learnable a M (Encrypted _ a m) \<Longrightarrow> learnable a M m"
  45           -- {* the body of a learnable message encrypted for the actor *}
  46       | listed_learnable:
  47           "m \<in> set l \<Longrightarrow> learnable a M (MessageList l) \<Longrightarrow> learnable a M m"
  48           -- {* any element of a learnable list of messages *}
  49
  50 text {* What messages can a particular actor construct from a particular set of
  51         messages? *}
  52 inductive constructible :: "actor \<Rightarrow> message set \<Rightarrow> message \<Rightarrow> bool" for a Ms
  53   where learnable_constructible:
  54           "M \<in> Ms \<Longrightarrow> learnable a M m \<Longrightarrow> constructible a Ms m"
  55           -- {* any message learnable from any message in the set *}
  56       | actorName_constructible: "constructible a Ms (ActorName _)"
  57           -- {* any actor's name *}
  58       | number_constructible: "constructible a Ms (Number _)"
  59           -- {* any number *}
  60       | signed_constructible:
  61           "constructible a Ms m \<Longrightarrow> constructible a Ms (Signature a m)"
  62           -- {* an otherwise constructible message, signed by this actor *}
  63       | encrypted_constructible:
  64           "constructible a Ms m \<Longrightarrow> constructible a Ms (Encrypted _ _ m)"
  65           -- {* an otherwise constructible message, encrypted to any pair of actors *}
  66       | listed_constructible:
  67           "(\<forall> m \<in> set l. constructible a Ms m)
  68             \<Longrightarrow> constructible a Ms (MessageList l)"
  69           -- {* a list of otherwise constructible messages *}
  70
  71 subsubsection {* Indistinguishability of messages *}
  72 datatype_new agent = CommunicationLayer | Actor actor
  73
  74 text {* What pairs of messages should we not expect a particular agent to be able
  75         to distinguish between, given a particular set of messages to work from?
  76         This definition isn't intended to express a limit on what an attacker might
  77         be able to do; rather, it's meant to limit what we might reasonably expect
  78         an honest agent to be able to do without resorting to sophisticated
  79         cryptanalysis or anything similarly difficult. *}
  80 inductive indistinguishable :: "agent \<Rightarrow> message set \<Rightarrow> message \<Rightarrow> message \<Rightarrow> bool"
  81   where "indistinguishable CommunicationLayer _ _ _"
  82       | "indistinguishable _ _ m m"
  83       | "\<not> constructible a Ms m \<Longrightarrow> \<not> constructible a Ms m'
  84           \<Longrightarrow> indistinguishable (Actor a) Ms (Signature _ m) (Signature _ m')"
  85       | "indistinguishable A Ms m m'
  86           \<Longrightarrow> indistinguishable A Ms (Signature a m) (Signature a m')"
  87       | "A \<noteq> Actor a \<Longrightarrow> A \<noteq> Actor b \<Longrightarrow> A \<noteq> Actor c \<Longrightarrow> A \<noteq> Actor d
  88           \<Longrightarrow> indistinguishable A _ (Encrypted a b _) (Encrypted c d _)"
  89       | "indistinguishable A Ms m m'
  90           \<Longrightarrow> indistinguishable A Ms (Encrypted a b m) (Encrypted a b m')"
  91       | "indistinguishable A Ms m m'
  92           \<Longrightarrow> indistinguishable A Ms (MessageList ms) (MessageList ms')
  93           \<Longrightarrow> indistinguishable A Ms
  94                 (MessageList (m # ms))
  95                 (MessageList (m' # ms'))"
  96
  97 lemma indistinguishable_symmetric:
  98   "indistinguishable A Ms m m' \<Longrightarrow> indistinguishable A Ms m' m"
  99 proof (induction rule: indistinguishable.induct)
 100   fix Ms m m'
 101   show "indistinguishable CommunicationLayer Ms m m'" by rule
 102   fix A
 103   show "indistinguishable A Ms m m" by rule
 104   fix a b c
 105   assume "\<not> constructible a Ms m'" and "\<not> constructible a Ms m"
 106   thus "indistinguishable (Actor a) Ms (Signature c m') (Signature b m)" by rule
 107 next
 108   fix A Ms m m' a
 109   assume "indistinguishable A Ms m' m"
 110   thus "indistinguishable A Ms (Signature a m') (Signature a m)" by rule
 111 next
 112   fix A Ms m m' a b c d
 113   assume "A \<noteq> Actor c" and "A \<noteq> Actor d" and "A \<noteq> Actor a" and "A \<noteq> Actor b"
 114   thus "indistinguishable A Ms (Encrypted c d m') (Encrypted a b m)" by rule
 115 next
 116   fix A Ms m m' a b
 117   assume "indistinguishable A Ms m' m"
 118   thus "indistinguishable A Ms (Encrypted a b m') (Encrypted a b m)" by rule
 119 next
 120   fix A Ms m m' ms ms'
 121   assume  "indistinguishable A Ms m' m"
 122     and   "indistinguishable A Ms (MessageList ms') (MessageList ms)"
 123   thus "indistinguishable A Ms (MessageList (m' # ms')) (MessageList (m # ms))"
 124     by rule
 125 qed
 126
 127 definition indistinguishability_map ::
 128   "agent \<Rightarrow> message set \<Rightarrow> (message \<Rightarrow> message) \<Rightarrow> bool" where
 129     "indistinguishability_map A Ms f
 130       \<longleftrightarrow> bij f
 131         \<and> (\<forall> m. indistinguishable A Ms m (f m)
 132               \<and> (\<forall> a b. (A = Actor a \<and> constructible a Ms m
 133                           \<longrightarrow> f (Signature b m) = Signature b (f m)
 134                         )
 135                       \<and> (A = Actor a \<or> A = Actor b
 136                           \<longrightarrow> f (Encrypted a b m) = Encrypted a b (f m)
 137                         )
 138                 )
 139           )
 140         \<and> (A \<noteq> CommunicationLayer
 141             \<longrightarrow> (\<forall> ms. f (MessageList ms) = MessageList (map f ms))
 142           )"
 143
 144 lemma learnable_indistinguishability_map:
 145   assumes im: "indistinguishability_map (Actor a) Ms f"
 146   shows "learnable a M m \<Longrightarrow> learnable a (f M) (f m)"
 147 proof (induction rule: learnable.induct)
 148   show "learnable a (f M) (f M)" by rule
 149   fix b m
 150   assume "learnable a (f M) (f (Encrypted a b m))"
 151   moreover
 152     from im have "f (Encrypted a b m) = Encrypted a b (f m)"
 153       by (unfold indistinguishability_map_def) simp
 154   ultimately show "learnable a (f M) (f m)" by (metis encrypted1_learnable)
 155 next
 156   fix b m
 157   assume "learnable a (f M) (f (Encrypted b a m))"
 158   moreover
 159     from im have "f (Encrypted b a m) = Encrypted b a (f m)"
 160       by (unfold indistinguishability_map_def) simp
 161   ultimately show "learnable a (f M) (f m)" by (metis encrypted2_learnable)
 162 next
 163   fix m ms
 164   assume  minms: "m \<in> set ms"
 165     and   learnablefms: "learnable a (f M) (f (MessageList ms))"
 166   from minms have fminfms: "f m \<in> set (map f ms)" by simp
 167   from im have "f (MessageList ms) = MessageList (map f ms)"
 168     by (unfold indistinguishability_map_def) simp
 169   with fminfms and learnablefms show "learnable a (f M) (f m)"
 170     by (metis listed_learnable)
 171 qed
 172
 173 lemma indistinguishable_message_type:
 174   "indistinguishable (Actor a) Ms m m' \<Longrightarrow> type_of_message m = type_of_message m'"
 175 proof (induction rule: indistinguishable.cases)
 176   assume "Actor a = CommunicationLayer"
 177   thus "type_of_message m = type_of_message m'" ..
 178 next
 179   fix n
 180   assume "m = n" and "m' = n"
 181   thus "type_of_message m = type_of_message m'" by simp
 182 next
 183   fix b c n n'
 184   assume "m = Signature b n" and "m' = Signature c n'"
 185   thus "type_of_message m = type_of_message m'" by simp
 186   thus "type_of_message m = type_of_message m'" .
 187 next
 188   fix b c d e n n'
 189   assume "m = Encrypted b c n" and "m' = Encrypted d e n'"
 190   thus "type_of_message m = type_of_message m'" by simp
 191   thus "type_of_message m = type_of_message m'" .
 192 next
 193   fix n ns n' ns'
 194   assume "m = MessageList (n # ns)" and "m' = MessageList (n' # ns')"
 195   thus "type_of_message m = type_of_message m'" by simp
 196 qed
 197
 198 type_synonym encrypted_message_data = "actor \<times> actor \<times> message"
 199 type_synonym
 200   encrypted_message_map = "encrypted_message_data \<Rightarrow> encrypted_message_data"
 201
 202 subsection {* Events *}
 203 datatype_new event
 204   = Send actor actor message  -- {* send a message from one actor to another *}
 205   | Receive actor message     -- {* an actor receives a message *}
 206   | Pay
 207       actor         -- {* payer *}
 208       actor         -- {* payee *}
 209       nat           -- {* specifies amount and manner of payment *}
 210       nat           -- {* payment id, intended to be unique to payer/payee pair*}
 211
 212 text {* Given a set of past events, which messages has a particular actor received? *}
 213 definition messages_received :: "actor \<Rightarrow> event set \<Rightarrow> message set"
 214   where "messages_received a es = {m. Receive a m \<in> es}"
 215
 216 text {* What can a particular agent do, given a set of past events? *}
 217 inductive doable :: "agent \<Rightarrow> event set \<Rightarrow> event \<Rightarrow> bool"
 218   where communicationLayer_transmit_doable:
 219           "(Send _ _ m) \<in> es \<Longrightarrow> doable CommunicationLayer es (Receive _ m)"
 220           -- {* the communication layer can cause anyone to receive any message
 221                 sent by anyone to anyone *}
 222       | constructible_sendable:
 223           "constructible a (messages_received a es) m
 224             \<Longrightarrow> doable (Actor a) es (Send a _ m)"
 225           -- {* an actor can send any message they can construct from those they've
 226                 received *}
 227       | pay_doable: "doable (Actor a) _ (Pay a _ _ _)"
 228           -- {* an actor can always pay anyone any amount with any payment id *}
 229
 230 text {* Which agent must have caused a particular event? *}
 231 fun causal_agent :: "event \<Rightarrow> agent"
 232   where send_cause: "causal_agent (Send a _ _) = Actor a"
 233       | receive_cause: "causal_agent (Receive _ _) = CommunicationLayer"
 234       | pay_cause: "causal_agent (Pay a _ _ _) = Actor a"
 235
 236 text {* If an event is doable by an agent, then that agent must be the causal one *}
 237 lemma doable_implies_causal:
 238   assumes "doable a es e"
 239   shows "causal_agent e = a"
 240   using assms by (cases rule: doable.cases) simp_all
 241
 242 text {* Which events affect a particular agent? *}
 243 inductive affected_agent :: "agent \<Rightarrow> event \<Rightarrow> bool"
 244   where sender_affected: "affected_agent (Actor a) (Send a _ _)"
 245       | send_affects_communication:
 246           "affected_agent CommunicationLayer (Send _ _ _)"
 247       | receiver_affected: "affected_agent (Actor a) (Receive a _)"
 248       | receive_affects_communication:
 249           "affected_agent CommunicationLayer (Receive _ _)"
 250       | payer_affected: "affected_agent (Actor a) (Pay a _ _ _)"
 251       | payee_affected: "affected_agent (Actor a) (Pay _ a _ _)"
 252
 253 text {* The causal agent is always affected *}
 254 lemma causal_affected: "affected_agent (causal_agent e) e"
 255   by (cases rule: causal_agent.induct) (simp_all add: affected_agent.simps)
 256
 257 fun lift_message_map_event
 258   :: "(message \<Rightarrow> message) \<Rightarrow> event \<Rightarrow> event"
 259   where "lift_message_map_event f (Send a b m) = Send a b (f m)"
 260       | "lift_message_map_event f (Receive a m) = Receive a (f m)"
 261       | "lift_message_map_event _ e = e"
 262
 263 subsection {* Histories *}
 264 type_synonym time = nat
 265 type_synonym history = "(event \<times> time) set"
 266
 267 text {* Which histories could possibly occur? *}
 268 definition possible_history :: "history \<Rightarrow> bool" where
 269   "possible_history h \<longleftrightarrow>
 270     (\<forall> (e, t) \<in> h. doable (causal_agent e) {f. \<exists> u < t. (f, u) \<in> h} e)"
 271
 272 text {* What events occurred before a given time? *}
 273 definition events_before :: "history \<Rightarrow> time \<Rightarrow> event set" where
 274   "events_before h t = {e. \<exists> u < t. (e, u) \<in> h}"
 275
 276 text {* What messages did a given agent receive before a given time? *}
 277 fun messages_received_before :: "agent \<Rightarrow> history \<Rightarrow> time \<Rightarrow> message set"
 278   where "messages_received_before CommunicationLayer _ _ = {}"
 279       | "messages_received_before (Actor a) h t
 280           = {m. Receive a m \<in> events_before h t}"
 281
 282 text {* What subhistory is relevant to a given agent before a given time? *}
 283 definition relevant_subhistory :: "agent \<Rightarrow> time \<Rightarrow> history \<Rightarrow> history" where
 284   "relevant_subhistory A t h = {(e, t') \<in> h. affected_agent A e \<and> t' < t}"
 285
 286 end