/*

 Dublin City University,
 M.Sc. in Security and Forensic Computing 2005/2006
 
 CA548 - Secure Software Development
 Lecturer: Dr. David Sinclair
 
 Student: Sebastian Wolfgarten, 55135811
 
 Description: Formal specification of an
 electronic locking system using Promela.

 Date: 10/April/2006

*/

/* Channel specifications */
mtype = { valid_user, invalid_user, keypad_ready, server_ready };
chan server_to_keypad = [1] of { mtype };
chan keypad_to_server = [1] of { short,short,short,short };
chan keypad_to_user = [1] of { mtype };
chan user_to_keypad = [4] of { short };

/* Definitions for the test cases */
mtype = { case1, case2, case3, case4, case5, case6, case7, case8, case9, do_timeout, keypad_done, server_done };
chan test_sequencer = [1] of { mtype };

/* Global variables */
bool fire_alarm = false;
bool kill_server = false;

init {

	run central_server();
	run test_case1();
	run test_case2();
	run test_case3();
	run test_case4();
	run test_case5();
	run test_case6();
	run test_case7();
	run test_case8();
	run test_case9();
	test_sequencer!case1; 

}

proctype central_server() {

	/* The system codes */
	short valid_codes[10];
	
	valid_codes[0] = 1115;
	valid_codes[1] = 1238;
	valid_codes[2] = 4142;
	valid_codes[3] = 9012;
	valid_codes[4] = 1292;
	valid_codes[5] = 8901;
	valid_codes[6] = 1572;
	valid_codes[7] = 3221;
	valid_codes[8] = 7361;
	valid_codes[9] = 2384;

	/* The admin code - could hold more than one if necessary */
	short admin_codes[1];
	
	admin_codes[0] = 7781;
	
	/* Initial state of codes*/
	short key1;	
	short key2;
	short key3;
	short key4;

	/* Is user valid? (=a valid code was entered) */
	bool is_valid_user = false;

	/* Is admin user? (=admin code was entered) */
	bool is_admin_user = false;

	/* Is duress situation? */
	bool is_duress = false;

	/* Which was the last code the system has encountered? */
	short last_code = 0;

	/* Counter for wrong codes */
	short ctr_wrong_codes = 0;

	/* Counter for the same wrong code */
	short ctr_same_wrong_code = 0;

	/* One variable to hold key1,key2,key3 and key4 */
	short user_input = 0;

	printf("Central system up and running...\n");
	printf("\n");
	
	/* If necessary, more than one keypad could be started here. */
	printf("Activating keypad.\n");
	run keypad(0);
	
	do

		:: test_sequencer?server_done -> break

		:: keypad_to_server?key1,key2,key3,key4;
			printf("Server retr: %d-%d-%d-%d\n",key1,key2,key3,key4);
				
			printf("Verifying user input...\n");
					
			byte position = 0;
			user_input = key1*1000+key2*100+key3*10+key4;
	
			do

				/* Did the user send a valid signal */
				:: (valid_codes[position] == user_input) -> 
				
					printf("Code %d verified.\n",valid_codes[position]);
					is_valid_user = true;
					server_to_keypad!valid_user;

					/* 

						These variables are used for generating an alarm if
						a) a user enters the same invalid code three times in a row or
						b) 10 invalid codes are entered sequentially.
	
					*/
					last_code = 0;
					ctr_wrong_codes = 0;
					ctr_same_wrong_code = 0;
					break;

				/* Is $code-1 a valid code? If so, send a duress signal!!! */
				:: (valid_codes[position] == user_input-1) -> 
					
					printf("Code %d verified.\n",valid_codes[position]);
					is_valid_user = true;
					server_to_keypad!valid_user;
					printf("ALERT: Duress code entered!\n");
					printf("Sending alert signal...\n");
					is_duress = true;
					break;
					
				/* The spec says that only 10 codes are allowed in the list of valid codes */
				:: ( position == 9 ) -> 
					
					printf("Code %d NOT verified.\n",user_input);
					printf("Please try again.\n");
			
					/* 

						This section is used for generating an alarm if
						a) a user enters the same invalid code three times in a row or
						b) 10 invalid codes are entered in sequence.
	
					*/
					ctr_wrong_codes++;
					
					if

						:: (user_input == last_code) -> 

							ctr_same_wrong_code++;

						:: else ->

							skip;

					fi;
					last_code = user_input;

					/* Generate alarm if 3 or 10 invalid codes are entered */
					if

						:: (ctr_same_wrong_code == 2) ->
							
							printf("ALARM: User entered the same invalid code three times in a row!\n");
							ctr_same_wrong_code = 0;
						
						:: (ctr_wrong_codes == 9) ->

							printf("ALARM: 10 invalid codes were entered in sequence!\n");

						:: else ->

							skip;

					fi;

					if

						/* An invalid code was entered. Is it maybe an admin code? */
			
						:: (admin_codes[0] == user_input) ->

							printf("\n");
							printf("Admin code entered!\n");
							is_valid_user = false;
							is_admin_user = true;
				
							printf("\n");
							printf("::: ADMIN MENU :::\n\n");			
							printf("(1) Add new user.\n");			
							printf("(2) Delete user.\n");			
							printf("(3) Modify existing user.\n");			
							printf("\n");			

						:: else ->

							skip;

					fi;

					is_valid_user = false;
					server_to_keypad!invalid_user;
					break;
				
				:: (kill_server == true) ->
				
					printf("Server is shutting down...\n");
					goto shutdown
						
				:: else -> 
					
					position++;
					
			od;

			position = 0;

	od;

shutdown:
	skip

}

/* 

	A number of these keypads will be activated by the central system
	as soon as the central system is started.

	The user processes will send individual keys to the keypad
	and the keypad will turn them into an array which is then send
	on to the server.

*/
 
proctype keypad(int number) {

	/* Variables for user input */
	short key1 = -1;	
	short key2 = -1;
	short key3 = -1;
	short key4 = -1;

	/* Some variables for the keypad proctype */
	bool send_beep_sound = false;
	short door_ctr = 5;	
	bool open_door = false;
	
	printf("Keypad number %d started.\n\n",number);

	do

	:: (1) ->

		keypad_to_user!keypad_ready;

		do

			:: test_sequencer?keypad_done -> goto shutdown
			:: user_to_keypad?key1 -> break
			:: (fire_alarm == true) -> 

				printf("ALERT: Fire alarm detected. Opening all doors!\n");
				atomic {
							
					open_door = true;
					fire_alarm = false;
				
				}

		od;

		do

			:: user_to_keypad?key2 -> break
			:: (fire_alarm == true) -> 

				printf("ALERT: Fire alarm detected. Opening all doors!\n");
				atomic {
							
					open_door = true;
					fire_alarm = false;	
		
				}
				
		od;

		do

			:: user_to_keypad?key3 -> break
			:: (fire_alarm == true) -> 

				printf("ALERT: Fire alarm detected. Opening all doors!\n");
				atomic {
							
					open_door = true;
					fire_alarm = false;
					
				}
		
		od;

		do

			:: user_to_keypad?key4 -> break
			:: (fire_alarm == true) -> 

				printf("ALERT: Fire alarm detected. Opening all doors!\n");
				atomic {
							
					open_door = true;
					fire_alarm = false;
					
				}

		od;

					printf("Keypad retr: %d\n",key1);
					printf("Keypad retr: %d\n",key2);
					printf("Keypad retr: %d\n",key3);
					printf("Keypad retr: %d\n",key4);
					
					if
				
						/* Some variables for the keypad proctype */
						:: (key1 == 99 || key2 == 99 || key3 == 99 || key4 == 99) -> 
					
							printf("A timeout occurred while entering the keys.\n");
															
						:: else ->
						
							printf("Sending keys to server...\n");
							keypad_to_server!key1,key2,key3,key4;
									
							if 
										
								:: server_to_keypad?invalid_user ->
										
									printf("Unknown/invalid code. Please try again.\n");
									open_door = false;
									send_beep_sound = true;
										
								:: server_to_keypad?valid_user ->
										
									printf("Valid code. Opening door.\n");
									open_door = true;
										
									printf("Will close door in %d seconds...\n",door_ctr);
										
									atomic {
								
										do
										
											:: (door_ctr > 0) ->
										
												printf("%d second(s).\n",door_ctr);
												door_ctr--;
										
											:: (door_ctr == 0) ->
										
												printf("Closing door!\n");
												open_door = false;
												break
										
										od;
						
										door_ctr = 5;
										
									}

								:: timeout ->

									printf("The keypad was unable to connect to the central server!\n");
									printf("Door will be opened.\n");
									open_door = true;
				
							fi;
			fi;

	od;
shutdown:
	skip
}

proctype test_case1() {

	test_sequencer?case1;

	/* First test case: Send valid user code */
	printf("Running 1st test case: Sending a valid user code.\n");

	/* Variables for user input */
	byte input1 = 7;	
	byte input2 = 3;
	byte input3 = 6;
	byte input4 = 1;
	
	if

		:: keypad_to_user?keypad_ready ->

			user_to_keypad!input1;
			user_to_keypad!input2;
			user_to_keypad!input3;
			user_to_keypad!input4;
				
			printf("The user entered: %d-%d-%d-%d.\n",input1,input2,input3,input4);
	
	fi;

	test_sequencer!case2;

}

proctype test_case2() {

	test_sequencer?case2;

	/* Second test case: Send invalid user code */
	printf("Running 2nd test case: Sending an invalid user code.\n");

	/* Variables for user input */
	byte input1 = 3;	
	byte input2 = 8;
	byte input3 = 9;
	byte input4 = 4;
	
	if

		:: keypad_to_user?keypad_ready ->

			user_to_keypad!input1;
			user_to_keypad!input2;
			user_to_keypad!input3;
			user_to_keypad!input4;
				
			printf("The user entered: %d-%d-%d-%d.\n",input1,input2,input3,input4);
	
	fi;

	test_sequencer!case3;

}

proctype test_case3() {

	test_sequencer?case3;

	/* Third test case: Cause duress signal (valid code +1) */
	printf("Running 3rd test case: Sending a duress user code.\n");

	/* Variables for user input */
	byte input1 = 7;	
	byte input2 = 3;
	byte input3 = 6;
	byte input4 = 2;
	
	if

		:: keypad_to_user?keypad_ready ->

			user_to_keypad!input1;
			user_to_keypad!input2;
			user_to_keypad!input3;
			user_to_keypad!input4;
				
			printf("The user entered: %d-%d-%d-%d.\n",input1,input2,input3,input4);
	
	fi;

	test_sequencer!case4;

}

proctype test_case4() {

	test_sequencer?case4;

	/* Fourth test case: Send admin code */
	printf("Running 4th test case: Sending an admin code.\n");

	/* Variables for user input */
	byte input1 = 7;	
	byte input2 = 7;
	byte input3 = 8;
	byte input4 = 1;
	
	if

		:: keypad_to_user?keypad_ready ->

			user_to_keypad!input1;
			user_to_keypad!input2;
			user_to_keypad!input3;
			user_to_keypad!input4;
				
			printf("The user entered: %d-%d-%d-%d.\n",input1,input2,input3,input4);
	
	fi;

	test_sequencer!case5;

}

proctype test_case5() {

	test_sequencer?case5;

	/* Fifth test case: A timeout occurs while entering a code */
	printf("Running 5th test case: A timeout occurs while entering a code.\n");

	/* Variables for user input */
	byte input1 = 1;	
	byte input2 = 4;
	byte input3 = 6;
	byte input4 = 99;
	
	if

		:: keypad_to_user?keypad_ready ->

			user_to_keypad!input1;
			user_to_keypad!input2;
			user_to_keypad!input3;
			user_to_keypad!input4;
				
			printf("The user entered: %d-%d-%d-%d.\n",input1,input2,input3,input4);
	
	fi;

	test_sequencer!case6;

}

proctype test_case6() {

	test_sequencer?case6;

	/* Sixth test case: Same invalid code (1461) is entered 3 times in a row */
	printf("Running 6th test case: Same invalid code is entered 3 times in a row.\n");

	/* Variables for user input */
	byte input1 = 1;	
	byte input2 = 4;
	byte input3 = 6;
	byte input4 = 1;
	
	if

		:: keypad_to_user?keypad_ready ->

			user_to_keypad!input1;
			user_to_keypad!input2;
			user_to_keypad!input3;
			user_to_keypad!input4;
				
			printf("The user entered: %d-%d-%d-%d.\n",input1,input2,input3,input4);
	
	fi;

	if

		:: keypad_to_user?keypad_ready ->

			user_to_keypad!input1;
			user_to_keypad!input2;
			user_to_keypad!input3;
			user_to_keypad!input4;
				
			printf("The user entered: %d-%d-%d-%d.\n",input1,input2,input3,input4);
	
	fi;

	if

		:: keypad_to_user?keypad_ready ->

			user_to_keypad!input1;
			user_to_keypad!input2;
			user_to_keypad!input3;
			user_to_keypad!input4;
				
			printf("The user entered: %d-%d-%d-%d.\n",input1,input2,input3,input4);
	
	fi;

	test_sequencer!case7;

}

proctype test_case7() {

	test_sequencer?case7;

	/* Seventh test case: A fire alarm is triggered */
	printf("Running 7th test case: A fire alarm is triggered.\n");

	fire_alarm = true;

	/* wait until the alarm has been noticed */
	(fire_alarm == false);

	test_sequencer!case8;

}

proctype test_case8() {

	test_sequencer?case8;

	/* Eigth test case: 10 invalid codes entered in a row. */
	printf("Running 8th test case: 10 invalid codes entered in a row.\n");

	/* Variables for user input */
	byte input1 = 1;	
	byte input2 = 1;
	byte input3 = 1;
	byte input4 = 1;
	
	if

		:: keypad_to_user?keypad_ready ->

			user_to_keypad!input1;
			user_to_keypad!input2;
			user_to_keypad!input3;
			user_to_keypad!input4;
				
			printf("The user entered: %d-%d-%d-%d.\n",input1,input2,input3,input4);
	
	fi;

	input1 = 1;	
	input2 = 1;
	input3 = 1;
	input4 = 2;
	
	if

		:: keypad_to_user?keypad_ready ->

			user_to_keypad!input1;
			user_to_keypad!input2;
			user_to_keypad!input3;
			user_to_keypad!input4;
				
			printf("The user entered: %d-%d-%d-%d.\n",input1,input2,input3,input4);
	
	fi;

	input1 = 2;	
	input2 = 2;
	input3 = 2;
	input4 = 2;
	
	if

		:: keypad_to_user?keypad_ready ->

			user_to_keypad!input1;
			user_to_keypad!input2;
			user_to_keypad!input3;
			user_to_keypad!input4;
				
			printf("The user entered: %d-%d-%d-%d.\n",input1,input2,input3,input4);
	
	fi;

	input1 = 3;	
	input2 = 3;
	input3 = 3;
	input4 = 3;
	
	if

		:: keypad_to_user?keypad_ready ->

			user_to_keypad!input1;
			user_to_keypad!input2;
			user_to_keypad!input3;
			user_to_keypad!input4;
				
			printf("The user entered: %d-%d-%d-%d.\n",input1,input2,input3,input4);
	
	fi;

	input1 = 4;	
	input2 = 4;
	input3 = 4;
	input4 = 4;
	
	if

		:: keypad_to_user?keypad_ready ->

			user_to_keypad!input1;
			user_to_keypad!input2;
			user_to_keypad!input3;
			user_to_keypad!input4;
				
			printf("The user entered: %d-%d-%d-%d.\n",input1,input2,input3,input4);
	
	fi;

	input1 = 5;	
	input2 = 5;
	input3 = 5;
	input4 = 5;
	
	if

		:: keypad_to_user?keypad_ready ->

			user_to_keypad!input1;
			user_to_keypad!input2;
			user_to_keypad!input3;
			user_to_keypad!input4;
				
			printf("The user entered: %d-%d-%d-%d.\n",input1,input2,input3,input4);
	
	fi;

	input1 = 6;	
	input2 = 6;
	input3 = 6;
	input4 = 6;
	
	if

		:: keypad_to_user?keypad_ready ->

			user_to_keypad!input1;
			user_to_keypad!input2;
			user_to_keypad!input3;
			user_to_keypad!input4;
				
			printf("The user entered: %d-%d-%d-%d.\n",input1,input2,input3,input4);
	
	fi;

	input1 = 7;	
	input2 = 7;
	input3 = 7;
	input4 = 7;
	
	if

		:: keypad_to_user?keypad_ready ->

			user_to_keypad!input1;
			user_to_keypad!input2;
			user_to_keypad!input3;
			user_to_keypad!input4;
				
			printf("The user entered: %d-%d-%d-%d.\n",input1,input2,input3,input4);
	
	fi;

	input1 = 8;	
	input2 = 8;
	input3 = 8;
	input4 = 8;
	
	if

		:: keypad_to_user?keypad_ready ->

			user_to_keypad!input1;
			user_to_keypad!input2;
			user_to_keypad!input3;
			user_to_keypad!input4;
				
			printf("The user entered: %d-%d-%d-%d.\n",input1,input2,input3,input4);
	
	fi;

	input1 = 9;	
	input2 = 9;
	input3 = 9;
	input4 = 9;
	
	if

		:: keypad_to_user?keypad_ready ->

			user_to_keypad!input1;
			user_to_keypad!input2;
			user_to_keypad!input3;
			user_to_keypad!input4;
				
			printf("The user entered: %d-%d-%d-%d.\n",input1,input2,input3,input4);
	
	fi;

	test_sequencer!case9;

}

proctype test_case9() {

	test_sequencer?case9;

	/* Eigth test case: Keypad lost connection to server. */
	printf("Running 9th test case: Keypad lost connection to server.\n");

	kill_server = true;

	test_sequencer!keypad_done;
	test_sequencer!server_done;

}