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