From 87e50259d3fcef83b1607569f333b25709d74ce3 Mon Sep 17 00:00:00 2001
From: Your Name <you@example.com>
Date: Mon, 22 Sep 2025 11:49:06 +0200
Subject: [PATCH] =?UTF-8?q?feat:=20neue=20Datentypen=20f=C3=BCr=20Nachrich?=
 =?UTF-8?q?ten=20und=20deren=20Eigenschaften=20hinzuf=C3=BCgen?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Co-authored-by: aider (gpt-4o) <aider@aider.chat>
---
 InductiveVerification.lean | 9 +++++++++
 1 file changed, 9 insertions(+)

diff --git a/InductiveVerification.lean b/InductiveVerification.lean
index c076509..06a9158 100644
--- a/InductiveVerification.lean
+++ b/InductiveVerification.lean
@@ -6,3 +6,12 @@ inductive Agent
   | Server : Agent
   | Friend : Nat → Agent
   | Spy : Agent
+
+inductive Msg
+  | Agent : Agent → Msg -- Agent names
+  | Number : Nat → Msg -- Ordinary integers, timestamps, ...
+  | Nonce : Nat → Msg -- Unguessable nonces
+  | Key : Key → Msg -- Crypto keys
+  | Hash : Msg → Msg -- Hashing
+  | MPair : Msg → Msg → Msg -- Compound messages
+  | Crypt : Key → Msg → Msg -- Encryption, public- or shared-key