diff --git a/spdl/splice-as-hc-cj.spdl b/spdl/splice-as-hc-cj.spdl
new file mode 100644
index 0000000..1463e61
--- /dev/null
+++ b/spdl/splice-as-hc-cj.spdl
@@ -0,0 +1,66 @@
+usertype TimeStamp, LifeTime;
+
+const pk: Function;
+secret sk: Function;
+inversekeys (pk,sk);
+
+protocol spliceAShcCJ(C,AS,S)
+{
+        role C
+	{
+		const N1,N2: Nonce;
+		const T: TimeStamp;
+		const L: LifeTime;
+
+		send_1(C,AS,  C, S, N1 );
+		read_2(AS,C,  AS, {AS, C, N1, S, pk(S)}sk(AS) );
+		send_3(C,S,   C, S, {T, L, {C, N2}pk(S)}sk(C) );
+		read_6(S,C,   S, C, {N2}pk(C) );
+
+		claim_7(C, Secret, N2);
+		claim_9(C, Niagree);
+		claim_10(C, Nisynch);
+	}
+
+	role AS
+	{
+		var N1,N3: Nonce;
+
+		read_1(C,AS,  C, S, N1 );
+		send_2(AS,C,  AS, {AS, C, N1, S, pk(S)}sk(AS) );
+		read_4(S,AS,  S, C, N3 );
+		send_5(AS,S,  AS, {AS, S, N3, C, pk(C)}sk(AS) );
+	}
+
+	role S
+	{
+		const N3: Nonce;
+		var N2: Nonce;
+		var T: TimeStamp;
+		var L: LifeTime;
+
+		var ni: Nonce;
+		const nr: Nonce;
+
+		read_3(C,S,   C, S, {T, L, {C, N2}pk(S)}sk(C) );
+		send_4(S,AS,  S, C, N3 );
+		read_5(AS,S,  AS, {AS, S, N3, C, pk(C)}sk(AS) );
+		send_6(S,C,   S, C, {N2}pk(C) );
+
+		claim_8(S, Secret, N2);
+		claim_11(S, Niagree);
+		claim_12(S, Nisynch);
+	}
+}
+
+const Al,Bo,Eve: Agent;
+
+untrusted Eve;
+const ne: Nonce;
+compromised sk(Eve);
+
+run spliceAShcCJ.C(Agent,Agent,Agent);
+run spliceAShcCJ.AS(Agent,Agent,Agent);
+run spliceAShcCJ.S(Agent,Agent,Agent);
+
+
diff --git a/spdl/splice-as-hc.spdl b/spdl/splice-as-hc.spdl
new file mode 100644
index 0000000..d2bf6d5
--- /dev/null
+++ b/spdl/splice-as-hc.spdl
@@ -0,0 +1,66 @@
+usertype TimeStamp, LifeTime;
+
+const pk: Function;
+secret sk: Function;
+inversekeys (pk,sk);
+
+protocol spliceAShc(C,AS,S)
+{
+        role C
+	{
+		const N1,N2: Nonce;
+		const T: TimeStamp;
+		const L: LifeTime;
+
+		send_1(C,AS,  C, S, N1 );
+		read_2(AS,C,  AS, {AS, C, N1, S, 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);
+		claim_9(C, Niagree);
+		claim_10(C, Nisynch);
+	}
+
+	role AS
+	{
+		var N1,N3: Nonce;
+
+		read_1(C,AS,  C, S, N1 );
+		send_2(AS,C,  AS, {AS, C, N1, S, pk(S)}sk(AS) );
+		read_4(S,AS,  S, C, N3 );
+		send_5(AS,S,  AS, {AS, S, N3, C, pk(C)}sk(AS) );
+	}
+
+	role S
+	{
+		const N3: Nonce;
+		var N2: Nonce;
+		var T: TimeStamp;
+		var L: LifeTime;
+
+		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, C, pk(C)}sk(AS) );
+		send_6(S,C,   S, C, {S, N2}pk(C) );
+
+		claim_8(S, Secret, N2);
+		claim_11(S, Niagree);
+		claim_12(S, Nisynch);
+	}
+}
+
+const Al,Bo,Eve: Agent;
+
+untrusted Eve;
+const ne: Nonce;
+compromised sk(Eve);
+
+run spliceAShc.C(Agent,Agent,Agent);
+run spliceAShc.AS(Agent,Agent,Agent);
+run spliceAShc.S(Agent,Agent,Agent);
+
+