From 89d7fd696a0f1a88feb4eb37ebec536bbb844f8d Mon Sep 17 00:00:00 2001
From: ccremers <ccremers@4f7d145f-a0d4-0310-ae10-d96cc04433c1>
Date: Fri, 15 Apr 2005 13:07:57 +0000
Subject: [PATCH] - Added more explanations.

---
 spdl/ns3.spdl | 18 +++++++++++++++++-
 1 file changed, 17 insertions(+), 1 deletion(-)

diff --git a/spdl/ns3.spdl b/spdl/ns3.spdl
index 26b3081..c957d2a 100644
--- a/spdl/ns3.spdl
+++ b/spdl/ns3.spdl
@@ -1,7 +1,15 @@
+/* 
+ * Needham-Schroeder protocol
+ */
+
+// PKI infrastructure
+
 const pk: Function;
 secret sk: Function;
 inversekeys (pk,sk);
 
+// The protocol description
+
 protocol ns3(I,R)
 {
 	role I
@@ -33,11 +41,19 @@ protocol ns3(I,R)
 	}
 }
 
-const Alice,Bob,Eve: Agent;
+// The agents in the system
 
+const Alice,Bob: Agent;
+
+// An untrusted agent, with leaked information
+
+const Eve: Agent;
 untrusted Eve;
 const ne: Nonce;
 compromised sk(Eve);
 
+// The runs (only needed for the modelchecker algorithm)
+
 run ns3.I(Agent,Agent);
 run ns3.R(Agent,Agent);
+