Modified repository structure

module ePassport_MainModule {

    import from ePassport_Values all;    

    import from ePassport_TestSystem all;    

    import from ePassport_Types all;

    import from ePassport_Messages all;

	import from ePassport_Pics all;	

	import from ePassport_Pixits all;

control {

   		 }

}

/*

 *	@author 	ETSI

 *  @version 	$URL: $

 *				$Id:  $

 *	@desc		This module contains message  definitions related to the test cases for testing ePassport devices.

 *			

 *

 */

 module ePassport_Messages {

	//LibCommon

	import from LibCommon_DataStrings all;

	import from LibCommon_TextStrings all;

	import from LibCommon_BasicTypesAndValues all;

	//Ats

	import from ePassport_Types all;

	import from ePassport_Values all;

	import from ePassport_TestSystem all;

	import from ePassport_Pixits all;

	const octetstring c_rnd_icc:='81d989f97303f9c6'O;

// The Test Adapter should have filled an array of hexstring with the content of the file

// The TTCN requests here datalength hexstring values of the file=filename, from pointer pt 

external function fx_findstring ( in charstring v_activefile, inout Oct2 v_offset, inout LengthE v_datalength  ) return octetstring;

external function fx_bacauth ( inout octetstring v_rnd_ifd, in octetstring c_rnd_icc, inout octetstring Kicc  ) return octetstring;

external function fx_activeauth ( inout octetstring v_rnd_ifd ) return octetstring;

external function fx_verify_Certificate( in octetstring v_psodata ) return boolean;

external function fx_verify_Signature( in octetstring v_signature ) return boolean;

//function for initializing the system and start the ePassport procedure

function f_start() runs on MRTD

{

// import certicate configuration from TA ext function

// get certificate to IS

	mgmt.send(m_start);

	alt{

			[] mgmt.receive(mw_getdata_mrz) 

					{

					mgmt.send(m_setdata_mrz);

					}

			[] mgmt.receive(mw_getdata_cert) 

					{

					mgmt.send(m_setdata_cert);

					}

			[] mgmt.receive

					{

					mgmt.send(m_setdata_cert);  // to change to ERROR

					}

		}

	alt{

			[] mgmt.receive(mw_getdata_mrz) 

					{

					mgmt.send(m_setdata_mrz);

					}

			[] mgmt.receive(mw_getdata_cert) 

					{

					mgmt.send(m_setdata_cert);

					}

			[] mgmt.receive

					{

					mgmt.send(m_setdata_cert);  // to change to ERROR

					}

		}

}

// Altstep definition 

altstep a_mgmt(in Oct2 p_failCode) runs on MRTD {

	[v_checkpoint] mgmt.receive(mw_report(p_failCode)) 

		{

		setverdict(pass);

		}

	[] mgmt.receive 

		{

		setverdict(fail);

		stop

		}

	[] t_guard.timeout 

		{

		setverdict(fail);

		stop

		}

}

// Generic function for reading an active

function f_waitRead(inout template EFfile p_file) runs on MRTD

{

		var EFfile v_file:=valueof(p_file);

		var Command v_command;

		var charstring v_activefile:= "000000";

		var Oct2 v_offset:='0000'O;

		var integer v_size:=0;

		var Response_Data v_data;

		var octetstring v_datalength;

		var Oct2 w1w2:='6400'O;    // must be initialized to right value !!!

	// we could do a while here instead of the ALT Repeat

		alt{

				[] mrtdport.receive(mw_selectByFileID(v_file.fileID)) -> value v_command 

					{

					v_activefile:=v_file.filename;

					mrtdport.send(m_responseOK);

					repeat;

					}

				[] mrtdport.receive(mw_readShortEF(v_file.shortFID)) -> value v_command 

					{

					v_offset:=bit2oct('00000000'B & v_command.p2);   // the offset must be 256 bytes max. it needs to be defined in the typing !!!

					v_datalength:=v_command.lengthE;

					v_activefile:=v_file.filename;	

					v_size:= oct2int(v_offset) + oct2int(v_datalength);

						if (v_size > v_file.filesize) 

						{ 	f_error(w1w2); }

						else

						{

						v_data := fx_findstring(v_activefile, v_offset, v_datalength);

						mrtdport.send(m_response_read(v_data));

						}

					if (v_size !=v_file.filesize) {repeat;}         // if repeat, it means the transfer is not complete

					}

				// Maybe this should be forbidden. requesting a read without specifying EF the first time !!!	

				[] mrtdport.receive(mw_readActiveEF) -> value v_command 

					{

					// if v_activefile== "000000", it means that no Select has been received first nor a Read with filename specified.

					// so we send an error message. 

					// maybe an option is forgotten here -> if the readActiveEF is received directly, requesting an already read file.

					//if v_activename is != than 00, it means that a Select or ReafFile has been already received.

					if (v_activefile =="000000") {f_error(w1w2);}

					else {

					v_offset:=bit2oct((v_command.p1) & (v_command.p2));  

					v_datalength:=v_command.lengthE;

					v_data := fx_findstring(v_activefile, v_offset, v_datalength);

					mrtdport.send(m_response_read(v_data));

				//	v_offset:= int2oct(oct2int(v_offset) + oct2int(v_datalength), 2);

					if (v_size !=v_file.filesize) {repeat;} // if repeat, it means the transfer is not complete

					}

					}

				[] mrtdport.receive {

					w1w2:='6400'O;  // execution error   -> to better defined

					f_error(w1w2);

					}

			}

}// end of function f_waitRead

//  function for checking the satus of the MRTD

function f_checkStatus () runs on MRTD return boolean

{

return true;

}// end of function f_checkStatus

// Generic function for sending error message

function f_error (inout Oct2 w1w2) runs on MRTD

{

	mrtdport.send(m_responseNOK(w1w2));

	setverdict (inconc);

	stop;

}// end of function f_error

// Start the MRTD Test sequence :  Standard Inspection Procedure (SIP)

function f_SIP (inout template ConfigurationSet p_cfg) runs on MRTD

{

		var ConfigurationSet v_cfg:=valueof(p_cfg);

		var boolean PassiveAuth:=false;

		var boolean ActiveAuth:=false;

		var boolean DG15:=true;   //AA optional should be defibed in a PIXIT

		var Command v_command;

		var Oct2 w1w2:='6982'O;

	f_wait_application();

	f_bac();

	f_waitRead(v_cfg.efcom);

	f_passiveAuth(v_cfg.efsod);

		PassiveAuth:=true;

		if (DG15) {

					f_waitRead(v_cfg.dg15);

					f_activeAuth(v_cfg.dg15);

				}

		f_waitRead(v_cfg.dg1);

		f_waitRead(v_cfg.dg2);

}	// end of function f_SIP

// First message to be received while reading the ePassport

function f_wait_application ()runs on MRTD

{

	var Command v_command;

	var Oct2 w1w2:='6902'O;

			alt

				{

				[] mrtdport.receive(mw_application) -> value v_command 

					{

					mrtdport.send(m_responseOK);

					}

				[] mrtdport.receive {

					f_error(w1w2);

					}

				}

}

// Start the MRTD Test sequence : Advanced Inspection Procedure (AIP) including EAC

function f_AIP (inout template ConfigurationSet p_cfg) runs on MRTD

{

		var ConfigurationSet v_cfg:=valueof(p_cfg);

		var boolean BAC:=false;

		var boolean SecureMessage:=false;

		var boolean PassiveAuth:=false;

		var boolean ActiveAuth:=false;

		var boolean DG15:=true;   //AA optional should be defibed in a PIXIT

		var Command v_command;

//		var Oct1 v_activeSFID:= '1e'O;

		var Oct2 w1w2:='6902'O;

	f_wait_application();

	f_bac();

	BAC:=true;

	SecureMessage:=true;	// it needs to inform the TA that the messages are now encrypted 

							//with Secure Messaging

	f_waitRead(v_cfg.efcom);

	f_waitRead(v_cfg.dg14);

	f_chipAuth(v_cfg.dg14);

	f_passiveAuth(v_cfg.efsod);

		if (DG15) {

					f_waitRead(v_cfg.dg15);

					f_activeAuth(v_cfg.dg15);

				}

	PassiveAuth:=true;

	f_waitRead(v_cfg.dg1);

	f_waitRead(v_cfg.dg2);

	f_waitRead(v_cfg.efcvca);

	f_terminalAuth(v_cfg.efcvca);

	f_waitRead(v_cfg.dg3);

	f_waitRead(v_cfg.dg4);

}	// end of function f_AIP

 // Function Basic Access Control Authentication 

function f_bac () runs on MRTD

{

		var boolean SecureMessage:=false;

		var Command v_command;

		var Response_Data v_data;

		var LengthE datalength:='00'O;

	//	var octetstring v_rnd_ifd;

		var octetstring v_ifd;

		var Oct16 Kicc:='000102030405060708090a0b0c0d0e0f'O;  // Keying material of MRTD

		var Oct2 w1w2:='0000'O;	

	alt 

		{

		//	The IFD requests a challenge RND.ICC by sending the GET CHALLENGE command. The ICC

 		//	generates and responds with a nonce RND.ICC.

		[] mrtdport.receive(mw_getchallenge) -> value v_command 

				{

					v_data := c_rnd_icc;						

					mrtdport.send(m_response_read(v_data));				// the MRTD sends its random challenge to IS

				}

		[] mrtdport.receive(mw_selectfile_EF_COM)  {

		//	v_activeSFID:='1e'O;

			w1w2:='6982'O;     			// security status not satisfied

			mrtdport.send(m_responseNOK(w1w2));   

			repeat;

			}

		[] mrtdport.receive(mw_readbinary_EF_COM)  {

		//	v_activeSFID:='1e'O;

			w1w2:='6982'O; 			 	// security status not satisfied

			mrtdport.send(m_responseNOK(w1w2));		

			repeat;

			}

		[] mrtdport.receive

			{

			f_error(w1w2);

			}

		}

		// If get_Challenge has been received, the MRTD is waiting now External Authenticate message.

		// The IFD performs the following operations:

		// a) Generate a nonce RND.IFD and keying material K.IFD.

		// b) Generate the concatenation S = RND.IFD || RND.ICC || K.IFD

		// c) Compute the cryptogram E_IFD = E[K_ENC](S).

		// d) Compute the checksum M_IFD = MAC[K_MAC](E_IFD).

		// e) Send a MUTUAL AUTHENTICATE command using the data E_IFD || M_IFD.

		alt

			{

			[] mrtdport.receive(mw_extauthenticate) -> value v_command  

			// the IS sends the encrypted challenge generated with its keying material

			// Kpcd and RND of IS and the rnd of the mrtd,then derived form Kenc and Kmac

				{

				v_ifd:=v_command.command_data;

		// The ICC performs the following operations:

		// a) Check the checksum M_IFD of the cryptogram E_IFD.

		// b) Decrypt the cryptogram E_IFD.

		// c) Extract RND.ICC from S and check if IFD returned the correct value.

		// d) Generate keying material K.ICC.

		// e) Generate the concatenation R = RND.ICC || RND.IFD || K.ICC

		// f) Compute the cryptogram E_ICC = E[K_ENC](R).

		// g) Compute the checksum M_ICC = MAC[K_MAC](E_ICC).

		// h) Send the response using the data E_ICC || M_ICC.

				v_data:= fx_bacauth(v_ifd, c_rnd_icc, Kicc);  	// the MRTD decrypts the encrypted challenge of IS, and send back its encrypted

				// calulating KSenc, KSmac and SSC used for Secure Message

		//		v_sm:=fx_SM(Kicc,v_ifd);   v_sm is here a record of 3 octetstring KSenc, KSmac and SSC

				mrtdport.send(m_response_read(v_data));				

				SecureMessage:=true;	// it needs to inform the TA that the messages are now encrypted 

										//with Secure Messaging							}

				}

			[] mrtdport.receive

				{

				f_error(w1w2);

				}

			}

			// The IFD performs the following operations:

			// a) Check the checksum M_ICC of the cryptogram E_ICC.

			// b) Decrypt the cryptogram E_ICC.

			// c) Extract RND.IFD from R and check if ICC returned the correct value.

}// end of function f_bac

// Passive Authentication triggered by reading of EF.SOD

function f_passiveAuth (inout template EFfile p_file) runs on MRTD

{

	var EFfile v_file:=valueof(p_file);

	f_waitRead(v_file);  // here a template of EF.SOD

}// end of function f_passiveAuth

// Active Authentication triggered by reading of DG15

function f_activeAuth (inout template EFfile p_file) runs on MRTD

{

		var EFfile v_file:=valueof(p_file);

		var Command v_command;

		var Oct2 w1w2:='6300'O

		var octetstring v_rnd_ifd;

		var Response_Data v_data;

	//	f_waitRead(v_file); // here a template of EF.DG15

		alt {

				[] mrtdport.receive(mw_intauthenticate) -> value v_command {

					v_rnd_ifd:=v_command.command_data;

					// see Supplement 9303 Annex B for a worked example of MRTD signature calculation

					v_data:= fx_activeauth (v_rnd_ifd);

					mrtdport.send(m_response_read(v_data));

					// here we could check if the IS sends a error message following the verification 

					// of MRTD signature.

					// if (no error message)=> setverdict(pass) meaning Active Authentication successful

					}

				[] mrtdport.receive {

					f_error(w1w2);

					}

			}

}// end of function f_activeAuth

// Chip Authentication triggered by reading of DG14

function f_chipAuth (inout template EFfile p_file) runs on MRTD

{

		var EFfile v_file:=valueof(p_file);

		var Command v_command;

		var octetstring v_keyreference;

		var Oct2 w1w2:='6300'O

// The MRTD chip sends its static Diffie-Hellman public key PKPICC, and the domain parameters

// DPICC to the inspection system. These infos are contained in DG14.

//	f_waitRead(v_file);  // here a template of EF.DG14

// The inspection system generates an ephemeral Diffie-Hellman key pair (^SKPCD;^PKPCD;DPICC),

// and sends the ephemeral public key^PKPCD to the MRTD chip, via the MSE:SetKAT message.

			alt {

				[] mrtdport.receive(mw_mse_SetKAT) -> value v_command {

					v_keyreference:=v_command.command_data;

					// Both the MRTD chip and the inspection system compute the following:

					// a) The shared secret K = KA(SKPICC;^PKPCD;DPICC) = KA(^SKPCD;PKPICC;DPICC)

					// b) The session keys KMAC and KEnc derived from K for Secure Messaging.

					// c) The hash of the inspection systems ephemeral public key H(^PKPCD) for Terminal Authentication.

					// fx_chipAuth();

					mrtdport.send(m_responseOK);

					// to be continue till end of Chip authentication ...

					}

				[] mrtdport.receive {

					f_error(w1w2);

					}

				}

	// In the EAc spec, the ChipAuth MUST be directly followed by PassiveAuth

	// However in the trace , the SM is checked by reading the EF.COM a seocnd time

	//	f_waitRead(m_EF_COM);  

	// or any read or command

	// the purpose is th verify the SM

	// mrtdport.receive (mw_readbinary or mw_select)

	//if SM is correct, then 	mrtdport.send(m_responseOK); else error				

}// end of function f_chipAuth

// Terminal Authentication triggered by reading of EF.CVCA

function f_terminalAuth (inout template EFfile p_file) runs on MRTD

{

		var EFfile v_file:=valueof(p_file);

		var Command v_command;

		var Response_Data v_data;

		var octetstring v_keyreference;

		var Oct2 w1w2:='6300'O

		var octetstring v_signature;

//	f_waitRead(v_file);  // here a template of EF.CVCA

	// ?? to make a for or while in order to perform Certificate verification (steps MSE_SetDST + PSO)  for 

	// every CV certificate to be verified

	// reading of the certificate chain

	f_mse_SetDST();   // here we need to use a template for CVCA link certificate

	f_mse_SetDST();	// here we need to use a template for DV certificate

	f_mse_SetDST(); // here we need to use a template for IS  certificate

	// The MRTD is waiting a MSE:SetAT message with a key reference

		alt {

				[] mrtdport.receive(mw_mse_SetAT) -> value v_command 

					{

					v_keyreference:=v_command.command_data;

					mrtdport.send(m_responseOK);

					}// end of mse_SetAT

					[] mrtdport.receive

						{

						f_error(w1w2);

						}

			} 

	// The MRTD is waiting a Get_Challenge message in order that the IS requests the RpIcc RND key

		alt {

				[] mrtdport.receive(mw_getchallenge) -> value v_command 

					{

					v_data := c_rnd_icc; // need to anwser the right data RpIcc

					mrtdport.send(m_response_read(v_data));

					}

				[] mrtdport.receive

					{

					f_error(w1w2);

					}

			} //end of get_challenge

	// The MRTD is waiting an External Authenticate message including the signature of the IS

		alt

			{

				[] mrtdport.receive(mw_extauthenticate) -> value v_command 

					{ 

						// External Authenticate in the data field , the signature generated by the IS		

						// if the signature generated by the IS is valid then the Authentication is successfull

						// the correct Certificate must be passed as parameter in the external function

						// in order to verify signature. 

								if (fx_verify_Signature(v_command.command_data))

									{mrtdport.send(m_responseOK);}  

								else {f_error(w1w2);}

					}

				[] mrtdport.receive

					{

					f_error(w1w2);

					}

			} // end if ext_authenticate

} // end of function f_terminalAuth

// Perform Security Operation : Verify Certificate. Part of the Terminal Authentication

// see TR-03110 EAC spec B.2.2

function f_mse_SetDST() runs on MRTD

	{

		var Command v_command;

		var octetstring v_keyreference;

		var Oct2 w1w2:='6300'O

// The MRTD is waiting for a MSE:SetDST message including the IS key reference

			alt	

				{

				[] mrtdport.receive(mw_mse_SetDST) -> value v_command 

					{

					v_keyreference:=v_command.command_data;

					mrtdport.send(m_responseOK);

					}

				[] mrtdport.receive 

					{

					f_error(w1w2);

					}

				}

// The MRTD is waiting for a PSO:Verify Certificate

			alt {

				[] mrtdport.receive(mw_pso_VerifyCertificate) -> value v_command 

					{

					// if the Certificate Body and the Signature are OK then the certificate was successfully validated

					// and the public key has been imported

					// see TR-03110 EAC spec B.2.2

					 // the correct Certificate must be passed as parameter in the external function

					// in order to verify IS and DV and link CAVA certificates. 

						if (fx_verify_Certificate(v_command.command_data))

				 			{mrtdport.send(m_responseOK);}

						else {f_error(w1w2);}

							}

				[] mrtdport.receive {

					f_error(w1w2);

					}

				}

	} // end of function f_mse_SetDST

// end of module 

}

/**

 *	@author 	

 *  @version 	$URL: $

 *				$Id:  $

 *	@desc		This module contains PICS parameters related to the test cases for testing ePassport devices.

 *

 */

module ePassport_Pics {

	//LibCommon

	import from LibCommon_DataStrings all;

	import from LibCommon_TextStrings all;

	import from LibCommon_BasicTypesAndValues all;

	//Ats

	import from ePassport_Types all;

	import from ePassport_Values all;

group CommonPics {

	/**

	* @remark 	Reference: TODO Spec + Clause ref

	* @desc 	What is the the type of the IUT?

	*/

	modulepar { IutType PIC_IUT := e_IS }

} // end group CommonPics

}

/**

 *	@author 	

 *  @version 	$URL: $

 *				$Id:  $

 *	@desc		This module contains PIXIT parameters related to the test cases for testing ePassport devices

 *				When Testing a ePassport Reader device (Inspection System), the operator shall complete the PICS/PIXIT parameters contained in:

 *				- the Common_parameters group

 *		

 *  

 */

module ePassport_Pixits {

	//LibCommon

	import from LibCommon_DataStrings all;

	import from LibCommon_TextStrings all;

	import from LibCommon_BasicTypesAndValues all;

	//Ats

//	import from ePassport_Types all;

//	import from ePassport_Values all;

	/** 

	@desc 	Definition of Pixits which apply to all ePassport devices

	*/

	group commonPixits {

		/** 

		@desc 	PIXITs related to timers

		*/

		group commonTimerPixits {

			/** 

			@desc 	Precision of timers in percentage (default is 5 percent).

			*/

			modulepar { float PXT_TIMER_PRECISION := 5.0 }

			/** 

			@desc	Guard timer to control a reaction from the IUT to a stimulus sent by the tester (e.g. a message).

					On expiry of this timer, the IUT is considered not to be be able to send the expected response.

			*/

			modulepar {float PXT_TAC := 2.0}

			/** 

			@desc	Guard timer to control a non-reaction from the IUT to a stimulus sent by the tester (e.g. a message).

					On expiry of this timer, it is considered that, as it is expected in the test purpose,

					the IUT has not responded to the stimulus.

			*/

			modulepar {float PXT_TNOAC := 5.0}

			/** 

			@desc	Wait for an implicit send. This guard timer is used to limitated the time where the tester is waiting

		 		for the response of the IUT that is triggered by an action from the test operator.

				On expiry of this timer, it is considered that the action has not succeeded, and thus the test case will be terminated

				with the verdict inconclusive.

			*/

			modulepar {float PXT_TWAIT := 60.0}

			/** 

			@desc	This guard timer is used to control the timeout of a test case.

			 		If , e.g. an external function does not return, then this timer will fire after PXT_TGUARD seconds.

					On expiry of this timer, it is considered that the test case did not finish within the given test cae life time,

					and will therefore be terminated.

			*/

			modulepar {float PXT_TGUARD := 300.0}

		}//end commonTimerPixits

	}//end commonPixits