diff --git a/gui/Protocols/IEEE-WIMAX/pkmv2rsa.spdl b/gui/Protocols/IEEE-WIMAX/pkmv2rsa.spdl
new file mode 100644
index 0000000..73133a7
--- /dev/null
+++ b/gui/Protocols/IEEE-WIMAX/pkmv2rsa.spdl
@@ -0,0 +1,46 @@
+/* 
+ * PKMv2-RSA
+ *
+ * Initial model by:	Sjouke Mauw, Sasa Radomirovic (2007)
+ * Model changes:	Cas Cremers (Nov 2012)
+ *
+ * Analysed in:		"A framework for compositional verification of security protocols"
+ * 			With S. Andova, K. Gjosteen, S. Mauw, S. Mjolsnes, and S. Radomirovic.
+ * 			Information and Computation, Special issue on Computer Security: 
+ * 			Foundations and Automated Reasoning, Volume 206, Issues 2-4, pp. 425-459,
+ * 			Elsevier, 2008. 
+ */
+
+// The protocol description
+
+protocol pkmv2rsa(MS,BS)
+{
+	role MS
+	{
+		fresh msrand, said: Nonce;
+		var prepak, bsrand: Nonce;
+
+		send_rsa1(MS,BS, {msrand, said, MS}sk(MS) );
+		recv_rsa2(BS,MS, {msrand, bsrand,{prepak,MS}pk(MS),BS}sk(BS) );
+		send_rsa3(MS,BS, {bsrand}sk(MS) );
+
+		claim_rsai3(MS,Niagree);
+		claim_rsai4(MS,Nisynch);
+		claim_rsai5(MS,SKR,prepak);
+	}	
+	
+	role BS
+	{
+		var msrand, said: Nonce;
+		fresh prepak, bsrand: Nonce;
+
+		recv_rsa1(MS,BS, {msrand, said, MS}sk(MS) );
+		send_rsa2(BS,MS, {msrand, bsrand,{prepak,MS}pk(MS),BS}sk(BS) );
+		recv_rsa3(MS,BS, {bsrand}sk(MS) );
+
+		claim_rsar3(BS,Niagree);
+		claim_rsar4(BS,Nisynch);
+		claim_rsar5(BS,SKR,prepak);
+	}
+}
+
diff --git a/gui/Protocols/IEEE-WIMAX/pkmv2rsacorrected.spdl b/gui/Protocols/IEEE-WIMAX/pkmv2rsacorrected.spdl
new file mode 100644
index 0000000..4bd5205
--- /dev/null
+++ b/gui/Protocols/IEEE-WIMAX/pkmv2rsacorrected.spdl
@@ -0,0 +1,46 @@
+/* 
+ * PKMv2-RSA
+ *
+ * Initial model by:	Sjouke Mauw, Sasa Radomirovic (2007)
+ * Model changes:	Cas Cremers (Nov 2012)
+ *
+ * Analysed in:		"A framework for compositional verification of security protocols"
+ * 			With S. Andova, K. Gjosteen, S. Mauw, S. Mjolsnes, and S. Radomirovic.
+ * 			Information and Computation, Special issue on Computer Security: 
+ * 			Foundations and Automated Reasoning, Volume 206, Issues 2-4, pp. 425-459,
+ * 			Elsevier, 2008. 
+ */
+
+// The protocol description
+
+protocol pkmv2rsa(MS,BS)
+{
+	role MS
+	{
+		fresh msrand, said: Nonce;
+		var prepak, bsrand: Nonce;
+
+		send_rsa1(MS,BS, {msrand, said, MS}sk(MS) );
+		recv_rsa2(BS,MS, {msrand, bsrand,{prepak,MS}pk(MS),BS}sk(BS) );
+		send_rsa3(MS,BS, {bsrand,BS}sk(MS) );
+
+		claim_rsai3(MS,Niagree);
+		claim_rsai4(MS,Nisynch);
+		claim_rsai5(MS,SKR,prepak);
+	}	
+	
+	role BS
+	{
+		var msrand, said: Nonce;
+		fresh prepak, bsrand: Nonce;
+
+		recv_rsa1(MS,BS, {msrand, said, MS}sk(MS) );
+		send_rsa2(BS,MS, {msrand, bsrand,{prepak,MS}pk(MS),BS}sk(BS) );
+		recv_rsa3(MS,BS, {bsrand,BS}sk(MS) );
+
+		claim_rsar3(BS,Niagree);
+		claim_rsar4(BS,Nisynch);
+		claim_rsar5(BS,SKR,prepak);
+	}
+}
+
diff --git a/gui/Protocols/IEEE-WIMAX/pkmv2satek.spdl b/gui/Protocols/IEEE-WIMAX/pkmv2satek.spdl
new file mode 100644
index 0000000..b166a1b
--- /dev/null
+++ b/gui/Protocols/IEEE-WIMAX/pkmv2satek.spdl
@@ -0,0 +1,63 @@
+/* 
+ * PKMv2-SA-TEK
+ *
+ * Initial model by:	Sjouke Mauw, Sasa Radomirovic (2007)
+ * Model changes:	Cas Cremers (Nov 2012)
+ *
+ * Analysed in:		"A framework for compositional verification of security protocols"
+ * 			With S. Andova, K. Gjosteen, S. Mauw, S. Mjolsnes, and S. Radomirovic.
+ * 			Information and Computation, Special issue on Computer Security: 
+ * 			Foundations and Automated Reasoning, Volume 206, Issues 2-4, pp. 425-459,
+ * 			Elsevier, 2008. 
+ */
+
+// Setup
+
+hashfunction hash;
+hashfunction prepak;
+const akid;
+const u,d;
+
+// The protocol description
+
+protocol pkmv2satek(MS,BS)
+{
+  role MS
+  {
+    fresh msrand': Nonce;
+    var bsrand', tek0, tek1: Nonce;
+
+    recv_satek1(BS,MS, bsrand',akid,
+      hash(d,prepak(MS,BS),BS,MS,bsrand',akid) );
+    send_satek2(MS,BS, msrand',bsrand',akid,
+      hash(u,prepak(MS,BS),BS,MS,msrand',bsrand',akid) );
+    recv_satek3(BS,MS,
+    msrand',bsrand',akid,{tek0,tek1}hash(prepak(MS,BS)),
+      hash(d,prepak(MS,BS),msrand',bsrand',akid,{tek0,tek1}hash(prepak(MS,BS))));
+
+    claim_rsai3(MS,Niagree);
+    claim_rsai4(MS,Nisynch);
+    claim_rsai6(MS,SKR,tek0);
+    claim_rsai7(MS,SKR,tek1);
+  } 
+  
+  role BS
+  {
+    var msrand': Nonce;
+    fresh bsrand', tek0, tek1: Nonce;
+
+    send_satek1(BS,MS, bsrand',akid,
+      hash(d,prepak(MS,BS),BS,MS,bsrand',akid) );
+    recv_satek2(MS,BS, msrand',bsrand',akid,
+      hash(u,prepak(MS,BS),BS,MS,msrand',bsrand',akid) );
+    send_satek3(BS,MS,
+    msrand',bsrand',akid,{tek0,tek1}hash(prepak(MS,BS)),
+      hash(d,prepak(MS,BS),msrand',bsrand',akid,{tek0,tek1}hash(prepak(MS,BS))));
+
+    claim_rsar3(BS,Niagree);
+    claim_rsar4(BS,Nisynch);
+    claim_rsar6(BS,SKR,tek0);
+    claim_rsar7(BS,SKR,tek1);
+  }
+}
+
diff --git a/gui/Protocols/IEEE-WIMAX/pqr.spdl b/gui/Protocols/IEEE-WIMAX/pqr.spdl
new file mode 100644
index 0000000..731d369
--- /dev/null
+++ b/gui/Protocols/IEEE-WIMAX/pqr.spdl
@@ -0,0 +1,84 @@
+/* 
+ * PKMv2-RSA
+ *
+ * Initial model by:	Sjouke Mauw, Sasa Radomirovic (2007)
+ * Model changes:	Cas Cremers (Nov 2012)
+ *
+ * Analysed in:		"A framework for compositional verification of security protocols"
+ * 			With S. Andova, K. Gjosteen, S. Mauw, S. Mjolsnes, and S. Radomirovic.
+ * 			Information and Computation, Special issue on Computer Security: 
+ * 			Foundations and Automated Reasoning, Volume 206, Issues 2-4, pp. 425-459,
+ * 			Elsevier, 2008. 
+ */
+
+// Setup
+
+hashfunction hash;
+hashfunction prepak;
+const akid;
+const u,d;
+
+// The protocol description
+
+protocol rsaplussatek(MS,BS)
+
+{
+  role MS
+  {
+    fresh msrand, msrand', said, c: Nonce;
+    var prepak, bsrand, bsrand', tek0, tek1, tek2, tek3: Nonce;
+
+    send_rsa1(MS,BS, {msrand, said, MS}sk(MS) );
+    recv_rsa2(BS,MS, {msrand, bsrand,{prepak,MS}pk(MS),BS}sk(BS) );
+    send_rsa3(MS,BS, {bsrand, BS}sk(MS) );
+
+    recv_satek1(BS,MS, bsrand',akid,
+      hash(d,prepak,BS,MS,bsrand',akid) );
+    send_satek2(MS,BS, msrand',bsrand',akid,
+      hash(u,prepak,BS,MS,msrand',bsrand',akid) );
+    recv_satek3(BS,MS,
+    msrand',bsrand',akid,{tek0,tek1}hash(prepak),
+      hash(d,prepak,msrand',bsrand',akid,{tek0,tek1}hash(prepak)));
+
+    send_tekup1(MS,BS,{c}hash(prepak));
+    recv_tekup2(BS,MS,{c,tek2,tek3}hash(prepak));
+
+    claim_rsai3(MS,Niagree);
+    claim_rsai4(MS,Nisynch);
+    claim_rsai5(MS,SKR,prepak);
+    claim_rsai6(MS,SKR,tek0);
+    claim_rsai7(MS,SKR,tek1);
+    claim_rsar8(MS,SKR,tek2);
+    claim_rsar9(MS,SKR,tek3);
+  } 
+  
+  role BS
+  {
+    var msrand, msrand', said, c: Nonce;
+    fresh prepak, bsrand, bsrand', tek0, tek1, tek2, tek3: Nonce;
+
+    recv_rsa1(MS,BS, {msrand, said, MS}sk(MS) );
+    send_rsa2(BS,MS, {msrand, bsrand,{prepak,MS}pk(MS),BS}sk(BS) );
+    recv_rsa3(MS,BS, {bsrand, BS}sk(MS) );
+
+    send_satek1(BS,MS, bsrand',akid,
+      hash(d,prepak,BS,MS,bsrand',akid) );
+    recv_satek2(MS,BS, msrand',bsrand',akid,
+      hash(u,prepak,BS,MS,msrand',bsrand',akid) );
+    send_satek3(BS,MS,
+    msrand',bsrand',akid,{tek0,tek1}hash(prepak),
+      hash(d,prepak,msrand',bsrand',akid,{tek0,tek1}hash(prepak)));
+
+    recv_tekup1(MS,BS,{c}hash(prepak));
+    send_tekup2(BS,MS,{c,tek2,tek3}hash(prepak));
+
+    claim_rsar3(BS,Niagree);
+    claim_rsar4(BS,Nisynch);
+    claim_rsar5(BS,SKR,prepak);
+    claim_rsar6(BS,SKR,tek0);
+    claim_rsar7(BS,SKR,tek1);
+    claim_rsar8(BS,SKR,tek2);
+    claim_rsar9(BS,SKR,tek3);
+  }
+}
+
diff --git a/gui/Protocols/IEEE-WIMAX/rsaplussatek.spdl b/gui/Protocols/IEEE-WIMAX/rsaplussatek.spdl
new file mode 100644
index 0000000..eb15dde
--- /dev/null
+++ b/gui/Protocols/IEEE-WIMAX/rsaplussatek.spdl
@@ -0,0 +1,74 @@
+/* 
+ * PKMv2-RSA
+ *
+ * Initial model by:	Sjouke Mauw, Sasa Radomirovic (2007)
+ * Model changes:	Cas Cremers (Nov 2012)
+ *
+ * Analysed in:		"A framework for compositional verification of security protocols"
+ * 			With S. Andova, K. Gjosteen, S. Mauw, S. Mjolsnes, and S. Radomirovic.
+ * 			Information and Computation, Special issue on Computer Security: 
+ * 			Foundations and Automated Reasoning, Volume 206, Issues 2-4, pp. 425-459,
+ * 			Elsevier, 2008. 
+ */
+
+// Setup
+
+hashfunction hash;
+hashfunction prepak;
+const akid;
+const u,d;
+
+// The protocol description
+
+protocol rsaplussatek(MS,BS)
+
+{
+  role MS
+  {
+    fresh msrand, msrand', said: Nonce;
+    var prepak, bsrand, bsrand', tek0, tek1: Nonce;
+
+    send_rsa1(MS,BS, {msrand, said, MS}sk(MS) );
+    recv_rsa2(BS,MS, {msrand, bsrand,{prepak,MS}pk(MS),BS}sk(BS) );
+    send_rsa3(MS,BS, {bsrand}sk(MS) );
+
+    recv_satek1(BS,MS, bsrand',akid,
+      hash(d,prepak,BS,MS,bsrand',akid) );
+    send_satek2(MS,BS, msrand',bsrand',akid,
+      hash(u,prepak,BS,MS,msrand',bsrand',akid) );
+    recv_satek3(BS,MS,
+    msrand',bsrand',akid,{tek0,tek1}hash(prepak),
+      hash(d,prepak,msrand',bsrand',akid,{tek0,tek1}hash(prepak)));
+
+    claim_rsai3(MS,Niagree);
+    claim_rsai4(MS,Nisynch);
+//    claim_rsai5(MS,SKR,prepak);
+//    claim_rsai6(MS,SKR,tek0);
+//    claim_rsai7(MS,SKR,tek1);
+  } 
+  
+  role BS
+  {
+    var msrand, msrand', said: Nonce;
+    fresh prepak, bsrand, bsrand', tek0, tek1: Nonce;
+
+    recv_rsa1(MS,BS, {msrand, said, MS}sk(MS) );
+    send_rsa2(BS,MS, {msrand, bsrand,{prepak,MS}pk(MS),BS}sk(BS) );
+    recv_rsa3(MS,BS, {bsrand}sk(MS) );
+
+    send_satek1(BS,MS, bsrand',akid,
+      hash(d,prepak,BS,MS,bsrand',akid) );
+    recv_satek2(MS,BS, msrand',bsrand',akid,
+      hash(u,prepak,BS,MS,msrand',bsrand',akid) );
+    send_satek3(BS,MS,
+    msrand',bsrand',akid,{tek0,tek1}hash(prepak),
+      hash(d,prepak,msrand',bsrand',akid,{tek0,tek1}hash(prepak)));
+
+    claim_rsar3(BS,Niagree);
+    claim_rsar4(BS,Nisynch);
+//    claim_rsar5(BS,SKR,prepak);
+//    claim_rsar6(BS,SKR,tek0);
+//    claim_rsar7(BS,SKR,tek1);
+  }
+}
+
diff --git a/gui/Protocols/IEEE-WIMAX/rsaplussatekcorrected.spdl b/gui/Protocols/IEEE-WIMAX/rsaplussatekcorrected.spdl
new file mode 100644
index 0000000..b8051d8
--- /dev/null
+++ b/gui/Protocols/IEEE-WIMAX/rsaplussatekcorrected.spdl
@@ -0,0 +1,73 @@
+/* 
+ * PKMv2-RSA
+ *
+ * Initial model by:	Sjouke Mauw, Sasa Radomirovic (2007)
+ * Model changes:	Cas Cremers (Nov 2012)
+ *
+ * Analysed in:		"A framework for compositional verification of security protocols"
+ * 			With S. Andova, K. Gjosteen, S. Mauw, S. Mjolsnes, and S. Radomirovic.
+ * 			Information and Computation, Special issue on Computer Security: 
+ * 			Foundations and Automated Reasoning, Volume 206, Issues 2-4, pp. 425-459,
+ * 			Elsevier, 2008. 
+ */
+
+// Setup
+
+hashfunction hash;
+hashfunction prepak;
+const akid;
+const u,d;
+
+// The protocol description
+
+protocol rsaplussatek(MS,BS)
+
+{
+  role MS
+  {
+    fresh msrand, msrand', said: Nonce;
+    var prepak, bsrand, bsrand', tek0, tek1: Nonce;
+
+    send_rsa1(MS,BS, {msrand, said, MS}sk(MS) );
+    recv_rsa2(BS,MS, {msrand, bsrand,{prepak,MS}pk(MS),BS}sk(BS) );
+    send_rsa3(MS,BS, {bsrand, BS}sk(MS) );
+
+    recv_satek1(BS,MS, bsrand',akid,
+      hash(d,prepak,BS,MS,bsrand',akid) );
+    send_satek2(MS,BS, msrand',bsrand',akid,
+      hash(u,prepak,BS,MS,msrand',bsrand',akid) );
+    recv_satek3(BS,MS,
+    msrand',bsrand',akid,{tek0,tek1}hash(prepak),
+      hash(d,prepak,msrand',bsrand',akid,{tek0,tek1}hash(prepak)));
+
+    claim_rsai3(MS,Niagree);
+    claim_rsai4(MS,Nisynch);
+    claim_rsai5(MS,SKR,prepak);
+    claim_rsai6(MS,SKR,tek0);
+    claim_rsai7(MS,SKR,tek1);
+  } 
+  
+  role BS
+  {
+    var msrand, msrand', said: Nonce;
+    fresh prepak, bsrand, bsrand', tek0, tek1: Nonce;
+
+    recv_rsa1(MS,BS, {msrand, said, MS}sk(MS) );
+    send_rsa2(BS,MS, {msrand, bsrand,{prepak,MS}pk(MS),BS}sk(BS) );
+    recv_rsa3(MS,BS, {bsrand, BS}sk(MS) );
+
+    send_satek1(BS,MS, bsrand',akid,
+      hash(d,prepak,BS,MS,bsrand',akid) );
+    recv_satek2(MS,BS, msrand',bsrand',akid,
+      hash(u,prepak,BS,MS,msrand',bsrand',akid) );
+    send_satek3(BS,MS,
+    msrand',bsrand',akid,{tek0,tek1}hash(prepak),
+      hash(d,prepak,msrand',bsrand',akid,{tek0,tek1}hash(prepak)));
+
+    claim_rsar3(BS,Niagree);
+    claim_rsar4(BS,Nisynch);
+    claim_rsar5(BS,SKR,prepak);
+    claim_rsar6(BS,SKR,tek0);
+    claim_rsar7(BS,SKR,tek1);
+  }
+}