diff --git a/spdl/problems-johanselst.spdl b/spdl/problems-johanselst.spdl
new file mode 100644
index 0000000..20e23ac
--- /dev/null
+++ b/spdl/problems-johanselst.spdl
@@ -0,0 +1,83 @@
+/* 
+ * Some authentication protocol
+ * 
+ * Version by Johan Selst. Seems to segfault at a simple -r4 execution
+ * with the modelchecker.
+ *
+ * Reported on 2005-05-11.
+ */
+
+// PKI infrastructure
+
+const pk: Function;
+secret sk: Function;
+inversekeys (pk,sk);
+
+// The protocol description
+
+protocol as3a(X, I, Y)
+{
+	role X
+	{
+		var nix: Nonce;
+
+		read_1(I, X, nix);
+		send_2(X, I, {I,nix}sk(X));
+	}
+
+	role I
+	{
+		const nix, niy: Nonce;
+
+		send_1(I, X, nix);
+		read_2(X, I, {I,nix}sk(X));
+		send_3(I, Y, niy);
+		read_4(Y, I, {niy,I}sk(Y));
+		claim_i1(I, Nisynch);
+	}	
+
+	role Y
+	{
+		var niy: Nonce;
+
+		read_3(I, Y, niy);
+		send_4(Y, I, {niy,I}sk(Y));
+	}
+}
+
+// The trusted agents in the system
+
+const Alice,Bob,Carol: Agent;
+
+// An untrusted agent, with leaked information
+
+const Eve: Agent;
+untrusted Eve;
+compromised sk(Eve);
+
+// The runs (only needed for the modelchecker algorithm)
+
+run as3a.X(Agent,Agent,Agent);
+run as3a.I(Agent,Agent,Agent);
+run as3a.Y(Agent,Agent,Agent);
+
+run as3a.X(Agent,Agent,Agent);
+run as3a.I(Agent,Agent,Agent);
+run as3a.Y(Agent,Agent,Agent);
+
+run as3a.X(Agent,Agent,Agent);
+run as3a.I(Agent,Agent,Agent);
+run as3a.Y(Agent,Agent,Agent);
+
+run as3a.X(Agent,Agent,Agent);
+run as3a.I(Agent,Agent,Agent);
+run as3a.Y(Agent,Agent,Agent);
+
+run as3a.X(Agent,Agent,Agent);
+run as3a.I(Agent,Agent,Agent);
+run as3a.Y(Agent,Agent,Agent);
+
+run as3a.X(Agent,Agent,Agent);
+run as3a.I(Agent,Agent,Agent);
+run as3a.Y(Agent,Agent,Agent);
+