proposition: Theorem GHMAC_2K_GNMAC_equiv : forall k ls, let (k_Out, k_In) := splitVector b b k in let k' := Vector.append (h iv k_Out) (h iv k_In) in GHMAC_2K k ls = GNMAC k' ls.
proof: Proof. intuition. unfold GHMAC_2K, HMAC_spec.GHMAC_2K, GNMAC, HMAC_spec.GNMAC, b, HMAC_spec.b. remember (splitVector (c + p) (c + p) k) as z. destruct z. rewrite splitVector_append. unfold app_fpad, hash_words. simpl. trivial. Qed.
imports: FCF PRF SplitVector HMAC_spec