Commit ede99478 authored by berge's avatar berge
Browse files

Transformed many functions into altsteps (ongoing).

Modified testcases (many TODOs)
parent 4a4eaf69
Loading
Loading
Loading
Loading
+340 −203
Original line number Diff line number Diff line
@@ -15,6 +15,7 @@
	//Ats
	import from ePassport_TestSystem all;
	import from ePassport_Types all;
	import from ePassport_Values all;
	import from ePassport_Templates all;


@@ -38,9 +39,58 @@

	}
	
	group configurationFunctions {
	
		function f_cfUp() runs on MRTD {
			
			// map ports
			map(self:mgmt, system: system_mgmt);
			map(self:mrtdport, system: system_mrtdPort);
			
			// activate default
			activate(a_default);
		}	
	}

	group classFunctions {
		
		function f_getLogicalChannel(in Class p_class) 
		return integer {
			
			if(ischosen(p_class.first)) {
				return p_class.first.channelNumber;
			}
			else {
				return p_class.further.channelNumber;
			}
			
		} // end f_getLogicalChannel
		
	} // end classFunctions 

	group fileFunctions {
		
		function f_readFileData(
			in integer v_logicalChannel, 
			in integer v_offset, 
			in integer v_dataLength, 
			out octetstring v_data)
		return W1W2Status {
			
			return c_w1w2NormalProcessing;
			
		} //end f_readFileData
				
	} // end fileFunctions


	function f_initializeMRTD() runs on MRTD {
		
	} // end f_initializeMRTD


    //function for initializing the system and start the ePassport procedure
function f_start() runs on MRTD
    function f_initializeIS() runs on MRTD
    {
    // import certicate configuration from TA ext function
    // get certificate to IS
@@ -80,10 +130,22 @@ function f_start() runs on MRTD
    
    }

	group altsteps {

		group defaults {
    		altstep a_default() runs on MRTD {
    			[] t_guard.timeout {
    				log("**** a_default: Error: Lifetime of testcase has expired. Sopping TC now. ****");
            		setverdict(inconc);
            		stop
            	}
            	[] any timer.timeout {
            		log("**** a_default: Error: Unexpected timeout occured. ****");
            		setverdict(inconc);
            		stop
            	}        	
    		}


// Altstep definition 
            altstep a_mgmt(in Oct2 p_failCode) runs on MRTD {
            	
            	[v_checkpoint] mgmt.receive(mw_report(p_failCode)) 
@@ -95,186 +157,262 @@ altstep a_mgmt(in Oct2 p_failCode) runs on MRTD {
            		setverdict(fail);
            		stop
            		}
	[] t_guard.timeout 
		{
		setverdict(fail);
		stop
		}
            	
            }
		} // end defaults
		
		group inspectionProcedures {
			
			// Start the MRTD Test sequence :  Standard Inspection Procedure (SIP)
        	altstep a_standardInspectionProcedure (inout template ConfigurationSet p_cfg) runs on MRTD {
        	
        		var ConfigurationSet v_cfg:=valueof(p_cfg);
        		var boolean DG15:=true;   //AA optional should be defibed in a PIXIT
        
// Generic function for reading an active
function f_waitRead(inout template EFfile p_file) runs on MRTD
{
        		[] a_waitApplication();
        		
		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 PlainTextResponseData v_data;
		var LengthE v_datalength;
		var Oct2 w1w2:='6400'O;    // must be initialized to right value !!!
        		[] a_bac();
        		
        		[] a_waitRead(v_cfg.efcom);
        		
        		[] a_passiveAuthentication(v_cfg.efsod);
        		
	// we could do a while here instead of the ALT Repeat
        		[DG15] a_waitRead(v_cfg.dg15);
        		
		alt{
				[] mrtdport.receive(mw_selectByFileID(v_file.fileID)) -> value v_command 
					{
        		[DG15] a_activeAuthentication();
        	
					v_activefile:=v_file.filename;
					mrtdport.send(m_responseOK);
					repeat;
					}
        		[] a_waitRead(v_cfg.dg1);
        		
        		[] a_waitRead(v_cfg.dg2);
            	
				[] 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 !!!
            } // end a_standardInspectionProcedure
            
					v_datalength:=v_command.payload.plainText.lengthE;
            // Start the MRTD Test sequence : Advanced Inspection Procedure (AIP) including EAC
            altstep a_advancedInspectionProcedure() runs on MRTD {
            	
					v_activefile:=v_file.filename;	
					v_size:= oct2int(v_offset) + v_datalength;
            	[] a_waitApplication();
        		
        		[] a_bac();
        		
        		// TODO
            	
						if (v_size > v_file.filesize) 
						{ 	f_error(w1w2); }
						else
						{
						v_data := fx_findstring(v_activefile, v_offset, v_datalength);
            } // end a_standardInspectionProcedure
        			
						mrtdport.send(m_response_read(v_data));
		} // end inspectionProcedures        
		
		group authenticationProcedures {
			
			altstep a_passiveAuthentication (inout template EFfile p_file) runs on MRTD {
		
        		var EFfile v_file:=valueof(p_file);
        
        		[] a_waitRead(v_file)  { // here a template of EF.SOD
        		}
        	}
					if (v_size !=v_file.filesize) {repeat;}         // if repeat, it means the transfer is not complete
        	
        	altstep a_activeAuthentication (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 PlainTextResponseData v_data;
        
        	//	f_waitRead(v_file); // here a template of EF.DG15
        
        				[] mrtdport.receive(mw_intauthenticate) -> value v_command {
        					v_rnd_ifd:=v_command.payload.plainText.commandData;
        					
        					// 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);
        					}		
        	}
        			
				// Maybe this should be forbidden. requesting a read without specifying EF the first time !!!	
				[] mrtdport.receive(mw_readActiveEF) -> value v_command 
					{
		} // end authenticationProcedures

					// 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.
		group commandProcessing {
			
					if (v_activefile =="000000") {f_error(w1w2);}
					else {
			// First message to be received while reading the ePassport
            altstep a_waitApplication () runs on MRTD {
        
					v_offset:=bit2oct((v_command.p1) & (v_command.p2));  
        		[] mrtdport.receive(mw_application) {
        			mrtdport.send(m_responseOK);
        		}
        		
					v_datalength:=v_command.payload.plainText.lengthE;
        	} //end a_waitApplication
        			
					v_data := fx_findstring(v_activefile, v_offset, v_datalength);
        	altstep a_bac() runs on MRTD {
    	
					mrtdport.send(m_response_read(v_data));
            	var PlainTextResponseData v_data;
            	var octetstring v_ifd;
            	var Command v_command;
            	var Oct16 v_kicc:='000102030405060708090a0b0c0d0e0f'O;  // Keying material of MRTD
            	
				//	v_offset:= int2oct(oct2int(v_offset) + oct2int(v_datalength), 2);
            	[] mrtdport.receive(mw_getchallenge) {
            		v_data := c_rnd_icc;						
        			mrtdport.send(m_response_read(v_data));				// the MRTD sends its random challenge to IS
            	}
            	
					if (v_size !=v_file.filesize) {repeat;} // if repeat, it means the transfer is not complete
            	[] mrtdport.receive(mw_selectfile_EF_COM)  {
        			mrtdport.send(m_responseNOK(c_w1w2SecurityStatusNotSatisfied));   
        			repeat;
        			}
        								
        		[] mrtdport.receive(mw_readbinary_EF_COM)  {
        			mrtdport.send(m_responseNOK(c_w1w2SecurityStatusNotSatisfied));		
        			repeat;
        			}
        
        		[] 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
        				
				[] mrtdport.receive {
					w1w2:='6400'O;  // execution error   -> to better defined
					f_error(w1w2);
        			v_ifd := v_command.payload.plainText.commandData;
        				
            		// 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, v_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));				
        		}
        			
        		// FIXME
        		[] mrtdport.receive{
        			f_error(c_w1w2SecurityStatusNotSatisfied);
        		}
            } // end a_bac
                	
			
}// end of function f_waitRead
			altstep a_waitRead(inout template EFfile p_file) runs on MRTD {
		
        		var EFfile v_file := valueof(p_file);
        		var Command v_command;
        		var integer v_logicalChannel;
        		var octetstring v_data := ''O;
        		var integer v_dataLength;
        		var integer v_offset;
        		var W1W2Status v_result;
        		
        		// SELECT Command
            	[] mrtdport.receive(mw_selectByFileID(v_file.fileID)) -> value v_command {
            		
            		// set current file for logical channel
            		v_logicalChannel := f_getLogicalChannel(v_command.class);
            		vc_simu.currentFiles[v_logicalChannel] := v_file.filename;
            		
            		// TODO: reset offset ?
            		// TODO: re-check security ?
            				
//  function for checking the satus of the MRTD
function f_checkStatus () runs on MRTD return boolean
{
return true;
}// end of function f_checkStatus
            		mrtdport.send(m_responseOK);
            		repeat;
            	}
            		
            	// READ Command with short EF
        		[] mrtdport.receive(mw_readShortEF(v_file.shortFID)) -> value v_command {
        
        			// set current file for logical channel
            		v_logicalChannel := f_getLogicalChannel(v_command.class);
            		vc_simu.currentFiles[v_logicalChannel] := v_file.filename;
            					
        			v_offset := bit2int(v_command.p2);
        			v_dataLength := v_command.payload.plainText.lengthE;
          		
// Generic function for sending error message
function f_error (inout Oct2 w1w2) runs on MRTD
{
	mrtdport.send(m_responseNOK(w1w2));
	setverdict (inconc);
	stop;
            		v_result := f_readFileData(v_logicalChannel, v_offset, v_dataLength, v_data);
            		mrtdport.send(m_responseRead(v_data, v_result));
        			
}// end of function f_error
        			//TODO: repeat only if transfer is incomplete
        			repeat;
        		}
        
        		// READ Command (using current EF)
        		[] mrtdport.receive(mw_readCurrentEF) -> value v_command {
        		
        			// Check current file
        			v_logicalChannel := f_getLogicalChannel(v_command.class);
        			if(vc_simu.currentFiles[v_logicalChannel] == "") {
        				log(""); //TODO
        				mrtdport.send(m_responseNOK(c_w1w2NoCurrentEF));
        				repeat;
        			}
        		
        			v_offset := bit2int(v_command.p1 & v_command.p2);
        			
// Start the MRTD Test sequence :  Standard Inspection Procedure (SIP)
function f_SIP (inout template ConfigurationSet p_cfg) runs on MRTD
{
        			v_result := f_readFileData(v_logicalChannel, v_offset, v_dataLength, v_data);
            		mrtdport.send(m_responseRead(v_data, v_result));
        			 
		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
        			//TODO: repeat only if transfer is incomplete
        			repeat;			
        		}
        				
		var Command v_command;
		var Oct2 w1w2:='6982'O;
        		// TODO: receive statements for B1					
        				
	f_wait_application();
        	} // end of a_waitRead
    			
	f_bac();
		} // end commandProcessing

	f_waitRead(v_cfg.efcom);
	} // end altsteps

	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);
	group toBeRemoved {
		
        // Generic function for reading an active
        function f_waitRead(inout template EFfile p_file) runs on MRTD {
        	alt {
        		[] a_waitRead {
        			
}	// end of function f_SIP
        		}
        	}
        }
	} // end toBeRemoved
    


// 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

//  function for checking the satus of the MRTD
function f_checkStatus () runs on MRTD return boolean
{
				[] mrtdport.receive(mw_application) -> value v_command 
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_responseOK);
					}
	mrtdport.send(m_responseNOK(w1w2));
	setverdict (inconc);
	stop;

}// end of function f_error




				[] mrtdport.receive {
					f_error(w1w2);
					}
				}
	

}


	
@@ -297,7 +435,7 @@ function f_AIP (inout template ConfigurationSet p_cfg) runs on MRTD



	f_wait_application();
	a_waitApplication();
		
	f_bac();
	BAC:=true;
@@ -333,7 +471,6 @@ function f_AIP (inout template ConfigurationSet p_cfg) runs on MRTD


    

 // Function Basic Access Control Authentication 
function f_bac () runs on MRTD
{
+17 −3
Original line number Diff line number Diff line
@@ -82,7 +82,7 @@ module ePassport_Templates {
	// TEMPLATES m_start
    template (value) Response m_setdata_mrz := {
       	responseData := m_responseData(char2oct(PXT_MRZ)),   // to be change later by providing real data !!!
    	w1w2 := c_normalProcessing
    	w1w2 := c_w1w2NormalProcessing
    }

	// TEMPLATES mw_report
@@ -398,6 +398,14 @@ module ePassport_Templates {
            payload := mw_payload(omit, ?)
        }
        
        template Command mw_readCurrentEF := {
            class := mw_class_00,
            ins := e_readBinary, //'b0'O,
            p1 := '0???????'B,
            p2 := ?,
            payload := mw_payload(omit, ?)
        }

		template Command mw_readbinary_EF_COM := {  //00 b0 9e 00 06  
	    	class := mw_class_00,
			ins := e_readBinary, //'b0'O,
@@ -469,7 +477,7 @@ module ePassport_Templates {
		// Response OK
    	template (value) Response m_responseOK := {
    		responseData := omit,
    		w1w2 := c_normalProcessing
    		w1w2 := c_w1w2NormalProcessing
    	}
    
    	// Response Data Template
@@ -481,7 +489,13 @@ module ePassport_Templates {
		// Response Data Template
    	template (value) Response m_response_read(template (omit) PlainTextResponseData v_data) := {
    		responseData := {plainText := v_data},
    		w1w2 := c_normalProcessing
    		w1w2 := c_w1w2NormalProcessing
    	}
    	
    			// Response Data Template
    	template (value) Response m_responseRead(template (omit) PlainTextResponseData p_data, W1W2Status p_w1w2) := {
    		responseData := {plainText := p_data},
    		w1w2 := p_w1w2
    	}

		// Response Data Template
+424 −534

File changed.

Preview size limit exceeded, changes collapsed.

+5 −0
Original line number Diff line number Diff line
@@ -30,6 +30,11 @@ module ePassport_Types {
    		integer filesize	
    	};
        
        type enumerated MrtdConfiguration {
        	e_cfgDfltBac,
        	e_cfgDfltEac	
        }
        
        
        type record ConfigurationSet {
                
+23 −2
Original line number Diff line number Diff line
@@ -9,11 +9,32 @@
 
module ePassport_Values {

	//LibCommon
	import from LibCommon_DataStrings all;

	// ATS
	import from ePassport_Types all;	

	group w1w2_constants {
		const W1W2Status c_normalProcessing := '9000'O;
		const W1W2Status c_w1w2NormalProcessing := '9000'O;
		const W1W2Status c_w1w2SecurityStatusNotSatisfied := '6982'O;
		const W1W2Status c_w1w2NoCurrentEF := '6986'O;
			
	}	
	} // end w1w2_constants
	
	group automaticInterfaceSpecification {
		
		group failureCodes {
		
			const Oct2 c_aisNoFailure := '0000'O;
			const Oct2 c_aisTerminalAuthenticationFailure := '0800'O;
			const Oct2 c_aisFailureInEFSOD := '1100'O;
			const Oct2 c_aisFailureInDG3 := '1400'O;
			const Oct2 c_aisFailureInDG14 := '1f00'O;
			
			//TODO add more	
			
		} // end failureCodes
		
	} // end automaticInterfaceSpecification
} 
 No newline at end of file