diff --git a/spdl/splice-as.spdl b/spdl/splice-as.spdl
new file mode 100644
index 0000000..efef552
--- /dev/null
+++ b/spdl/splice-as.spdl
@@ -0,0 +1,58 @@
+const pk: Function;
+secret sk: Function;
+inversekeys (pk,sk);
+
+protocol spliceAS(C,AS,S)
+{
+        role C
+	{
+		const N1,N2: Nonce;
+		const T,L: Nonce;
+
+		send_1(C,AS,  C, S, N1 );
+		read_2(AS,C,  AS, {AS, C, N1, pk(S)}sk(AS) );
+		send_3(C,S,   C, S, {C, T, L, {N2}pk(S)}sk(C) );
+		read_6(S,C,   S, C, {S, N2}pk(C) );
+
+		claim_7(C, Secret, N2);
+	}
+
+	role AS
+	{
+		var N1,N3: Nonce;
+
+		read_1(C,AS,  C, S, N1 );
+		send_2(AS,C,  AS, {AS, C, N1, pk(S)}sk(AS) );
+		read_4(S,AS,  S, C, N3 );
+		send_5(AS,S,  AS, {AS, S, N3, pk(C)}sk(AS) );
+	}
+
+	role S
+	{
+		const N3: Nonce;
+		var N2: Nonce;
+		var T,L: Nonce;
+
+		var ni: Nonce;
+		const nr: Nonce;
+
+		read_3(C,S,   C, S, {C, T, L, {N2}pk(S)}sk(C) );
+		send_4(S,AS,  S, C, N3 );
+		read_5(AS,S,  AS, {AS, S, N3, pk(C)}sk(AS) );
+		send_6(S,C,   S, C, {S, N2}pk(C) );
+
+		claim_8(S, Secret, N2);
+	}
+}
+
+const Alice,Bob,Eve: Agent;
+
+untrusted Eve;
+const ne: Nonce;
+compromised sk(Eve);
+
+run spliceAS.C(Agent,Agent,Agent);
+run spliceAS.AS(Agent,Agent,Agent);
+run spliceAS.S(Agent,Agent,Agent);
+
+