(* The macros used in this file are defined in examples/hpke/lib.authkem.ocvl *)

(** Key Encapsulation Mechanism **)
type keypairseed_t [bounded,large].
type kemseed_t [fixed,large].
type skey_t [bounded,large].
type pkey_t [bounded,large].
type kemkey_t [fixed,large].
type kemciph_t [fixed,large].
type AuthEncap_res_t [fixed,large].
proba P_pk_coll.
proba Adv_Outsider_CCA.

expand Authenticated_KEM(keypairseed_t, pkey_t, skey_t, kemseed_t, AuthEncap_res_t, AuthDecap_res_t, kemkey_t, kemciph_t, skgen, pkgen, GenerateKeyPair, AuthEncap, AuthEncap_r, AuthEncap_key_r, AuthEncap_enc_r, AuthEncap_tuple, AuthEncap_None, AuthDecap, AuthDecap_Some, AuthDecap_None, P_pk_coll).
expand Outsider_CCA_Secure_Authenticated_KEM(keypairseed_t, pkey_t, skey_t, kemseed_t, AuthEncap_res_t, AuthDecap_res_t, kemkey_t, kemciph_t, skgen, pkgen, GenerateKeyPair, AuthEncap, AuthEncap_r, AuthEncap_key, AuthEncap_enc, AuthEncap_tuple, AuthEncap_None, AuthDecap, AuthDecap_Some, AuthDecap_None, Adv_Outsider_CCA).

process 0