- Added more explanations.

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);
+