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   | Signed actor message          -- {* a message signed by an actor *}
  13   | Encrypted actor actor message -- {* a message encrypted for two actors *}
  14   | MessageList "message list"    -- {* a list of messages *}
  15
  16 text {* What can a particular actor learn from a particular message? *}
  17 inductive learnable :: "actor \<Rightarrow> message \<Rightarrow> message \<Rightarrow> bool" for a M
  18   where identity_learnable: "learnable a M M"
  19           -- {* the message itself *}
  20       | signed_learnable: "learnable a M (Signed _ m) \<Longrightarrow> learnable a M m"
  21           -- {* the body of a learnable signed message *}
  22       | encrypted1_learnable: "learnable a M (Encrypted a _ m) \<Longrightarrow> learnable a M m"
  23       | encrypted2_learnable: "learnable a M (Encrypted _ a m) \<Longrightarrow> learnable a M m"
  24           -- {* the body of a learnable message encrypted for the actor *}
  25       | listed_learnable:
  26           "m \<in> set l \<Longrightarrow> learnable a M (MessageList l) \<Longrightarrow> learnable a M m"
  27           -- {* any element of a learnable list of messages *}
  28
  29 text {* What messages can a particular actor construct from a particular set of
  30         messages? *}
  31 inductive constructible :: "actor \<Rightarrow> message set \<Rightarrow> message \<Rightarrow> bool" for a Ms
  32   where learnable_constructible:
  33           "M \<in> Ms \<Longrightarrow> learnable a M m \<Longrightarrow> constructible a Ms m"
  34           -- {* any message learnable from any message in the set *}
  35       | actorName_constructible: "constructible a Ms (ActorName _)"
  36           -- {* any actor's name *}
  37       | number_constructible: "constructible a Ms (Number _)"
  38           -- {* any number *}
  39       | signed_constructible:
  40           "constructible a Ms m \<Longrightarrow> constructible a Ms (Signed a m)"
  41           -- {* an otherwise constructible message, signed by this actor *}
  42       | encrypted_constructible:
  43           "constructible a Ms m \<Longrightarrow> constructible a Ms (Encrypted _ _ m)"
  44           -- {* an otherwise constructible message, encrypted to any pair of actors *}
  45       | listed_constructible:
  46           "(\<forall> m \<in> set l. constructible a Ms m)
  47             \<Longrightarrow> constructible a Ms (MessageList l)"
  48           -- {* a list of otherwise constructible messages *}
  49
  50 subsubsection {* Indistinguishability of encrypted messages *}
  51 datatype_new agent = CommunicationLayer | Actor actor
  52 type_synonym encrypted_message_data = "actor \<times> actor \<times> message"
  53 type_synonym
  54   encrypted_message_map = "encrypted_message_data \<Rightarrow> encrypted_message_data"
  55
  56 text {* For a particular agent, does a particular encrypted message map leave
  57         messages indistinguishable from what they meant originally? *}
  58 definition indistinguishability_map :: "agent \<Rightarrow> encrypted_message_map \<Rightarrow> bool"
  59   where "indistinguishability_map a f \<longleftrightarrow>
  60           bij f \<and> (\<forall> b c m. a = Actor b \<or> a = Actor c \<longrightarrow> f (b, c, m) = (b, c, m))"
  61
  62 text {* Apply an encrypted message map to a message, from a particular agent's
  63         point of view *}
  64 function apply_encrypted_message_map
  65   :: "agent \<Rightarrow> encrypted_message_map \<Rightarrow> message \<Rightarrow> message"
  66   where "apply_encrypted_message_map _ _ (ActorName a) = ActorName a"
  67       | "apply_encrypted_message_map _ _ (Number n) = Number n"
  68       | "apply_encrypted_message_map A f (Signed a m)
  69           = Signed a (apply_encrypted_message_map A f m)"
  70       | "A = Actor a \<or> A = Actor b
  71           \<Longrightarrow> apply_encrypted_message_map A f (Encrypted a b m)
  72               = Encrypted a b (apply_encrypted_message_map A f m)"
  73       | "A \<noteq> Actor a \<and> A \<noteq> Actor b
  74           \<Longrightarrow> apply_encrypted_message_map A f (Encrypted a b m)
  75               = Encrypted
  76                   (fst (f (a, b, m)))
  77                   (fst (snd (f (a, b, m))))
  78                   (snd (snd (f (a, b, m))))"
  79       | "apply_encrypted_message_map A f (MessageList ms)
  80           = MessageList (map (apply_encrypted_message_map A f) ms)"
  81   by auto (metis message.exhaust)
  82
  83 subsection {* Events *}
  84 datatype_new event
  85   = Send actor actor message  -- {* send a message from one actor to another *}
  86   | Receive actor message     -- {* an actor receives a message *}
  87   | Pay
  88       actor         -- {* payer *}
  89       actor         -- {* payee *}
  90       nat           -- {* specifies amount and manner of payment *}
  91       nat           -- {* payment id, intended to be unique to payer/payee pair*}
  92
  93 text {* What can a particular agent do, given a set of past events? *}
  94 inductive doable :: "agent \<Rightarrow> event set \<Rightarrow> event \<Rightarrow> bool"
  95   where communicationLayer_transmit_doable:
  96           "(Send _ _ m) \<in> es \<Longrightarrow> doable CommunicationLayer es (Receive _ m)"
  97           -- {* the communication layer can cause anyone to receive any message
  98                 sent by anyone to anyone *}
  99       | constructible_sendable:
 100           "constructible a {M. Receive a M \<in> es} m
 101             \<Longrightarrow> doable (Actor a) es (Send a _ m)"
 102           -- {* an actor can send any message they can construct from those they've
 103                 received *}
 104       | pay_doable: "doable (Actor a) _ (Pay a _ _ _)"
 105           -- {* an actor can always pay anyone any amount with any payment id *}
 106
 107 text {* Which agent must have caused a particular event? *}
 108 fun causal_agent :: "event \<Rightarrow> agent"
 109   where send_cause: "causal_agent (Send a _ _) = Actor a"
 110       | receive_cause: "causal_agent (Receive _ _) = CommunicationLayer"
 111       | pay_cause: "causal_agent (Pay a _ _ _) = Actor a"
 112
 113 text {* If an event is doable by an agent, then that agent must be the causal one *}
 114 lemma doable_implies_causal:
 115   assumes "doable a es e"
 116   shows "causal_agent e = a"
 117   using assms by (cases rule: doable.cases) simp_all
 118
 119 text {* Which events affect a particular agent? *}
 120 inductive affected_agent :: "agent \<Rightarrow> event \<Rightarrow> bool"
 121   where sender_affected: "affected_agent (Actor a) (Send a _ _)"
 122       | send_affects_communication:
 123           "affected_agent CommunicationLayer (Send _ _ _)"
 124       | receiver_affected: "affected_agent (Actor a) (Receive a _)"
 125       | receive_affects_communication:
 126           "affected_agent CommunicationLayer (Receive _ _)"
 127       | payer_affected: "affected_agent (Actor a) (Pay a _ _ _)"
 128       | payee_affected: "affected_agent (Actor a) (Pay _ a _ _)"
 129
 130 text {* The causal agent is always affected *}
 131 lemma causal_affected: "affected_agent (causal_agent e) e"
 132   by (cases rule: causal_agent.induct) (simp_all add: affected_agent.simps)
 133
 134 fun apply_encrypted_message_map_event
 135   :: "agent \<Rightarrow> encrypted_message_map \<Rightarrow> event \<Rightarrow> event"
 136   where "apply_encrypted_message_map_event A f (Send a b m)
 137           = Send a b (apply_encrypted_message_map A f m)"
 138       | "apply_encrypted_message_map_event A f (Receive a m)
 139           = Receive a (apply_encrypted_message_map A f m)"
 140       | "apply_encrypted_message_map_event _ _ e = e"
 141
 142 subsection {* Histories *}
 143 type_synonym time = nat
 144 type_synonym history = "(event \<times> time) set"
 145
 146 text {* Which histories could possibly occur? *}
 147 definition possible_history :: "history \<Rightarrow> bool" where
 148   "possible_history h \<longleftrightarrow>
 149     (\<forall> (e, t) \<in> h. doable (causal_agent e) {f. \<exists> u < t. (f, u) \<in> h} e)"
 150
 151 end