diff --git a/spdl/misc/tls-BM-1.m4 b/spdl/misc/tls-BM-1.m4
new file mode 100644
index 0000000..2ccada2
--- /dev/null
+++ b/spdl/misc/tls-BM-1.m4
@@ -0,0 +1,65 @@
+/*
+ * This is a model of a version of the TLS protocol as modeled in
+ * Boyd, Mathuria "Protocols for Authentication and key establishment"
+ *
+ * It's a very simplified form.
+ */
+define(`msg1',`na')
+define(`msg2',`nb')
+define(`kab',`hash(pmk,na,nb)')
+define(`msg3a',`{ pmk }pk(B)')
+define(`M1',`hash(msg1,msg2,msg3a)')
+define(`msg3b',`{ M1 }sk(A)')
+define(`M2',`hash(msg1,msg2,msg3a,msg3b)')
+define(`msg3c',`{ M2 }kab')
+define(`msg3',`msg3a,msg3b,msg3c')
+define(`M3',`msg1,msg2,msg3')
+define(`msg4',`{ M3 }kab')
+
+/* below is just Scyther input and no further macro definitions */
+
+const pk,hash: Function;
+secret sk,unhash: Function;
+inversekeys(pk,sk);
+inversekeys(hash,unhash);
+
+const Alice, Bob, Eve: Agent;
+const Terence: Agent;
+
+protocol tls-bm-1(A,B)
+{
+	role A
+	{
+		const na: Nonce;
+		const pmk: Nonce;
+		var nb: Nonce;
+
+		send_1( A,B, msg1 );
+		read_2( B,A, msg2 );
+		send_3( A,B, msg3 );
+		read_4( B,A, msg4 );
+
+		claim_A1( A, Secret, kab );
+		claim_A2( A, Nisynch );
+	}	
+	
+	role B
+	{
+		var na: Nonce;
+		var pmk: Nonce;
+		const nb: Nonce;
+
+		read_1( A,B, msg1 );
+		send_2( B,A, msg2 );
+		read_3( A,B, msg3 );
+		send_4( B,A, msg4 );
+
+		claim_B1( B, Secret, kab );
+		claim_B2( B, Nisynch );
+	}
+}
+
+
+untrusted Eve;
+compromised sk(Eve);
+
diff --git a/spdl/misc/tls-BM-1.spdl b/spdl/misc/tls-BM-1.spdl
new file mode 100644
index 0000000..bd9287a
--- /dev/null
+++ b/spdl/misc/tls-BM-1.spdl
@@ -0,0 +1,65 @@
+/*
+ * This is a model of a version of the TLS protocol as modeled in
+ * Boyd, Mathuria "Protocols for Authentication and key establishment"
+ *
+ * It's a very simplified form.
+ */
+
+
+
+
+
+
+
+
+
+
+
+
+/* below is just Scyther input and no further macro definitions */
+
+const pk,hash: Function;
+secret sk,unhash: Function;
+inversekeys(pk,sk);
+inversekeys(hash,unhash);
+
+const Alice, Bob, Eve: Agent;
+const Terence: Agent;
+
+protocol tls-bm-1(A,B)
+{
+	role A
+	{
+		const na: Nonce;
+		const pmk: Nonce;
+		var nb: Nonce;
+
+		send_1( A,B, na );
+		read_2( B,A, nb );
+		send_3( A,B, { pmk }pk(B),{ hash(na,nb,{ pmk }pk(B)) }sk(A),{ hash(na,nb,{ pmk }pk(B),{ hash(na,nb,{ pmk }pk(B)) }sk(A)) }hash(pmk,na,nb) );
+		read_4( B,A, { na,nb,{ pmk }pk(B),{ hash(na,nb,{ pmk }pk(B)) }sk(A),{ hash(na,nb,{ pmk }pk(B),{ hash(na,nb,{ pmk }pk(B)) }sk(A)) }hash(pmk,na,nb) }hash(pmk,na,nb) );
+
+		claim_A1( A, Secret, hash(pmk,na,nb) );
+		claim_A2( A, Nisynch );
+	}	
+	
+	role B
+	{
+		var na: Nonce;
+		var pmk: Nonce;
+		const nb: Nonce;
+
+		read_1( A,B, na );
+		send_2( B,A, nb );
+		read_3( A,B, { pmk }pk(B),{ hash(na,nb,{ pmk }pk(B)) }sk(A),{ hash(na,nb,{ pmk }pk(B),{ hash(na,nb,{ pmk }pk(B)) }sk(A)) }hash(pmk,na,nb) );
+		send_4( B,A, { na,nb,{ pmk }pk(B),{ hash(na,nb,{ pmk }pk(B)) }sk(A),{ hash(na,nb,{ pmk }pk(B),{ hash(na,nb,{ pmk }pk(B)) }sk(A)) }hash(pmk,na,nb) }hash(pmk,na,nb) );
+
+		claim_B1( B, Secret, hash(pmk,na,nb) );
+		claim_B2( B, Nisynch );
+	}
+}
+
+
+untrusted Eve;
+compromised sk(Eve);
+