init - crashes on "testcases/mixed/test3.spec"

data/testcases/positive/test2.spec

+Roles role0 role1 role2 role3 role4 role5;
+
+Users user0 user1 user2 user3 user4 user5 user6 user7 user8 user9;
+
+UA <user9,role5>;
+
+CR <role5,role0> <role5,role4> <role5,role2>;
+
+CA <role5,role2,role0> <role5,TRUE,role0> <role5,role1,role0> <role5,role4,role1> <role5,role2&role4,role1> <role5,role2&role4&role3,role1> <role5,TRUE,role1> <role5,TRUE,role2> <role5,role1&role3&role0,role2> <role5,role4&role1&role0,role2> <role5,TRUE,role3> <role5,role4,role3> <role5,role2&role1&role0,role3> <role5,TRUE,role4> <role5,role1&role3&role0,role4> <role5,role2&role3&role0,role4> <role5,role2,role4>;
+
+ADMIN user9;
+
+SPEC user3 role4;
\ No newline at end of file

data/testcases/positive/test3.spec

+Roles role0 role1 role2 role3 role4 role5 role6 role7 role8 role9 role10 role11 role12 role13 role14 role15 role16 role17 role18 role19 role20;
+
+Users user0 user1 user2 user3 user4 user5 user6 user7 user8 user9 user10 user11 user12 user13 user14 user15 user16 user17 user18 user19 user20 user21 user22 user23 user24 user25 user26 user27 user28 user29 user30 user31 user32 user33 user34 user35 user36 user37 user38 user39 user40 user41 user42 user43 user44 user45 user46 user47 user48 user49;
+
+UA <user49,role20>;
+
+CR <FALSE,role9> <FALSE,role2> <role20,role10> <role20,role7> <role20,role4> <role20,role11> <role20,role0> <role20,role1> <role20,role3> <role20,role13> <role20,role19>;
+
+CA <role20,role15&role8&role9&role11,role0> <role20,TRUE,role0> <role20,role2&role3&role5&role12,role0> <role20,role10,role0> <role20,role2&role9,role1> <role20,role6&role11&role7,role1> <role20,role2&role4&role19&role12,role1> <role20,TRUE,role1> <role20,role11&role1&role10&role0,role2> <role20,role13&role3&role12,role2> <role20,role15&role3&role7,role2> <role20,role1&role10,role2> <role20,TRUE,role3> <role20,role18,role3> <role20,role0,role4> <role20,role15&role2&role5&role12,role4> <role20,role8&role18,role4> <role20,role14,role4> <role20,role17&role11&role10,role5> <role20,role6&role10&role0,role5> <role20,role2&role6,role5> <role20,TRUE,role5> <role20,role2&role14&role7,role6> <role20,role17&role3&role7,role6> <role20,role11&role7,role6> <role20,role13&role14&role10,role6> <role20,TRUE,role7> <role20,role13&role6,role7> <role20,role5,role7> <role20,role4&role16&role12,role7> <role20,role16&role18,role8> <role20,TRUE,role8> <role20,role15&role9&role6,role8> <role20,role13&role16&role5,role8> <role20,role4&role19,role9> <role20,role6&role18&role12,role9> <role20,role19&role3,role9> <role20,role2,role9> <role20,role2&role16,role10> <role20,TRUE,role10> <role20,role15&role16&role7,role10> <role20,role17&role11&role6&role12,role10> <role20,role2&role1&role14&role0,role11> <role20,TRUE,role11> <role20,role13&role6&role18,role11> <role20,role15&role9,role11> <role20,role9&role11&role14,role12> <role20,role9&role16,role12> <role20,role2&role10&role7,role12> <role20,role2,role12> <role20,role15&role9&role6,role13> <role20,role2&role4,role13> <role20,role15,role13> <role20,role8&role11&role6,role13> <role20,role11&role16&role5,role14> <role20,role6&role18&role7,role14> <role20,role18&role12,role14> <role20,role9,role14> <role20,role19&role11&role12&role5,role15> <role20,role8&role3&role10,role15> <role20,role2&role3&role14&role12,role15> <role20,role3,role15> <role20,TRUE,role16> <role20,role3,role16> <role20,role19&role11&role0,role16> <role20,role17&role15&role18,role16> <role20,TRUE,role17> <role20,role13&role8&role3&role10,role17> <role20,role9&role8&role16,role17> <role20,role11,role17> <role20,role15&role7&role12&role5,role18> <role20,role17&role15&role10,role18> <role20,role4&role8&role3&role10,role18> <role20,role8&role11,role18> <role20,role2&role8&role6&role14,role19> <role20,role6&role18&role7&role0,role19> <role20,role2,role19> <role20,role17,role19>;
+
+ADMIN user49;
+
+SPEC user41 role13;
\ No newline at end of file

data/testcases/positive/test4.spec

+Roles role0 role1 role2 role3 role4 role5 role6 role7 role8 role9 role10 role11 role12 role13 role14 role15 role16 role17 role18 role19 role20 role21 role22 role23 role24 role25 role26 role27 role28 role29 role30 role31 role32 role33 role34 role35 role36 role37 role38 role39 role40;
+
+Users user0 user1 user2 user3 user4 user5 user6 user7 user8 user9 user10 user11 user12 user13 user14 user15 user16 user17 user18 user19 user20 user21 user22 user23 user24 user25 user26 user27 user28 user29 user30 user31 user32 user33 user34 user35 user36 user37 user38 user39 user40 user41 user42 user43 user44 user45 user46 user47 user48 user49 user50 user51 user52 user53 user54 user55 user56 user57 user58 user59 user60 user61 user62 user63 user64 user65 user66 user67 user68 user69 user70 user71 user72 user73 user74 user75 user76 user77 user78 user79 user80 user81 user82 user83 user84 user85 user86 user87 user88 user89 user90 user91 user92 user93 user94 user95 user96 user97 user98 user99;
+
+UA <user99,role40>;
+
+CR <role40,role20> <role40,role36> <role40,role29> <role40,role11> <role40,role23> <role40,role2> <role40,role9> <role40,role15> <role40,role3> <role40,role39> <role40,role34> <role40,role27> <role40,role31> <role40,role6> <role40,role24> <role40,role13> <role40,role8> <role40,role12> <role40,role25> <role40,role26> <role40,role35> <role40,role21> <role40,role4> <role40,role19> <role40,role10> <role40,role0> <role40,role37>;
+
+CA <role40,role34&role30&role31,role0> <role40,role19&role28&role37,role0> <role40,role9&role12&role22,role0> <role40,role32&role26&role1&role35,role0> <role40,role31,role1> <role40,TRUE,role1> <role40,role17&role26&role38,role1> <role40,role27,role1> <role40,role34&role11&role3&role14,role2> <role40,role15&role21&role37,role2> <role40,role8&role29,role2> <role40,role4&role26&role11&role22,role2> <role40,role1,role3> <role40,role34,role3> <role40,role13&role23&role20,role3> <role40,role19,role3> <role40,TRUE,role4> <role40,role15&role6&role39,role4> <role40,role34&role32&role17&role10,role4> <role40,role31&role14&role24,role5> <role40,role19&role31&role1&role37,role5> <role40,role15&role26&role21&role20,role5> <role40,role0&role27,role5> <role40,role36&role23&role14&role5,role6> <role40,role33&role18&role7,role6> <role40,TRUE,role6> <role40,role38&role35,role6> <role40,TRUE,role7> <role40,role28&role27,role7> <role40,role9&role26&role6&role37,role7> <role40,role29,role8> <role40,role5,role8> <role40,role4&role22,role8> <role40,role34&role9&role28,role8> <role40,TRUE,role9> <role40,role23&role28&role39,role9> <role40,role15&role30&role24&role7,role9> <role40,role31&role24,role9> <role40,role25,role10> <role40,role17,role10> <role40,role16&role24&role27,role10> <role40,role34&role14&role3,role10> <role40,TRUE,role11> <role40,role17&role33&role20,role11> <role40,role8&role26&role18&role39,role11> <role40,role28&role37&role5,role11> <role40,role23&role26&role6&role0,role12> <role40,role37&role7,role12> <role40,role17&role13&role35,role12> <role40,role1&role35&role24&role5,role12> <role40,role23,role13> <role40,TRUE,role13> <role40,role31,role13> <role40,role9,role13> <role40,role13,role14> <role40,role11&role25,role14> <role40,role8&role24&role22,role14> <role40,role23&role27,role14> <role40,role3,role15> <role40,role1,role15> <role40,TRUE,role15> <role40,role34&role9&role26&role29,role15> <role40,role3&role25,role16> <role40,role4&role1,role16> <role40,role10&role7,role16> <role40,role9&role11&role29&role37,role16> <role40,role11&role3,role17> <role40,role9&role3,role17> <role40,role6,role17> <role40,role16&role18&role24&role27,role17> <role40,role17&role13&role23,role18> <role40,TRUE,role18> <role40,role1,role18> <role40,role9&role33&role14&role24,role18> <role40,role17&role9&role11,role19> <role40,role18&role25,role19> <role40,role26&role31,role19> <role40,role15&role36&role31&role37,role19> <role40,role30,role20> <role40,role17&role37,role20> <role40,TRUE,role20> <role40,role34&role15&role27,role20> <role40,role13&role16&role37,role21> <role40,role2&role3&role24&role27,role21> <role40,TRUE,role21> <role40,role34&role38&role37,role22> <role40,role20,role22> <role40,TRUE,role22> <role40,role36&role16&role35,role23> <role40,role1,role23> <role40,TRUE,role23> <role40,role2&role13&role30,role23> <role40,role0,role24> <role40,role34&role4&role6&role5,role24> <role40,role25,role24> <role40,TRUE,role24> <role40,role2,role25> <role40,role2&role9&role10&role27,role25> <role40,role2&role19&role21&role18,role25> <role40,role4&role33&role10,role25> <role40,role38,role26> <role40,role30&role19&role20,role26> <role40,role39,role26> <role40,role30&role16,role26> <role40,TRUE,role27> <role40,role5,role27> <role40,role3,role27> <role40,role4&role13&role9&role23,role28> <role40,TRUE,role28> <role40,role34&role30&role11,role28> <role40,role16&role12&role0&role22,role29> <role40,role2&role37,role29> <role40,TRUE,role29> <role40,TRUE,role30> <role40,role27,role30> <role40,role23&role11&role31&role0,role30> <role40,role2,role30> <role40,role6&role14,role31> <role40,TRUE,role31> <role40,role19&role1&role18&role25,role31> <role40,role34&role4&role36,role31> <role40,role9&role27,role32> <role40,role19&role38&role18,role32> <role40,role9&role1&role10,role32> <role40,role28&role6&role37,role32> <role40,role9&role16,role33> <role40,TRUE,role33> <role40,role19,role33> <role40,role17&role28&role6,role33> <role40,role11,role34> <role40,TRUE,role34> <role40,role13&role1,role34> <role40,role4&role1,role34> <role40,role37&role25,role35> <role40,role30&role28&role37&role10,role35> <role40,role6&role29,role35> <role40,TRUE,role35> <role40,role30&role26,role36> <role40,role14,role36> <role40,TRUE,role36> <role40,role31,role36> <role40,role28,role37> <role40,role15&role19&role3,role37> <role40,role32&role30,role37> <role40,role36,role37> <role40,role4,role38> <role40,role29&role39&role22,role38> <role40,role15&role29&role24,role38> <role40,role34&role4&role30&role33,role38> <role40,TRUE,role39> <role40,role28,role39>;
+
+ADMIN user99;
+
+SPEC user12 role39;
\ No newline at end of file

lib/rbac.g

+header {
+package mohawk;
+
+import java.util.Vector;
+import java.util.Stack;
+import java.util.HashMap;
+import java.util.Map;
+import mohawk.collections.PreCondProcessorInt;
+
+}
+
+class RBACParser extends Parser;
+
+options { k=3; }
+
+{
+	Vector<String> vRoles;
+	Vector<String> vUsers;
+	Vector<String> vAdmin;
+	Map<Integer, String> mRoleIndex;
+	Map<String, Integer> mRole2Index;
+	Map<Integer, String> mUserIndex;
+	Map<String,Vector<Integer>> mUA;
+	Map<String,Vector<CREntry>> mCR;
+	Map<String,Vector<CAEntry>> mCA;	
+	PreCondProcessorInt preCndP;
+	Stack<Integer> stackOperators;
+	Vector<String> vSpec; // This vector holds two strings - user and role that will be used in the LTL formulae
+	
+	// Indices for user and roles while parsing
+	// Each user has an index corresponding to the order in which the name appears in the list.
+	int iRoleIndex;
+	int iUserIndex;
+	
+
+	public void initRbac() {
+		
+		vRoles = new Vector<String>();
+		vUsers = new Vector<String>();
+		vAdmin = new Vector<String>();
+		mRoleIndex = new HashMap<Integer, String>();
+		mRole2Index = new HashMap<String,Integer>();
+		mUserIndex = new HashMap<Integer, String>();
+		mUA = new HashMap<String,Vector<Integer>>();
+		mCR = new HashMap<String,Vector<CREntry>>();
+		mCA = new HashMap<String,Vector<CAEntry>>();
+		vSpec = new Vector<String>();		
+	}
+	
+	public RBACInstance getRBAC() {
+		return new RBACInstance(vRoles, vUsers, vAdmin, mUA, mCR, mCA,vSpec);
+	}
+	
+	public void setUA(String strUser, String strRole) {
+	
+		Vector<Integer> vUserUA = mUA.get(strUser);		
+		if(vUserUA == null)
+		{
+			vUserUA = new Vector<Integer>();
+			mUA.put(strUser,vUserUA);
+		}
+		
+		int iRoleIndex = mRole2Index.get(strRole); //getMapKey(mRoleIndex, strRole);		
+		vUserUA.add(iRoleIndex);
+	}
+	
+	public void addCREntry(String inStrPreCond, String inStrRole) {
+		
+		CREntry crEntry = new CREntry(inStrPreCond, inStrRole);
+		Vector<CREntry> vCR = mCR.get(inStrRole);
+		
+		if(vCR == null)
+			vCR = new Vector<CREntry>();
+		
+		vCR.add(new CREntry(inStrPreCond, inStrRole));
+		mCR.put(inStrRole,vCR);
+	}
+	
+	public void addCAEntry(String inStrAdminRole, PreCondition pcPreCond, String inStrRole) {
+		
+		CAEntry caEntry = new CAEntry(inStrAdminRole, pcPreCond, inStrRole);
+		Vector<CAEntry> vCA = mCA.get(inStrRole);
+		
+		if(vCA == null)
+			vCA = new Vector<CAEntry>();
+		vCA.add(caEntry);
+		mCA.put(inStrRole,vCA);
+	}
+	/*	
+	private int getMapKey(Map<Integer,String> inMap, String inString) {
+		
+		for(int i=0; i<inMap.size(); i++) {
+			
+			if(inMap.get(i).equals(inString)) {
+				return i;
+			}
+		}
+		
+		System.out.println("Error - BTree::getMapIndex - Value not found in map");
+		return 0;
+	}
+	*/
+	
+	public void addSpec(String inStrUser, String inStrRole) {
+	
+		vSpec.add(inStrUser);
+		vSpec.add(inStrRole);
+	}
+	
+}
+
+roles : ("Roles" {iRoleIndex=0;} ) (n:ID {vRoles.add(n.getText()); 
+                                            mRoleIndex.put(iRoleIndex,n.getText()); 
+                                            mRole2Index.put(n.getText(),iRoleIndex);
+                                            iRoleIndex++; })+ SEMI;
+
+users : ("Users" {iUserIndex=0;} ) (u:ID {vUsers.add(u.getText()); 
+                                            mUserIndex.put(iUserIndex,u.getText());
+                                            iUserIndex++; })+ SEMI;
+
+ua : "UA" (LANGLE x:ID COMMA y:ID RANGLE { setUA(x.getText(),y.getText()); })+ SEMI;
+
+ca : "CA" (caentry)* SEMI;
+
+caentry : (LANGLE {preCndP = new PreCondProcessorInt(mRole2Index);}) d:ID COMMA e:precondition COMMA f:ID (RANGLE 
+{ 
+	try {
+  	PreCondition pcPreCond = preCndP.result(); 
+  	addCAEntry(d.getText(), pcPreCond, f.getText()); 
+  	}catch(Exception e) {
+  		e.printStackTrace();
+  	}	   
+}
+);
+
+precondition : atom (COND atom)* | "TRUE";
+
+atom : {int iNeg=0; } (n:NOT { iNeg=1; } )? (a:ID 
+{ 
+	try {
+	
+		if(iNeg == 0)
+			preCndP.add(a.getText());
+		else	
+			preCndP.addNeg(a.getText()); 
+			
+	} catch (Exception e) {
+		// TODO Auto-generated catch block
+		e.printStackTrace();
+	}
+} 
+);
+
+cr : "CR" (LANGLE mm:ID COMMA nn:ID RANGLE { addCREntry(mm.getText(),nn.getText()); })* SEMI;
+
+admin : "ADMIN" (u:ID { vAdmin.add(u.getText()); })+ SEMI;
+
+spec : "SPEC" (su:ID sr:ID { addSpec(su.getText(),sr.getText()); }) SEMI;
+
+class RBACLexer extends Lexer;
+
+options { k=2;}
+
+ID  :	('a'..'z'|'A'..'Z'|'_') ('a'..'z'|'A'..'Z'|'0'..'9'|'_')*
+    ;
+
+LANGLE : '<'
+ 	   ;
+
+RANGLE : '>'
+       ;
+
+COMMA : ','
+      ;
+
+COND : '&';
+     
+NOT : '-';	 	    
+
+SEMI : ';';
+
+WS : (' ' | '\t' | '\r' { newline();} | "\r\n" { newline();} | '\n' { newline(); } ) {$setType(Token.SKIP);}; 
+
+COMMENT :   "//" (~( '\n' | '\r' ))* ('\r')? '\n' {$setType(Token.SKIP);} ;

lib/rbac.st

+Roles $roles; separator=" "$;
+
+Users $users; separator=" "$;
+
+UA $ua; separator=" "$;
+
+CR $cr; separator=" "$;
+
+CA $ca; separator=" "$;
+
+ADMIN $adminusers; separator=" "$;
+
+SPEC $spec; separator=" "$;

lib/smvtemplate.st

+-- This NuSMV specification was automatically generated by the 
+-- RBAC2SMV tool.
+
+MODULE main
+VAR
+
+-- This section will contain state variables. For each user, we will have 
+-- an array. 
+
+$userarrays; separator=";\n"$;
+
+-- This section will contain enumerations for users and actions
+act : {ADD, REMOVE};
+user : {$users; separator=","$};
+admin : {$admin; separator=","$};
+role : $role$;
+
+ASSIGN
+
+-- Assigning UA
+$ua; separator=";\n"$;
+
+-- This section will contain state transition rules
+
+$transitions; separator= "\n-- Another user \n" $
+
+-- LTLSPEC
+
+LTLSPEC G ($user$[$roleindex$]=0)
\ No newline at end of file

lib/transitions.st

+next($roleindex1$) := 
+case
+$transition; separator=";\n" $
+1 : $roleindex2$; 
+esac;
\ No newline at end of file

src/mohawk/AbsRefine.java

+/**
+ * The MIT License
+ * 
+ * Copyright (c) 2010 Karthick Jayaraman
+ * 
+ * Permission is hereby granted, free of charge, to any person obtaining a copy
+ * of this software and associated documentation files (the "Software"), to deal
+ * in the Software without restriction, including without limitation the rights
+ * to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
+ * copies of the Software, and to permit persons to whom the Software is
+ * furnished to do so, subject to the following conditions:
+ * 
+ * The above copyright notice and this permission notice shall be included in
+ * all copies or substantial portions of the Software.
+ * 
+ * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+ * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
+ * FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
+ * AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
+ * LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
+ * OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN
+ * THE SOFTWARE. 
+ */
+package mohawk;
+
+import java.io.File;
+
+/**
+ * @author Karthick Jayaraman
+ * 
+ */
+public class AbsRefine {
+	
+	public static void main(String args[])
+	{
+		if(args.length < 1)
+		{
+			System.out.println("Usage: java -cp ./mohawk.jar mohawk.AbsRefine <rbacspec>");
+		}
+		
+		File rbacfile = new File(args[0]);
+		
+		if(!rbacfile.exists()) {
+			System.out.println("The RBAC specification file "+rbacfile+" does not exists.");
+			return;
+		}
+		
+		RBACSpecReader reader = new RBACSpecReader(args[0]);
+		RBACInstance rbac = reader.getRBAC();
+		
+		RolesAbsRefine absrefine = new RolesAbsRefine(rbac);
+		absrefine.absrefineloop();
+	}
+}

src/mohawk/CREntry.java

+/**
+ * The MIT License
+ * 
+ * Copyright (c) 2010 Karthick Jayaraman
+ * 
+ * Permission is hereby granted, free of charge, to any person obtaining a copy
+ * of this software and associated documentation files (the "Software"), to deal
+ * in the Software without restriction, including without limitation the rights
+ * to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
+ * copies of the Software, and to permit persons to whom the Software is
+ * furnished to do so, subject to the following conditions:
+ * 
+ * The above copyright notice and this permission notice shall be included in
+ * all copies or substantial portions of the Software.
+ * 
+ * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+ * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
+ * FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
+ * AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
+ * LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
+ * OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN
+ * THE SOFTWARE. 
+ */
+
+package mohawk;
+
+/**
+ * Each CREntry represents a rule for revocation. 
+ * The first entry describes the pre-conditions for the revocation.
+ * The preconditions essentially describes the roles the administrator should
+ * have to do the revocation.
+ *  
+ *			@author Karthick Jayaraman
+ */
+public class CREntry {
+
+	private String strPreCond;
+	private String strRole;
+	
+	public CREntry(String inPreCond, String inStr ) {
+		strPreCond = inPreCond;
+		strRole = inStr;
+	}
+	
+	public void setPreCond(String inPreCond) {
+		strPreCond = inPreCond;
+	}
+	
+	public String getPreCond() {
+		return strPreCond;
+	}
+	
+	public void setStrRole(String inStrRole) {
+		strRole = inStrRole;
+	}
+	
+	public String getStrRole() {
+		return strRole;
+	}
+	
+}