From e14fc12f88c10e3d77ef98387ff049bda84f53c7 Mon Sep 17 00:00:00 2001
From: Benjamin Lipp <blipp@rosenpass.eu>
Date: Mon, 1 Dec 2025 15:11:10 +0100
Subject: [PATCH] fix: add missing defines for 04_dos model

The newly (re-)added lines come from this pull request: https://github.com/rosenpass/rosenpass/pull/230
---
 analysis/config.mpv | 12 ++++++++++++
 1 file changed, 12 insertions(+)

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. *)