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 subsection {* Events *}
  51 datatype_new agent = CommunicationLayer | Actor actor
  52
  53 datatype_new event
  54   = Send actor actor message  -- {* send a message from one actor to another *}
  55   | Receive actor message     -- {* an actor receives a message *}
  56   | Pay
  57       actor         -- {* payer *}
  58       actor         -- {* payee *}
  59       nat           -- {* specifies amount and manner of payment *}
  60       nat           -- {* payment id, intended to be unique to payer/payee pair*}
  61
  62 text {* What can a particular agent do, given a set of past events? *}
  63 inductive doable :: "agent \<Rightarrow> event set \<Rightarrow> event \<Rightarrow> bool"
  64   where communicationLayer_transmit_doable:
  65           "(Send _ _ m) \<in> es \<Longrightarrow> doable CommunicationLayer es (Receive _ m)"
  66           -- {* the communication layer can cause anyone to receive any message
  67                 sent by anyone to anyone *}
  68       | constructible_sendable:
  69           "constructible a {M. Receive a M \<in> es} m
  70             \<Longrightarrow> doable (Actor a) es (Send a _ m)"
  71           -- {* an actor can send any message they can construct from those they've
  72                 received *}
  73       | pay_doable: "doable (Actor a) _ (Pay a _ _ _)"
  74           -- {* an actor can always pay anyone any amount with any payment id *}
  75
  76 text {* Which agent must have caused a particular event? *}
  77 fun causal_agent :: "event \<Rightarrow> agent"
  78   where send_cause: "causal_agent (Send a _ _) = Actor a"
  79       | receive_cause: "causal_agent (Receive _ _) = CommunicationLayer"
  80       | pay_cause: "causal_agent (Pay a _ _ _) = Actor a"
  81
  82 text {* If an event is doable by an agent, then that agent must be the causal one *}
  83 lemma doable_implies_causal:
  84   assumes "doable a es e"
  85   shows "causal_agent e = a"
  86   using assms by (cases rule: doable.cases) simp_all
  87
  88 text {* Which events affect a particular agent? *}
  89 inductive affected_agent :: "agent \<Rightarrow> event \<Rightarrow> bool"
  90   where sender_affected: "affected_agent (Actor a) (Send a _ _)"
  91       | send_affects_communication:
  92           "affected_agent CommunicationLayer (Send _ _ _)"
  93       | receiver_affected: "affected_agent (Actor a) (Receive a _)"
  94       | receive_affects_communication:
  95           "affected_agent CommunicationLayer (Receive _ _)"
  96       | payer_affected: "affected_agent (Actor a) (Pay a _ _ _)"
  97       | payee_affected: "affected_agent (Actor a) (Pay _ a _ _)"
  98
  99 text {* The causal agent is always affected *}
 100 lemma causal_affected: "affected_agent (causal_agent e) e"
 101   by (cases rule: causal_agent.induct) (simp_all add: affected_agent.simps)
 102
 103 subsection {* Histories *}
 104 type_synonym time = nat
 105 type_synonym history = "(event \<times> time) set"
 106
 107 text {* Which histories could possibly occur? *}
 108 definition possible_history :: "history \<Rightarrow> bool" where
 109   "possible_history h \<longleftrightarrow>
 110     (\<forall> (e, t) \<in> h. doable (causal_agent e) {f. \<exists> u < t. (f, u) \<in> h} e)"
 111
 112 end