Require Export Node.


Section Crypto.

  Context { n  : @Node }.

  Class Key :=
    MkKey
      {
        sending_key   : Set;
        receiving_key : Set;
      }.
  Context { pk : Key }.

  Definition sending_keys   := list sending_key.
  Definition receiving_keys := list receiving_key.

  (* "directed sending key" *)
  Record DSKey :=
    MkDSKey
      {
        dsk_dst : list name;  (* destinations *)
        dsk_key : sending_key (* key *)
      }.

  (* "directed receiving key" *)
  Record DRKey :=
    MkDRKey
      {
        drk_dst : list name;    (* sources *)
        drk_key : receiving_key (* key *)
      }.

  Record local_key_map : Set :=
    MkLocalKeyMap
    {
      lkm_sending_keys   : list DSKey;
      lkm_receiving_keys : list DRKey;
    }.

  Definition key_map := name (* Src *) -> local_key_map.


  Definition lookup_dskeys (km : local_key_map) (h : name) : list DSKey :=
    filter
      (fun dk => if in_dec name_dec h (dsk_dst dk) then true else false)
      (lkm_sending_keys km).

  Definition lookup_drkeys (km : local_key_map) (h : name) : list DRKey :=
    filter
      (fun dk => if in_dec name_dec h (drk_dst dk) then true else false)
      (lkm_receiving_keys km).

  Definition lookup_receiving_keys (km : local_key_map) (h : name) : list receiving_key :=
    map drk_key (lookup_drkeys km h).

  (* This is used to state that we can at least try to verify messages from nodes *)
  Definition has_receiving_key (km : local_key_map) (h : name) : Prop :=
    lookup_drkeys km h <> [].

  (* This says that if the source has a key for sending messages to [n] then the
     destination also has that key.
     We use this in sent_byz to talk about leaked keys.
     ---The sending keys are the ones that are supposed to be private *)
  Definition got_key_for (n : name) (kmsrc kmdst : local_key_map) : Prop :=
    exists k,
      In k (map dsk_key (lookup_dskeys kmsrc n))
      /\ In k (map dsk_key (lookup_dskeys kmdst n)).

  Class AuthTok :=
    MkAuthTok
      {
        Token     :> Set;
        Token_dec : Deq Token;
      }.
  Context { authtok : AuthTok }.

  Definition Tokens := list Token.

  Lemma Tokens_dec : Deq Tokens.
  Proof.
    introv.
    apply list_eq_dec; auto.
    apply Token_dec.
  Qed.


  (* NOTE: message = data + MAC (i.e. crypto data ) *)
  Class Data := MkData { data : Set }.
  Context { pd : Data }.

  Class AuthFun :=
    MkAuthFun
      {
        create : data -> sending_keys -> Tokens;
        verify : data -> name -> receiving_key -> Token -> bool;
      }.
  Context { authfun : AuthFun }.

  (* we might want a more fine grain function that only uses the keys meant for the
     intended recipient *)
  Definition authenticate
             (d   : data)
             (km  : local_key_map) : Tokens :=
    create d (map dsk_key (lkm_sending_keys km)).

  Record AuthenticatedData :=
    MkAuthData
      {
        am_data   :> data;
        am_auth   : Tokens
      }.

End Crypto.
