Commit 08ee7598 authored by berge's avatar berge
Browse files

Cleaned templates

parent 1cf03153
Loading
Loading
Loading
Loading
+16 −29
Original line number Diff line number Diff line
@@ -70,19 +70,6 @@
        	}        	
		}

        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
        		}
        	
        }
	} // end defaults
	
	group inspectionProcedures {
@@ -123,10 +110,10 @@
    		var octetstring v_rndIfd;
    		var octetstring v_response;
    
			[] mrtdport.receive(mw_intauthenticate) -> value v_command {
			[] mrtdport.receive(mw_intAuthenticate) -> value v_command {
   				v_rndIfd := v_command.payload.plainText.commandData;
				v_response := f_activeAuthentication(v_rndIfd);
				mrtdport.send(m_response_read(v_response));
				mrtdport.send(m_responseRead(v_response));
			}
    	} // end a_activeAuthentication
    	
@@ -136,7 +123,7 @@
    		var Command v_command;
    		var octetstring v_publicKeyPcd;

			[] mrtdport.receive(mw_mse_setKAT) -> value v_command {
			[] mrtdport.receive(mw_mseSetKAT) -> value v_command {
				v_publicKeyPcd := v_command.payload.plainText.commandData;
				f_chipAuthentication(v_publicKeyPcd);
				mrtdport.send(m_responseOK);
@@ -153,7 +140,7 @@
    		var octetstring v_certificate, v_signature;

           	// reading of the certificate chain
			[] mrtdport.receive(mw_mse_setDST) -> value v_command {
			[] mrtdport.receive(mw_mseSetDST) -> value v_command {
				v_dstCAR := v_command.payload.plainText.commandData;
				// TODO: check CAR exists
				
@@ -162,7 +149,7 @@
			}

			// The MRTD is waiting for a PSO:Verify Certificate
			[] mrtdport.receive(mw_pso_verifyCertificate) -> value v_command {
			[] mrtdport.receive(mw_psoVerifyCertificate) -> 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
@@ -183,7 +170,7 @@
			}

			// The MRTD is waiting a MSE:SetAT message with a key reference
			[] mrtdport.receive(mw_mse_setAT) -> value v_command {
			[] mrtdport.receive(mw_mseSetAT) -> value v_command {
				v_atCAR := v_command.payload.plainText.commandData;
				mrtdport.send(m_responseOK);
			}
@@ -191,7 +178,7 @@
			// The MRTD is waiting a Get_Challenge message in order that the IS requests the RpIcc RND key
			[] mrtdport.receive(mw_getChallenge) -> value v_command {
				v_rndIcc := f_generateRandomOctetstring(c_atNonceSize); 
				mrtdport.send(m_response_read(v_rndIcc));		
				mrtdport.send(m_responseRead(v_rndIcc));		
			}

			// The MRTD is waiting an External Authenticate message including the signature of the IS
@@ -216,7 +203,7 @@
		// First message to be received while reading the ePassport
        altstep a_waitApplication () runs on MRTD {
    
    		[] mrtdport.receive(mw_application) {
    		[] mrtdport.receive(mw_selectApplication) {
    			mrtdport.send(m_responseOK);
    				vc_simu.securityStatus := e_noSecurity;
    		}
@@ -237,14 +224,14 @@
        	[] mrtdport.receive(mw_getChallenge) {            		
        		// MRTD sends its random challenge to IS
        		v_rndIcc := f_generateRandomOctetstring(c_bacNonceSize);
    			mrtdport.send(m_response_read(v_rndIcc));				
    			mrtdport.send(m_responseRead(v_rndIcc));				
        	}
        	
    		[] mrtdport.receive(mw_extAuthenticate) -> value v_command {        				
    			v_challengeResponse := v_command.payload.plainText.commandData;
        		
        		v_response := f_basicAccessControl(v_rndIcc, v_challengeResponse);
        		mrtdport.send(m_response_read(v_response));
        		mrtdport.send(m_responseRead(v_response));
        		vc_simu.securityStatus := e_basicAccessControl;
    		}
    			
@@ -263,7 +250,7 @@
    		var W1W2Status v_result;
    		
    		// SELECT Command
        	[] mrtdport.receive(mw_selectByFileID(p_file.longFileId)) -> value v_command {
        	[] mrtdport.receive(mw_selectByFileId(p_file.longFileId)) -> value v_command {
        		
        		// set current file for logical channel
        		v_logicalChannel := f_getLogicalChannel(v_command.class);
@@ -287,7 +274,7 @@
      		
        		v_result := f_readFileData(vc_simu.currentFiles[v_logicalChannel], 
        			v_offset, v_dataLength, v_data);
        		mrtdport.send(m_responseRead(v_data, v_result));
        		mrtdport.send(m_responseReadWithStatus(v_data, v_result));

    			repeat;
    		}
@@ -307,7 +294,7 @@
    			
    			v_result := f_readFileData(vc_simu.currentFiles[v_logicalChannel],
    			 	v_offset, v_dataLength, v_data);
        		mrtdport.send(m_responseRead(v_data, v_result));
        		mrtdport.send(m_responseReadWithStatus(v_data, v_result));
    			 
    			repeat;			
    		}
@@ -354,7 +341,7 @@
      		
        		v_result := f_readFileData(vc_simu.currentFiles[v_logicalChannel], 
        			v_offset, v_dataLength, v_data);
        		mrtdport.send(m_responseRead(v_data, v_result));
        		mrtdport.send(m_responseReadWithStatus(v_data, v_result));
    			
    			repeat;
    		}
@@ -374,7 +361,7 @@
    			
    			v_result := f_readFileData(vc_simu.currentFiles[v_logicalChannel], 
    				v_offset, v_dataLength, v_data);
        		mrtdport.send(m_responseRead(v_data, v_result));
        		mrtdport.send(m_responseReadWithStatus(v_data, v_result));
    			 
    			repeat;			
    		}
@@ -386,7 +373,7 @@
		altstep a_refuseFileAccess(in FileInfo p_file) runs on MRTD {
		
			// SELECT Command
        	[] mrtdport.receive(mw_selectByFileID(p_file.longFileId)) {
        	[] mrtdport.receive(mw_selectByFileId(p_file.longFileId)) {
        		mrtdport.send(m_responseNOK(c_w1w2SecurityStatusNotSatisfied));
        		repeat;
        	}
+125 −164
Original line number Diff line number Diff line
@@ -16,6 +16,8 @@ module ePassport_Templates {
	import from ePassport_Values all;
	import from ePassport_Pixits all;	

	group automaticTestInterface {
		
    	// fake variable need to be declared later with the test mode
        // The type is WRONG, copied from the EFfile type
        // It may contain the certificate for the IS 
@@ -25,31 +27,6 @@ module ePassport_Templates {
    		w1w2 := '9999'O // ???
    	}	
    	
	template Payload mw_payload(
		template CommandData p_commandData, 
		template LengthE p_lengthE) := {
		plainText := {
	 		commandData := p_commandData,
        	lengthE := p_lengthE
		}
	}

	template Class mw_class_00 := {
		first := {
			chaining := e_lastOrOnlyCommand,
            sm := e_noSM,
            channelNumber := 0
		}
	}

	template Class mw_class_01 := {
		first := {
			chaining := e_lastOrOnlyCommand,
            sm := e_noSM,
            channelNumber := 1
		}
	}
	
    	// TEMPLATES m_get_data_certificate see Automatic Interface Proposal
    	template Command mw_getdata_cert := {
    		class := mw_class_01,		
@@ -59,12 +36,6 @@ module ePassport_Templates {
    		payload := mw_payload(omit, 0)
    	}    	
    	
	// TEMPLATES m_setdata_cert
	template (value) Response m_setdata_cert := {   // to be change later by defining a real function to provide certificate to the IS !!!
        responseData := omit,
        w1w2 := '9999'O // ???
	}

    	// TEMPLATES m_get_data_MRZ
        template Command mw_getdata_mrz := {
            class := mw_class_01,		
@@ -74,9 +45,10 @@ module ePassport_Templates {
            payload := mw_payload(omit, 0)
    	}
    	
	template (value) ResponseData m_responseData(
		template (value) PlainTextResponseData p_responseData) := {
		plainText := p_responseData	
    	// TEMPLATES m_setdata_cert
    	template (value) Response m_setdata_cert := {   // to be change later by defining a real function to provide certificate to the IS !!!
            responseData := omit,
            w1w2 := '9999'O // ???
    	}
    	
    	// TEMPLATES m_start
@@ -85,6 +57,51 @@ module ePassport_Templates {
        	w1w2 := c_w1w2NormalProcessing
        }
        
        template (value) ResponseData m_responseData(
			template (value) PlainTextResponseData p_responseData) := {
			plainText := p_responseData	
		}
        
	} // end automaticTestInterface

    

	template Payload mw_payload(
		template CommandData p_commandData, 
		template LengthE p_lengthE) := {
		plainText := {
	 		commandData := p_commandData,
        	lengthE := p_lengthE
		}
	}

	template Class mw_class(integer p_channelNumber) := {
		first := {
			chaining := e_lastOrOnlyCommand,
            sm := e_noSM,
            channelNumber := p_channelNumber
		}
	}


	template Class mw_class_00 := {
		first := {
			chaining := e_lastOrOnlyCommand,
            sm := e_noSM,
            channelNumber := 0
		}
	}

	template Class mw_class_01 := {
		first := {
			chaining := e_lastOrOnlyCommand,
            sm := e_noSM,
            channelNumber := 1
		}
	}
	
	group managementTemplates {

    	// TEMPLATES mw_report
        template Command mw_report(template Oct2 v_failCode) := {
    	   	class := mw_class_01,	
@@ -93,32 +110,23 @@ module ePassport_Templates {
    	  	p2 := ?,		
    	  	payload := mw_payload(v_failCode, 0)
    	}
	} // end managementTemplates

    group Command_templates
    {
		//SELECT TEMPLATES : Send APDU to the passport 00 a4 04 0c 07 a0 00 00 02 47 10 01                      
        template Command mw_application := {
		    class := mw_class_00,
			ins := e_select, //'a4'O,
			p1 := '00000100'B,
			p2 := '00001100'B,
			payload := mw_payload('a0000002471001'O, omit)
         }

    group commandTemplates {
    	
		//SELECT TEMPLATES 00 a4 02 0c 02 01 1e                           
        template Command mw_selectfile := {
		//SELECT TEMPLATES : Send APDU to the passport 00 a4 04 0c 07 a0 00 00 02 47 10 01                      
        template Command mw_selectApplication := {
		    class := mw_class_00,
			ins := e_select, //'a4'O,
			p1 := ?,
			p2 := ?,
			payload := mw_payload(?, omit)
			ins := e_select, 
			p1 := '00000100'B, // FIXME
			p2 := '00001100'B, // FIXME
			payload := mw_payload('a0000002471001'O, omit) // FIXME
         }

		//SELECT TEMPLATES 00 a4 02 0c 02 01 1e                           
        template Command mw_selectByFileID (LongFileId v_fileID) := {
        template Command mw_selectByFileId (LongFileId v_fileID) := {
		    class := mw_class_00,
			ins := e_select, //'a4'O,
			ins := e_select, 
			p1 := '000000??'B,
			p2 := '000011??'B,
			payload := mw_payload(v_fileID, omit)
@@ -126,137 +134,96 @@ module ePassport_Templates {
        
        template Command mw_selectAnyFile := {
		    class := mw_class_00,
			ins := e_select, //'a4'O,
			p1 := '000000??'B,
			p2 := '000011??'B,
			payload := mw_payload(?, omit)
        }

		//SELECT TEMPLATES 00 a4 02 0c 02 01 1e                           
        template Command mw_selectByFileName:= {
		    class := mw_class_00,
			ins := e_select, //'a4'O,
			p1 := '00000100'B,
			p2 := '000011??'B,
			ins := e_select, 
			p1 := '000000??'B, // FIXME
			p2 := '000011??'B, // FIXME
			payload := mw_payload(?, omit)
        }

		//SELECT TEMPLATES 00 a4 02 0c 02 01 1e                                          
        template Command mw_selectfile_EF_COM:= {
		    class := mw_class_00,
			ins := e_select, //'a4'O,
			p1 := '00000100'B,
			p2 := '000011??'B,
			payload := mw_payload('011e'O, omit)
        }

        template Command mw_readbinary := {
  			class := mw_class_00,
  			ins := e_readBinary, //'b0'O,
  			p1 := ?,
  			p2 := ?,
  			payload := mw_payload(omit, ?)
         }

 		template Command mw_readActiveEF := {
  			class := mw_class_00,
  			ins := e_readBinary, //'b0'O,
  			p1 := '0???????'B,
  			p2 := ?,
  			payload := mw_payload(omit, ?)
         }

        template Command mw_readShortEF (ShortFileId p_shortFileId) := {
            class := mw_class_00,
            ins := e_readBinary, //'b0'O,
            p1 := (oct2bit(p_shortFileId) or4b '10000000'B),    // '100?????'B,
            ins := e_readBinary, 
            p1 := (oct2bit(p_shortFileId) or4b '10000000'B),    // '100?????'B,  // FIXME
            p2 := ?,
            payload := mw_payload(omit, ?)
        }
        
        template Command mw_readAnyShortEF := {
        	class := mw_class_00,
            ins := e_readBinary, //'b0'O,
            p1 := '100?????'B,
            ins := e_readBinary, 
            p1 := '100?????'B,  // FIXME
            p2 := ?,
            payload := mw_payload(omit, ?)	
        }
        
        template Command mw_readCurrentEF := {
            class := mw_class_00,
            ins := e_readBinary, //'b0'O,
            p1 := '0???????'B,
            ins := e_readBinary, 
            p1 := '0???????'B,  // FIXME
            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,
			p1 := '10011110'B,    // '100?????'B,
			p2 := '00000000'B,
			payload := mw_payload(omit, ?)
        }
 
		template Command mw_getChallenge := {
	      	class := mw_class_00,
		  	ins := e_getChallenge, //'84'O,
		  	p1 := '00000000'B,  //to change
		  	p2 := '00000000'B,  //to change
		  	payload := mw_payload(omit, ?) //8?
		  	ins := e_getChallenge, 
		  	p1 := '00000000'B,  // FIXME
		  	p2 := '00000000'B,  // FIXME
		  	payload := mw_payload(omit, ?) //8? // FIXME
        }

		template Command mw_extAuthenticate := {
	    	class := mw_class_00,
			ins := e_externalOrMutualAuthenticate, //'82'O,
			p1 := '00000000'B,  //to change
			p2 := '00000000'B,  //to change
			ins := e_externalOrMutualAuthenticate, 
			p1 := '00000000'B,  // FIXME
			p2 := '00000000'B,  // FIXME
			payload := mw_payload(?, ?)
        }
        
		template Command mw_mse_setDST:= {
		template Command mw_intAuthenticate := {   ////// to modify : wrong template
	      	class := mw_class_00,
		  	ins := e_manageSecurityEnvironment, //'22'O,
		  	p1 := '1??????1'B,  //to change
		  	p2 := '10110110'B,  //to change
		  	//p1p2:= '81b6 'O,  //meaning Set DST   b8 of P1 and P2=B6
		  	ins := e_externalOrMutualAuthenticate, // FIXME
			p1 := '00000000'B,  // FIXME
		  	p2 := '00000000'B,  // FIXME
		  	payload := mw_payload(?, ?)
        }

		template Command mw_mse_setKAT:= {
		template Command mw_mseSetDST := {
	      	class := mw_class_00,
		  	ins := e_manageSecurityEnvironment, //'22'O,
		  	p1 := '01000001'B,  //meaning Set DST defined by bit7 of P1 and P2=A6 means KAT
		  	p2 := '10100110'B,  //meaning Set DST defined by bit7 of P1 and P2=A6 means KAT
		  	ins := e_manageSecurityEnvironment, 
		  	p1 := '1??????1'B,  // FIXME
		  	p2 := '10110110'B,  // FIXME
		  	//p1p2:= '81b6 'O,  //meaning Set DST   b8 of P1 and P2=B6
		  	payload := mw_payload(?, ?)
        }

		template Command mw_intauthenticate:= {   ////// to modify : wrong template
		template Command mw_mseSetKAT := {
	      	class := mw_class_00,
		  	ins := e_externalOrMutualAuthenticate, //'82'O,
			p1 := '00000000'B,  //to change
		  	p2 := '00000000'B,  //to change
		  	ins := e_manageSecurityEnvironment, 
		  	// FIXME
		  	p1 := '01000001'B,  //meaning Set DST defined by bit7 of P1 and P2=A6 means KAT
		  	p2 := '10100110'B,  //meaning Set DST defined by bit7 of P1 and P2=A6 means KAT
		  	payload := mw_payload(?, ?)
        }

		template Command mw_mse_setAT:= {
		template Command mw_mseSetAT := {
	      	class := mw_class_00,
		  	ins := e_manageSecurityEnvironment, //'22'O,
		  	p1 := '10000001'B,  // need to define correct P1 !!!!
		  	p2 := '10100100'B,  //need to define correct P2 !!!
		  	ins := e_manageSecurityEnvironment, 
		  	p1 := '10000001'B,  // FIXME
		  	p2 := '10100100'B, // FIXME
		  	payload := mw_payload(?, ?)
        }

		template Command mw_pso_verifyCertificate:= {
		template Command mw_psoVerifyCertificate := {
	      	class := mw_class_00,
		  	ins := e_performSecurityOperation, //'2a'O,
		  	p1 := '00000000'B,  //need to define correct P1 !!!
		  	p2 := '10111110'B,   //need to define correct P2 !!!
		  	ins := e_performSecurityOperation, 
		  	p1 := '00000000'B,  // FIXME
		  	p2 := '10111110'B,  // FIXME
		  	payload := mw_payload(?, ?)
        }
	}
	} // end commandTemplates

    group Response_templates {
    group responseTemplates {

		// Response OK
    	template (value) Response m_responseOK := {
@@ -264,29 +231,23 @@ module ePassport_Templates {
    		w1w2 := c_w1w2NormalProcessing
    	}
    
    	// Response Data Template
    	// Response NOK
    	template (value) Response m_responseNOK(W1W2Status v_w1w2) := {
    		responseData := omit,
    		w1w2 := v_w1w2
    	}

		// Response Data Template
    	template (value) Response m_response_read(template (omit) PlainTextResponseData v_data) := {
    	template (value) Response m_responseRead(template (omit) PlainTextResponseData v_data) := {
    		responseData := {plainText := v_data},
    		w1w2 := c_w1w2NormalProcessing
    	}
    	
    	// Response Data Template
    	template (value) Response m_responseRead(template (omit) PlainTextResponseData p_data, W1W2Status p_w1w2) := {
    	template (value) Response m_responseReadWithStatus(template (omit) PlainTextResponseData p_data, W1W2Status p_w1w2) := {
    		responseData := {plainText := p_data},
    		w1w2 := p_w1w2
    	}

		// Response Data Template
    	template (value) Response m_response(ResponseData v_data, W1W2Status v_w1w2) := {
    		responseData := v_data,
    		w1w2 := v_w1w2
    	}
	}
	} // end responseTemplates
} // end ePassport_Templates