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) e) \<and> p h t es)
  21     )"
  22
  23 text {* Does a particular protocol allow or disallow different things based on
  24         information an agent doesn't possess?  The idea behind this definition is
  25         that if a set of events is permissible in one history, and another history
  26         is indistinguishable from the first by the relevant agent, then the
  27         equivalent set of events should also be permissible. *}
  28 definition non_clairvoyant :: "agent \<Rightarrow> protocol \<Rightarrow> bool" where
  29   "non_clairvoyant A p \<longleftrightarrow>
  30     (\<forall> h i f t es.  possible_history h
  31                   \<and> possible_history i
  32                   \<and> indistinguishability_map A f
  33                   \<and> {(apply_encrypted_message_map_event A f e, u) | e u.
  34                         u < t \<and> (e, u) \<in> h \<and> affected_agent A e}
  35                       = {(e, u). u < t \<and> (e, u) \<in> i \<and> affected_agent A e}
  36                   \<and> p h t es
  37       \<longrightarrow> p i t (image (apply_encrypted_message_map_event A f) es)
  38     )"
  39
  40 subsection {* Timely delivery protocol *}
  41 text {* Does the communication layer get messages from one specific actor to
  42         another specific actor within a specified time limit? *}
  43 type_synonym duration = time
  44 definition timely_delivery :: "actor \<Rightarrow> actor \<Rightarrow> duration \<Rightarrow> protocol" where
  45   "timely_delivery a b d h t es \<longleftrightarrow>
  46     (\<forall> (e, u) \<in> h. \<forall> m. u + d = t
  47                       \<and> e = Send a b m
  48                       \<and> \<not>(\<exists> v. u < v \<and> v < t \<and> (Receive b m, v) \<in> h)
  49       \<longrightarrow> Receive b m \<in> es
  50     )"
  51
  52 end