Require Export Process.


Section CorrectKeys.

  Context { pd  : @Data }.
  Context { pn  : @Node }.
  Context { pk  : @Key }.
  Context { pat : @AuthTok }.
  Context { paf : @AuthFun pn pk pat pd }.
  Context { pm  : @Msg }.
  Context { pda : @DataAuth pd pn }.
  Context { qc  : @Quorum_context pn }.
  Context { dtc : @DTimeContext }.
  Context { iot : @IOTrusted }.


  Local Open Scope eo.
  Local Open Scope proc.


  Definition AXIOM_correct_keys {S}
             (sm : MUSystem S)
             (K  : forall (n : node_type), S n -> local_key_map)
             (eo : EventOrdering) : Prop :=
    forall (e  : Event) (i : node_type) (s : S i) (e' : Event),
      node_has_correct_trace_before e i
      -> e' ≼ e
      -> loc e' = node2name i
      -> state_sm_before_event (sm i) e' = Some s
      -> keys e' = K i s.

End CorrectKeys.
