diff --git a/analysis/config.mpv b/analysis/config.mpv index 5fed8df..4f7deea 100644 --- a/analysis/config.mpv +++ b/analysis/config.mpv @@ -88,6 +88,18 @@ set verboseCompleted=VERBOSE. #define SES_EV(...) #endif +#if COOKIE_EVENTS +#define COOKIE_EV(...) __VA_ARGS__ +#else +#define COOKIE_EV(...) +#endif + +#if KEM_EVENTS +#define KEM_EV(...) __VA_ARGS__ +#else +#define KEM_EV(...) +#endif + (* TODO: Authentication timing properties *) (* TODO: Proof that every adversary submitted package is equivalent to one generated by the proper algorithm using different coins. This probably requires introducing an oracle that extracts the coins used and explicitly adding the notion of coins used for Packet->Packet steps and an inductive RNG notion. *)