Require Export Crypto.


Section AuthMsg.

  Context { pd  : @Data }.
  Context { pk  : @Key }.
  Context { pn  : @Node }.
  Context { pat : AuthTok }.
  Context { paf : @AuthFun pn pk pat pd }.

  (* from the data we should be able to extract some info like who send it *)
  Class DataAuth :=
    MkDataAuth
      {
        data_auth : name (* self *) -> data -> option name
      }.
  Context { pda : DataAuth }.

  Definition verify_authenticated_data_key (n : name) (m : AuthenticatedData) (k : receiving_key) : bool :=
    existsb (fun token => verify (am_data m) n k token) (am_auth m).

  Definition verify_authenticated_data_keys (n : name) (m : AuthenticatedData) (ks : receiving_keys) : bool :=
    existsb (verify_authenticated_data_key n m) ks.


  Definition verify_authenticated_data
             (slf  : name)
             (m    : AuthenticatedData)
             (keys : local_key_map) : bool :=
    match data_auth slf (am_data m) with
    | Some name => verify_authenticated_data_keys name m (lookup_receiving_keys keys name)
    | None => false
    end.

  Definition verify_one_auth_data
             (slf : name)
             (km  : local_key_map)
             (a   : AuthenticatedData) : bool :=
     verify_authenticated_data slf a km.

  Fixpoint verify_list_auth_data
           (slf : name)
           (km  : local_key_map)
           (l   : list AuthenticatedData) : bool :=
    match l with
    | [] => true
    | entry :: entries =>
      verify_one_auth_data slf km entry
      &&
      verify_list_auth_data slf km entries
    end.


End AuthMsg.
