RTTP.thy

   1 header {* Responsible Trust Traversal Protocol *}
   2 theory RTTP
   3 imports
   4   Main
   5   Communication
   6   Protocols
   7 begin
   8
   9 inductive signatures_for_complete_agreement
  10   :: "nat \<Rightarrow> message list \<Rightarrow> message list \<Rightarrow> message list \<Rightarrow> bool" for i
  11   where "signatures_for_complete_agreement i [] [m] []"
  12       | "signatures_for_complete_agreement i as (m' # ms) sigs
  13         \<Longrightarrow> signatures_for_complete_agreement
  14                 i
  15                 ((ActorName a) # as)
  16                 (m # m' # ms)
  17                 ((Signature a (MessageList [Number i, m, m'])) # sigs)"
  18
  19 fun complete_agreement :: "message \<Rightarrow> bool" where
  20   "complete_agreement
  21     ( MessageList
  22       [ Number i
  23       , MessageList as
  24       , MessageList ps
  25       , MessageList sigs
  26       ]
  27     )
  28     \<longleftrightarrow> distinct as
  29       \<and> list_all (\<lambda> p. type_of_message p = EncryptedType) ps
  30       \<and> signatures_for_complete_agreement i as (last ps # ps) sigs"
  31   | "complete_agreement _ = False"
  32
  33 definition rttp_promises
  34   :: "actor
  35   \<Rightarrow> (actor \<Rightarrow> duration)
  36   \<Rightarrow> (actor \<Rightarrow> payment \<Rightarrow> actor \<Rightarrow> payment \<Rightarrow> bool)
  37   \<Rightarrow> protocol"
  38   where "rttp_promises a d w h t es
  39     \<longleftrightarrow> ( \<forall> i b a' m a'' c m'
  40               . Construct a
  41                   ( Signature a
  42                     ( MessageList
  43                       [ Number i
  44                       , Encrypted b a' m
  45                       , Encrypted a'' c m'
  46                       ]
  47                     )
  48                   )
  49                 \<in> es
  50             \<longrightarrow> a' = a
  51               \<and> a'' = a
  52               \<and> ( \<exists> t x t' y
  53                     . m = MessageList [Number t, Number x]
  54                     \<and> m' = MessageList [Number t', Number y]
  55                     \<and> t' + d b < t
  56                     \<and> w b x c y
  57                 )
  58               \<and> ( \<forall> b' M c' M'
  59                       . Construct a
  60                           ( Signature a
  61                             ( MessageList
  62                               [ Number i
  63                               , Encrypted b' a M
  64                               , Encrypted a c' M'
  65                               ]
  66                             )
  67                           )
  68                         \<in> events_before h t \<union> es
  69                     \<longrightarrow> c' = c \<and> M' = m'
  70                 )
  71         )"
  72
  73 end