diff --git a/spdl/SPORE/andrew-ban-concrete.spdl b/spdl/SPORE/andrew-ban-concrete.spdl
index 059f917..7cbde7c 100644
--- a/spdl/SPORE/andrew-ban-concrete.spdl
+++ b/spdl/SPORE/andrew-ban-concrete.spdl
@@ -24,33 +24,33 @@ secret k: Function;
 
 protocol andrewConcrete(I,R)
 {
-	role I
-	{
-		const ni: Nonce;
-		var nr: Nonce;
+    role I
+    {
+        const ni: Nonce;
+        var nr: Nonce;
         var kir: SessionKey;
         
-		send_1(I,R, I,ni );
-		read_2(R,I, {ni,kir}k(I,R) );
-		send_3(I,R, {ni}kir);
+        send_1(I,R, I,ni );
+        read_2(R,I, {ni,kir}k(I,R) );
+        send_3(I,R, {ni}kir);
         claim_4(I,Secret,kir);
-		claim_5(I,Nisynch);
-		read_6(R,I, nr);
-	}	
-	
-	role R
-	{
-		var ni: Nonce;
-		const nr: Nonce;
+        claim_5(I,Nisynch);
+        read_6(R,I, nr);
+    }    
+    
+    role R
+    {
+        var ni: Nonce;
+        const nr: Nonce;
         const kir: SessionKey;
 
-		read_1(I,R, I,ni );
-		send_2(R,I, {ni,kir}k(I,R) );
-		read_3(I,R, {ni}kir);
-		send_6(R,I, nr);
-		claim_7(R,Secret,kir);
-		claim_8(R,Nisynch);
-	}
+        read_1(I,R, I,ni );
+        send_2(R,I, {ni,kir}k(I,R) );
+        read_3(I,R, {ni}kir);
+        send_6(R,I, nr);
+        claim_7(R,Secret,kir);
+        claim_8(R,Nisynch);
+    }
 }
 
 const Alice,Bob,Eve: Agent;
diff --git a/spdl/SPORE/andrew-ban.spdl b/spdl/SPORE/andrew-ban.spdl
index 1aa9b8b..dee1d2f 100644
--- a/spdl/SPORE/andrew-ban.spdl
+++ b/spdl/SPORE/andrew-ban.spdl
@@ -16,37 +16,37 @@ secret k: Function;
 
 protocol andrewBan(I,R)
 {
-	role I
-	{
-		const ni: Nonce;
-		var nr,nr2: Nonce;
-		var kir: SessionKey;
+    role I
+    {
+        const ni: Nonce;
+        var nr,nr2: Nonce;
+        var kir: SessionKey;
 
-		send_1(I,R, I,{ni}k(I,R) );
-		read_2(R,I, {ni,nr}k(I,R) );
-		send_3(I,R, {nr}k(I,R) );
-		read_4(R,I, {kir,nr2,ni}k(I,R) );
-		claim_5(I,Nisynch);
-		claim_5b(I,Niagree);
-		claim_6(I,Secret, kir);
-		claim_7(I,Secret, k(I,R));
-	}	
-	
-	role R
-	{
-		var ni: Nonce;
-		const nr,nr2: Nonce;
-		const kir: SessionKey;
+        send_1(I,R, I,{ni}k(I,R) );
+        read_2(R,I, {ni,nr}k(I,R) );
+        send_3(I,R, {nr}k(I,R) );
+        read_4(R,I, {kir,nr2,ni}k(I,R) );
+        claim_5(I,Nisynch);
+        claim_5b(I,Niagree);
+        claim_6(I,Secret, kir);
+        claim_7(I,Secret, k(I,R));
+    }    
+    
+    role R
+    {
+        var ni: Nonce;
+        const nr,nr2: Nonce;
+        const kir: SessionKey;
 
-		read_1(I,R, I,{ni}k(I,R) );
-		send_2(R,I, {ni,nr}k(I,R) );
-		read_3(I,R, {nr}k(I,R) );
-		send_4(R,I, {kir,nr2,ni}k(I,R) );
-		claim_8(R,Nisynch);
-		claim_8b(R,Niagree);
-		claim_9(R,Secret, kir);
-		claim_10(R,Secret, k(I,R));
-	}
+        read_1(I,R, I,{ni}k(I,R) );
+        send_2(R,I, {ni,nr}k(I,R) );
+        read_3(I,R, {nr}k(I,R) );
+        send_4(R,I, {kir,nr2,ni}k(I,R) );
+        claim_8(R,Nisynch);
+        claim_8b(R,Niagree);
+        claim_9(R,Secret, kir);
+        claim_10(R,Secret, k(I,R));
+    }
 }
 
 const Alice,Bob,Eve: Agent;
diff --git a/spdl/SPORE/andrew-lowe-ban.spdl b/spdl/SPORE/andrew-lowe-ban.spdl
index 6693afb..bbb0468 100644
--- a/spdl/SPORE/andrew-lowe-ban.spdl
+++ b/spdl/SPORE/andrew-lowe-ban.spdl
@@ -23,33 +23,33 @@ secret k: Function;
 
 protocol andrewLoweBan(I,R)
 {
-	role I
-	{
-		const ni: Nonce;
-		var nr: Nonce;
-		var kir: SessionKey;
+    role I
+    {
+        const ni: Nonce;
+        var nr: Nonce;
+        var kir: SessionKey;
 
-		send_1(I,R, I,ni );
-		read_2(R,I, {ni,kir,R}k(I,R) );
-		send_3(I,R, {ni}kir );
-		claim_5(I,Nisynch);
-		claim_6(I,Secret, kir);
-		read_4(R,I, nr );
-	}	
-	
-	role R
-	{
-		var ni: Nonce;
-		const nr: Nonce;
-		const kir: SessionKey;
+        send_1(I,R, I,ni );
+        read_2(R,I, {ni,kir,R}k(I,R) );
+        send_3(I,R, {ni}kir );
+        claim_5(I,Nisynch);
+        claim_6(I,Secret, kir);
+        read_4(R,I, nr );
+    }    
+    
+    role R
+    {
+        var ni: Nonce;
+        const nr: Nonce;
+        const kir: SessionKey;
 
-		read_1(I,R, I,ni );
-		send_2(R,I, {ni,kir,R}k(I,R) );
-		read_3(I,R, {ni}kir );
-		send_4(R,I, nr );
-		claim_8(R,Nisynch);
-		claim_9(R,Secret, kir);
-	}
+        read_1(I,R, I,ni );
+        send_2(R,I, {ni,kir,R}k(I,R) );
+        read_3(I,R, {ni}kir );
+        send_4(R,I, nr );
+        claim_8(R,Nisynch);
+        claim_9(R,Secret, kir);
+    }
 }
 
 const Alice,Bob,Eve: Agent;
diff --git a/spdl/SPORE/andrew.spdl b/spdl/SPORE/andrew.spdl
index ae53219..bd88ebd 100644
--- a/spdl/SPORE/andrew.spdl
+++ b/spdl/SPORE/andrew.spdl
@@ -15,33 +15,33 @@ const succ: Function;
 
 protocol andrew(I,R)
 {
-	role I
-	{
-		const ni: Nonce;
-		var nr,nr2: Nonce;
-		var kir: SessionKey;
+    role I
+    {
+        const ni: Nonce;
+        var nr,nr2: Nonce;
+        var kir: SessionKey;
 
-		send_1(I,R, I,{ni}k(I,R) );
-		read_2(R,I, {succ(ni),nr}k(I,R) );
-		send_3(I,R, {succ(nr)}k(I,R) );
-		read_4(R,I, {kir,nr2}k(I,R) );
-		claim_5(I,Secret,kir);
-		claim_6(I,Nisynch);
-	}	
-	
-	role R
-	{
-		var ni: Nonce;
-		const nr,nr2: Nonce;
-		const kir: SessionKey;
+        send_1(I,R, I,{ni}k(I,R) );
+        read_2(R,I, {succ(ni),nr}k(I,R) );
+        send_3(I,R, {succ(nr)}k(I,R) );
+        read_4(R,I, {kir,nr2}k(I,R) );
+        claim_5(I,Secret,kir);
+        claim_6(I,Nisynch);
+    }    
+    
+    role R
+    {
+        var ni: Nonce;
+        const nr,nr2: Nonce;
+        const kir: SessionKey;
 
-		read_1(I,R, I,{ni}k(I,R) );
-		send_2(R,I, {succ(ni),nr}k(I,R) );
-		read_3(I,R, {succ(nr)}k(I,R) );
-		send_4(R,I, {kir,nr2}k(I,R) );
-		claim_7(R,Secret,kir);
-		claim_8(R,Nisynch);
-	}
+        read_1(I,R, I,{ni}k(I,R) );
+        send_2(R,I, {succ(ni),nr}k(I,R) );
+        read_3(I,R, {succ(nr)}k(I,R) );
+        send_4(R,I, {kir,nr2}k(I,R) );
+        claim_7(R,Secret,kir);
+        claim_8(R,Nisynch);
+    }
 }
 
 const Alice,Bob,Eve: Agent;
diff --git a/spdl/SPORE/ccitt509-1.spdl b/spdl/SPORE/ccitt509-1.spdl
index 4f84af6..8cd3354 100644
--- a/spdl/SPORE/ccitt509-1.spdl
+++ b/spdl/SPORE/ccitt509-1.spdl
@@ -16,24 +16,24 @@ usertype Timestamp;
 
 protocol ccitt5091(I,R)
 {
-	role I
-	{
-		const Ta: Timestamp;
+    role I
+    {
+        const Ta: Timestamp;
         const Na,Xa,Ya: Nonce;
-		send_1(I,R, I,{Ta, Na, R, Xa,{Ya}pk(R)}sk(I));
+        send_1(I,R, I,{Ta, Na, R, Xa,{Ya}pk(R)}sk(I));
         # claim_2(I,Nisynch);
         # This claim is useless as there are no preceding read events
-	}	
-	
-	role R
-	{
-		var Ta: Timestamp;
+    }    
+    
+    role R
+    {
+        var Ta: Timestamp;
         var Na,Xa,Ya: Nonce;
 
-		read_1(I,R, I,{Ta, Na, R, Xa,{Ya}pk(R)}sk(I));
-		claim_3(R,Nisynch);
+        read_1(I,R, I,{Ta, Na, R, Xa,{Ya}pk(R)}sk(I));
+        claim_3(R,Nisynch);
         # There should also be Fresh Xa and Fresh Ya claims here
-	}
+    }
 }
 
 const Alice,Bob,Eve: Agent;
diff --git a/spdl/SPORE/ccitt509-1c.spdl b/spdl/SPORE/ccitt509-1c.spdl
index e6fc1db..a8b8560 100644
--- a/spdl/SPORE/ccitt509-1c.spdl
+++ b/spdl/SPORE/ccitt509-1c.spdl
@@ -15,24 +15,24 @@ usertype Timestamp;
 
 protocol ccitt5091c(I,R)
 {
-	role I
-	{
-		const Ta: Timestamp;
+    role I
+    {
+        const Ta: Timestamp;
         const Na,Xa,Ya: Nonce;
-		send_1(I,R, I,{Ta, Na, R, Xa,{Ya,{hash(Ya)}sk(I)}pk(R)}sk(I));
+        send_1(I,R, I,{Ta, Na, R, Xa,{Ya,{hash(Ya)}sk(I)}pk(R)}sk(I));
         # claim_2(I,Nisynch);
         # This claim is useless as there are no preceding read events
-	}	
-	
-	role R
-	{
-		var Ta: Timestamp;
+    }    
+    
+    role R
+    {
+        var Ta: Timestamp;
         var Na,Xa,Ya: Nonce;
 
-		read_1(I,R, I,{Ta, Na, R, Xa,{Ya,{hash(Ya)}sk(I)}pk(R)}sk(I));
-		claim_3(R,Nisynch);
+        read_1(I,R, I,{Ta, Na, R, Xa,{Ya,{hash(Ya)}sk(I)}pk(R)}sk(I));
+        claim_3(R,Nisynch);
         # There should also be Fresh Xa and Fresh Ya claims here
-	}
+    }
 }
 
 const Alice,Bob,Eve: Agent;
diff --git a/spdl/SPORE/ccitt509-3.spdl b/spdl/SPORE/ccitt509-3.spdl
index c42bba0..dbb9e87 100644
--- a/spdl/SPORE/ccitt509-3.spdl
+++ b/spdl/SPORE/ccitt509-3.spdl
@@ -15,31 +15,31 @@ usertype Timestamp;
 
 protocol ccitt5093(I,R)
 {
-	role I
-	{
-		const Ta: Timestamp;
+    role I
+    {
+        const Ta: Timestamp;
         var Tb: Timestamp;
         const Na,Xa,Ya: Nonce;
         var Xb,Nb,Yb: Nonce;
-		send_1(I,R, I,{Ta, Na, R, Xa,{Ya}pk(R)}sk(I));
+        send_1(I,R, I,{Ta, Na, R, Xa,{Ya}pk(R)}sk(I));
         read_2(R,I, R,{Tb, Nb, I, Na, Xb,{Yb}pk(I)}sk(R));
         send_3(I,R, I, {Nb}sk(I));
         claim_4(I,Nisynch);
-	}	
-	
-	role R
-	{
-		var Ta: Timestamp;
+    }    
+    
+    role R
+    {
+        var Ta: Timestamp;
         const Tb: Timestamp;
         var Na,Xa,Ya: Nonce;
         const Xb,Yb,Nb: Nonce;
 
-		read_1(I,R, I,{Ta, Na, R, Xa,{Ya}pk(R)}sk(I));
+        read_1(I,R, I,{Ta, Na, R, Xa,{Ya}pk(R)}sk(I));
         send_2(R,I, R,{Tb, Nb, I, Na, Xb,{Yb}pk(I)}sk(R));
         read_3(I,R, I, {Nb}sk(I));
-		claim_5(R,Nisynch);
+        claim_5(R,Nisynch);
         # There should also be Fresh Xa and Fresh Ya claims here
-	}
+    }
 }
 
 const Alice,Bob,Eve: Agent;
diff --git a/spdl/SPORE/ccitt509-ban3.spdl b/spdl/SPORE/ccitt509-ban3.spdl
index d01a089..b69c34b 100644
--- a/spdl/SPORE/ccitt509-ban3.spdl
+++ b/spdl/SPORE/ccitt509-ban3.spdl
@@ -17,28 +17,28 @@ inversekeys(pk,sk);
 
 protocol ccitt509ban3(I,R)
 {
-	role I
-	{
+    role I
+    {
         const Na,Xa,Ya: Nonce;
         var Xb,Nb,Yb: Nonce;
 
-		send_1(I,R, I,{Na, R, Xa,{Ya}pk(R)}sk(I));
+        send_1(I,R, I,{Na, R, Xa,{Ya}pk(R)}sk(I));
         read_2(R,I, R,{Nb, I, Na, Xb,{Yb}pk(I)}sk(R));
         send_3(I,R, I,{R, Nb}sk(I));
         claim_4(I,Nisynch);
-	}	
-	
-	role R
-	{
+    }    
+    
+    role R
+    {
         var Na,Xa,Ya: Nonce;
         const Xb,Yb,Nb: Nonce;
 
-		read_1(I,R, I,{Na, R, Xa,{Ya}pk(R)}sk(I));
+        read_1(I,R, I,{Na, R, Xa,{Ya}pk(R)}sk(I));
         send_2(R,I, R,{Nb, I, Na, Xb,{Yb}pk(I)}sk(R));
         read_3(I,R, I,{R, Nb}sk(I));
-		claim_5(R,Nisynch);
+        claim_5(R,Nisynch);
         # There should also be Fresh Xa and Fresh Ya claims here
-	}
+    }
 }
 
 const Alice,Bob,Eve: Agent;
diff --git a/spdl/SPORE/denning-sacco-lowe.spdl b/spdl/SPORE/denning-sacco-lowe.spdl
index fde57ed..2c4bb10 100644
--- a/spdl/SPORE/denning-sacco-lowe.spdl
+++ b/spdl/SPORE/denning-sacco-lowe.spdl
@@ -21,42 +21,42 @@ const dec: PseudoFunction;
 
 protocol denningSaccoLowe(I,R,S)
 {
-	role I
-	{
+    role I
+    {
         var W: Ticket;
-		var Kir: SessionKey;
+        var Kir: SessionKey;
         var T: TimeStamp;
         var Nr: Nonce;
 
-		send_1(I,S, I,R );
-		read_2(S,I, {R, Kir, T, W}k(I,S) );
-		send_3(I,R, W);
+        send_1(I,S, I,R );
+        read_2(S,I, {R, Kir, T, W}k(I,S) );
+        send_3(I,R, W);
         read_4(R,I, {Nr}Kir);
         send_5(I,R, {{Nr}dec}Kir);
-		claim_6(I,Niagree);
-	}	
-	
-	role R
-	{
+        claim_6(I,Niagree);
+    }    
+    
+    role R
+    {
         var Kir: SessionKey;
         var T: TimeStamp;
         const Nr: Nonce;
 
-		read_3(I,R, {Kir,I,T}k(R,S));
+        read_3(I,R, {Kir,I,T}k(R,S));
         send_4(R,I, {Nr}Kir);
         read_5(I,R, {{Nr}dec}Kir);
-		claim_8(R,Niagree);
-	}
-	
+        claim_8(R,Niagree);
+    }
+    
     role S
-	{
+    {
         var W: Ticket;
-		const Kir: SessionKey;
+        const Kir: SessionKey;
         const T: TimeStamp;
 
-		read_1(I,S, I,R );
-		send_2(S,I, {R, Kir, T, {Kir, I,T}k(R,S)}k(I,S));
-	}	
+        read_1(I,S, I,R );
+        send_2(S,I, {R, Kir, T, {Kir, I,T}k(R,S)}k(I,S));
+    }    
 }
 
 const Alice,Bob,Simon,Eve: Agent;
diff --git a/spdl/SPORE/denning-sacco.spdl b/spdl/SPORE/denning-sacco.spdl
index 1b8e6b6..2b27823 100644
--- a/spdl/SPORE/denning-sacco.spdl
+++ b/spdl/SPORE/denning-sacco.spdl
@@ -16,36 +16,36 @@ secret k: Function;
 
 protocol denningSacco(I,R,S)
 {
-	role I
-	{
+    role I
+    {
         var W: Ticket;
-		var Kir: SessionKey;
-        var T: TimeStamp;
-
-		send_1(I,S, I,R );
-		read_2(S,I, {R, Kir, T, W}k(I,S) );
-		send_3(I,R, W);
-		claim_4(I,Nisynch);
-	}	
-	
-	role R
-	{
         var Kir: SessionKey;
         var T: TimeStamp;
 
-		read_3(I,R, {Kir,I,T}k(R,S));
-		claim_8(R,Nisynch);
-	}
-	
+        send_1(I,S, I,R );
+        read_2(S,I, {R, Kir, T, W}k(I,S) );
+        send_3(I,R, W);
+        claim_4(I,Nisynch);
+    }    
+    
+    role R
+    {
+        var Kir: SessionKey;
+        var T: TimeStamp;
+
+        read_3(I,R, {Kir,I,T}k(R,S));
+        claim_8(R,Nisynch);
+    }
+    
     role S
-	{
+    {
         var W: Ticket;
-		const Kir: SessionKey;
+        const Kir: SessionKey;
         const T: TimeStamp;
 
-		read_1(I,S, I,R );
-		send_2(S,I, {R, Kir, T, {Kir, I,T}k(R,S)}k(I,S));
-	}	
+        read_1(I,S, I,R );
+        send_2(S,I, {R, Kir, T, {Kir, I,T}k(R,S)}k(I,S));
+    }    
 }
 
 const Alice,Bob,Simon,Eve: Agent;
diff --git a/spdl/SPORE/kaochow-v2.spdl b/spdl/SPORE/kaochow-v2.spdl
index 6ce2b78..b8007b3 100644
--- a/spdl/SPORE/kaochow-v2.spdl
+++ b/spdl/SPORE/kaochow-v2.spdl
@@ -14,45 +14,45 @@ secret k: Function;
 
 protocol kaochow2(I,R,S)
 {
-	role I
-	{
-		const ni: Nonce;
-		var nr: Nonce;
-		var kir,kt: Sessionkey;
+    role I
+    {
+        const ni: Nonce;
+        var nr: Nonce;
+        var kir,kt: Sessionkey;
 
-		send_1 (I,S, I,R,ni);
-		read_3 (R,I, R, {I,R,ni,kir,kt}k(I,S), {ni, kir}kt, nr );
-		send_4 (I,R, {nr,kir}kt );
+        send_1 (I,S, I,R,ni);
+        read_3 (R,I, R, {I,R,ni,kir,kt}k(I,S), {ni, kir}kt, nr );
+        send_4 (I,R, {nr,kir}kt );
 
-		claim_5 (I, Nisynch);
-		claim_6 (I, Niagree);
-		claim_7 (I, Secret, kir);
-	}	
-	
-	role R
-	{
-		var ni: Nonce;
-		const nr: Nonce;
-		var kir,kt: Sessionkey;
-		var T: Ticket;
+        claim_5 (I, Nisynch);
+        claim_6 (I, Niagree);
+        claim_7 (I, Secret, kir);
+    }    
+    
+    role R
+    {
+        var ni: Nonce;
+        const nr: Nonce;
+        var kir,kt: Sessionkey;
+        var T: Ticket;
 
-		read_2 (S,R, T, { I,R,ni,kir,kt }k(R,S)  ); 
-		send_3 (R,I, R, T, {ni, kir}kt, nr );
-		read_4 (I,R, {nr,kir}kt );
+        read_2 (S,R, T, { I,R,ni,kir,kt }k(R,S)  ); 
+        send_3 (R,I, R, T, {ni, kir}kt, nr );
+        read_4 (I,R, {nr,kir}kt );
 
-		claim_8 (R, Nisynch);
-		claim_9 (R, Niagree);
-		claim_10 (R, Secret, kir);
-	}
+        claim_8 (R, Nisynch);
+        claim_9 (R, Niagree);
+        claim_10 (R, Secret, kir);
+    }
 
-	role S
-	{
-		var ni: Nonce;
-		const kir, kt: Sessionkey;
+    role S
+    {
+        var ni: Nonce;
+        const kir, kt: Sessionkey;
 
-		read_1 (I,S, I,R,ni);
-		send_2 (S,R, {I,R,ni,kir,kt}k(I,S), { I,R,ni,kir,kt }k(R,S)  ); 
-	}
+        read_1 (I,S, I,R,ni);
+        send_2 (S,R, {I,R,ni,kir,kt}k(I,S), { I,R,ni,kir,kt }k(R,S)  ); 
+    }
 }
 
 const Alice,Bob,Simon,Eve: Agent;
diff --git a/spdl/SPORE/kaochow-v3.spdl b/spdl/SPORE/kaochow-v3.spdl
index 22067f3..11a2a3d 100644
--- a/spdl/SPORE/kaochow-v3.spdl
+++ b/spdl/SPORE/kaochow-v3.spdl
@@ -15,47 +15,47 @@ secret k: Function;
 
 protocol kaochow3(I,R,S)
 {
-	role I
-	{
-		const ni: Nonce;
-		var nr: Nonce;
-		var kir,kt: Sessionkey;
-		var T2: Ticket;
+    role I
+    {
+        const ni: Nonce;
+        var nr: Nonce;
+        var kir,kt: Sessionkey;
+        var T2: Ticket;
 
-		send_1 (I,S, I,R,ni);
-		read_3 (R,I, R, {I,R,ni,kir,kt}k(I,S), {ni, kir}kt, nr, T2 );
-		send_4 (I,R, {nr,kir}kt, T2 );
+        send_1 (I,S, I,R,ni);
+        read_3 (R,I, R, {I,R,ni,kir,kt}k(I,S), {ni, kir}kt, nr, T2 );
+        send_4 (I,R, {nr,kir}kt, T2 );
 
-		claim_5 (I, Nisynch);
-		claim_6 (I, Niagree);
-		claim_7 (I, Secret, kir);
-	}	
-	
-	role R
-	{
-		var ni: Nonce;
-		const nr: Nonce;
-		var kir,kt: Sessionkey;
-		var T: Ticket;
-		const tr: Timestamp;
+        claim_5 (I, Nisynch);
+        claim_6 (I, Niagree);
+        claim_7 (I, Secret, kir);
+    }    
+    
+    role R
+    {
+        var ni: Nonce;
+        const nr: Nonce;
+        var kir,kt: Sessionkey;
+        var T: Ticket;
+        const tr: Timestamp;
 
-		read_2 (S,R, T, { I,R,ni,kir,kt }k(R,S)  ); 
-		send_3 (R,I, R, T, {ni, kir}kt, nr, {I,R,tr,kir}k(R,S) );
-		read_4 (I,R, {nr,kir}kt, {I,R,tr,kir}k(R,S) );
+        read_2 (S,R, T, { I,R,ni,kir,kt }k(R,S)  ); 
+        send_3 (R,I, R, T, {ni, kir}kt, nr, {I,R,tr,kir}k(R,S) );
+        read_4 (I,R, {nr,kir}kt, {I,R,tr,kir}k(R,S) );
 
-		claim_8 (R, Nisynch);
-		claim_9 (R, Niagree);
-		claim_10 (R, Secret, kir);
-	}
+        claim_8 (R, Nisynch);
+        claim_9 (R, Niagree);
+        claim_10 (R, Secret, kir);
+    }
 
-	role S
-	{
-		var ni: Nonce;
-		const kir, kt: Sessionkey;
+    role S
+    {
+        var ni: Nonce;
+        const kir, kt: Sessionkey;
 
-		read_1 (I,S, I,R,ni);
-		send_2 (S,R, {I,R,ni,kir,kt}k(I,S), { I,R,ni,kir,kt }k(R,S)  ); 
-	}
+        read_1 (I,S, I,R,ni);
+        send_2 (S,R, {I,R,ni,kir,kt}k(I,S), { I,R,ni,kir,kt }k(R,S)  ); 
+    }
 }
 
 const Alice,Bob,Simon,Eve: Agent;
diff --git a/spdl/SPORE/kaochow.spdl b/spdl/SPORE/kaochow.spdl
index 842b127..c9eca39 100644
--- a/spdl/SPORE/kaochow.spdl
+++ b/spdl/SPORE/kaochow.spdl
@@ -14,45 +14,45 @@ secret k: Function;
 
 protocol kaochow(I,R,S)
 {
-	role I
-	{
-		const ni: Nonce;
-		var nr: Nonce;
-		var kir: Sessionkey;
+    role I
+    {
+        const ni: Nonce;
+        var nr: Nonce;
+        var kir: Sessionkey;
 
-		send_1 (I,S, I,R,ni);
-		read_3 (R,I, {I,R,ni,kir}k(I,S), {ni}kir, nr );
-		send_4 (I,R, {nr}kir );
+        send_1 (I,S, I,R,ni);
+        read_3 (R,I, {I,R,ni,kir}k(I,S), {ni}kir, nr );
+        send_4 (I,R, {nr}kir );
 
-		claim_5 (I, Nisynch);
-		claim_6 (I, Niagree);
-		claim_7 (I, Secret, kir);
-	}	
-	
-	role R
-	{
-		var ni: Nonce;
-		const nr: Nonce;
-		var kir: Sessionkey;
-		var T;
+        claim_5 (I, Nisynch);
+        claim_6 (I, Niagree);
+        claim_7 (I, Secret, kir);
+    }    
+    
+    role R
+    {
+        var ni: Nonce;
+        const nr: Nonce;
+        var kir: Sessionkey;
+        var T;
 
-		read_2 (S,R, T, { I,R,ni,kir }k(R,S) ); 
-		send_3 (R,I, T, {ni}kir, nr );
-		read_4 (I,R, {nr}kir );
+        read_2 (S,R, T, { I,R,ni,kir }k(R,S) ); 
+        send_3 (R,I, T, {ni}kir, nr );
+        read_4 (I,R, {nr}kir );
 
-		claim_8 (R, Nisynch);
-		claim_9 (R, Niagree);
-		claim_10 (R, Secret, kir);
-	}
+        claim_8 (R, Nisynch);
+        claim_9 (R, Niagree);
+        claim_10 (R, Secret, kir);
+    }
 
-	role S
-	{
-		var ni: Nonce;
-		const kir: Sessionkey;
+    role S
+    {
+        var ni: Nonce;
+        const kir: Sessionkey;
 
-		read_1 (I,S, I,R,ni);
-		send_2 (S,R, {I,R,ni,kir}k(I,S), { I,R,ni,kir }k(R,S)  ); 
-	}
+        read_1 (I,S, I,R,ni);
+        send_2 (S,R, {I,R,ni,kir}k(I,S), { I,R,ni,kir }k(R,S)  ); 
+    }
 }
 
 const Alice,Bob,Simon,Eve: Agent;
diff --git a/spdl/SPORE/ksl-lowe.spdl b/spdl/SPORE/ksl-lowe.spdl
index f952381..25e8da3 100644
--- a/spdl/SPORE/ksl-lowe.spdl
+++ b/spdl/SPORE/ksl-lowe.spdl
@@ -25,58 +25,58 @@ compromised k(e,s);
 
 protocol kslLowe(A,B,S)
 {
-	role A
-	{
-		const Na, Ma: Nonce;
-		var Nc, Mb: Nonce;
-		var T: Ticket;
-		var Kab: SessionKey;
-		
-		send_1(A,B, Na, A);
-		read_4(B,A, { Na,B,Kab }k(A,S), T, Nc, {B,Na}Kab );
-		send_5(A,B, { Nc }Kab );
-		
-		send_6(A,B, Ma,T );
-		read_7(B,A, Mb,{Ma, B}Kab );
-		send_8(A,B, {A,Mb}Kab );
+    role A
+    {
+        const Na, Ma: Nonce;
+        var Nc, Mb: Nonce;
+        var T: Ticket;
+        var Kab: SessionKey;
+        
+        send_1(A,B, Na, A);
+        read_4(B,A, { Na,B,Kab }k(A,S), T, Nc, {B,Na}Kab );
+        send_5(A,B, { Nc }Kab );
+        
+        send_6(A,B, Ma,T );
+        read_7(B,A, Mb,{Ma, B}Kab );
+        send_8(A,B, {A,Mb}Kab );
 
-		claim_A1(A,Secret, Kab);
-		claim_A2(A,Niagree);
-		claim_A3(A,Nisynch);
-	}
+        claim_A1(A,Secret, Kab);
+        claim_A2(A,Niagree);
+        claim_A3(A,Nisynch);
+    }
 
-	role B
-	{
-		var Na,Ma: Nonce;
-		const Nb,Nc,Mb: Nonce;
-		var Kab: SessionKey;
-		const Kbb: TicketKey;
-		const Tb: GeneralizedTimestamp;
-		var T: Ticket;
-		
-		read_1(A,B, Na, A);
-		send_2(B,S, Na, A, Nb, B );
-		read_3(S,B, { A, Nb, Kab }k(B,S), T );
-		send_4(B,A, T, { Tb, A, Kab }Kbb, Nc, {B, Na}Kab );
-		read_5(A,B, { Nc }Kab );
-		
-		read_6(A,B, Ma,{ Tb, A, Kab }Kbb );
-		send_7(B,A, Mb,{Ma,B}Kab );
-		read_8(A,B, {A,Mb}Kab );
+    role B
+    {
+        var Na,Ma: Nonce;
+        const Nb,Nc,Mb: Nonce;
+        var Kab: SessionKey;
+        const Kbb: TicketKey;
+        const Tb: GeneralizedTimestamp;
+        var T: Ticket;
+        
+        read_1(A,B, Na, A);
+        send_2(B,S, Na, A, Nb, B );
+        read_3(S,B, { A, Nb, Kab }k(B,S), T );
+        send_4(B,A, T, { Tb, A, Kab }Kbb, Nc, {B, Na}Kab );
+        read_5(A,B, { Nc }Kab );
+        
+        read_6(A,B, Ma,{ Tb, A, Kab }Kbb );
+        send_7(B,A, Mb,{Ma,B}Kab );
+        read_8(A,B, {A,Mb}Kab );
 
-		claim_B1(B,Secret, Kab);
-		claim_B2(B,Niagree);
-		claim_B3(B,Nisynch);
-	}
+        claim_B1(B,Secret, Kab);
+        claim_B2(B,Niagree);
+        claim_B3(B,Nisynch);
+    }
 
-	role S
-	{
-		var Na, Nb: Nonce;
-		const Kab: SessionKey;
+    role S
+    {
+        var Na, Nb: Nonce;
+        const Kab: SessionKey;
 
-		read_2(B,S, Na, A, Nb, B );
-		send_3(S,B, { A, Nb, Kab }k(B,S), { Na,B,Kab }k(A,S) );
-	}
+        read_2(B,S, Na, A, Nb, B );
+        send_3(S,B, { A, Nb, Kab }k(B,S), { Na,B,Kab }k(A,S) );
+    }
 }
 
 run kslLowe.A(a,b,s);
diff --git a/spdl/SPORE/ksl.spdl b/spdl/SPORE/ksl.spdl
index 8c8f821..bbb2c31 100644
--- a/spdl/SPORE/ksl.spdl
+++ b/spdl/SPORE/ksl.spdl
@@ -22,58 +22,58 @@ compromised k(e,s);
 
 protocol ksl(A,B,S)
 {
-	role A
-	{
-		const Na, Ma: Nonce;
-		var Nc, Mb: Nonce;
-		var T: Ticket;
-		var Kab: SessionKey;
-		
-		send_1(A,B, Na, A);
-		read_4(B,A, { Na,B,Kab }k(A,S), T, Nc, {Na}Kab );
-		send_5(A,B, { Nc }Kab );
-		
-		send_6(A,B, Ma,T );
-		read_7(B,A, Mb,{Ma}Kab );
-		send_8(A,B, {Mb}Kab );
+    role A
+    {
+        const Na, Ma: Nonce;
+        var Nc, Mb: Nonce;
+        var T: Ticket;
+        var Kab: SessionKey;
+        
+        send_1(A,B, Na, A);
+        read_4(B,A, { Na,B,Kab }k(A,S), T, Nc, {Na}Kab );
+        send_5(A,B, { Nc }Kab );
+        
+        send_6(A,B, Ma,T );
+        read_7(B,A, Mb,{Ma}Kab );
+        send_8(A,B, {Mb}Kab );
 
-		claim_A1(A,Secret, Kab);
-		claim_A2(A,Niagree);
-		claim_A3(A,Nisynch);
-	}
+        claim_A1(A,Secret, Kab);
+        claim_A2(A,Niagree);
+        claim_A3(A,Nisynch);
+    }
 
-	role B
-	{
-		var Na,Ma: Nonce;
-		const Nb,Nc,Mb: Nonce;
-		var Kab: SessionKey;
-		const Kbb: TicketKey;
-		const Tb: GeneralizedTimestamp;
-		var T: Ticket;
-		
-		read_1(A,B, Na, A);
-		send_2(B,S, Na, A, Nb, B );
-		read_3(S,B, { Nb, A, Kab }k(B,S), T );
-		send_4(B,A, T, { Tb, A, Kab }Kbb, Nc, {Na}Kab );
-		read_5(A,B, { Nc }Kab );
-		
-		read_6(A,B, Ma,{ Tb, A, Kab }Kbb );
-		send_7(B,A, Mb,{Ma}Kab );
-		read_8(A,B, {Mb}Kab );
+    role B
+    {
+        var Na,Ma: Nonce;
+        const Nb,Nc,Mb: Nonce;
+        var Kab: SessionKey;
+        const Kbb: TicketKey;
+        const Tb: GeneralizedTimestamp;
+        var T: Ticket;
+        
+        read_1(A,B, Na, A);
+        send_2(B,S, Na, A, Nb, B );
+        read_3(S,B, { Nb, A, Kab }k(B,S), T );
+        send_4(B,A, T, { Tb, A, Kab }Kbb, Nc, {Na}Kab );
+        read_5(A,B, { Nc }Kab );
+        
+        read_6(A,B, Ma,{ Tb, A, Kab }Kbb );
+        send_7(B,A, Mb,{Ma}Kab );
+        read_8(A,B, {Mb}Kab );
 
-		claim_B1(B,Secret, Kab);
-		claim_B2(B,Niagree);
-		claim_B3(B,Nisynch);
-	}
+        claim_B1(B,Secret, Kab);
+        claim_B2(B,Niagree);
+        claim_B3(B,Nisynch);
+    }
 
-	role S
-	{
-		var Na, Nb: Nonce;
-		const Kab: SessionKey;
+    role S
+    {
+        var Na, Nb: Nonce;
+        const Kab: SessionKey;
 
-		read_2(B,S, Na, A, Nb, B );
-		send_3(S,B, { Nb, A, Kab }k(B,S), { Na,B,Kab }k(A,S) );
-	}
+        read_2(B,S, Na, A, Nb, B );
+        send_3(S,B, { Nb, A, Kab }k(B,S), { Na,B,Kab }k(A,S) );
+    }
 }
 
 run ksl.A(a,b,s);
diff --git a/spdl/SPORE/needham-schroeder-lowe.spdl b/spdl/SPORE/needham-schroeder-lowe.spdl
index 6b6393a..399ce52 100644
--- a/spdl/SPORE/needham-schroeder-lowe.spdl
+++ b/spdl/SPORE/needham-schroeder-lowe.spdl
@@ -16,22 +16,22 @@ inversekeys(pk,sk);
 
 protocol needhamschroederpkLowe(I,R,S)
 {
-	role I
-	{
+    role I
+    {
         const Ni: Nonce;
         var Nr: Nonce;
 
-		send_1(I,S, (I,R));
+        send_1(I,S, (I,R));
         read_2(S,I, {pk(R), R}sk(S));
         send_3(I,R,{Ni,I}pk(R));
         read_6(R,I, {Ni,Nr,R}pk(I));
         send_7(I,R, {Nr}pk(R));
         claim_I1(I,Secret,Ni);
         claim_I2(I,Secret,Nr);
-	}	
-	
-	role R
-	{
+    }    
+    
+    role R
+    {
         const Nr: Nonce;
         var Ni: Nonce;
         
@@ -42,7 +42,7 @@ protocol needhamschroederpkLowe(I,R,S)
         read_7(I,R,{Nr}pk(R));
         claim_R1(R,Secret,Nr);
         claim_R2(R,Secret,Ni);
-	}
+    }
 
     role S
     {
diff --git a/spdl/SPORE/needham-schroeder-sk-amend.spdl b/spdl/SPORE/needham-schroeder-sk-amend.spdl
index 31c3dcf..656a140 100644
--- a/spdl/SPORE/needham-schroeder-sk-amend.spdl
+++ b/spdl/SPORE/needham-schroeder-sk-amend.spdl
@@ -23,8 +23,8 @@ usertype Ticket;
 
 protocol needhamschroederskamend(I,R,S)
 {
-	role I
-	{
+    role I
+    {
         const Ni: Nonce;
         var Nr: Nonce;
         var Kir: SessionKey;
@@ -40,10 +40,10 @@ protocol needhamschroederskamend(I,R,S)
         
         claim_I2(I,Secret,Kir);
         claim_I3(I,Nisynch);
-	}	
-	
-	role R
-	{
+    }    
+    
+    role R
+    {
         const Nr: Nonce;
         var Kir: SessionKey;
         
@@ -54,7 +54,7 @@ protocol needhamschroederskamend(I,R,S)
         read_7(I,R,{{Nr}dec}Kir);
         claim_R1(R,Secret,Nr);
         claim_R3(R,Nisynch);
-	}
+    }
 
     role S
     {
diff --git a/spdl/SPORE/needham-schroeder-sk.spdl b/spdl/SPORE/needham-schroeder-sk.spdl
index 26508ba..851d440 100644
--- a/spdl/SPORE/needham-schroeder-sk.spdl
+++ b/spdl/SPORE/needham-schroeder-sk.spdl
@@ -19,24 +19,24 @@ usertype Ticket;
 
 protocol needhamschroedersk(I,R,S)
 {
-	role I
-	{
+    role I
+    {
         const Ni: Nonce;
         var Nr: Nonce;
         var Kir: SessionKey;
         var T: Ticket;
         
-		send_1(I,S,(I,R,Ni));
+        send_1(I,S,(I,R,Ni));
         read_2(S,I, {Ni,R,Kir,T}k(I,S));
         send_3(I,R,T);
         read_4(R,I,{Nr}Kir);
         send_5(I,R,{{Nr}dec}Kir);
         claim_I2(I,Secret,Kir);
         claim_I3(I,Nisynch);
-	}	
-	
-	role R
-	{
+    }    
+    
+    role R
+    {
         const Nr: Nonce;
         var Kir: SessionKey;
         
@@ -45,7 +45,7 @@ protocol needhamschroedersk(I,R,S)
         read_5(I,R,{{Nr}dec}Kir);
         claim_R1(R,Secret,Kir);
         claim_R3(R,Nisynch);
-	}
+    }
 
     role S
     {
diff --git a/spdl/SPORE/needham-schroeder.spdl b/spdl/SPORE/needham-schroeder.spdl
index b73385d..37bbd6d 100644
--- a/spdl/SPORE/needham-schroeder.spdl
+++ b/spdl/SPORE/needham-schroeder.spdl
@@ -16,22 +16,22 @@ inversekeys(pk,sk);
 
 protocol needhamschroederpk(I,R,S)
 {
-	role I
-	{
+    role I
+    {
         const Ni: Nonce;
         var Nr: Nonce;
 
-		send_1(I,S,(I,R));
+        send_1(I,S,(I,R));
         read_2(S,I, {pk(R), R}sk(S));
         send_3(I,R,{Ni,I}pk(R));
         read_6(R,I, {Ni, Nr}pk(I));
         send_7(I,R, {Nr}pk(R));
         claim_I1(I,Secret,Ni);
         claim_I2(I,Secret,Nr);
-	}	
-	
-	role R
-	{
+    }    
+    
+    role R
+    {
         const Nr: Nonce;
         var Ni: Nonce;
         
@@ -42,7 +42,7 @@ protocol needhamschroederpk(I,R,S)
         read_7(I,R,{Nr}pk(R));
         claim_R1(R,Secret,Nr);
         claim_R2(R,Secret,Ni);
-	}
+    }
 
     role S
     {
diff --git a/spdl/SPORE/neumannstub-hwang.spdl b/spdl/SPORE/neumannstub-hwang.spdl
index d8a7230..ed76187 100644
--- a/spdl/SPORE/neumannstub-hwang.spdl
+++ b/spdl/SPORE/neumannstub-hwang.spdl
@@ -25,55 +25,55 @@ compromised k(e,s);
 
 protocol neustubHwang(I,R,S)
 {
-	role I
-	{
-		const Ni,Mi: Nonce;
-		var Nr,Mr: Nonce;
-		var T: Ticket;
+    role I
+    {
+        const Ni,Mi: Nonce;
+        var Nr,Mr: Nonce;
+        var T: Ticket;
         var Tb: TimeStamp;
-		var Kir: SessionKey;
-		
-		send_1(I,R, I, Ni);
-		read_3(S,I, { R,Ni,Kir,Tb}k(I,S), T, Nr);
+        var Kir: SessionKey;
+        
+        send_1(I,R, I, Ni);
+        read_3(S,I, { R,Ni,Kir,Tb}k(I,S), T, Nr);
         send_4(I,R,T,{Nr}Kir);
         send_5(I,R,Mi,T);
-		read_6(R,I,Mr,{Mr}Kir);
-		send_7(I,R,{Mr}Kir);
-		
-		claim_I1(I,Secret, Kir);
-		claim_I2(I,Niagree);
-		claim_I3(I,Nisynch);
-	}
+        read_6(R,I,Mr,{Mr}Kir);
+        send_7(I,R,{Mr}Kir);
+        
+        claim_I1(I,Secret, Kir);
+        claim_I2(I,Niagree);
+        claim_I3(I,Nisynch);
+    }
 
-	role R
-	{
-		var Ni,Mi: Nonce;
-		const Nr,Mr: Nonce;
-		var Kir: SessionKey;
-		const Tb: TimeStamp;
-		var T: Ticket;
-		
+    role R
+    {
+        var Ni,Mi: Nonce;
+        const Nr,Mr: Nonce;
+        var Kir: SessionKey;
+        const Tb: TimeStamp;
+        var T: Ticket;
+        
         read_1(I,R, I, Ni);
         send_2(R,S, R, {I, Ni, Tb, Nr}k(R,S));
         read_4(I,R,{I,Kir,Tb}k(R,S),{Nr}Kir);
         read_5(I,R,Mi,T);
-		send_6(R,I,Mr,{Mr}Kir);
-		read_7(I,R,{Mr}Kir);
-	
-		claim_R1(R,Secret, Kir);
-		claim_R2(R,Niagree);
-		claim_R3(R,Nisynch);
-	}
+        send_6(R,I,Mr,{Mr}Kir);
+        read_7(I,R,{Mr}Kir);
+    
+        claim_R1(R,Secret, Kir);
+        claim_R2(R,Niagree);
+        claim_R3(R,Nisynch);
+    }
 
-	role S
-	{
-		var Ni, Nr: Nonce;
-		const Kir: SessionKey;
+    role S
+    {
+        var Ni, Nr: Nonce;
+        const Kir: SessionKey;
         var Tb: TimeStamp;
 
-		read_2(R,S, R, {I,Ni,Tb,Nr}k(R,S));
-		send_3(S,I, { R, Ni, Kir, Tb}k(I,S), { I,Kir,Tb}k(R,S),Nr );
-	}
+        read_2(R,S, R, {I,Ni,Tb,Nr}k(R,S));
+        send_3(S,I, { R, Ni, Kir, Tb}k(I,S), { I,Kir,Tb}k(R,S),Nr );
+    }
 }
 
 run neustubHwang.A(a,b,s);
diff --git a/spdl/SPORE/neumannstub.spdl b/spdl/SPORE/neumannstub.spdl
index 07e97de..b551818 100644
--- a/spdl/SPORE/neumannstub.spdl
+++ b/spdl/SPORE/neumannstub.spdl
@@ -22,55 +22,55 @@ compromised k(e,s);
 
 protocol neustub(I,R,S)
 {
-	role I
-	{
-		const Ni,Mi: Nonce;
-		var Nr,Mr: Nonce;
-		var T: Ticket;
+    role I
+    {
+        const Ni,Mi: Nonce;
+        var Nr,Mr: Nonce;
+        var T: Ticket;
         var Tb: TimeStamp;
-		var Kir: SessionKey;
-		
-		send_1(I,R, I, Ni);
-		read_3(S,I, { R,Ni,Kir,Tb}k(I,S), T, Nr);
+        var Kir: SessionKey;
+        
+        send_1(I,R, I, Ni);
+        read_3(S,I, { R,Ni,Kir,Tb}k(I,S), T, Nr);
         send_4(I,R,T,{Nr}Kir);
         send_5(I,R,Mi,T);
-		read_6(R,I,Mr,{Mi}Kir);
-		send_7(I,R,{Mr}Kir);
-		
-		claim_I1(I,Secret, Kir);
-		claim_I2(I,Niagree);
-		claim_I3(I,Nisynch);
-	}
+        read_6(R,I,Mr,{Mi}Kir);
+        send_7(I,R,{Mr}Kir);
+        
+        claim_I1(I,Secret, Kir);
+        claim_I2(I,Niagree);
+        claim_I3(I,Nisynch);
+    }
 
-	role R
-	{
-		var Ni,Mi: Nonce;
-		const Nr,Mr: Nonce;
-		var Kir: SessionKey;
-		const Tb: TimeStamp;
-		var T: Ticket;
-		
+    role R
+    {
+        var Ni,Mi: Nonce;
+        const Nr,Mr: Nonce;
+        var Kir: SessionKey;
+        const Tb: TimeStamp;
+        var T: Ticket;
+        
         read_1(I,R, I, Ni);
         send_2(R,S, R, {I, Ni, Tb}k(R,S),Nr);
         read_4(I,R,{I,Kir,Tb}k(R,S),{Nr}Kir);
         read_5(I,R,Mi,T);
-		send_6(R,I,Mr,{Mi}Kir);
-		read_7(I,R,{Mr}Kir);
-	
-		claim_R1(R,Secret, Kir);
-		claim_R2(R,Niagree);
-		claim_R3(R,Nisynch);
-	}
+        send_6(R,I,Mr,{Mi}Kir);
+        read_7(I,R,{Mr}Kir);
+    
+        claim_R1(R,Secret, Kir);
+        claim_R2(R,Niagree);
+        claim_R3(R,Nisynch);
+    }
 
-	role S
-	{
-		var Ni, Nr: Nonce;
-		const Kir: SessionKey;
+    role S
+    {
+        var Ni, Nr: Nonce;
+        const Kir: SessionKey;
         var Tb: TimeStamp;
 
-		read_2(R,S, R, {I,Ni,Tb}k(R,S), Nr);
-		send_3(S,I, { R, Ni, Kir, Tb}k(I,S), { I,Kir,Tb}k(R,S),Nr );
-	}
+        read_2(R,S, R, {I,Ni,Tb}k(R,S), Nr);
+        send_3(S,I, { R, Ni, Kir, Tb}k(I,S), { I,Kir,Tb}k(R,S),Nr );
+    }
 }
 
 run neustub.A(a,b,s);
diff --git a/spdl/SPORE/otwayrees.spdl b/spdl/SPORE/otwayrees.spdl
index 274edc3..f6fd1d8 100644
--- a/spdl/SPORE/otwayrees.spdl
+++ b/spdl/SPORE/otwayrees.spdl
@@ -16,44 +16,44 @@ usertype String,SessionKey,Ticket;
 
 protocol otwayrees(I,R,S)
 {
-	role I
-	{
-		const Ni : Nonce;
-		const M : String;
-		var Kir : SessionKey;
+    role I
+    {
+        const Ni : Nonce;
+        const M : String;
+        var Kir : SessionKey;
 
-		send_1(I,R, M,I,R,{Ni,M,I,R}k(I,S) );
-		read_4(R,I, M,{Ni,Kir}k(I,S) );
+        send_1(I,R, M,I,R,{Ni,M,I,R}k(I,S) );
+        read_4(R,I, M,{Ni,Kir}k(I,S) );
 
-		claim_I1(I, Secret,Kir);
+        claim_I1(I, Secret,Kir);
         #claim_I2(I, Nisynch);
-	}
+    }
 
-	role R
-	{
-		var M : String;
-		const Nr : Nonce;
-		var Kir : SessionKey;
-		var T1,T2: Ticket;
+    role R
+    {
+        var M : String;
+        const Nr : Nonce;
+        var Kir : SessionKey;
+        var T1,T2: Ticket;
 
-		read_1(I,R, M,I,R, T1 );
-		send_2(R,S, M,I,R, T1, { Nr,M,I,R }k(R,S) );
-		read_3(S,R, M, T2, { Nr,Kir }k(R,S) );
-		send_4(R,I, M, T2 );
+        read_1(I,R, M,I,R, T1 );
+        send_2(R,S, M,I,R, T1, { Nr,M,I,R }k(R,S) );
+        read_3(S,R, M, T2, { Nr,Kir }k(R,S) );
+        send_4(R,I, M, T2 );
 
-		claim_R1(R, Secret,Kir);
+        claim_R1(R, Secret,Kir);
         #claim_R2(R, Nisynch);
-	}
+    }
 
-	role S
-	{
-		var Ni,Nr : Nonce;
-		var M : String;
-		const Kir : SessionKey;
-		
-		read_2(R,S, M,I,R, { Ni,M,I,R}k(I,S), { Nr,M,I,R }k(R,S) );
-		send_3(S,R, M, { Ni,Kir }k(I,S) , { Nr,Kir }k(R,S) );
-	}
+    role S
+    {
+        var Ni,Nr : Nonce;
+        var M : String;
+        const Kir : SessionKey;
+        
+        read_2(R,S, M,I,R, { Ni,M,I,R}k(I,S), { Nr,M,I,R }k(R,S) );
+        send_3(S,R, M, { Ni,Kir }k(I,S) , { Nr,Kir }k(R,S) );
+    }
 }
 
 const Alice, Bob, Eve, Simon: Agent;
diff --git a/spdl/SPORE/smartright.spdl b/spdl/SPORE/smartright.spdl
index 788e073..d2d27cb 100644
--- a/spdl/SPORE/smartright.spdl
+++ b/spdl/SPORE/smartright.spdl
@@ -25,9 +25,9 @@ const Vor: XorKey;
 
 protocol smartright(I,R)
 {
-	role I
-	{
-		const VoKey: SessionKey;
+    role I
+    {
+        const VoKey: SessionKey;
         const VoR: XorKey;
         const CW;
         var VoRi: Nonce;
@@ -35,10 +35,10 @@ protocol smartright(I,R)
         send_1(I,R, {VoKey,{CW}VoR}k(I,R));
         read_2(R,I, VoRi);
         send_3(I,R, VoR, {{VoRi}hash}VoKey);
-	}	
-	
-	role R
-	{
+    }    
+    
+    role R
+    {
         var T: Ticket;
         var VoR: XorKey;
         var VoKey: SessionKey;
@@ -48,8 +48,8 @@ protocol smartright(I,R)
         send_2(R,I, VoRi);
         read_3(I,R, VoR,{{VoRi}hash}VoKey);
 
-		claim_R1(R,Nisynch);
-	}
+        claim_R1(R,Nisynch);
+    }
 }
 
 const Alice,Bob,Eve: Agent;
diff --git a/spdl/SPORE/splice-as-cj.spdl b/spdl/SPORE/splice-as-cj.spdl
index a7be252..8ce1d39 100644
--- a/spdl/SPORE/splice-as-cj.spdl
+++ b/spdl/SPORE/splice-as-cj.spdl
@@ -21,50 +21,50 @@ inversekeys (inc,dec);
 protocol spliceASCJ(I,R,S)
 {
         role I
-	{
-		const N1,N2: Nonce;
-		const T: TimeStamp;
-		const L: LifeTime;
+    {
+        const N1,N2: Nonce;
+        const T: TimeStamp;
+        const L: LifeTime;
 
-		send_1(I,S,  I, R, N1 );
-		read_2(S,I,  S, {S, I, N1, R, pk(R)}sk(S) );
-		send_3(I,R,  I, R, {T, L, {I, N2}pk(R)}sk(I) );
-		read_6(R,I,  R, I, {{N2}inc}pk(I) );
+        send_1(I,S,  I, R, N1 );
+        read_2(S,I,  S, {S, I, N1, R, pk(R)}sk(S) );
+        send_3(I,R,  I, R, {T, L, {I, N2}pk(R)}sk(I) );
+        read_6(R,I,  R, I, {{N2}inc}pk(I) );
 
-		claim_7(I, Secret, N2);
-		claim_9(I, Niagree);
-		claim_10(I, Nisynch);
-	}
+        claim_7(I, Secret, N2);
+        claim_9(I, Niagree);
+        claim_10(I, Nisynch);
+    }
 
-	role S
-	{
-		var N1,N3: Nonce;
+    role S
+    {
+        var N1,N3: Nonce;
 
-		read_1(I,S,  I, R, N1 );
-		send_2(S,I,  S, {S, I, N1, R, pk(R)}sk(S) );
-		read_4(R,S, R, I, N3 );
-		send_5(S,R,  S, {S, R, N3, pk(I)}sk(S) );
-	}
+        read_1(I,S,  I, R, N1 );
+        send_2(S,I,  S, {S, I, N1, R, pk(R)}sk(S) );
+        read_4(R,S, R, I, N3 );
+        send_5(S,R,  S, {S, R, N3, pk(I)}sk(S) );
+    }
 
-	role R
-	{
-		const N3: Nonce;
-		var N2: Nonce;
-		var T: TimeStamp;
-		var L: LifeTime;
+    role R
+    {
+        const N3: Nonce;
+        var N2: Nonce;
+        var T: TimeStamp;
+        var L: LifeTime;
 
-		var ni: Nonce;
-		const nr: Nonce;
+        var ni: Nonce;
+        const nr: Nonce;
 
-		read_3(I,R, I, R, {T, L, {I, N2}pk(R)}sk(I) );
-		send_4(R,S, R, I, N3 );
-		read_5(S,R, S, {S, R, N3, pk(I)}sk(S) );
-		send_6(R,I, R, I, {{N2}inc}pk(I) );
+        read_3(I,R, I, R, {T, L, {I, N2}pk(R)}sk(I) );
+        send_4(R,S, R, I, N3 );
+        read_5(S,R, S, {S, R, N3, pk(I)}sk(S) );
+        send_6(R,I, R, I, {{N2}inc}pk(I) );
 
-		claim_8(R, Secret, N2);
-		claim_11(R, Niagree);
-		claim_12(R, Nisynch);
-	}
+        claim_8(R, Secret, N2);
+        claim_11(R, Niagree);
+        claim_12(R, Nisynch);
+    }
 }
 
 const Alice,Bob,Simon,Eve: Agent;
diff --git a/spdl/SPORE/splice-as-hc.spdl b/spdl/SPORE/splice-as-hc.spdl
index 931132b..8ddf292 100644
--- a/spdl/SPORE/splice-as-hc.spdl
+++ b/spdl/SPORE/splice-as-hc.spdl
@@ -16,50 +16,50 @@ inversekeys (inc,dec);
 protocol spliceASHC(I,R,S)
 {
         role I
-	{
-		const N1,N2: Nonce;
-		const T: TimeStamp;
-		const L: LifeTime;
+    {
+        const N1,N2: Nonce;
+        const T: TimeStamp;
+        const L: LifeTime;
 
-		send_1(I,S,  I, R, N1 );
-		read_2(S,I,  S, {S, I, N1, R, pk(R)}sk(S) );
-		send_3(I,R,  I, R, {I, T, L, {N2}pk(R)}sk(I) );
-		read_6(R,I,  R, I, {R, {N2}inc}pk(I) );
+        send_1(I,S,  I, R, N1 );
+        read_2(S,I,  S, {S, I, N1, R, pk(R)}sk(S) );
+        send_3(I,R,  I, R, {I, T, L, {N2}pk(R)}sk(I) );
+        read_6(R,I,  R, I, {R, {N2}inc}pk(I) );
 
-		claim_7(I, Secret, N2);
-		claim_9(I, Niagree);
-		claim_10(I, Nisynch);
-	}
+        claim_7(I, Secret, N2);
+        claim_9(I, Niagree);
+        claim_10(I, Nisynch);
+    }
 
-	role S
-	{
-		var N1,N3: Nonce;
+    role S
+    {
+        var N1,N3: Nonce;
 
-		read_1(I,S,  I, R, N1 );
-		send_2(S,I,  S, {S, I, N1, R, pk(R)}sk(S) );
-		read_4(R,S, R, I, N3 );
-		send_5(S,R,  S, {S, R, N3, I, pk(I)}sk(S) );
-	}
+        read_1(I,S,  I, R, N1 );
+        send_2(S,I,  S, {S, I, N1, R, pk(R)}sk(S) );
+        read_4(R,S, R, I, N3 );
+        send_5(S,R,  S, {S, R, N3, I, pk(I)}sk(S) );
+    }
 
-	role R
-	{
-		const N3: Nonce;
-		var N2: Nonce;
-		var T: TimeStamp;
-		var L: LifeTime;
+    role R
+    {
+        const N3: Nonce;
+        var N2: Nonce;
+        var T: TimeStamp;
+        var L: LifeTime;
 
-		var ni: Nonce;
-		const nr: Nonce;
+        var ni: Nonce;
+        const nr: Nonce;
 
-		read_3(I,R, I, R, {I, T, L, {N2}pk(R)}sk(I) );
-		send_4(R,S, R, I, N3 );
-		read_5(S,R, S, {S, R, N3, I, pk(I)}sk(S) );
-		send_6(R,I, R, I, {R, {N2}inc}pk(I) );
+        read_3(I,R, I, R, {I, T, L, {N2}pk(R)}sk(I) );
+        send_4(R,S, R, I, N3 );
+        read_5(S,R, S, {S, R, N3, I, pk(I)}sk(S) );
+        send_6(R,I, R, I, {R, {N2}inc}pk(I) );
 
-		claim_8(R, Secret, N2);
-		claim_11(R, Niagree);
-		claim_12(R, Nisynch);
-	}
+        claim_8(R, Secret, N2);
+        claim_11(R, Niagree);
+        claim_12(R, Nisynch);
+    }
 }
 
 const Alice,Bob,Simon,Eve: Agent;
diff --git a/spdl/SPORE/splice-as.spdl b/spdl/SPORE/splice-as.spdl
index 6952245..72f223c 100644
--- a/spdl/SPORE/splice-as.spdl
+++ b/spdl/SPORE/splice-as.spdl
@@ -21,50 +21,50 @@ inversekeys (inc,dec);
 protocol spliceAS(I,R,S)
 {
         role I
-	{
-		const N1,N2: Nonce;
-		const T: TimeStamp;
-		const L: LifeTime;
+    {
+        const N1,N2: Nonce;
+        const T: TimeStamp;
+        const L: LifeTime;
 
-		send_1(I,S,  I, R, N1 );
-		read_2(S,I,  S, {S, I, N1, pk(R)}sk(S) );
-		send_3(I,R,  I, R, {I, T, L, {N2}pk(R)}sk(I) );
-		read_6(R,I,  R, I, {R, {N2}inc}pk(I) );
+        send_1(I,S,  I, R, N1 );
+        read_2(S,I,  S, {S, I, N1, pk(R)}sk(S) );
+        send_3(I,R,  I, R, {I, T, L, {N2}pk(R)}sk(I) );
+        read_6(R,I,  R, I, {R, {N2}inc}pk(I) );
 
-		claim_7(I, Secret, N2);
-		claim_9(I, Niagree);
-		claim_10(I, Nisynch);
-	}
+        claim_7(I, Secret, N2);
+        claim_9(I, Niagree);
+        claim_10(I, Nisynch);
+    }
 
-	role S
-	{
-		var N1,N3: Nonce;
+    role S
+    {
+        var N1,N3: Nonce;
 
-		read_1(I,S,  I, R, N1 );
-		send_2(S,I,  S, {S, I, N1, pk(R)}sk(S) );
-		read_4(R,S, R, I, N3 );
-		send_5(S,R,  S, {S, R, N3, pk(I)}sk(S) );
-	}
+        read_1(I,S,  I, R, N1 );
+        send_2(S,I,  S, {S, I, N1, pk(R)}sk(S) );
+        read_4(R,S, R, I, N3 );
+        send_5(S,R,  S, {S, R, N3, pk(I)}sk(S) );
+    }
 
-	role R
-	{
-		const N3: Nonce;
-		var N2: Nonce;
-		var T: TimeStamp;
-		var L: LifeTime;
+    role R
+    {
+        const N3: Nonce;
+        var N2: Nonce;
+        var T: TimeStamp;
+        var L: LifeTime;
 
-		var ni: Nonce;
-		const nr: Nonce;
+        var ni: Nonce;
+        const nr: Nonce;
 
-		read_3(I,R, I, R, {I, T, L, {N2}pk(R)}sk(I) );
-		send_4(R,S, R, I, N3 );
-		read_5(S,R, S, {S, R, N3, pk(I)}sk(S) );
-		send_6(R,I, R, I, {R, {N2}inc}pk(I) );
+        read_3(I,R, I, R, {I, T, L, {N2}pk(R)}sk(I) );
+        send_4(R,S, R, I, N3 );
+        read_5(S,R, S, {S, R, N3, pk(I)}sk(S) );
+        send_6(R,I, R, I, {R, {N2}inc}pk(I) );
 
-		claim_8(R, Secret, N2);
-		claim_11(R, Niagree);
-		claim_12(R, Nisynch);
-	}
+        claim_8(R, Secret, N2);
+        claim_11(R, Niagree);
+        claim_12(R, Nisynch);
+    }
 }
 
 const Alice,Bob,Simon,Eve: Agent;
diff --git a/spdl/SPORE/tmn.spdl b/spdl/SPORE/tmn.spdl
index 173abca..f3934a0 100644
--- a/spdl/SPORE/tmn.spdl
+++ b/spdl/SPORE/tmn.spdl
@@ -12,37 +12,37 @@ inversekeys(pk,sk);
 
 protocol tmn(I,R,S)
 {
-	role I
-	{
-		const Ki: Key;
-		var Kr: Key;
+    role I
+    {
+        const Ki: Key;
+        var Kr: Key;
 
-		send_1(I,S, R,{Ki}pk(S) );
-		read_4(S,I, R,{Kr}Ki );
+        send_1(I,S, R,{Ki}pk(S) );
+        read_4(S,I, R,{Kr}Ki );
 
-		claim_I1(I,Secret,Ki);
-		claim_I2(I,Secret,Kr);
-	}	
-	
-	role R
-	{
-		const Kr: Key;
+        claim_I1(I,Secret,Ki);
+        claim_I2(I,Secret,Kr);
+    }    
+    
+    role R
+    {
+        const Kr: Key;
 
-		read_2(S,R, I );
-		send_3(R,S, I, { Kr }pk(S) );
+        read_2(S,R, I );
+        send_3(R,S, I, { Kr }pk(S) );
 
-		claim_R1(R,Secret,Kr);
-	}
+        claim_R1(R,Secret,Kr);
+    }
 
-	role S
-	{
-		var Ki,Kr: Key;
+    role S
+    {
+        var Ki,Kr: Key;
 
-		read_1(I,S, R,{Ki}pk(S) );
-		send_2(S,R, I );
-		read_3(R,S, I, { Kr }pk(S) );
-		send_4(S,I, R,{Kr}Ki );
-	}
+        read_1(I,S, R,{Ki}pk(S) );
+        send_2(S,R, I );
+        read_3(R,S, I, { Kr }pk(S) );
+        send_4(S,I, R,{Kr}Ki );
+    }
 }
 
 const Alice,Bob,Eve,Simon: Agent;
diff --git a/spdl/SPORE/wmf-lowe.spdl b/spdl/SPORE/wmf-lowe.spdl
index a74118d..66c992d 100644
--- a/spdl/SPORE/wmf-lowe.spdl
+++ b/spdl/SPORE/wmf-lowe.spdl
@@ -18,44 +18,44 @@ secret k: Function;
 
 protocol wmfLowe(I,R,S)
 {
-	role I
-	{
-		const Kir: Key;
+    role I
+    {
+        const Kir: Key;
         const Ti: TimeStamp;
-		var Kr: Key;
+        var Kr: Key;
         var Nr: Nonce;
 
-		send_1(I,S, I, {Ti, R, Kir}k(I,S)); 
+        send_1(I,S, I, {Ti, R, Kir}k(I,S)); 
         read_3(R,I,{Nr}Kir);
         send_4(I,R,{{Nr}succ}Kir);
 
-		claim_I1(I,Secret,Kir);
+        claim_I1(I,Secret,Kir);
         claim_I2(I,Nisynch);
-	}	
-	
-	role R
-	{
+    }    
+    
+    role R
+    {
         var Ts: TimeStamp;
         var Kir: Key;
         const Nr: Nonce;
 
-		read_2(S,R, {Ts, I, Kir}k(R,S) );
+        read_2(S,R, {Ts, I, Kir}k(R,S) );
         send_3(R,I, {Nr}Kir);
         read_4(I,R, {{Nr}succ}Kir);
 
-		claim_R1(R,Secret,Kir);
+        claim_R1(R,Secret,Kir);
         claim_R2(R,Nisynch);
-	}
+    }
 
-	role S
-	{
-		var Kir: Key;
+    role S
+    {
+        var Kir: Key;
         const Ts: TimeStamp;
         var Ti: TimeStamp;
 
-		read_1(I,S, I,{Ti, R, Kir}k(I,S) );
+        read_1(I,S, I,{Ti, R, Kir}k(I,S) );
         send_2(S,R, {Ts, I, Kir}k(R,S));
-	}
+    }
 }
 
 const Alice,Bob,Eve,Simon: Agent;
diff --git a/spdl/SPORE/wmf.spdl b/spdl/SPORE/wmf.spdl
index cd953ff..0a01f83 100644
--- a/spdl/SPORE/wmf.spdl
+++ b/spdl/SPORE/wmf.spdl
@@ -11,37 +11,37 @@ secret k: Function;
 
 protocol wmf(I,R,S)
 {
-	role I
-	{
-		const Kir: Key;
+    role I
+    {
+        const Kir: Key;
         const Ti: TimeStamp;
-		var Kr: Key;
+        var Kr: Key;
 
-		send_1(I,S, I, {Ti, R, Kir}k(I,S)); 
+        send_1(I,S, I, {Ti, R, Kir}k(I,S)); 
 
-		claim_I1(I,Secret,Kir);
-	}	
-	
-	role R
-	{
+        claim_I1(I,Secret,Kir);
+    }    
+    
+    role R
+    {
         var Ts: TimeStamp;
         var Kir: Key;
 
-		read_2(S,R, {Ts, I, Kir}k(R,S) );
+        read_2(S,R, {Ts, I, Kir}k(R,S) );
 
-		claim_R1(R,Secret,Kir);
+        claim_R1(R,Secret,Kir);
         claim_R2(R,Nisynch);
-	}
+    }
 
-	role S
-	{
-		var Kir: Key;
+    role S
+    {
+        var Kir: Key;
         const Ts: TimeStamp;
         var Ti: TimeStamp;
 
-		read_1(I,S, I,{Ti, R, Kir}k(I,S) );
+        read_1(I,S, I,{Ti, R, Kir}k(I,S) );
         send_2(S,R, {Ts, I, Kir}k(R,S));
-	}
+    }
 }
 
 const Alice,Bob,Eve,Simon: Agent;
diff --git a/spdl/SPORE/woo-lam-pi-1.spdl b/spdl/SPORE/woo-lam-pi-1.spdl
index 21dee6d..945043f 100644
--- a/spdl/SPORE/woo-lam-pi-1.spdl
+++ b/spdl/SPORE/woo-lam-pi-1.spdl
@@ -14,18 +14,18 @@ secret k: Function;
 
 protocol woolamPi1(I,R,S)
 {
-	role I
-	{
-		var Nr: Nonce;
+    role I
+    {
+        var Nr: Nonce;
 
-		send_1(I,R, I); 
+        send_1(I,R, I); 
         read_2(R,I, Nr);
         send_3(I,R, {I,R,Nr}k(I,S));
 
-	}	
-	
-	role R
-	{
+    }    
+    
+    role R
+    {
         const Nr: Nonce;
         var T: Ticket;
 
@@ -36,15 +36,15 @@ protocol woolamPi1(I,R,S)
         read_5(S,R, {I,R, Nr}k(R,S));
         
         claim_R1(R,Nisynch);
-	}
+    }
 
-	role S
-	{
+    role S
+    {
         var Nr: Nonce;
         
         read_4(R,S, {I,R, {I,R,Nr}k(I,S)}k(R,S));
         send_5(S,R, {I,R,Nr}k(R,S));
-	}
+    }
 }
 
 const Alice,Bob,Eve,Simon: Agent;
diff --git a/spdl/SPORE/woo-lam-pi-2.spdl b/spdl/SPORE/woo-lam-pi-2.spdl
index f885ec9..11d5faf 100644
--- a/spdl/SPORE/woo-lam-pi-2.spdl
+++ b/spdl/SPORE/woo-lam-pi-2.spdl
@@ -14,18 +14,18 @@ secret k: Function;
 
 protocol woolamPi2(I,R,S)
 {
-	role I
-	{
-		var Nr: Nonce;
+    role I
+    {
+        var Nr: Nonce;
 
-		send_1(I,R, I); 
+        send_1(I,R, I); 
         read_2(R,I, Nr);
         send_3(I,R, {I,Nr}k(I,S));
 
-	}	
-	
-	role R
-	{
+    }    
+    
+    role R
+    {
         const Nr: Nonce;
         var T: Ticket;
 
@@ -36,15 +36,15 @@ protocol woolamPi2(I,R,S)
         read_5(S,R, {I, Nr}k(R,S));
         
         claim_R1(R,Nisynch);
-	}
+    }
 
-	role S
-	{
+    role S
+    {
         var Nr: Nonce;
         
         read_4(R,S, {I, {I,Nr}k(I,S)}k(R,S));
         send_5(S,R, {I,Nr}k(R,S));
-	}
+    }
 }
 
 const Alice,Bob,Eve,Simon: Agent;
diff --git a/spdl/SPORE/woo-lam-pi-3.spdl b/spdl/SPORE/woo-lam-pi-3.spdl
index 932afbf..06e7237 100644
--- a/spdl/SPORE/woo-lam-pi-3.spdl
+++ b/spdl/SPORE/woo-lam-pi-3.spdl
@@ -14,18 +14,18 @@ secret k: Function;
 
 protocol woolamPi3(I,R,S)
 {
-	role I
-	{
-		var Nr: Nonce;
+    role I
+    {
+        var Nr: Nonce;
 
-		send_1(I,R, I); 
+        send_1(I,R, I); 
         read_2(R,I, Nr);
         send_3(I,R, {Nr}k(I,S));
 
-	}	
-	
-	role R
-	{
+    }    
+    
+    role R
+    {
         const Nr: Nonce;
         var T: Ticket;
 
@@ -36,15 +36,15 @@ protocol woolamPi3(I,R,S)
         read_5(S,R, {I, Nr}k(R,S));
         
         claim_R1(R,Nisynch);
-	}
+    }
 
-	role S
-	{
+    role S
+    {
         var Nr: Nonce;
         
         read_4(R,S, {I, {Nr}k(I,S)}k(R,S));
         send_5(S,R, {I,Nr}k(R,S));
-	}
+    }
 }
 
 const Alice,Bob,Eve,Simon: Agent;
diff --git a/spdl/SPORE/woo-lam-pi-f.spdl b/spdl/SPORE/woo-lam-pi-f.spdl
index edbecfb..72680bf 100644
--- a/spdl/SPORE/woo-lam-pi-f.spdl
+++ b/spdl/SPORE/woo-lam-pi-f.spdl
@@ -14,18 +14,18 @@ secret k: Function;
 
 protocol woolamPif(I,R,S)
 {
-	role I
-	{
-		var Nr: Nonce;
+    role I
+    {
+        var Nr: Nonce;
 
-		send_1(I,R, I); 
+        send_1(I,R, I); 
         read_2(R,I, Nr);
         send_3(I,R, {I,R,Nr}k(I,S));
 
-	}	
-	
-	role R
-	{
+    }    
+    
+    role R
+    {
         const Nr: Nonce;
         var T: Ticket;
 
@@ -36,15 +36,15 @@ protocol woolamPif(I,R,S)
         read_5(S,R, {I, R, Nr}k(R,S));
         
         claim_R1(R,Nisynch);
-	}
+    }
 
-	role S
-	{
+    role S
+    {
         var Nr: Nonce;
         
         read_4(R,S, {I, R, Nr,{I,R,Nr}k(I,S)}k(R,S));
         send_5(S,R, {I, R, Nr}k(R,S));
-	}
+    }
 }
 
 const Alice,Bob,Eve,Simon: Agent;
diff --git a/spdl/SPORE/woo-lam-pi.spdl b/spdl/SPORE/woo-lam-pi.spdl
index 37b7233..fc8385f 100644
--- a/spdl/SPORE/woo-lam-pi.spdl
+++ b/spdl/SPORE/woo-lam-pi.spdl
@@ -18,18 +18,18 @@ secret k: Function;
 
 protocol woolamPi(I,R,S)
 {
-	role I
-	{
-		var Nr: Nonce;
+    role I
+    {
+        var Nr: Nonce;
 
-		send_1(I,R, I); 
+        send_1(I,R, I); 
         read_2(R,I, Nr);
         send_3(I,R, {Nr}k(I,S));
 
-	}	
-	
-	role R
-	{
+    }    
+    
+    role R
+    {
         const Nr: Nonce;
         var T: Ticket;
 
@@ -40,15 +40,15 @@ protocol woolamPi(I,R,S)
         read_5(S,R, {Nr}k(R,S));
         
         claim_R1(R,Nisynch);
-	}
+    }
 
-	role S
-	{
+    role S
+    {
         var Nr: Nonce;
         
         read_4(R,S, {I,{Nr}k(I,S)}k(R,S));
         send_5(S,R, {Nr}k(R,S));
-	}
+    }
 }
 
 const Alice,Bob,Eve,Simon: Agent;
diff --git a/spdl/SPORE/woo-lam.spdl b/spdl/SPORE/woo-lam.spdl
index b494771..fc1b160 100644
--- a/spdl/SPORE/woo-lam.spdl
+++ b/spdl/SPORE/woo-lam.spdl
@@ -16,25 +16,25 @@ secret k: Function;
 
 protocol woolam(I,R,S)
 {
-	role I
-	{
+    role I
+    {
         const N1: Nonce;
         var Kir: Key;
-		var N2: Nonce;
+        var N2: Nonce;
 
-		send_1(I,R, I, N1); 
+        send_1(I,R, I, N1); 
         read_2(R,I, R, N2);
         send_3(I,R, {I, R, N1, N2}k(I,S));
         read_6(R,I, {R, N1, N2, Kir}k(I,S), {N1,N2}Kir);
         send_7(I,R, {N2}Kir);
         
 
-		claim_I1(I,Secret,Kir);
+        claim_I1(I,Secret,Kir);
         claim_I2(I,Nisynch);
-	}	
-	
-	role R
-	{
+    }    
+    
+    role R
+    {
         const N2: Nonce;
         var N1: Nonce;
         var Kir: Key;
@@ -48,18 +48,18 @@ protocol woolam(I,R,S)
         send_6(R,I, T2, {N1,N2}Kir);
         read_7(I,R, {N2}Kir);
         
-		claim_R1(R,Secret,Kir);
+        claim_R1(R,Secret,Kir);
         claim_R2(R,Nisynch);
-	}
+    }
 
-	role S
-	{
-		const Kir: Key;
+    role S
+    {
+        const Kir: Key;
         var N1,N2: Nonce;
 
         read_4(R,S, {I, R, N1, N2}k(I,S), {I, R, N1, N2}k(R,S));
         send_5(S,R, {R, N1, N2, Kir}k(I,S), {I, N1, N2, Kir}k(R,S));
-	}
+    }
 }
 
 const Alice,Bob,Eve,Simon: Agent;
diff --git a/spdl/SPORE/yahalom-ban.spdl b/spdl/SPORE/yahalom-ban.spdl
index 17220b0..f4eb64e 100644
--- a/spdl/SPORE/yahalom-ban.spdl
+++ b/spdl/SPORE/yahalom-ban.spdl
@@ -15,44 +15,44 @@ usertype Ticket, Key;
 
 protocol yahalomBAN(I,R,S)
 {
-	role I
-	{
-		const Ni: Nonce;
-		var Nr: Nonce;
-		var T: Ticket;
-		var Kir: Key;
+    role I
+    {
+        const Ni: Nonce;
+        var Nr: Nonce;
+        var T: Ticket;
+        var Kir: Key;
 
-		send_1(I,R, I,Ni);
-		read_3(S,I, Nr, {R,Kir,Ni}k(I,S), T );
-		send_4(I,R, T, {Nr}Kir );
+        send_1(I,R, I,Ni);
+        read_3(S,I, Nr, {R,Kir,Ni}k(I,S), T );
+        send_4(I,R, T, {Nr}Kir );
 
-		claim_I1(I, Secret,Kir);
-		claim_I2(I, Nisynch);
-	}
+        claim_I1(I, Secret,Kir);
+        claim_I2(I, Nisynch);
+    }
 
-	role R
-	{
-		const Nr: Nonce;
-		var Ni: Nonce;
-		var T: Ticket;
-		var Kir: Key;
+    role R
+    {
+        const Nr: Nonce;
+        var Ni: Nonce;
+        var T: Ticket;
+        var Kir: Key;
 
-		read_1(I,R, I,Ni);
-		send_2(R,S, R, Nr, {I,Ni}k(R,S) );
-		read_4(I,R, {I,Kir,Nr}k(R,S) , {Nr}Kir );
+        read_1(I,R, I,Ni);
+        send_2(R,S, R, Nr, {I,Ni}k(R,S) );
+        read_4(I,R, {I,Kir,Nr}k(R,S) , {Nr}Kir );
 
-		claim_R1(R, Secret,Kir);
+        claim_R1(R, Secret,Kir);
         claim_R2(R, Nisynch);
-	}
+    }
 
-	role S
-	{
-		const Kir: Key;
-		var Ni,Nr: Nonce;
+    role S
+    {
+        const Kir: Key;
+        var Ni,Nr: Nonce;
 
-		read_2(R,S, R, {I,Ni,Nr}k(R,S) );
-		send_3(S,I, {R,Kir,Ni,Nr}k(I,S), {I,Kir}k(R,S) );
-	}
+        read_2(R,S, R, {I,Ni,Nr}k(R,S) );
+        send_3(S,I, {R,Kir,Ni,Nr}k(I,S), {I,Kir}k(R,S) );
+    }
 }
 
 const Alice,Bob,Simon : Agent;
diff --git a/spdl/SPORE/yahalom-lowe.spdl b/spdl/SPORE/yahalom-lowe.spdl
index ab0c6e5..65790f9 100644
--- a/spdl/SPORE/yahalom-lowe.spdl
+++ b/spdl/SPORE/yahalom-lowe.spdl
@@ -12,44 +12,44 @@ usertype Key;
 
 protocol yahalomLowe(I,R,S)
 {
-	role I
-	{
-		const Ni: Nonce;
-		var Nr: Nonce;
-		var Kir: Key;
+    role I
+    {
+        const Ni: Nonce;
+        var Nr: Nonce;
+        var Kir: Key;
 
-		send_1(I,R, I,Ni);
-		read_3(S,I, {R,Kir,Ni,Nr}k(I,S) );
-		send_5(I,R, {I, R, S, Nr}Kir );
+        send_1(I,R, I,Ni);
+        read_3(S,I, {R,Kir,Ni,Nr}k(I,S) );
+        send_5(I,R, {I, R, S, Nr}Kir );
 
-		claim_I1(I, Secret,Kir);
-		claim_I2(I, Nisynch);
-	}
+        claim_I1(I, Secret,Kir);
+        claim_I2(I, Nisynch);
+    }
 
-	role R
-	{
-		const Nr: Nonce;
-		var Ni: Nonce;
-		var Kir: Key;
+    role R
+    {
+        const Nr: Nonce;
+        var Ni: Nonce;
+        var Kir: Key;
 
-		read_1(I,R, I,Ni);
-		send_2(R,S, {I,Ni,Nr}k(R,S) );
-		read_4(S,R, {I,Kir}k(R,S));
-		read_5(I,R, {I, R, S, Nr}Kir);
+        read_1(I,R, I,Ni);
+        send_2(R,S, {I,Ni,Nr}k(R,S) );
+        read_4(S,R, {I,Kir}k(R,S));
+        read_5(I,R, {I, R, S, Nr}Kir);
 
-		claim_R1(R, Secret,Kir);
+        claim_R1(R, Secret,Kir);
         claim_R2(R, Nisynch);
-	}
+    }
 
-	role S
-	{
-		const Kir: Key;
-		var Ni,Nr: Nonce;
+    role S
+    {
+        const Kir: Key;
+        var Ni,Nr: Nonce;
 
-		read_2(R,S, {I,Ni,Nr}k(R,S) );
-		send_3(S,I, {R,Kir,Ni,Nr}k(I,S));
+        read_2(R,S, {I,Ni,Nr}k(R,S) );
+        send_3(S,I, {R,Kir,Ni,Nr}k(I,S));
         send_4(S,R, {I,Kir}k(R,S));
-	}
+    }
 }
 
 const Alice,Bob,Simon : Agent;
diff --git a/spdl/SPORE/yahalom-paulson.spdl b/spdl/SPORE/yahalom-paulson.spdl
index bed720d..b94aa96 100644
--- a/spdl/SPORE/yahalom-paulson.spdl
+++ b/spdl/SPORE/yahalom-paulson.spdl
@@ -15,44 +15,44 @@ usertype Ticket, Key;
 
 protocol yahalomPaulson(I,R,S)
 {
-	role I
-	{
-		const Ni: Nonce;
-		var Nr: Nonce;
-		var T: Ticket;
-		var Kir: Key;
+    role I
+    {
+        const Ni: Nonce;
+        var Nr: Nonce;
+        var T: Ticket;
+        var Kir: Key;
 
-		send_1(I,R, I,Ni);
-		read_3(S,I, Nr, {R,Kir,Ni}k(I,S), T );
-		send_4(I,R, T, {Nr}Kir );
+        send_1(I,R, I,Ni);
+        read_3(S,I, Nr, {R,Kir,Ni}k(I,S), T );
+        send_4(I,R, T, {Nr}Kir );
 
-		claim_I1(I, Secret,Kir);
-		claim_I2(I, Nisynch);
-	}
+        claim_I1(I, Secret,Kir);
+        claim_I2(I, Nisynch);
+    }
 
-	role R
-	{
-		const Nr: Nonce;
-		var Ni: Nonce;
-		var T: Ticket;
-		var Kir: Key;
+    role R
+    {
+        const Nr: Nonce;
+        var Ni: Nonce;
+        var T: Ticket;
+        var Kir: Key;
 
-		read_1(I,R, I,Ni);
-		send_2(R,S, R, Nr, {I,Ni}k(R,S) );
-		read_4(I,R, {I,R, Kir, Nr}k(R,S) , {Nr}Kir );
+        read_1(I,R, I,Ni);
+        send_2(R,S, R, Nr, {I,Ni}k(R,S) );
+        read_4(I,R, {I,R, Kir, Nr}k(R,S) , {Nr}Kir );
 
-		claim_R1(R, Secret,Kir);
+        claim_R1(R, Secret,Kir);
         claim_R2(R, Nisynch);
-	}
+    }
 
-	role S
-	{
-		const Kir: Key;
-		var Ni,Nr: Nonce;
+    role S
+    {
+        const Kir: Key;
+        var Ni,Nr: Nonce;
 
-		read_2(R,S, R, Nr, {I,Ni}k(R,S) );
-		send_3(S,I, Nr, {R,Kir,Ni}k(I,S), {I,R,Kir,Nr}k(R,S) );
-	}
+        read_2(R,S, R, Nr, {I,Ni}k(R,S) );
+        send_3(S,I, Nr, {R,Kir,Ni}k(I,S), {I,R,Kir,Nr}k(R,S) );
+    }
 }
 
 const Alice,Bob,Simon : Agent;
diff --git a/spdl/SPORE/yahalom.spdl b/spdl/SPORE/yahalom.spdl
index 126f5f3..d30354c 100644
--- a/spdl/SPORE/yahalom.spdl
+++ b/spdl/SPORE/yahalom.spdl
@@ -15,44 +15,44 @@ usertype Ticket, Key;
 
 protocol yahalom(I,R,S)
 {
-	role I
-	{
-		const Ni: Nonce;
-		var Nr: Nonce;
-		var T: Ticket;
-		var Kir: Key;
+    role I
+    {
+        const Ni: Nonce;
+        var Nr: Nonce;
+        var T: Ticket;
+        var Kir: Key;
 
-		send_1(I,R, I,Ni);
-		read_3(S,I, {R,Kir,Ni,Nr}k(I,S), T );
-		send_4(I,R, T, {Nr}Kir );
+        send_1(I,R, I,Ni);
+        read_3(S,I, {R,Kir,Ni,Nr}k(I,S), T );
+        send_4(I,R, T, {Nr}Kir );
 
-		claim_I1(I, Secret,Kir);
-		claim_I2(I, Nisynch);
-	}
+        claim_I1(I, Secret,Kir);
+        claim_I2(I, Nisynch);
+    }
 
-	role R
-	{
-		const Nr: Nonce;
-		var Ni: Nonce;
-		var T: Ticket;
-		var Kir: Key;
+    role R
+    {
+        const Nr: Nonce;
+        var Ni: Nonce;
+        var T: Ticket;
+        var Kir: Key;
 
-		read_1(I,R, I,Ni);
-		send_2(R,S, R, {I,Ni,Nr}k(R,S) );
-		read_4(I,R, {I,Kir}k(R,S) , {Nr}Kir );
+        read_1(I,R, I,Ni);
+        send_2(R,S, R, {I,Ni,Nr}k(R,S) );
+        read_4(I,R, {I,Kir}k(R,S) , {Nr}Kir );
 
-		claim_R1(R, Secret,Kir);
+        claim_R1(R, Secret,Kir);
         claim_R2(R, Nisynch);
-	}
+    }
 
-	role S
-	{
-		const Kir: Key;
-		var Ni,Nr: Nonce;
+    role S
+    {
+        const Kir: Key;
+        var Ni,Nr: Nonce;
 
-		read_2(R,S, R, {I,Ni,Nr}k(R,S) );
-		send_3(S,I, {R,Kir,Ni,Nr}k(I,S), {I,Kir}k(R,S) );
-	}
+        read_2(R,S, R, {I,Ni,Nr}k(R,S) );
+        send_3(S,I, {R,Kir,Ni,Nr}k(I,S), {I,Kir}k(R,S) );
+    }
 }
 
 const Alice,Bob,Simon : Agent;