Protocols.thy

   1 header {* Useful definitions for reasoning about protocols *}
   2 theory Protocols
   3 imports
   4   Main
   5   Communication
   6 begin
   7
   8 type_synonym protocol = "history \<Rightarrow> time \<Rightarrow> event set \<Rightarrow> bool"
   9
  10 text {* Has a particular agent satisfied a particular protocol at a particular time?
  11         *}
  12 definition satisfied_protocol_at :: "agent \<Rightarrow> protocol \<Rightarrow> history \<Rightarrow> time \<Rightarrow> bool"
  13   where "satisfied_protocol_at a p h t = p h t {e. (e, t) \<in> h \<and> causal_agent e = a}"
  14
  15 text {* If a particular agent has always satisfied a particular protocol in the
  16         past, is it always possible for them to continue to satisfy it now? *}
  17 definition continuously_satisfiable :: "agent \<Rightarrow> protocol \<Rightarrow> bool" where
  18   "continuously_satisfiable a p \<longleftrightarrow>
  19     (\<forall> h t. possible_history h \<and> (\<forall> u < t. satisfied_protocol_at a p h u)
  20       \<longrightarrow> (\<exists> es.  (\<forall> e \<in> es. doable a (events_before h t) (events_at h t) e)
  21                 \<and> p h t es)
  22     )"
  23
  24 text {* Does a particular protocol allow or disallow different things based on
  25         information an agent doesn't possess?  The idea behind this definition is
  26         that if a set of events is permissible in one history, and another history
  27         is indistinguishable from the first by the relevant agent, then the
  28         equivalent set of events should also be permissible. *}
  29 definition non_clairvoyant :: "agent \<Rightarrow> protocol \<Rightarrow> bool" where
  30   "non_clairvoyant A p \<longleftrightarrow>
  31     (\<forall> h h' f t es. possible_history h
  32                   \<and> possible_history h'
  33                   \<and> indistinguishability_map A (messages_received_before A h t) f
  34                   \<and> image (apfst (lift_message_map_event f))
  35                           (relevant_subhistory A t h)
  36                       = relevant_subhistory A t h'
  37                   \<and> p h t es
  38       \<longrightarrow> p h' t (image (lift_message_map_event f) es)
  39     )"
  40
  41 subsection {* Meet (conjunction) of protocols *}
  42 definition protocol_Meet :: "protocol set \<Rightarrow> protocol" where
  43   "protocol_Meet ps h t es = (\<forall> p \<in> ps. p h t es)"
  44
  45 theorem Meet_non_clairvoyant:
  46   assumes each_non_clairvoyant: "\<forall> p \<in> ps. non_clairvoyant A p"
  47   shows "non_clairvoyant A (protocol_Meet ps)"
  48 proof -
  49   { fix h h' f t es
  50     assume  hypotheses: "possible_history h
  51                   \<and> possible_history h'
  52                   \<and> indistinguishability_map A (messages_received_before A h t) f
  53                   \<and> image (apfst (lift_message_map_event f))
  54                           (relevant_subhistory A t h)
  55                       = relevant_subhistory A t h'"
  56       and   Meetsatisfied: "protocol_Meet ps h t es"
  57     have
  58       "protocol_Meet ps h' t (image (lift_message_map_event f) es)"
  59     proof -
  60       { fix p
  61         assume "p \<in> ps"
  62         with Meetsatisfied
  63           have satisfied: "p h t es" by (unfold protocol_Meet_def) auto
  64         from each_non_clairvoyant and `p \<in> ps`
  65           have "non_clairvoyant A p" ..
  66         with hypotheses and satisfied
  67           have satisfied':
  68                 "p h' t (image (lift_message_map_event f) es)"
  69             by (unfold non_clairvoyant_def) auto
  70       }
  71       thus
  72         "protocol_Meet ps h' t (image (lift_message_map_event f) es)"
  73           by (unfold protocol_Meet_def) auto
  74     qed
  75   }
  76   thus "non_clairvoyant A (protocol_Meet ps)" by (unfold non_clairvoyant_def) auto
  77 qed
  78
  79 subsection {* Timely delivery protocol *}
  80 text {* Does the communication layer get messages from one specific actor to
  81         another specific actor within a specified time limit? *}
  82 type_synonym duration = time
  83 definition timely_delivery :: "actor \<Rightarrow> actor \<Rightarrow> duration \<Rightarrow> protocol" where
  84   "timely_delivery a b d h t es \<longleftrightarrow>
  85     (\<forall> m s.  s + d = t
  86           \<and> (Send a b m, s) \<in> h
  87           \<and> \<not>(\<exists> r. s < r \<and> r < t \<and> (Receive b m, r) \<in> h)
  88       \<longrightarrow> Receive b m \<in> es
  89     )"
  90
  91 theorem timely_delivery_continuously_satisfiable:
  92   assumes "d > 0"
  93   shows "continuously_satisfiable CommunicationLayer (timely_delivery a b d)"
  94 proof -
  95   { fix h t
  96     let ?es = "{Receive b m | a b m u. u + d = t \<and> (Send a b m, u) \<in> h}"
  97     have "( \<forall> e \<in> ?es
  98               . doable CommunicationLayer (events_before h t) (events_at h t) e
  99           )
 100           \<and> timely_delivery a b d h t ?es"
 101     proof default+
 102       fix e
 103       assume "e \<in> ?es"
 104       then obtain a b m u
 105         where "e = Receive b m"
 106           and "u + d = t"
 107           and "(Send a b m, u) \<in> h"
 108             by auto
 109       from `d > 0` and `u + d = t` and `(Send a b m, u) \<in> h`
 110       have "Send a b m \<in> events_before h t"
 111         by (unfold events_before_def) (auto simp add: exI [of _ "t - d"])
 112       thus "doable CommunicationLayer (events_before h t) (events_at h t) e"
 113         by (unfold `e = Receive b m`) (rule communicationLayer_transmit_doable)
 114     next
 115       show "timely_delivery a b d h t ?es" by (unfold timely_delivery_def) auto
 116     qed
 117   }
 118   thus "continuously_satisfiable CommunicationLayer (timely_delivery a b d)"
 119     by (unfold continuously_satisfiable_def) blast
 120 qed
 121
 122 theorem timely_delivery_non_clairvoyant:
 123   assumes "d > 0"
 124   shows "non_clairvoyant CommunicationLayer (timely_delivery a b d)"
 125 proof -
 126   { fix h h' f t es
 127     assume  indistinguishable:
 128               "image (apfst (lift_message_map_event f))
 129                   (relevant_subhistory CommunicationLayer t h)
 130                 = relevant_subhistory CommunicationLayer t h'"
 131       and   timely: "timely_delivery a b d h t es"
 132     have "timely_delivery a b d h' t (image (lift_message_map_event f) es)"
 133     proof -
 134       { fix s m'
 135         assume  timeup: "s + d = t"
 136           and   sent': "(Send a b m', s) \<in> h'"
 137           and   notreceived': "\<not>(\<exists> r. s < r \<and> r < t \<and> (Receive b m', r) \<in> h')"
 138         from timeup and `d > 0` have "s < t" by simp
 139         with sent'
 140           have "(Send a b m', s) \<in> relevant_subhistory CommunicationLayer t h'"
 141             by (unfold relevant_subhistory_def)
 142                 (simp add: send_affects_communication)
 143         with indistinguishable
 144           obtain x
 145             where apfstx: "(Send a b m', s) = apfst (lift_message_map_event f) x"
 146               and xin: "x \<in> relevant_subhistory CommunicationLayer t h"
 147             by blast
 148         from apfstx have sndx: "snd x = s" by (rule apfst_convE) simp
 149         from apfstx
 150           have "Send a b m' = fst (apfst (lift_message_map_event f) x)"
 151             by (metis fst_conv)
 152         then obtain m
 153           where fstx: "fst x = Send a b m" and mapm: "f m = m'"
 154             by (cases "fst x") auto
 155         from fstx and sndx and xin have sent: "(Send a b m, s) \<in> h"
 156           by (unfold relevant_subhistory_def) auto
 157
 158         have notreceived: "\<not>(\<exists> r. s < r \<and> r < t \<and> (Receive b m, r) \<in> h)"
 159         proof
 160           assume "\<exists> r. s < r \<and> r < t \<and> (Receive b m, r) \<in> h"
 161           then obtain r
 162             where sr: "s < r"
 163               and rt: "r < t"
 164               and received: "(Receive b m, r) \<in> h"
 165                 by auto
 166           from rt and received
 167             have "(Receive b m, r) \<in> relevant_subhistory CommunicationLayer t h"
 168               by (unfold relevant_subhistory_def)
 169                   (simp add: receive_affects_communication)
 170           with indistinguishable
 171             have "apfst (lift_message_map_event f) (Receive b m, r)
 172                     \<in> relevant_subhistory CommunicationLayer t h'"
 173               by blast
 174           with mapm
 175             have "(Receive b m', r) \<in> h'"
 176               by (unfold relevant_subhistory_def) simp
 177           with sr and rt and notreceived' show False by simp
 178         qed
 179         with timely and timeup and sent have "Receive b m \<in> es"
 180           by (unfold timely_delivery_def) auto
 181         with mapm
 182           have "Receive b m' \<in> image (lift_message_map_event f) es" by force
 183       }
 184       thus "timely_delivery a b d h' t (image (lift_message_map_event f) es)"
 185         by (unfold timely_delivery_def) auto
 186     qed
 187   }
 188   thus "non_clairvoyant CommunicationLayer (timely_delivery a b d)"
 189     by (unfold non_clairvoyant_def) auto
 190 qed
 191
 192 subsection {* Self-encryption protocol *}
 193 text {* This protocol requires an actor who is constructing a new encrypted message
 194         to include themselves in the pair of actors who can decrypt it. *}
 195 definition self_encryption :: "actor \<Rightarrow> protocol" where
 196   "self_encryption a h t es = (
 197     \<forall> b c d m M.  a \<noteq> c
 198                 \<and> a \<noteq> d
 199                 \<and> learnable a M (Encrypted c d m)
 200                 \<and> Send a b M \<in> es
 201       \<longrightarrow> (\<exists> M'. learnable a M' (Encrypted c d m)
 202                 \<and> Receive a M' \<in> events_before h t
 203           )
 204   )"
 205
 206 theorem self_encryption_non_clairvoyant:
 207   "non_clairvoyant (Actor a) (self_encryption a)"
 208 proof -
 209   { fix h h' f t es
 210     assume  im: "indistinguishability_map
 211                   (Actor a) (messages_received_before (Actor a) h t) f"
 212       and   fsubhistory: "image (apfst (lift_message_map_event f))
 213                                 (relevant_subhistory (Actor a) t h)
 214                             = relevant_subhistory (Actor a) t h'"
 215       and   satisfied: "self_encryption a h t es"
 216     from im have bij: "bij f" unfolding indistinguishability_map_def ..
 217     have "self_encryption a h' t (image (lift_message_map_event f) es)"
 218     proof -
 219       { fix b c' d' n N
 220         assume  ac': "a \<noteq> c'"
 221           and   ad': "a \<noteq> d'"
 222           and   learnable': "learnable a N (Encrypted c' d' n)"
 223           and   sendable': "Send a b N \<in> image (lift_message_map_event f) es"
 224         from sendable' and sendable'_implies_sendable obtain M
 225           where mapM: "f M = N" and sendable: "Send a b M \<in> es"
 226             by blast
 227         from bij and mapM have mapN: "inv f N = M" by simp
 228         from im and learnable'
 229           have "learnable a (inv f N) (inv f (Encrypted c' d' n))"
 230             by (rule learnable_inverse_indistinguishability_map)
 231         hence "learnable a M (inv f (Encrypted c' d' n))"
 232           by (subst mapN [symmetric])
 233         moreover
 234           from im
 235             have "indistinguishable
 236                     (Actor a)
 237                     (messages_received_before (Actor a) h t)
 238                     (inv f (Encrypted c' d' n))
 239                     (f (inv f (Encrypted c' d' n)))"
 240               by (unfold indistinguishability_map_def) blast
 241           with bij
 242             have "type_of_message (inv f (Encrypted c' d' n)) = EncryptedType"
 243               by (simp add: indistinguishable_message_type)
 244           then obtain c and d and m
 245               where invfenccdn: "inv f (Encrypted c' d' n) = Encrypted c d m"
 246             by (induction rule: message.induct) auto
 247         ultimately have learnable: "learnable a M (Encrypted c d m)" by simp
 248         from bij and invfenccdn
 249           have fenccdm: "f (Encrypted c d m) = Encrypted c' d' n"
 250             by simp
 251         with im and ac' and ad' have "a \<noteq> c" and "a \<noteq> d"
 252           by (unfold indistinguishability_map_def) auto
 253         with satisfied and learnable and sendable
 254           obtain M' where learnableM': "learnable a M' (Encrypted c d m)"
 255                       and received: "Receive a M' \<in> events_before h t"
 256             by (unfold self_encryption_def) blast
 257         let ?N' = "f M'"
 258         from    learnableM'
 259             and fenccdm
 260             and im
 261             and learnable_indistinguishability_map
 262           have learnableN': "learnable a ?N' (Encrypted c' d' n)" by metis
 263         from received
 264           obtain t' where tt': "t' < t" and "(Receive a M', t') \<in> h"
 265             by (unfold events_before_def) auto
 266         hence "(Receive a M', t') \<in> relevant_subhistory (Actor a) t h"
 267           by (unfold relevant_subhistory_def) (simp add: receiver_affected)
 268         hence "apfst (lift_message_map_event f) (Receive a M', t')
 269               \<in> image (apfst (lift_message_map_event f))
 270                       (relevant_subhistory (Actor a) t h)"
 271           by (rule imageI)
 272         with fsubhistory and tt' have "Receive a ?N' \<in> events_before h' t"
 273           by (unfold events_before_def relevant_subhistory_def) auto
 274         with learnableN'
 275           have "\<exists> N'. learnable a N' (Encrypted c' d' n)
 276                     \<and> Receive a N' \<in> events_before h' t"
 277             by auto
 278       }
 279       thus "self_encryption a h' t (image (lift_message_map_event f) es)"
 280         by (unfold self_encryption_def) blast
 281     qed
 282   }
 283   thus "non_clairvoyant (Actor a) (self_encryption a)"
 284     by (unfold non_clairvoyant_def) auto
 285 qed
 286
 287 end