From a911f567058fe8e13a623a3b9da73b82bf8341c7 Mon Sep 17 00:00:00 2001
From: Cas Cremers <cas.cremers@gmail.com>
Date: Thu, 15 Nov 2012 12:10:06 +0100
Subject: [PATCH] Added ISO/IEC 9798 models.

---
 gui/Protocols/ISO-9798/Makefile               | 16 ++++
 gui/Protocols/ISO-9798/iso25-tag.spdl         | 78 +++++++++++++++
 gui/Protocols/ISO-9798/iso26-tag.spdl         | 95 +++++++++++++++++++
 .../ISO-9798/isoiec-9798-2-1-udkey.spdl       | 35 +++++++
 gui/Protocols/ISO-9798/isoiec-9798-2-1.spdl   | 55 +++++++++++
 .../ISO-9798/isoiec-9798-2-2-udkey.spdl       | 40 ++++++++
 gui/Protocols/ISO-9798/isoiec-9798-2-2.spdl   | 59 ++++++++++++
 .../ISO-9798/isoiec-9798-2-3-udkey.spdl       | 49 ++++++++++
 gui/Protocols/ISO-9798/isoiec-9798-2-3.spdl   | 67 +++++++++++++
 .../ISO-9798/isoiec-9798-2-4-udkey.spdl       | 50 ++++++++++
 gui/Protocols/ISO-9798/isoiec-9798-2-4.spdl   | 88 +++++++++++++++++
 gui/Protocols/ISO-9798/isoiec-9798-2-5.spdl   | 93 ++++++++++++++++++
 gui/Protocols/ISO-9798/isoiec-9798-2-6.spdl   | 90 ++++++++++++++++++
 gui/Protocols/ISO-9798/isoiec-9798-3-1.spdl   | 33 +++++++
 gui/Protocols/ISO-9798/isoiec-9798-3-2.spdl   | 39 ++++++++
 gui/Protocols/ISO-9798/isoiec-9798-3-3.spdl   | 44 +++++++++
 gui/Protocols/ISO-9798/isoiec-9798-3-4.spdl   | 46 +++++++++
 gui/Protocols/ISO-9798/isoiec-9798-3-5.spdl   | 49 ++++++++++
 gui/Protocols/ISO-9798/isoiec-9798-3-6-1.cpp  | 12 +++
 gui/Protocols/ISO-9798/isoiec-9798-3-6-1.spdl | 69 ++++++++++++++
 gui/Protocols/ISO-9798/isoiec-9798-3-6-2.cpp  | 12 +++
 gui/Protocols/ISO-9798/isoiec-9798-3-6-2.spdl | 69 ++++++++++++++
 .../ISO-9798/isoiec-9798-3-6.template         | 68 +++++++++++++
 gui/Protocols/ISO-9798/isoiec-9798-3-7-1.cpp  | 12 +++
 gui/Protocols/ISO-9798/isoiec-9798-3-7-1.spdl | 66 +++++++++++++
 gui/Protocols/ISO-9798/isoiec-9798-3-7-2.cpp  | 12 +++
 gui/Protocols/ISO-9798/isoiec-9798-3-7-2.spdl | 68 +++++++++++++
 .../ISO-9798/isoiec-9798-3-7.template         | 67 +++++++++++++
 .../ISO-9798/isoiec-9798-4-1-udkey.spdl       | 39 ++++++++
 gui/Protocols/ISO-9798/isoiec-9798-4-1.spdl   | 58 +++++++++++
 .../ISO-9798/isoiec-9798-4-2-udkey.spdl       | 43 +++++++++
 gui/Protocols/ISO-9798/isoiec-9798-4-2.spdl   | 62 ++++++++++++
 .../ISO-9798/isoiec-9798-4-3-udkey.spdl       | 50 ++++++++++
 gui/Protocols/ISO-9798/isoiec-9798-4-3.spdl   | 69 ++++++++++++++
 .../ISO-9798/isoiec-9798-4-4-udkey.spdl       | 52 ++++++++++
 gui/Protocols/ISO-9798/isoiec-9798-4-4.spdl   | 75 +++++++++++++++
 36 files changed, 1929 insertions(+)
 create mode 100644 gui/Protocols/ISO-9798/Makefile
 create mode 100644 gui/Protocols/ISO-9798/iso25-tag.spdl
 create mode 100644 gui/Protocols/ISO-9798/iso26-tag.spdl
 create mode 100644 gui/Protocols/ISO-9798/isoiec-9798-2-1-udkey.spdl
 create mode 100644 gui/Protocols/ISO-9798/isoiec-9798-2-1.spdl
 create mode 100644 gui/Protocols/ISO-9798/isoiec-9798-2-2-udkey.spdl
 create mode 100644 gui/Protocols/ISO-9798/isoiec-9798-2-2.spdl
 create mode 100644 gui/Protocols/ISO-9798/isoiec-9798-2-3-udkey.spdl
 create mode 100644 gui/Protocols/ISO-9798/isoiec-9798-2-3.spdl
 create mode 100644 gui/Protocols/ISO-9798/isoiec-9798-2-4-udkey.spdl
 create mode 100644 gui/Protocols/ISO-9798/isoiec-9798-2-4.spdl
 create mode 100644 gui/Protocols/ISO-9798/isoiec-9798-2-5.spdl
 create mode 100644 gui/Protocols/ISO-9798/isoiec-9798-2-6.spdl
 create mode 100644 gui/Protocols/ISO-9798/isoiec-9798-3-1.spdl
 create mode 100644 gui/Protocols/ISO-9798/isoiec-9798-3-2.spdl
 create mode 100644 gui/Protocols/ISO-9798/isoiec-9798-3-3.spdl
 create mode 100644 gui/Protocols/ISO-9798/isoiec-9798-3-4.spdl
 create mode 100644 gui/Protocols/ISO-9798/isoiec-9798-3-5.spdl
 create mode 100644 gui/Protocols/ISO-9798/isoiec-9798-3-6-1.cpp
 create mode 100644 gui/Protocols/ISO-9798/isoiec-9798-3-6-1.spdl
 create mode 100644 gui/Protocols/ISO-9798/isoiec-9798-3-6-2.cpp
 create mode 100644 gui/Protocols/ISO-9798/isoiec-9798-3-6-2.spdl
 create mode 100644 gui/Protocols/ISO-9798/isoiec-9798-3-6.template
 create mode 100644 gui/Protocols/ISO-9798/isoiec-9798-3-7-1.cpp
 create mode 100644 gui/Protocols/ISO-9798/isoiec-9798-3-7-1.spdl
 create mode 100644 gui/Protocols/ISO-9798/isoiec-9798-3-7-2.cpp
 create mode 100644 gui/Protocols/ISO-9798/isoiec-9798-3-7-2.spdl
 create mode 100644 gui/Protocols/ISO-9798/isoiec-9798-3-7.template
 create mode 100644 gui/Protocols/ISO-9798/isoiec-9798-4-1-udkey.spdl
 create mode 100644 gui/Protocols/ISO-9798/isoiec-9798-4-1.spdl
 create mode 100644 gui/Protocols/ISO-9798/isoiec-9798-4-2-udkey.spdl
 create mode 100644 gui/Protocols/ISO-9798/isoiec-9798-4-2.spdl
 create mode 100644 gui/Protocols/ISO-9798/isoiec-9798-4-3-udkey.spdl
 create mode 100644 gui/Protocols/ISO-9798/isoiec-9798-4-3.spdl
 create mode 100644 gui/Protocols/ISO-9798/isoiec-9798-4-4-udkey.spdl
 create mode 100644 gui/Protocols/ISO-9798/isoiec-9798-4-4.spdl

diff --git a/gui/Protocols/ISO-9798/Makefile b/gui/Protocols/ISO-9798/Makefile
new file mode 100644
index 0000000..e0a1179
--- /dev/null
+++ b/gui/Protocols/ISO-9798/Makefile
@@ -0,0 +1,16 @@
+
+outputs= isoiec-9798-3-6-1.spdl isoiec-9798-3-6-2.spdl \
+	 isoiec-9798-3-7-1.spdl isoiec-9798-3-7-2.spdl
+
+all:	$(outputs)
+
+isoiec-9798-3-6-%.spdl:	isoiec-9798-3-6-%.cpp isoiec-9798-3-6.template
+	cpp -C -P $< >$@
+
+isoiec-9798-3-7-%.spdl:	isoiec-9798-3-7-%.cpp isoiec-9798-3-7.template
+	cpp -C -P $< >$@
+
+clean:
+	\rm -f $(outputs)
+
+
diff --git a/gui/Protocols/ISO-9798/iso25-tag.spdl b/gui/Protocols/ISO-9798/iso25-tag.spdl
new file mode 100644
index 0000000..a97164b
--- /dev/null
+++ b/gui/Protocols/ISO-9798/iso25-tag.spdl
@@ -0,0 +1,78 @@
+/*
+ * Modeled from ISO/IEC 9798
+ * Modeler: Cas Cremers, Dec. 2010
+ *
+ * symmetric
+ * ttp
+ * four-pass
+ * mutual
+ *
+ * Modeling notes:
+ * - The use of TNb in message 4, as specified by the ISO standard, is
+ *   different from other models, in which it was TNa.
+ */
+usertype SessionKey;
+usertype Tag;
+
+const t1,t2a,t2b,t3,t4,t5: Tag;
+
+protocol isoiec-9798-2-5(A,B,P)
+{
+	role A
+	{
+		fresh TVPa: Nonce;
+		var T: Ticket;
+		fresh TNa: Nonce;
+		var TNb: Nonce;
+		var Kab: SessionKey;
+		fresh Text1,Text5,Text6: Ticket;
+		var Text3,Text4,Text7,Text8: Ticket;
+
+		send_1(A,P, TVPa, B, Text1);
+		recv_2(P,A, Text4, { t2a, TVPa, Kab, B, Text3 }k(A,P), T );
+		claim(A,Running,B,Kab,Text5);
+		send_3(A,B, Text6, T, { t3, TNa, B, Text5 }Kab );
+		recv_4(B,A, Text8, { t4, TNb, A, Text7 }Kab );
+
+		claim(A,Commit,B,Kab,Text5,Text7);
+		claim(A,Secret,Kab);
+		claim(A,Secret,Text5);
+		claim(A,Secret,Text7);
+		claim(A,Alive);
+		claim(A,Weakagree);
+	}
+	role B
+	{
+		var TNp: Nonce;
+		var TNa: Nonce;
+		fresh TNb: Nonce;
+		var Kab: SessionKey;
+		fresh Text7,Text8: Ticket;
+		var Text2,Text5,Text6: Ticket;
+
+		recv_3(A,B, Text6, { t2b, TNp, Kab, A, Text2  }k(B,P), {
+		t3, TNa, B, Text5 }Kab );
+		claim(B,Running,A,Kab,Text5,Text7);
+		send_4(B,A, Text8, { t4, TNb, A, Text7 }Kab );
+
+		claim(B,Commit,A,Kab,Text5);
+		claim(B,Secret,Kab);
+		claim(B,Secret,Text5);
+		claim(B,Secret,Text7);
+		claim(B,Alive);
+		claim(B,Weakagree);
+	}
+	role P
+	{
+		var TVPa: Nonce;
+		fresh TNp: Nonce;
+		fresh Kab: SessionKey;
+		fresh Text2,Text3,Text4: Ticket;
+		var Text1: Ticket;
+
+		recv_1(A,P, TVPa, B, Text1);
+		send_2(P,A, Text4, { t2a, TVPa, Kab, B, Text3 }k(A,P),
+				  { t2b, TNp, Kab, A, Text2  }k(B,P) );
+	}
+}
+
diff --git a/gui/Protocols/ISO-9798/iso26-tag.spdl b/gui/Protocols/ISO-9798/iso26-tag.spdl
new file mode 100644
index 0000000..ced5d02
--- /dev/null
+++ b/gui/Protocols/ISO-9798/iso26-tag.spdl
@@ -0,0 +1,95 @@
+/*
+ * Modeled from ISO/IEC 9798
+ * Modeler: Cas Cremers, Dec. 2010
+ *
+ * symmetric
+ * ttp
+ * five-pass
+ * mutual
+ *
+ * MPA Attack reported by Mathuria:
+ * - Type flaw MPA when in parallel with Abadi-Needham protocol.
+ *
+ */
+usertype Tag;
+
+const t1,t2,t3,t4,t5: Tag;
+
+protocol isoiec-9798-2-6-tag(A,B,P)
+{
+	role A
+	{
+		var Rb: Nonce;
+		fresh Ra,Rpa: Nonce;
+		var Kab: SessionKey;
+		var T: Ticket;
+		fresh Text2,Text6,Text7: Ticket;
+		var Text1,Text4,Text5,Text8,Text9: Ticket;
+
+		recv_1(B,A, Rb, Text1);
+		send_2(A,P, Ra, Rb, B, Text2);
+		recv_3(P,A, Text5, {t1, Ra,Kab,B,Text4}k(A,P), T );
+		claim(A,Running,B,Kab,Text6);
+		send_4(A,B, Text7, T, {t3,Rpa,Rb,Text6}Kab );
+		recv_5(B,A, Text9, {t4,Rb,Rpa,Text8}Kab );
+
+		claim(A,Commit,B,Kab,Text6,Text8);
+		claim(A,Secret,Kab);
+		claim(A,Secret,Text6);
+		claim(A,Secret,Text8);
+		claim(A,Alive);
+		claim(A,Weakagree);
+	}
+	role B
+	{
+		fresh Rb: Nonce;
+		var Rpa: Nonce;
+		var Kab: SessionKey;
+		fresh Text1,Text8,Text9: Ticket;
+		var Text3,Text6,Text7: Ticket;
+
+		send_1(B,A, Rb, Text1);
+		recv_4(A,B, Text7, {t2,Rb,Kab,A,Text3}k(B,P), {t3,Rpa,Rb,Text6}Kab );
+		claim(B,Running,A,Kab,Text6,Text8);
+		send_5(B,A, Text9, {t4,Rb,Rpa,Text8}Kab );
+		
+		claim(B,Commit,A,Kab,Text6);
+		claim(B,Secret,Kab);
+		claim(B,Secret,Text6);
+		claim(B,Secret,Text8);
+		claim(B,Alive);
+		claim(B,Weakagree);
+	}
+	role P
+	{
+		var Ra, Rb: Nonce;
+		fresh Kab: SessionKey;
+		fresh Text3,Text4,Text5: Ticket;
+		var Text2: Ticket;
+
+		recv_2(A,P, Ra, Rb, B, Text2);
+		send_3(P,A, Text5, {t1,Ra,Kab,B,Text4}k(A,P),
+				  {t2,Rb,Kab,A,Text3}k(B,P) );
+	}
+}
+
+protocol @keysymm26(A,B,P)
+{
+	role A
+	{
+		var TVPN: Nonce;
+		var Kab: SessionKey;
+		var Text: Ticket;
+		var Tag: Ticket;
+
+		recv_!1(B,A, { Tag,TVPN, Kab, B, Text }k(P,A) );
+		send_!2(A,B, { Tag,TVPN, Kab, B, Text }k(A,P) );
+	}
+	role B
+	{
+	}
+	role P
+	{
+	}
+}
+
diff --git a/gui/Protocols/ISO-9798/isoiec-9798-2-1-udkey.spdl b/gui/Protocols/ISO-9798/isoiec-9798-2-1-udkey.spdl
new file mode 100644
index 0000000..e1f8be6
--- /dev/null
+++ b/gui/Protocols/ISO-9798/isoiec-9798-2-1-udkey.spdl
@@ -0,0 +1,35 @@
+/*
+ * Modeled from ISO/IEC 9798
+ * Modeler: Cas Cremers, Dec. 2010
+ *
+ * symmetric
+ * one-pass
+ * unilateral
+ *
+ * Note: the identity B may be ommitted, if
+ *   (a) the environment disallows such attacks, or
+ *   (b) a unidirectional key is used
+ */
+protocol isoiec-9798-2-1-udkey(A,B)
+{
+	role A
+	{
+		fresh TNA: Nonce;
+		fresh Text1,Text2: Ticket;
+
+		claim(A,Running,B,TNA,Text1);
+		send_1(A,B, Text2, { TNA, Text1 }k(A,B) );
+	}
+	role B
+	{
+		var TNA: Nonce;
+		var Text1,Text2: Ticket;
+
+		recv_1(A,B, Text2, { TNA, Text1 }k(A,B) );
+
+		claim(B,Commit,A,TNA,Text1);
+		claim(B,Alive);
+		claim(B,Weakagree);
+	}
+}
+
diff --git a/gui/Protocols/ISO-9798/isoiec-9798-2-1.spdl b/gui/Protocols/ISO-9798/isoiec-9798-2-1.spdl
new file mode 100644
index 0000000..0d47be3
--- /dev/null
+++ b/gui/Protocols/ISO-9798/isoiec-9798-2-1.spdl
@@ -0,0 +1,55 @@
+/*
+ * Modeled from ISO/IEC 9798
+ * Modeler: Cas Cremers, Dec. 2010
+ *
+ * symmetric
+ * one-pass
+ * unilateral
+ *
+ * Note: the identity B may be ommitted, if
+ *   (a) the environment disallows such attacks, or
+ *   (b) a unidirectional key is used
+ */
+protocol @keysymm-21(A,B)
+{
+	role A
+	{
+		var T: Nonce;
+		var Text: Ticket;
+
+		recv_!1(B,A, { T, A, Text }k(A,B) );
+		send_!2(A,B, { T, A, Text }k(B,A) );
+	}
+	role B
+	{
+		var T: Nonce;
+		var Text: Ticket;
+
+		recv_!3(A,B, { T, B, Text }k(A,B) );
+		send_!4(B,A, { T, B, Text }k(B,A) );
+	}
+}
+
+protocol isoiec-9798-2-1(A,B)
+{
+	role A
+	{
+		fresh TNA: Nonce;
+		fresh Text1,Text2: Ticket;
+
+		claim(A,Running,B,TNA,Text1);
+		send_1(A,B, Text2, { TNA, B, Text1 }k(A,B) );
+	}
+	role B
+	{
+		var TNA: Nonce;
+		var Text1,Text2: Ticket;
+
+		recv_1(A,B, Text2, { TNA, B, Text1 }k(A,B) );
+
+		claim(B,Commit,A,TNA,Text1);
+		claim(B,Alive);
+		claim(B,Weakagree);
+	}
+}
+
diff --git a/gui/Protocols/ISO-9798/isoiec-9798-2-2-udkey.spdl b/gui/Protocols/ISO-9798/isoiec-9798-2-2-udkey.spdl
new file mode 100644
index 0000000..314aa8e
--- /dev/null
+++ b/gui/Protocols/ISO-9798/isoiec-9798-2-2-udkey.spdl
@@ -0,0 +1,40 @@
+/*
+ * Modeled from ISO/IEC 9798
+ * Modeler: Cas Cremers, Dec. 2010
+ *
+ * symmetric
+ * two-pass
+ * unilateral
+ *
+ * Note: the identity A may be ommitted, if
+ *   (a) the environment disallows such attacks, or
+ *   (b) a unidirectional key is used
+ *
+ */
+protocol isoiec-9798-2-2-udkey(A,B)
+{
+	role A
+	{
+		var RB: Nonce;
+		var Text1: Ticket;
+		fresh Text2,Text3: Ticket;
+
+		recv_1(B,A, RB,Text1 );
+		claim(A,Running,B,RB,Text2);
+		send_2(A,B, Text3, { RB, Text2 }k(B,A) );
+	}
+	role B
+	{
+		fresh RB: Nonce;
+		fresh Text1: Ticket;
+		var Text2,Text3: Ticket;
+
+		send_1(B,A, RB,Text1 );
+		recv_2(A,B, Text3, { RB, Text2 }k(B,A) );
+
+		claim(B,Commit,A,RB,Text2);
+		claim(B,Alive);
+		claim(B,Weakagree);
+	}
+}
+
diff --git a/gui/Protocols/ISO-9798/isoiec-9798-2-2.spdl b/gui/Protocols/ISO-9798/isoiec-9798-2-2.spdl
new file mode 100644
index 0000000..fc1ae68
--- /dev/null
+++ b/gui/Protocols/ISO-9798/isoiec-9798-2-2.spdl
@@ -0,0 +1,59 @@
+/*
+ * Modeled from ISO/IEC 9798
+ * Modeler: Cas Cremers, Dec. 2010
+ *
+ * symmetric
+ * two-pass
+ * unilateral
+ *
+ * Note: the identity A may be ommitted, if
+ *   (a) the environment disallows such attacks, or
+ *   (b) a unidirectional key is used
+ */
+protocol @keysymm-22(A,B)
+{
+	role A
+	{
+		var T: Nonce;
+		var Text: Ticket;
+
+		recv_!1(B,A, { T, A, Text }k(A,B) );
+		send_!2(A,B, { T, A, Text }k(B,A) );
+	}
+	role B
+	{
+		var T: Nonce;
+		var Text: Ticket;
+
+		recv_!3(A,B, { T, B, Text }k(A,B) );
+		send_!4(B,A, { T, B, Text }k(B,A) );
+	}
+}
+
+protocol isoiec-9798-2-2(A,B)
+{
+	role A
+	{
+		var RB: Nonce;
+		var Text1: Ticket;
+		fresh Text2,Text3: Ticket;
+
+		recv_1(B,A, RB,Text1 );
+		claim(A,Running,B,RB,Text2);
+		send_2(A,B, Text3, { RB, B, Text2 }k(B,A) );
+	}
+	role B
+	{
+		fresh RB: Nonce;
+		fresh Text1: Ticket;
+		var Text2,Text3: Ticket;
+
+		send_1(B,A, RB,Text1 );
+		recv_2(A,B, Text3, { RB, B, Text2 }k(B,A) );
+
+		claim(B,Commit,A,RB,Text2);
+		claim(B,Alive);
+		claim(B,Weakagree);
+	}
+}
+
diff --git a/gui/Protocols/ISO-9798/isoiec-9798-2-3-udkey.spdl b/gui/Protocols/ISO-9798/isoiec-9798-2-3-udkey.spdl
new file mode 100644
index 0000000..9fddf69
--- /dev/null
+++ b/gui/Protocols/ISO-9798/isoiec-9798-2-3-udkey.spdl
@@ -0,0 +1,49 @@
+/*
+ * Modeled from ISO/IEC 9798
+ * Modeler: Cas Cremers, Dec. 2010
+ *
+ * symmetric
+ * two-pass
+ * mutual
+ *
+ * Note: the identity inside the encryption may be ommitted, if
+ *   (a) the environment disallows such attacks, or
+ *   (b) a unidirectional key is used
+ *
+ * In case (b), modeled here, the second key is reversed.
+ *
+ */
+protocol isoiec-9798-2-3-udkey(A,B)
+{
+	role A
+	{
+		fresh TNA: Nonce;
+		var TNB: Nonce;
+		fresh Text1,Text2: Ticket;
+		var Text3,Text4: Ticket;
+
+		claim(A,Running,B,TNA,Text1);
+		send_1(A,B, Text2, { TNA, Text1 }k(A,B) );
+		recv_2(B,A, Text4, { TNB, Text3 }k(B,A) );
+
+		claim(A,Commit,B,TNB,Text3);
+		claim(A,Alive);
+		claim(A,Weakagree);
+	}
+	role B
+	{
+		var TNA: Nonce;
+		fresh TNB: Nonce;
+		var Text1,Text2: Ticket;
+		fresh Text3,Text4: Ticket;
+
+		recv_1(A,B, Text2, { TNA, Text1 }k(A,B) );
+		claim(B,Running,A,TNB,Text3);
+		send_2(B,A, Text4, { TNB, Text3 }k(B,A) );
+
+		claim(B,Commit,A,TNA,Text1);
+		claim(B,Alive);
+		claim(B,Weakagree);
+	}
+}
+
diff --git a/gui/Protocols/ISO-9798/isoiec-9798-2-3.spdl b/gui/Protocols/ISO-9798/isoiec-9798-2-3.spdl
new file mode 100644
index 0000000..6f2f86b
--- /dev/null
+++ b/gui/Protocols/ISO-9798/isoiec-9798-2-3.spdl
@@ -0,0 +1,67 @@
+/*
+ * Modeled from ISO/IEC 9798
+ * Modeler: Cas Cremers, Dec. 2010
+ *
+ * symmetric
+ * two-pass
+ * mutual
+ *
+ * Note: the identity inside the encryption may be ommitted, if
+ *   (a) the environment disallows such attacks, or
+ *   (b) a unidirectional key is used
+ *
+ */
+protocol @keysymm-23(A,B)
+{
+	role A
+	{
+		var T: Nonce;
+		var Text: Ticket;
+
+		recv_!1(B,A, { T, A, Text }k(A,B) );
+		send_!2(A,B, { T, A, Text }k(B,A) );
+	}
+	role B
+	{
+		var T: Nonce;
+		var Text: Ticket;
+
+		recv_!3(A,B, { T, B, Text }k(A,B) );
+		send_!4(B,A, { T, B, Text }k(B,A) );
+	}
+}
+
+protocol isoiec-9798-2-3(A,B)
+{
+	role A
+	{
+		fresh TNA: Nonce;
+		var TNB: Nonce;
+		fresh Text1,Text2: Ticket;
+		var Text3,Text4: Ticket;
+
+		claim(A,Running,B,TNA,Text1);
+		send_1(A,B, Text2, { TNA, B, Text1 }k(A,B) );
+		recv_2(B,A, Text4, { TNB, A, Text3 }k(A,B) );
+
+		claim(A,Commit,B,TNB,Text3);
+		claim(A,Alive);
+		claim(A,Weakagree);
+	}
+	role B
+	{
+		var TNA: Nonce;
+		fresh TNB: Nonce;
+		var Text1,Text2: Ticket;
+		fresh Text3,Text4: Ticket;
+
+		recv_1(A,B, Text2, { TNA, B, Text1 }k(A,B) );
+		claim(B,Running,A,TNB,Text3);
+		send_2(B,A, Text4, { TNB, A, Text3 }k(A,B) );
+
+		claim(B,Commit,A,TNA,Text1);
+		claim(B,Alive);
+		claim(B,Weakagree);
+	}
+}
+
diff --git a/gui/Protocols/ISO-9798/isoiec-9798-2-4-udkey.spdl b/gui/Protocols/ISO-9798/isoiec-9798-2-4-udkey.spdl
new file mode 100644
index 0000000..28694de
--- /dev/null
+++ b/gui/Protocols/ISO-9798/isoiec-9798-2-4-udkey.spdl
@@ -0,0 +1,50 @@
+/*
+ * Modeled from ISO/IEC 9798
+ * Modeler: Cas Cremers, Dec. 2010
+ *
+ * symmetric
+ * three-pass
+ * mutual
+ *
+ * Note: the identity inside the encryption may be ommitted, if
+ *   (a) the environment disallows such attacks, or
+ *   (b) a unidirectional key is used
+ *
+ * In case (b), modeled here, the second key is reversed.
+ */
+protocol isoiec-9798-2-4-udkey(A,B)
+{
+	role A
+	{
+		var RB: Nonce;
+		fresh RA: Nonce;
+		var Text1,Text4,Text5: Ticket;
+		fresh Text2,Text3: Ticket;
+
+		recv_1(B,A, RB,Text1 );
+		claim(A,Running,B,RA,RB,Text2);
+		send_2(A,B, Text3, { RA, RB, Text2 }k(A,B) );
+		recv_3(B,A, Text5, { RB, RA, Text4 }k(B,A) );
+
+		claim(A,Commit,B,RA,RB,Text2,Text4);
+		claim(A,Alive);
+		claim(A,Weakagree);
+	}
+	role B
+	{
+		fresh RB: Nonce;
+		var RA: Nonce;
+		fresh Text1,Text4,Text5: Ticket;
+		var Text2,Text3: Ticket;
+
+		send_1(B,A, RB,Text1 );
+		recv_2(A,B, Text3, { RA, RB, Text2 }k(A,B) );
+		claim(B,Running,A,RA,RB,Text2,Text4);
+		send_3(B,A, Text5, { RB, RA, Text4 }k(B,A) );
+
+		claim(B,Commit,A,RA,RB,Text2);
+		claim(B,Alive);
+		claim(B,Weakagree);
+	}
+}
+
diff --git a/gui/Protocols/ISO-9798/isoiec-9798-2-4.spdl b/gui/Protocols/ISO-9798/isoiec-9798-2-4.spdl
new file mode 100644
index 0000000..5d709c0
--- /dev/null
+++ b/gui/Protocols/ISO-9798/isoiec-9798-2-4.spdl
@@ -0,0 +1,88 @@
+/*
+ * Modeled from ISO/IEC 9798
+ * Modeler: Cas Cremers, Dec. 2010
+ *
+ * symmetric
+ * three-pass
+ * mutual
+ *
+ * Note: the identity inside the encryption may be ommitted, if
+ *   (a) the environment disallows such attacks, or
+ *   (b) a unidirectional key is used
+ */
+protocol @keysymm-24a(A,B)
+{
+	role A
+	{
+		var T1,T2: Nonce;
+		var Text: Ticket;
+
+		recv_!1(B,A, { T1, T2, A, Text }k(A,B) );
+		send_!2(A,B, { T1, T2, A, Text }k(B,A) );
+	}
+	role B
+	{
+		var T1,T2: Nonce;
+		var Text: Ticket;
+
+		recv_!3(A,B, { T1, T2, B, Text }k(A,B) );
+		send_!4(B,A, { T1, T2, B, Text }k(B,A) );
+	}
+}
+
+protocol @keysymm-24b(A,B)
+{
+	role A
+	{
+		var T1,T2: Nonce;
+		var Text: Ticket;
+
+		recv_!1(B,A, { T1, T2, Text }k(A,B) );
+		send_!2(A,B, { T1, T2, Text }k(B,A) );
+	}
+	role B
+	{
+		var T1,T2: Nonce;
+		var Text: Ticket;
+
+		recv_!3(A,B, { T1, T2, Text }k(A,B) );
+		send_!4(B,A, { T1, T2, Text }k(B,A) );
+	}
+}
+
+protocol isoiec-9798-2-4(A,B)
+{
+	role A
+	{
+		var RB: Nonce;
+		fresh RA: Nonce;
+		var Text1,Text4,Text5: Ticket;
+		fresh Text2,Text3: Ticket;
+
+		recv_1(B,A, RB,Text1 );
+		claim(A,Running,B,RA,RB,Text2);
+		send_2(A,B, Text3, { RA, RB, B, Text2 }k(A,B) );
+		recv_3(B,A, Text5, { RB, RA, Text4 }k(A,B) );
+
+		claim(A,Commit,B,RA,RB,Text2,Text4);
+		claim(A,Alive);
+		claim(A,Weakagree);
+	}
+	role B
+	{
+		fresh RB: Nonce;
+		var RA: Nonce;
+		fresh Text1,Text4,Text5: Ticket;
+		var Text2,Text3: Ticket;
+
+		send_1(B,A, RB,Text1 );
+		recv_2(A,B, Text3, { RA, RB, B, Text2 }k(A,B) );
+		claim(B,Running,A,RA,RB,Text2,Text4);
+		send_3(B,A, Text5, { RB, RA, Text4 }k(A,B) );
+
+		claim(B,Commit,A,RA,RB,Text2);
+		claim(B,Alive);
+		claim(B,Weakagree);
+	}
+}
+
diff --git a/gui/Protocols/ISO-9798/isoiec-9798-2-5.spdl b/gui/Protocols/ISO-9798/isoiec-9798-2-5.spdl
new file mode 100644
index 0000000..7a98c0d
--- /dev/null
+++ b/gui/Protocols/ISO-9798/isoiec-9798-2-5.spdl
@@ -0,0 +1,93 @@
+/*
+ * Modeled from ISO/IEC 9798
+ * Modeler: Cas Cremers, Dec. 2010
+ *
+ * symmetric
+ * ttp
+ * four-pass
+ * mutual
+ *
+ * Modeling notes:
+ * - The use of TNb in message 4, as specified by the ISO standard, is
+ *   different from other models, in which it was TNa.
+ */
+usertype SessionKey;
+
+protocol isoiec-9798-2-5(A,B,P)
+{
+	role A
+	{
+		fresh TVPa: Nonce;
+		var T: Ticket;
+		fresh TNa: Nonce;
+		var TNb: Nonce;
+		var Kab: SessionKey;
+		fresh Text1,Text5,Text6: Ticket;
+		var Text3,Text4,Text7,Text8: Ticket;
+
+		send_1(A,P, TVPa, B, Text1);
+		recv_2(P,A, Text4, { TVPa, Kab, B, Text3 }k(A,P), T );
+		claim(A,Running,B,Kab,Text5);
+		send_3(A,B, Text6, T, { TNa, B, Text5 }Kab );
+		recv_4(B,A, Text8, { TNb, A, Text7 }Kab );
+
+		claim(A,Commit,B,Kab,Text5,Text7);
+		claim(A,Secret,Kab);
+		claim(A,Secret,Text5);
+		claim(A,Secret,Text7);
+		claim(A,Alive);
+		claim(A,Weakagree);
+	}
+	role B
+	{
+		var TNp: Nonce;
+		var TNa: Nonce;
+		fresh TNb: Nonce;
+		var Kab: SessionKey;
+		fresh Text7,Text8: Ticket;
+		var Text2,Text5,Text6: Ticket;
+
+		recv_3(A,B, Text6, { TNp, Kab, A, Text2  }k(B,P), { TNa, B, Text5 }Kab );
+		claim(B,Running,A,Kab,Text5,Text7);
+		send_4(B,A, Text8, { TNb, A, Text7 }Kab );
+
+		claim(B,Commit,A,Kab,Text5);
+		claim(B,Secret,Kab);
+		claim(B,Secret,Text5);
+		claim(B,Secret,Text7);
+		claim(B,Alive);
+		claim(B,Weakagree);
+	}
+	role P
+	{
+		var TVPa: Nonce;
+		fresh TNp: Nonce;
+		fresh Kab: SessionKey;
+		fresh Text2,Text3,Text4: Ticket;
+		var Text1: Ticket;
+
+		recv_1(A,P, TVPa, B, Text1);
+		send_2(P,A, Text4, { TVPa, Kab, B, Text3 }k(A,P),
+				  { TNp, Kab, A, Text2  }k(B,P) );
+	}
+}
+
+protocol @keysymm25(A,B,P)
+{
+	role A
+	{
+		var TVPN: Nonce;
+		var Kab: SessionKey;
+		var Text: Ticket;
+
+		recv_!1(B,A, { TVPN, Kab, B, Text }k(P,A) );
+		send_!2(A,B, { TVPN, Kab, B, Text }k(A,P) );
+	}
+	role B
+	{
+	}
+	role P
+	{
+	}
+}
+
diff --git a/gui/Protocols/ISO-9798/isoiec-9798-2-6.spdl b/gui/Protocols/ISO-9798/isoiec-9798-2-6.spdl
new file mode 100644
index 0000000..703885b
--- /dev/null
+++ b/gui/Protocols/ISO-9798/isoiec-9798-2-6.spdl
@@ -0,0 +1,90 @@
+/*
+ * Modeled from ISO/IEC 9798
+ * Modeler: Cas Cremers, Dec. 2010
+ *
+ * symmetric
+ * ttp
+ * five-pass
+ * mutual
+ *
+ * MPA Attack reported by Mathuria:
+ * - Type flaw MPA when in parallel with Abadi-Needham protocol.
+ *
+ */
+protocol isoiec-9798-2-6(A,B,P)
+{
+	role A
+	{
+		var Rb: Nonce;
+		fresh Ra,Rpa: Nonce;
+		var Kab: SessionKey;
+		var T: Ticket;
+		fresh Text2,Text6,Text7: Ticket;
+		var Text1,Text4,Text5,Text8,Text9: Ticket;
+
+		recv_1(B,A, Rb, Text1);
+		send_2(A,P, Ra, Rb, B, Text2);
+		recv_3(P,A, Text5, {Ra,Kab,B,Text4}k(A,P), T );
+		claim(A,Running,B,Kab,Text6);
+		send_4(A,B, Text7, T, {Rpa,Rb,Text6}Kab );
+		recv_5(B,A, Text9, {Rb,Rpa,Text8}Kab );
+
+		claim(A,Commit,B,Kab,Text6,Text8);
+		claim(A,Secret,Kab);
+		claim(A,Secret,Text6);
+		claim(A,Secret,Text8);
+		claim(A,Alive);
+		claim(A,Weakagree);
+	}
+	role B
+	{
+		fresh Rb: Nonce;
+		var Rpa: Nonce;
+		var Kab: SessionKey;
+		fresh Text1,Text8,Text9: Ticket;
+		var Text3,Text6,Text7: Ticket;
+
+		send_1(B,A, Rb, Text1);
+		recv_4(A,B, Text7, {Rb,Kab,A,Text3}k(B,P), {Rpa,Rb,Text6}Kab );
+		claim(B,Running,A,Kab,Text6,Text8);
+		send_5(B,A, Text9, {Rb,Rpa,Text8}Kab );
+		
+		claim(B,Commit,A,Kab,Text6);
+		claim(B,Secret,Kab);
+		claim(B,Secret,Text6);
+		claim(B,Secret,Text8);
+		claim(B,Alive);
+		claim(B,Weakagree);
+	}
+	role P
+	{
+		var Ra, Rb: Nonce;
+		fresh Kab: SessionKey;
+		fresh Text3,Text4,Text5: Ticket;
+		var Text2: Ticket;
+
+		recv_2(A,P, Ra, Rb, B, Text2);
+		send_3(P,A, Text5, {Ra,Kab,B,Text4}k(A,P),
+				  {Rb,Kab,A,Text3}k(B,P) );
+	}
+}
+
+protocol @keysymm26(A,B,P)
+{
+	role A
+	{
+		var TVPN: Nonce;
+		var Kab: SessionKey;
+		var Text: Ticket;
+
+		recv_!1(B,A, { TVPN, Kab, B, Text }k(P,A) );
+		send_!2(A,B, { TVPN, Kab, B, Text }k(A,P) );
+	}
+	role B
+	{
+	}
+	role P
+	{
+	}
+}
+
diff --git a/gui/Protocols/ISO-9798/isoiec-9798-3-1.spdl b/gui/Protocols/ISO-9798/isoiec-9798-3-1.spdl
new file mode 100644
index 0000000..42b5667
--- /dev/null
+++ b/gui/Protocols/ISO-9798/isoiec-9798-3-1.spdl
@@ -0,0 +1,33 @@
+/*
+ * Modeled from ISO/IEC 9798
+ * Modeler: Cas Cremers, Dec. 2010
+ *
+ * signature
+ * one-pass
+ * unilateral
+ */
+const Cert: Function;
+
+protocol isoiec-9798-3-1(A,B)
+{
+	role A
+	{
+		fresh TNA: Nonce;
+		fresh Text1,Text2: Ticket;
+
+		claim(A,Running,B,TNA,Text1);
+		send_1(A,B, Cert(A),TNA,B,Text2, { TNA, B, Text1 }sk(A) );
+	}
+	role B
+	{
+		var TNA: Nonce;
+		var Text1,Text2: Ticket;
+
+		recv_1(A,B, Cert(A),TNA,B,Text2, { TNA, B, Text1 }sk(A) );
+
+		claim(B,Commit,A,TNA,Text1);
+		claim(B,Alive);
+		claim(B,Weakagree);
+	}
+}
+
diff --git a/gui/Protocols/ISO-9798/isoiec-9798-3-2.spdl b/gui/Protocols/ISO-9798/isoiec-9798-3-2.spdl
new file mode 100644
index 0000000..97f5c68
--- /dev/null
+++ b/gui/Protocols/ISO-9798/isoiec-9798-3-2.spdl
@@ -0,0 +1,39 @@
+/*
+ * Modeled from ISO/IEC 9798
+ * Modeler: Cas Cremers, Dec. 2010
+ *
+ * signature
+ * two-pass
+ * unilateral
+ */
+const Cert: Function;
+
+protocol isoiec-9798-3-2(A,B)
+{
+	role A
+	{
+		var Rb: Nonce;
+		fresh Ra: Nonce;
+		var Text1: Ticket;
+		fresh Text2,Text3: Ticket;
+
+		recv_1(B,A, Rb,Text1 );
+		claim(A,Running,B,Ra,Rb,Text2);
+		send_2(A,B, Cert(A),Ra,Rb,B,Text3, { Ra, Rb, B, Text2 }sk(A) );
+	}
+	role B
+	{
+		fresh Rb: Nonce;
+		var Ra: Nonce;
+		fresh Text1: Ticket;
+		var Text2,Text3: Ticket;
+
+		send_1(B,A, Rb,Text1 );
+		recv_2(A,B, Cert(A),Ra,Rb,B,Text3, { Ra, Rb, B, Text2 }sk(A) );
+
+		claim(B,Commit,A,Ra,Rb,Text2);
+		claim(B,Alive);
+		claim(B,Weakagree);
+	}
+}
+
diff --git a/gui/Protocols/ISO-9798/isoiec-9798-3-3.spdl b/gui/Protocols/ISO-9798/isoiec-9798-3-3.spdl
new file mode 100644
index 0000000..ca1d944
--- /dev/null
+++ b/gui/Protocols/ISO-9798/isoiec-9798-3-3.spdl
@@ -0,0 +1,44 @@
+/*
+ * Modeled from ISO/IEC 9798
+ * Modeler: Cas Cremers, Dec. 2010
+ *
+ * signature
+ * two-pass
+ * mutual
+ */
+const Cert: Function;
+
+protocol isoiec-9798-3-3(A,B)
+{
+	role A
+	{
+		fresh TNA: Nonce;
+		var TNB: Nonce;
+		fresh Text1,Text2: Ticket;
+		var Text3,Text4: Ticket;
+
+		claim(A,Running,B,TNA,Text1);
+		send_1(A,B, Cert(A), TNA, B,Text2, { TNA, B, Text1 }sk(A) );
+		recv_2(B,A, Cert(B), TNB, A,Text4, { TNB, A, Text3 }sk(B) );
+
+		claim(A,Commit,B,TNB,Text3);
+		claim(A,Alive);
+		claim(A,Weakagree);
+	}
+	role B
+	{
+		var TNA: Nonce;
+		fresh TNB: Nonce;
+		var Text1,Text2: Ticket;
+		fresh Text3,Text4: Ticket;
+
+		recv_1(A,B, Cert(A), TNA, B,Text2, { TNA, B, Text1 }sk(A) );
+		claim(B,Running,A,TNB,Text3);
+		send_2(B,A, Cert(B), TNB, A,Text4, { TNB, A, Text3 }sk(B) );
+
+		claim(B,Commit,A,TNA,Text1);
+		claim(B,Alive);
+		claim(B,Weakagree);
+	}
+}
+
diff --git a/gui/Protocols/ISO-9798/isoiec-9798-3-4.spdl b/gui/Protocols/ISO-9798/isoiec-9798-3-4.spdl
new file mode 100644
index 0000000..f8bfbbc
--- /dev/null
+++ b/gui/Protocols/ISO-9798/isoiec-9798-3-4.spdl
@@ -0,0 +1,46 @@
+/*
+ * Modeled from ISO/IEC 9798
+ * Modeler: Cas Cremers, Dec. 2010
+ *
+ * signature
+ * three-pass
+ * mutual
+ */
+const Cert: Function;
+
+protocol isoiec-9798-3-4(A,B)
+{
+	role A
+	{
+		var RB: Nonce;
+		fresh RA: Nonce;
+		var Text1,Text4,Text5: Ticket;
+		fresh Text2,Text3: Ticket;
+
+		recv_1(B,A, RB,Text1 );
+		claim(A,Running,B,RA,RB,Text2);
+		send_2(A,B, Cert(B), RA,RB,B,Text3, { RA, RB, B, Text2 }sk(A) );
+		recv_3(B,A, Cert(A), RB,RA,A,Text5, { RB, RA, A, Text4 }sk(B) );
+
+		claim(A,Commit,B,RA,RB,Text2,Text4);
+		claim(A,Alive);
+		claim(A,Weakagree);
+	}
+	role B
+	{
+		fresh RB: Nonce;
+		var RA: Nonce;
+		fresh Text1,Text4,Text5: Ticket;
+		var Text2,Text3: Ticket;
+
+		send_1(B,A, RB,Text1 );
+		recv_2(A,B, Cert(B), RA,RB,B,Text3, { RA, RB, B, Text2 }sk(A) );
+		claim(B,Running,A,RA,RB,Text2,Text4);
+		send_3(B,A, Cert(A), RB,RA,A,Text5, { RB, RA, A, Text4 }sk(B) );
+
+		claim(B,Commit,A,RA,RB,Text2);
+		claim(B,Alive);
+		claim(B,Weakagree);
+	}
+}
+
diff --git a/gui/Protocols/ISO-9798/isoiec-9798-3-5.spdl b/gui/Protocols/ISO-9798/isoiec-9798-3-5.spdl
new file mode 100644
index 0000000..237e56f
--- /dev/null
+++ b/gui/Protocols/ISO-9798/isoiec-9798-3-5.spdl
@@ -0,0 +1,49 @@
+/*
+ * Modeled from ISO/IEC 9798
+ * Modeler: Cas Cremers, Dec. 2010
+ *
+ * signature
+ * two-pass
+ * mutual
+ * parallel
+ */
+const Cert: Function;
+
+protocol isoiec-9798-3-5(A,B)
+{
+	role A
+	{
+		fresh RA: Nonce;
+		var RB: Nonce;
+		fresh Text1,Text3,Text4: Ticket;
+		var Text2,Text5,Text6: Ticket;
+		
+		send_1(A,B, Cert(A), RA,Text1 );
+		recv_2(B,A, Cert(B), RB,Text2 );
+		recv_3(B,A, RB,RA,A,Text6, { RB, RA, A, Text5 }sk(B) );
+		claim(A,Running,B,RA,RB,Text3,Text5);
+		send_4(A,B, RA,RB,B,Text4, { RA, RB, B, Text3 }sk(A) );
+
+		claim(A,Commit,B,RA,RB,Text5);
+		claim(A,Alive);
+		claim(A,Weakagree);
+	}
+	role B
+	{
+		var RA: Nonce;
+		fresh RB: Nonce;
+		var Text1,Text3,Text4: Ticket;
+		fresh Text2,Text5,Text6: Ticket;
+
+		recv_1(A,B, Cert(A), RA,Text1 );
+		send_2(B,A, Cert(B), RB,Text2 );
+		claim(B,Running,A,RA,RB,Text5);
+		send_3(B,A, RB,RA,A,Text6, { RB, RA, A, Text5 }sk(B) );
+		recv_4(A,B, RA,RB,B,Text4, { RA, RB, B, Text3 }sk(A) );
+
+		claim(B,Commit,A,RA,RB,Text3,Text5);
+		claim(B,Alive);
+		claim(B,Weakagree);
+	}
+}
+
diff --git a/gui/Protocols/ISO-9798/isoiec-9798-3-6-1.cpp b/gui/Protocols/ISO-9798/isoiec-9798-3-6-1.cpp
new file mode 100644
index 0000000..fb5b93b
--- /dev/null
+++ b/gui/Protocols/ISO-9798/isoiec-9798-3-6-1.cpp
@@ -0,0 +1,12 @@
+#define NAME isoiec-9798-3-6-1
+#define IA A
+#define IB B
+#define ResA A,pk(A)
+#define ResB B,pk(B)
+#define TokenAB Text9,ResA,{Rb,ResA,Text5}sk(T),{Rb,Ra,B,A,Text8}sk(A)
+#define TokenBA Ra,Rb,Text3,{B,Ra,Rb,A,Text2}sk(B)
+#define TokenTA ResA,ResB,{Rpa,ResB,Text6}sk(T),{Rb,ResA,Text5}sk(T)
+
+#include "isoiec-9798-3-6.template"
+
+
diff --git a/gui/Protocols/ISO-9798/isoiec-9798-3-6-1.spdl b/gui/Protocols/ISO-9798/isoiec-9798-3-6-1.spdl
new file mode 100644
index 0000000..51545a6
--- /dev/null
+++ b/gui/Protocols/ISO-9798/isoiec-9798-3-6-1.spdl
@@ -0,0 +1,69 @@
+
+
+/*
+ * Modeled from ISO standard
+ *
+ * signature
+ * ttp
+ * five-pass
+ * mutual
+ *
+ * A initiates and also communicates with T
+ *
+ * parameters:
+ *
+ * 	NAME
+ * 	IA
+ * 	IB
+ * 	ResA
+ * 	ResB
+ * 	TokenAB
+ * 	TokenBA (although identical in both cases)
+ * 	TokenTA
+ *
+ */
+protocol isoiec-9798-3-6-1(A,B,T)
+{
+ role A
+ {
+  fresh Ra,Rpa: Nonce;
+  fresh Text1,Text4,Text8,Text9: Ticket;
+  var Rb: Nonce;
+  var Text2,Text3;
+  var Text5,Text6,Text7: Ticket;
+
+  send_1(A,B, Ra,A,Text1);
+  recv_2(B,A, B,Ra,Rb,Text3,{B,Ra,Rb,A,Text2}sk(B));
+  send_3(A,T, Rpa,Rb,A,B,Text4);
+  recv_4(T,A, Text7,A,pk(A),B,pk(B),{Rpa,B,pk(B),Text6}sk(T),{Rb,A,pk(A),Text5}sk(T));
+  claim(A,Running,B,Ra,Rb,Text8);
+  send_5(A,B, Text9,A,pk(A),{Rb,A,pk(A),Text5}sk(T),{Rb,Ra,B,A,Text8}sk(A));
+
+  claim(A,Commit,B,Ra,Rb,Text2);
+  claim(A,Alive);
+ }
+ role B
+ {
+  var Ra,Rpa: Nonce;
+  var Text1,Text5,Text8,Text9: Ticket;
+  fresh Text2,Text3,Text4: Ticket;
+  fresh Rb: Nonce;
+
+  recv_1(A,B, Ra,A,Text1);
+  claim(B,Running,A,Ra,Rb,Text2);
+  send_2(B,A, B,Ra,Rb,Text3,{B,Ra,Rb,A,Text2}sk(B));
+  recv_5(A,B, Text9,A,pk(A),{Rb,A,pk(A),Text5}sk(T),{Rb,Ra,B,A,Text8}sk(A));
+
+  claim(B,Commit,A,Ra,Rb,Text8);
+  claim(B,Alive);
+ }
+ role T
+ {
+  var Rpa, Rb: Nonce;
+  var Text4: Ticket;
+  fresh Text5,Text6,Text7: Ticket;
+
+  recv_3(A,T, Rpa,Rb,A,B,Text4);
+  send_4(T,A, Text7,A,pk(A),B,pk(B),{Rpa,B,pk(B),Text6}sk(T),{Rb,A,pk(A),Text5}sk(T));
+ }
+}
diff --git a/gui/Protocols/ISO-9798/isoiec-9798-3-6-2.cpp b/gui/Protocols/ISO-9798/isoiec-9798-3-6-2.cpp
new file mode 100644
index 0000000..d40ca51
--- /dev/null
+++ b/gui/Protocols/ISO-9798/isoiec-9798-3-6-2.cpp
@@ -0,0 +1,12 @@
+#define NAME isoiec-9798-3-6-2
+#define IA A
+#define IB B
+#define ResA A,pk(A)
+#define ResB B,pk(B)
+#define TokenAB Rpa,Text9,TokenTA,{Rb,Ra,B,A,Text8}sk(A)
+#define TokenBA Ra,Rb,Text3,{B,Ra,Rb,A,Text2}sk(B)
+#define TokenTA ResA,ResB,{Rpa,Rb,ResA,ResB,Text5}sk(T)
+
+#include "isoiec-9798-3-6.template"
+
+
diff --git a/gui/Protocols/ISO-9798/isoiec-9798-3-6-2.spdl b/gui/Protocols/ISO-9798/isoiec-9798-3-6-2.spdl
new file mode 100644
index 0000000..3debbc7
--- /dev/null
+++ b/gui/Protocols/ISO-9798/isoiec-9798-3-6-2.spdl
@@ -0,0 +1,69 @@
+
+
+/*
+ * Modeled from ISO standard
+ *
+ * signature
+ * ttp
+ * five-pass
+ * mutual
+ *
+ * A initiates and also communicates with T
+ *
+ * parameters:
+ *
+ * 	NAME
+ * 	IA
+ * 	IB
+ * 	ResA
+ * 	ResB
+ * 	TokenAB
+ * 	TokenBA (although identical in both cases)
+ * 	TokenTA
+ *
+ */
+protocol isoiec-9798-3-6-2(A,B,T)
+{
+ role A
+ {
+  fresh Ra,Rpa: Nonce;
+  fresh Text1,Text4,Text8,Text9: Ticket;
+  var Rb: Nonce;
+  var Text2,Text3;
+  var Text5,Text6,Text7: Ticket;
+
+  send_1(A,B, Ra,A,Text1);
+  recv_2(B,A, B,Ra,Rb,Text3,{B,Ra,Rb,A,Text2}sk(B));
+  send_3(A,T, Rpa,Rb,A,B,Text4);
+  recv_4(T,A, Text7,A,pk(A),B,pk(B),{Rpa,Rb,A,pk(A),B,pk(B),Text5}sk(T));
+  claim(A,Running,B,Ra,Rb,Text8);
+  send_5(A,B, Rpa,Text9,A,pk(A),B,pk(B),{Rpa,Rb,A,pk(A),B,pk(B),Text5}sk(T),{Rb,Ra,B,A,Text8}sk(A));
+
+  claim(A,Commit,B,Ra,Rb,Text2);
+  claim(A,Alive);
+ }
+ role B
+ {
+  var Ra,Rpa: Nonce;
+  var Text1,Text5,Text8,Text9: Ticket;
+  fresh Text2,Text3,Text4: Ticket;
+  fresh Rb: Nonce;
+
+  recv_1(A,B, Ra,A,Text1);
+  claim(B,Running,A,Ra,Rb,Text2);
+  send_2(B,A, B,Ra,Rb,Text3,{B,Ra,Rb,A,Text2}sk(B));
+  recv_5(A,B, Rpa,Text9,A,pk(A),B,pk(B),{Rpa,Rb,A,pk(A),B,pk(B),Text5}sk(T),{Rb,Ra,B,A,Text8}sk(A));
+
+  claim(B,Commit,A,Ra,Rb,Text8);
+  claim(B,Alive);
+ }
+ role T
+ {
+  var Rpa, Rb: Nonce;
+  var Text4: Ticket;
+  fresh Text5,Text6,Text7: Ticket;
+
+  recv_3(A,T, Rpa,Rb,A,B,Text4);
+  send_4(T,A, Text7,A,pk(A),B,pk(B),{Rpa,Rb,A,pk(A),B,pk(B),Text5}sk(T));
+ }
+}
diff --git a/gui/Protocols/ISO-9798/isoiec-9798-3-6.template b/gui/Protocols/ISO-9798/isoiec-9798-3-6.template
new file mode 100644
index 0000000..e8b6a80
--- /dev/null
+++ b/gui/Protocols/ISO-9798/isoiec-9798-3-6.template
@@ -0,0 +1,68 @@
+/*
+ * Modeled from ISO standard
+ *
+ * signature
+ * ttp
+ * five-pass
+ * mutual
+ *
+ * A initiates and also communicates with T
+ *
+ * parameters:
+ *
+ * 	NAME
+ * 	IA
+ * 	IB
+ * 	ResA
+ * 	ResB
+ * 	TokenAB
+ * 	TokenBA (although identical in both cases)
+ * 	TokenTA
+ *
+ */
+protocol NAME(A,B,T)
+{
+	role A
+	{
+		fresh Ra,Rpa: Nonce;
+		fresh Text1,Text4,Text8,Text9: Ticket;
+		var Rb: Nonce;
+		var Text2,Text3;
+		var Text5,Text6,Text7: Ticket;
+
+		send_1(A,B, Ra,IA,Text1);
+		recv_2(B,A, IB,TokenBA);
+		send_3(A,T, Rpa,Rb,IA,IB,Text4);
+		recv_4(T,A, Text7,TokenTA);
+		claim(A,Running,B,Ra,Rb,Text8);
+		send_5(A,B, TokenAB);
+
+		claim(A,Commit,B,Ra,Rb,Text2);
+		claim(A,Alive);
+	}
+	role B
+	{
+		var Ra,Rpa: Nonce;
+		var Text1,Text5,Text8,Text9: Ticket;
+		fresh Text2,Text3,Text4: Ticket;
+		fresh Rb: Nonce;
+
+		recv_1(A,B, Ra,IA,Text1);
+		claim(B,Running,A,Ra,Rb,Text2);
+		send_2(B,A, IB,TokenBA);
+		recv_5(A,B, TokenAB);
+
+		claim(B,Commit,A,Ra,Rb,Text8);
+		claim(B,Alive);
+	}
+	role T
+	{
+		var Rpa, Rb: Nonce;
+		var Text4: Ticket;
+		fresh Text5,Text6,Text7: Ticket;
+
+		recv_3(A,T, Rpa,Rb,IA,IB,Text4);
+		send_4(T,A, Text7,TokenTA);
+	}
+}
+
diff --git a/gui/Protocols/ISO-9798/isoiec-9798-3-7-1.cpp b/gui/Protocols/ISO-9798/isoiec-9798-3-7-1.cpp
new file mode 100644
index 0000000..fd97211
--- /dev/null
+++ b/gui/Protocols/ISO-9798/isoiec-9798-3-7-1.cpp
@@ -0,0 +1,12 @@
+#define NAME isoiec-9798-3-7-1
+#define IA A
+#define IB B
+#define ResA A,pk(A)
+#define ResB B,pk(B)
+#define TokenAB Text7,Ra,ResA,{Rb,ResA,Text3}sk(T),{Rb,Ra,B,A,Text6}sk(A)
+#define TokenBA Ra,Rb,Text9,{A,Ra,Rb,B,Text8}sk(B)
+#define TokenTA ResA,ResB,{Rpa,ResB,Text4}sk(T),{Rb,ResA,Text3}sk(T)
+
+#include "isoiec-9798-3-7.template"
+
+
diff --git a/gui/Protocols/ISO-9798/isoiec-9798-3-7-1.spdl b/gui/Protocols/ISO-9798/isoiec-9798-3-7-1.spdl
new file mode 100644
index 0000000..516ceb0
--- /dev/null
+++ b/gui/Protocols/ISO-9798/isoiec-9798-3-7-1.spdl
@@ -0,0 +1,66 @@
+/*
+ * Modeled from ISO standard
+ *
+ * signature
+ * ttp
+ * five-pass
+ * mutual
+ *
+ * B initiates and A communicates with T
+ *
+ * parameters:
+ *
+ * 	NAME
+ * 	IA
+ * 	IB
+ * 	ResA
+ * 	ResB
+ * 	TokenAB
+ * 	TokenBA (although identical in both cases)
+ * 	TokenTA
+ *
+ */
+protocol isoiec-9798-3-7-1(A,B,T)
+{
+ role A
+ {
+  fresh Ra,Rpa: Nonce;
+  var Rb: Nonce;
+  var Text1,Text3,Text4,Text5,Text8,Text9: Ticket;
+  fresh Text2,Text6,Text7: Ticket;
+
+  recv_1(B,A, Rb,B,Text1 );
+  send_2(A,T, Rpa,Rb,A,Text2 );
+  recv_3(T,A, Text5, A,pk(A),B,pk(B),{Rpa,B,pk(B),Text4}sk(T),{Rb,A,pk(A),Text3}sk(T) );
+  claim(A,Running,B,Ra,Rb,Text6);
+  send_4(A,B, A, Text7,Ra,A,pk(A),{Rb,A,pk(A),Text3}sk(T),{Rb,Ra,B,A,Text6}sk(A) );
+  recv_5(B,A, Ra,Rb,Text9,{A,Ra,Rb,B,Text8}sk(B) );
+
+  claim(A,Commit,B,Ra,Rb,Text8);
+  claim(A,Alive);
+ }
+ role B
+ {
+  fresh Text1,Text8,Text9: Ticket;
+  fresh Rb: Nonce;
+  var Text3,Text4,Text6,Text7: Ticket;
+  var Ra,Rpa: Nonce;
+
+  send_1(B,A, Rb,B,Text1 );
+  recv_4(A,B, A, Text7,Ra,A,pk(A),{Rb,A,pk(A),Text3}sk(T),{Rb,Ra,B,A,Text6}sk(A) );
+  claim(B,Running,A,Ra,Rb,Text8);
+  send_5(B,A, Ra,Rb,Text9,{A,Ra,Rb,B,Text8}sk(B) );
+
+  claim(B,Commit,A,Ra,Rb,Text6);
+  claim(B,Alive);
+ }
+ role T
+ {
+  var Rpa,Rb: Nonce;
+  var Text2: Ticket;
+  fresh Text3,Text4,Text5: Ticket;
+
+  recv_2(A,T, Rpa,Rb,A,Text2 );
+  send_3(T,A, Text5, A,pk(A),B,pk(B),{Rpa,B,pk(B),Text4}sk(T),{Rb,A,pk(A),Text3}sk(T) );
+ }
+}
diff --git a/gui/Protocols/ISO-9798/isoiec-9798-3-7-2.cpp b/gui/Protocols/ISO-9798/isoiec-9798-3-7-2.cpp
new file mode 100644
index 0000000..6ca070b
--- /dev/null
+++ b/gui/Protocols/ISO-9798/isoiec-9798-3-7-2.cpp
@@ -0,0 +1,12 @@
+#define NAME isoiec-9798-3-7-2
+#define IA A
+#define IB B
+#define ResA A,pk(A)
+#define ResB B,pk(B)
+#define TokenAB Rpa,Text7,TokenTA,{Rb,Ra,B,A,Text6}sk(A)
+#define TokenBA Ra,Rb,Text9,{Ra,Rb,A,B,Text8}sk(B)
+#define TokenTA ResA,ResB,{Rpa,Rb,ResA,ResB,Text3}sk(T)
+
+#include "isoiec-9798-3-7.template"
+
+
diff --git a/gui/Protocols/ISO-9798/isoiec-9798-3-7-2.spdl b/gui/Protocols/ISO-9798/isoiec-9798-3-7-2.spdl
new file mode 100644
index 0000000..98ce424
--- /dev/null
+++ b/gui/Protocols/ISO-9798/isoiec-9798-3-7-2.spdl
@@ -0,0 +1,68 @@
+
+
+/*
+ * Modeled from ISO standard
+ *
+ * signature
+ * ttp
+ * five-pass
+ * mutual
+ *
+ * B initiates and A communicates with T
+ *
+ * parameters:
+ *
+ * 	NAME
+ * 	IA
+ * 	IB
+ * 	ResA
+ * 	ResB
+ * 	TokenAB
+ * 	TokenBA (although identical in both cases)
+ * 	TokenTA
+ *
+ */
+protocol isoiec-9798-3-7-2(A,B,T)
+{
+ role A
+ {
+  fresh Ra,Rpa: Nonce;
+  var Rb: Nonce;
+  var Text1,Text3,Text4,Text5,Text8,Text9: Ticket;
+  fresh Text2,Text6,Text7: Ticket;
+
+  recv_1(B,A, Rb,B,Text1 );
+  send_2(A,T, Rpa,Rb,A,Text2 );
+  recv_3(T,A, Text5, A,pk(A),B,pk(B),{Rpa,Rb,A,pk(A),B,pk(B),Text3}sk(T) );
+  claim(A,Running,B,Ra,Rb,Text6);
+  send_4(A,B, A, Rpa,Text7,A,pk(A),B,pk(B),{Rpa,Rb,A,pk(A),B,pk(B),Text3}sk(T),{Rb,Ra,B,A,Text6}sk(A) );
+  recv_5(B,A, Ra,Rb,Text9,{Ra,Rb,A,B,Text8}sk(B) );
+
+  claim(A,Commit,B,Ra,Rb,Text8);
+  claim(A,Alive);
+ }
+ role B
+ {
+  fresh Text1,Text8,Text9: Ticket;
+  fresh Rb: Nonce;
+  var Text3,Text4,Text6,Text7: Ticket;
+  var Ra,Rpa: Nonce;
+
+  send_1(B,A, Rb,B,Text1 );
+  recv_4(A,B, A, Rpa,Text7,A,pk(A),B,pk(B),{Rpa,Rb,A,pk(A),B,pk(B),Text3}sk(T),{Rb,Ra,B,A,Text6}sk(A) );
+  claim(B,Running,A,Ra,Rb,Text8);
+  send_5(B,A, Ra,Rb,Text9,{Ra,Rb,A,B,Text8}sk(B) );
+
+  claim(B,Commit,A,Ra,Rb,Text6);
+  claim(B,Alive);
+ }
+ role T
+ {
+  var Rpa,Rb: Nonce;
+  var Text2: Ticket;
+  fresh Text3,Text4,Text5: Ticket;
+
+  recv_2(A,T, Rpa,Rb,A,Text2 );
+  send_3(T,A, Text5, A,pk(A),B,pk(B),{Rpa,Rb,A,pk(A),B,pk(B),Text3}sk(T) );
+ }
+}
diff --git a/gui/Protocols/ISO-9798/isoiec-9798-3-7.template b/gui/Protocols/ISO-9798/isoiec-9798-3-7.template
new file mode 100644
index 0000000..8d9491a
--- /dev/null
+++ b/gui/Protocols/ISO-9798/isoiec-9798-3-7.template
@@ -0,0 +1,67 @@
+/*
+ * Modeled from ISO standard
+ *
+ * signature
+ * ttp
+ * five-pass
+ * mutual
+ *
+ * B initiates and A communicates with T
+ *
+ * parameters:
+ *
+ * 	NAME
+ * 	IA
+ * 	IB
+ * 	ResA
+ * 	ResB
+ * 	TokenAB
+ * 	TokenBA (although identical in both cases)
+ * 	TokenTA
+ *
+ */
+protocol NAME(A,B,T)
+{
+	role A
+	{
+		fresh Ra,Rpa: Nonce;
+		var Rb: Nonce;
+		var Text1,Text3,Text4,Text5,Text8,Text9: Ticket;
+		fresh Text2,Text6,Text7: Ticket;
+
+		recv_1(B,A, Rb,IB,Text1 );
+		send_2(A,T, Rpa,Rb,IA,Text2 );
+		recv_3(T,A, Text5, TokenTA );
+		claim(A,Running,B,Ra,Rb,Text6);
+		send_4(A,B, IA, TokenAB );
+		recv_5(B,A, TokenBA );
+
+		claim(A,Commit,B,Ra,Rb,Text8);
+		claim(A,Alive);
+	}
+	role B
+	{
+		fresh Text1,Text8,Text9: Ticket;
+		fresh Rb: Nonce;
+		var Text3,Text4,Text6,Text7: Ticket;
+		var Ra,Rpa: Nonce;
+
+		send_1(B,A, Rb,IB,Text1 );
+		recv_4(A,B, IA, TokenAB );
+		claim(B,Running,A,Ra,Rb,Text8);
+		send_5(B,A, TokenBA );
+
+		claim(B,Commit,A,Ra,Rb,Text6);
+		claim(B,Alive);
+	}
+	role T
+	{
+		var Rpa,Rb: Nonce;
+		var Text2: Ticket;
+		fresh Text3,Text4,Text5: Ticket;
+
+		recv_2(A,T, Rpa,Rb,IA,Text2 );
+		send_3(T,A, Text5, TokenTA );
+	}
+}
+
diff --git a/gui/Protocols/ISO-9798/isoiec-9798-4-1-udkey.spdl b/gui/Protocols/ISO-9798/isoiec-9798-4-1-udkey.spdl
new file mode 100644
index 0000000..6a955d0
--- /dev/null
+++ b/gui/Protocols/ISO-9798/isoiec-9798-4-1-udkey.spdl
@@ -0,0 +1,39 @@
+/*
+ * Modeled from ISO/IEC 9798
+ * Modeler: Cas Cremers, Dec. 2010
+ *
+ * ccf
+ * one-pass
+ * unilateral
+ *
+ * Unidirectional key version.
+ * 
+ * Modeling notes:
+ *
+ * - The keyed CCF (f_kab(x)) is modeled as f(x,kab)
+ */
+hashfunction f;
+
+protocol isoiec-9798-4-1-udkey(A,B)
+{
+	role A
+	{
+		fresh Text1,Text2: Ticket;
+		fresh TNA: Nonce;
+
+		claim(A,Running,B,TNA,Text1);
+		send_1(A,B, TNA, Text2, f( TNA, Text1 ,k(A,B) ) );
+	}
+	role B
+	{
+		var TNA: Nonce;
+		var Text1,Text2: Ticket;
+
+		recv_1(A,B, TNA, Text2, f( TNA, Text1 ,k(A,B) ) );
+
+		claim(B,Commit,A,TNA,Text1);
+		claim(B,Alive);
+		claim(B,Weakagree);
+	}
+}
+
diff --git a/gui/Protocols/ISO-9798/isoiec-9798-4-1.spdl b/gui/Protocols/ISO-9798/isoiec-9798-4-1.spdl
new file mode 100644
index 0000000..f3a5b95
--- /dev/null
+++ b/gui/Protocols/ISO-9798/isoiec-9798-4-1.spdl
@@ -0,0 +1,58 @@
+/*
+ * Modeled from ISO/IEC 9798
+ * Modeler: Cas Cremers, Dec. 2010, Feb. 2011.
+ *
+ * History:
+ * 
+ * - v2.0, Feb. 2011:
+ *   Added key symmetry emulation protocol.
+ *
+ * ccf
+ * one-pass
+ * unilateral
+ *
+ * The identifier B is optional and may be omitted if the key is unidirectional.
+ * 
+ * Modeling notes:
+ *
+ * - The keyed CCF (f_kab(x)) is modeled as f(x,kab)
+ */
+hashfunction f;
+
+protocol @keysymm-41(A,B)
+{
+	role A
+	{
+		var X,Y,Z: Ticket;
+
+		recv_!1(B,A, f(X,Y,Z, k(A,B) ) );
+		send_!2(A,B, f(X,Y,Z, k(B,A) ) );
+	}
+	role B
+	{
+	}
+}
+
+protocol isoiec-9798-4-1(A,B)
+{
+	role A
+	{
+		fresh Text1,Text2: Ticket;
+		fresh TNA: Nonce;
+
+		claim(A,Running,B,TNA,Text1);
+		send_1(A,B, TNA, Text2, f( TNA, B, Text1 ,k(A,B) ) );
+	}
+	role B
+	{
+		var TNA: Nonce;
+		var Text1,Text2: Ticket;
+
+		recv_1(A,B, TNA, Text2, f( TNA, B, Text1 ,k(A,B) ) );
+
+		claim(B,Commit,A,TNA,Text1);
+		claim(B,Alive);
+		claim(B,Weakagree);
+	}
+}
+
diff --git a/gui/Protocols/ISO-9798/isoiec-9798-4-2-udkey.spdl b/gui/Protocols/ISO-9798/isoiec-9798-4-2-udkey.spdl
new file mode 100644
index 0000000..c1e292f
--- /dev/null
+++ b/gui/Protocols/ISO-9798/isoiec-9798-4-2-udkey.spdl
@@ -0,0 +1,43 @@
+/*
+ * Modeled from ISO/IEC 9798
+ * Modeler: Cas Cremers, Dec. 2010
+ *
+ * ccf
+ * unilateral
+ * two-pass
+ * 
+ * Unidirectional key version.
+ * 
+ * Modeling notes:
+ *
+ * - The keyed CCF (f_kab(x)) is modeled as f(x,kab)
+ */
+hashfunction f;
+
+protocol isoiec-9798-4-2-udkey(A,B)
+{
+	role A
+	{
+		var Rb: Nonce;
+		var Text1: Ticket;
+		fresh Text2,Text3: Ticket;
+
+		recv_1(B,A, Rb,Text1 );
+		claim(A,Running,B,Rb,Text2);
+		send_2(A,B, Text3, f( Rb, Text2, k(A,B)) );
+	}
+	role B
+	{
+		fresh Rb: Nonce;
+		fresh Text1: Ticket;
+		var Text2,Text3: Ticket;
+
+		send_1(B,A, Rb,Text1 );
+		recv_2(A,B, Text3, f( Rb, Text2, k(A,B)) );
+
+		claim(B,Commit,A,Rb,Text2);
+		claim(B,Alive);
+		claim(B,Weakagree);
+	}
+}
+
diff --git a/gui/Protocols/ISO-9798/isoiec-9798-4-2.spdl b/gui/Protocols/ISO-9798/isoiec-9798-4-2.spdl
new file mode 100644
index 0000000..d2bd4a9
--- /dev/null
+++ b/gui/Protocols/ISO-9798/isoiec-9798-4-2.spdl
@@ -0,0 +1,62 @@
+/*
+ * Modeled from ISO/IEC 9798
+ * Modeler: Cas Cremers, Dec. 2010, Feb. 2011.
+ *
+ * History:
+ * 
+ * - v2.0, Feb. 2011:
+ *   Added key symmetry emulation protocol.
+ *
+ * ccf
+ * unilateral
+ * two-pass
+ * 
+ * The identifier B is optional and may be omitted if the key is unidirectional.
+ * 
+ * Modeling notes:
+ *
+ * - The keyed CCF (f_kab(x)) is modeled as f(x,kab)
+ */
+hashfunction f;
+
+protocol @keysymm-42(A,B)
+{
+	role A
+	{
+		var X,Y,Z: Ticket;
+
+		recv_!1(B,A, f(X,Y,Z, k(A,B) ) );
+		send_!2(A,B, f(X,Y,Z, k(B,A) ) );
+	}
+	role B
+	{
+	}
+}
+
+protocol isoiec-9798-4-2(A,B)
+{
+	role A
+	{
+		var Rb: Nonce;
+		var Text1: Ticket;
+		fresh Text2,Text3: Ticket;
+
+		recv_1(B,A, Rb,Text1 );
+		claim(A,Running,B,Rb,Text2);
+		send_2(A,B, Text3, f( Rb, B, Text2, k(A,B)) );
+	}
+	role B
+	{
+		fresh Rb: Nonce;
+		fresh Text1: Ticket;
+		var Text2,Text3: Ticket;
+
+		send_1(B,A, Rb,Text1 );
+		recv_2(A,B, Text3, f( Rb, B, Text2, k(A,B)) );
+
+		claim(B,Commit,A,Rb,Text2);
+		claim(B,Alive);
+		claim(B,Weakagree);
+	}
+}
+
diff --git a/gui/Protocols/ISO-9798/isoiec-9798-4-3-udkey.spdl b/gui/Protocols/ISO-9798/isoiec-9798-4-3-udkey.spdl
new file mode 100644
index 0000000..4371591
--- /dev/null
+++ b/gui/Protocols/ISO-9798/isoiec-9798-4-3-udkey.spdl
@@ -0,0 +1,50 @@
+/*
+ * Modeled from ISO/IEC 9798
+ * Modeler: Cas Cremers, Dec. 2010
+ *
+ * ccf
+ * two-pass
+ * mutual
+ *
+ * Unidirectional key version.
+ * 
+ * Modeling notes:
+ *
+ * - The keyed CCF (f_kab(x)) is modeled as f(x,kab)
+ */
+hashfunction f;
+
+protocol isoiec-9798-4-3-udkey(A,B)
+{
+	role A
+	{
+		fresh Text1,Text2: Ticket;
+		var Text3,Text4: Ticket;
+		fresh TNa: Nonce;
+		var TNb: Nonce;
+
+		claim(A,Running,B,TNa,Text1);
+		send_1(A,B, TNa, Text2, f(TNa,Text1, k(A,B) ) );
+		recv_2(B,A, TNb, Text4, f(TNb,Text3, k(B,A) ) );
+
+		claim(A,Commit,B,TNb,Text3);
+		claim(A,Alive);
+		claim(A,Weakagree);
+	}
+	role B
+	{
+		var TNa: Nonce;
+		fresh TNb: Nonce;
+		var Text1,Text2: Ticket;
+		fresh Text3,Text4: Ticket;
+
+		recv_1(A,B, TNa, Text2, f(TNa,Text1, k(A,B) ) );
+		claim(B,Running,A,TNb,Text3);
+		send_2(B,A, TNb, Text4, f(TNb,Text3, k(B,A) ) );
+
+		claim(B,Commit,A,TNa,Text1);
+		claim(B,Alive);
+		claim(B,Weakagree);
+	}
+}
+
diff --git a/gui/Protocols/ISO-9798/isoiec-9798-4-3.spdl b/gui/Protocols/ISO-9798/isoiec-9798-4-3.spdl
new file mode 100644
index 0000000..a5902e2
--- /dev/null
+++ b/gui/Protocols/ISO-9798/isoiec-9798-4-3.spdl
@@ -0,0 +1,69 @@
+/*
+ * Modeled from ISO/IEC 9798
+ * Modeler: Cas Cremers, Dec. 2010, Feb. 2011.
+ *
+ * History:
+ * 
+ * - v2.0, Feb. 2011:
+ *   Added key symmetry emulation protocol.
+ *
+ * ccf
+ * two-pass
+ * mutual
+ *
+ * The identifiers B,A are optional and may be (independently) be omitted if the key is unidirectional.
+ * 
+ * Modeling notes:
+ *
+ * - The keyed CCF (f_kab(x)) is modeled as f(x,kab)
+ */
+hashfunction f;
+
+protocol @keysymm-43(A,B)
+{
+	role A
+	{
+		var X,Y,Z: Ticket;
+
+		recv_!1(B,A, f(X,Y,Z, k(A,B) ) );
+		send_!2(A,B, f(X,Y,Z, k(B,A) ) );
+	}
+	role B
+	{
+	}
+}
+
+protocol isoiec-9798-4-3(A,B)
+{
+	role A
+	{
+		fresh Text1,Text2: Ticket;
+		var Text3,Text4: Ticket;
+		fresh TNa: Nonce;
+		var TNb: Nonce;
+
+		claim(A,Running,B,TNa,Text1);
+		send_1(A,B, TNa, Text2, f(TNa,B,Text1, k(A,B) ) );
+		recv_2(B,A, TNb, Text4, f(TNb,A,Text3, k(A,B) ) );
+
+		claim(A,Commit,B,TNb,Text3);
+		claim(A,Alive);
+		claim(A,Weakagree);
+	}
+	role B
+	{
+		var TNa: Nonce;
+		fresh TNb: Nonce;
+		var Text1,Text2: Ticket;
+		fresh Text3,Text4: Ticket;
+
+		recv_1(A,B, TNa, Text2, f(TNa,B,Text1, k(A,B) ) );
+		claim(B,Running,A,TNb,Text3);
+		send_2(B,A, TNb, Text4, f(TNb,A,Text3, k(A,B) ) );
+
+		claim(B,Commit,A,TNa,Text1);
+		claim(B,Alive);
+		claim(B,Weakagree);
+	}
+}
+
diff --git a/gui/Protocols/ISO-9798/isoiec-9798-4-4-udkey.spdl b/gui/Protocols/ISO-9798/isoiec-9798-4-4-udkey.spdl
new file mode 100644
index 0000000..27e5466
--- /dev/null
+++ b/gui/Protocols/ISO-9798/isoiec-9798-4-4-udkey.spdl
@@ -0,0 +1,52 @@
+/*
+ * Modeled from ISO/IEC 9798
+ * Modeler: Cas Cremers, Dec. 2010
+ *
+ * ccf
+ * mutual
+ * three-pass
+ * 
+ * Unidirectional key version.
+ * 
+ * Modeling notes:
+ *
+ * - The keyed CCF (f_kab(x)) is modeled as f(x,kab)
+ */
+hashfunction f;
+
+protocol isoiec-9798-4-4-udkey(A,B)
+{
+	role A
+	{
+		fresh Ra: Nonce;
+		var Rb: Nonce;
+		var Text1,Text4,Text5: Ticket;
+		fresh Text2,Text3: Ticket;
+
+		recv_1(B,A, Rb, Text1 );
+		claim(A,Running,B,Ra,Rb,Text2);
+		send_2(A,B, Ra, Text3, f(Ra,Rb,Text2, k(A,B) ) );
+		recv_3(B,A, Text5, f(Rb,Ra,Text4, k(B,A) ) );
+
+		claim(A,Commit,B,Ra,Rb,Text2,Text4);
+		claim(A,Alive);
+		claim(A,Weakagree);
+	}
+	role B
+	{
+		var Ra: Nonce;
+		fresh Rb: Nonce;
+		fresh Text1,Text4,Text5: Ticket;
+		var Text2,Text3: Ticket;
+
+		send_1(B,A, Rb, Text1 );
+		recv_2(A,B, Ra, Text3, f(Ra,Rb,Text2, k(A,B) ) );
+		claim(B,Running,A,Ra,Rb,Text2,Text4);
+		send_3(B,A, Text5, f(Rb,Ra,Text4, k(B,A) ) );
+
+		claim(B,Commit,A,Ra,Rb,Text2);
+		claim(B,Alive);
+		claim(B,Weakagree);
+	}
+}
+
diff --git a/gui/Protocols/ISO-9798/isoiec-9798-4-4.spdl b/gui/Protocols/ISO-9798/isoiec-9798-4-4.spdl
new file mode 100644
index 0000000..f796369
--- /dev/null
+++ b/gui/Protocols/ISO-9798/isoiec-9798-4-4.spdl
@@ -0,0 +1,75 @@
+/*
+ * Modeled from ISO/IEC 9798
+ * Modeler: Cas Cremers, Dec. 2010, Feb. 2011.
+ *
+ * History:
+ * 
+ * - v2.0, Feb. 2011:
+ *   Added key symmetry emulation protocol.
+ *
+ * ccf
+ * mutual
+ * three-pass
+ * 
+ * The identifier B is optional and may be omitted if the key is unidirectional.
+ * 
+ * Modeling notes:
+ *
+ * - The keyed CCF (f_kab(x)) is modeled as f(x,kab)
+ */
+hashfunction f;
+
+protocol @keysymm-44(A,B)
+{
+	role A
+	{
+		var X,Y,Z: Ticket;
+
+		recv_!1(B,A, f(X,Y,Z, k(A,B) ) );
+		send_!2(A,B, f(X,Y,Z, k(B,A) ) );
+	}
+	role B
+	{
+		var X,Y,Z,ZZ: Ticket;
+
+		recv_!3(A,B, f(X,Y,Z,ZZ, k(A,B) ) );
+		send_!4(B,A, f(X,Y,Z,ZZ, k(B,A) ) );
+	}
+}
+
+protocol isoiec-9798-4-4(A,B)
+{
+	role A
+	{
+		fresh Ra: Nonce;
+		var Rb: Nonce;
+		var Text1,Text4,Text5: Ticket;
+		fresh Text2,Text3: Ticket;
+
+		recv_1(B,A, Rb, Text1 );
+		claim(A,Running,B,Ra,Rb,Text2);
+		send_2(A,B, Ra, Text3, f(Ra,Rb,B,Text2, k(A,B) ) );
+		recv_3(B,A, Text5, f(Rb,Ra,Text4, k(A,B) ) );
+
+		claim(A,Commit,B,Ra,Rb,Text2,Text4);
+		claim(A,Alive);
+		claim(A,Weakagree);
+	}
+	role B
+	{
+		var Ra: Nonce;
+		fresh Rb: Nonce;
+		fresh Text1,Text4,Text5: Ticket;
+		var Text2,Text3: Ticket;
+
+		send_1(B,A, Rb, Text1 );
+		recv_2(A,B, Ra, Text3, f(Ra,Rb,B,Text2, k(A,B) ) );
+		claim(B,Running,A,Ra,Rb,Text2,Text4);
+		send_3(B,A, Text5, f(Rb,Ra,Text4, k(A,B) ) );
+
+		claim(B,Commit,A,Ra,Rb,Text2);
+		claim(B,Alive);
+		claim(B,Weakagree);
+	}
+}
+