fact: Definition HMAC_RKA_A : OracleComp (Bvector b * Bvector c) (Bvector c) bool := k_Out <--$ OC_Query _ (opad, iv); k_In <--$ OC_Query _ (ipad, iv); [b, _] <--$2 $ A _ _ (f_oracle GNMAC _ (Vector.append k_Out k_In)) tt; $ ret b.
imports: FCF PRF SplitVector HMAC_spec