Communication.thy

   1 header {* Communication layer *}
   2 theory Communication
   3 imports Main
   4 begin
   5
   6 type_synonym actor = nat
   7 datatype_new agent = CommunicationLayer | Actor actor
   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 datatype_new event
  17   = Send actor actor message  -- {* send a message from one actor to another *}
  18   | Receive actor message     -- {* an actor receives a message *}
  19   | Pay
  20       actor         -- {* payer *}
  21       actor         -- {* payee *}
  22       nat           -- {* specifies amount and manner of payment *}
  23       nat           -- {* payment id, intended to be unique to payer/payee pair*}
  24
  25 inductive learnable :: "actor \<Rightarrow> event set \<Rightarrow> message \<Rightarrow> bool" for a E
  26   where received: "Receive a m \<in> E \<Longrightarrow> learnable a E m"
  27       | signed: "learnable a E (Signed _ m) \<Longrightarrow> learnable a E m"
  28       | encrypted1: "learnable a E (Encrypted a _ m) \<Longrightarrow> learnable a E m"
  29       | encrypted2: "learnable a E (Encrypted _ a m) \<Longrightarrow> learnable a E m"
  30       | listed: "m \<in> set l \<Longrightarrow> learnable a E (MessageList l) \<Longrightarrow> learnable a E m"
  31
  32 end