Commit 72c6aff7 authored by berge's avatar berge
Browse files

Many changes due to refactoring. Still unstable.

parent ede99478
Loading
Loading
Loading
Loading
+386 −452

File changed.

Preview size limit exceeded, changes collapsed.

+12 −6
Original line number Diff line number Diff line
@@ -10,13 +10,19 @@

module ePassport_MainModule {
    
    // ATS
    import from ePassport_Testcases all; 

	

    control {    
    
    	
    	
    	execute(TC_ISO7816_A02());  
    	execute(TC_ISO7816_D02());  
    	execute(TC_ISO7816_E06());   
    	execute(TC_ISO7816_E08());  
    	execute(TC_ISO7816_E11());  
    	execute(TC_ISO7816_E18());   
    	execute(TC_LDS_B25());   
    	execute(TC_LDS_D12());  
    	execute(TC_LDS_F04());    
    	execute(TC_LDS_H37());        	
    }
}
+60 −138
Original line number Diff line number Diff line
@@ -86,7 +86,7 @@ module ePassport_Templates {
    }

	// TEMPLATES mw_report
    template Command mw_report(Oct2 v_failCode) := {
    template Command mw_report(template Oct2 v_failCode) := {
	   	class := mw_class_01,	
	  	ins := e_putDataWithDataBytes, //'da'O,			
	  	p1 := '00001111'B,   	
@@ -97,173 +97,79 @@ module ePassport_Templates {
    group simpleFileTemplates {
    	
		// TEMPLATES EF.COM file
        template (value) EFfile m_file_EF_COM := {
        template (value) EFfile m_fileCOM := {
		    filename := "EF.COM",
			shortFID := '1e'O,
			fileID := '011e'O,
			filesize := PXT_SIZE_EFCOM
			fileID := '011e'O
		}

		// TEMPLATES EF.SOD file
        template (value) EFfile m_file_EF_SOD := {
        template (value) EFfile m_fileSOD := {
		    filename := "EF.SOD",
			shortFID := '1d'O,
			fileID := '011d'O,
			filesize := PXT_SIZE_EFSOD
			fileID := '011d'O
		}

		// TEMPLATES DG1 file
        template (value) EFfile m_file_DG1 := {
        template (value) EFfile m_fileDG1 := {
		    filename := "EF.DG1",
			shortFID := '01'O,
			fileID := '0101'O,
			filesize := PXT_SIZE_DG1
			fileID := '0101'O
		}

		// TEMPLATES DG2 file
        template (value) EFfile m_file_DG2 := {
        template (value) EFfile m_fileDG2 := {
		    filename := "EF.DG2",
			shortFID := '02'O,
			fileID := '0102'O,
			filesize := PXT_SIZE_DG2
			fileID := '0102'O
		}

		// TEMPLATES DG3 file
        template (value) EFfile m_file_DG3 := {
        template (value) EFfile m_fileDG3 := {
		    filename := "EF.DG3",
			shortFID := '03'O,
			fileID := '0103'O,
			filesize := PXT_SIZE_DG3
			fileID := '0103'O
		}

		// TEMPLATES DG4 file
        template (value) EFfile m_file_DG4 := {
        template (value) EFfile m_fileDG4 := {
		    filename := "EF.DG4",
			shortFID := '04'O,
			fileID := '0104'O,
			filesize := PXT_SIZE_DG4
			fileID := '0104'O
		}

		// TEMPLATES DG14 file
        template (value) EFfile m_file_DG14 := {
        template (value) EFfile m_fileDG14 := {
		    filename := "EF.DG14",
			shortFID := '0e'O,
			fileID := '010e'O,
			filesize := PXT_SIZE_DG14
			fileID := '010e'O
		 }

		// TEMPLATES DG15 file
        template (value) EFfile m_file_DG15 := {
        template (value) EFfile m_fileDG15 := {
		    filename := "EF.DG15",
			shortFID := '0f'O,
			fileID := '010f'O,
			filesize := PXT_SIZE_DG15
			fileID := '010f'O
		}


		// TEMPLATES EF.CVCA file
        template (value) EFfile m_file_EF_CVCA := {
        template (value) EFfile m_fileCVCA := {
		    filename := "EF.CVCA",
			shortFID := '1c'O,
			fileID := '011c'O,
			filesize := PXT_SIZE_EFCVCA
			fileID := '011c'O
		}
	}//group Simple_files_templates



    group Modified_files_templates
    {
		// TEMPLATES EF.SOD file modified according E_06
        template (value) EFfile m_file_EF_SOD_E06 := {
		    filename := "EF.CVCA.E06",
			shortFID := '1c'O,
			fileID := '011c'O,
			filesize := PXT_SIZE_EFSOD
		}

		// TEMPLATES EF.CVCA_E08 file
        template (value) EFfile m_file_EF_CVCA_E08 := {
		    filename := "EF.CVCA.E08",
			shortFID := '1c'O,
			fileID := '011c'O,
			filesize := PXT_SIZE_EFCVCA
		}

		// TEMPLATES EF.SOD_E08 file
        template (value) EFfile m_file_EF_SOD_E08 := {
		    filename := "EF.SOD.E08",
			shortFID := '1d'O,
			fileID := '011d'O,
			filesize := PXT_SIZE_EFSOD
		}

		// TEMPLATES DG1_LDS_B25 file
        template (value) EFfile m_file_DG1_LDS_B25 := {
		    filename := "EF.DG1.LDS_B25",
			shortFID := '01'O,
			fileID := '0101'O,
			filesize := PXT_SIZE_DG1
		}

		// TEMPLATES EF.SOD file
        template (value) EFfile m_file_EF_SOD_LDS_B25 := {
		    filename := "EF.SOD.LDS_B25",
			shortFID := '1d'O,
			fileID := '011d'O,
			filesize := PXT_SIZE_EFSOD
		}

		// TEMPLATES DG3_LDS_D12 file
        template (value) EFfile m_file_DG3_LDS_D12 := {
		    filename := "EF.DG3.LDS_D12",
			shortFID := '01'O,
			fileID := '0101'O,
			filesize := PXT_SIZE_DG3
		}

		// TEMPLATES EF.SOD file LDS_D12
        template (value) EFfile m_file_EF_SOD_LDS_D12 := {
		    filename := "EF.SOD.LDS_D12",
			shortFID := '1d'O,
			fileID := '011d'O,
			filesize := PXT_SIZE_EFSOD
		}

		// TEMPLATES DG3_LDS_F04 file
        template (value) EFfile m_file_DG14_LDS_F04 := {
		    filename := "EF.DG14.LDS_F04",
			shortFID := '01'O,
			fileID := '0101'O,
			filesize := PXT_SIZE_DG14
		}

		// TEMPLATES EF.SOD file LDS_F04
        template (value) EFfile m_file_EF_SOD_LDS_F04 := {
		    filename := "EF.SOD.LDS_F04",
			shortFID := '1d'O,
			fileID := '011d'O,
			filesize := PXT_SIZE_EFSOD
		}

		// TEMPLATES EF.SOD file LDS_H37
        template (value) EFfile m_file_EF_SOD_LDS_H37 := {
		    filename := "EF.SOD.LDS_H37",
			shortFID := '1d'O,
			fileID := '011d'O,
			filesize := PXT_SIZE_EFSOD
		}
	}


    group ConfigSet_templates {
    	
        // TEMPLATES Configuration set
        template (value) ConfigurationSet m_cfg_plain := {
            efcom := m_file_EF_COM,
    		efsod := m_file_EF_SOD,
    		dg1 := m_file_DG1,
    		dg2 := m_file_DG2,
            efcom := m_fileCOM,
    		efsod := m_fileSOD,
    		dg1 := m_fileDG1,
    		dg2 := m_fileDG2,
    		dg3 := omit,
    		dg4 :=omit,
    		dg14 :=omit,
@@ -276,10 +182,10 @@ module ePassport_Templates {
    	};
    
    	template (value) ConfigurationSet m_cfg_bac := {
            efcom := m_file_EF_COM,
    		efsod := m_file_EF_SOD,
    		dg1 := m_file_DG1,
    		dg2 := m_file_DG2,
            efcom := m_fileCOM,
    		efsod := m_fileSOD,
    		dg1 := m_fileDG1,
    		dg2 := m_fileDG2,
    		dg3 := omit,
    		dg4 := omit,
    		dg14 := omit,
@@ -292,13 +198,13 @@ module ePassport_Templates {
    	};
    
    	template (value) ConfigurationSet m_cfg_eac := {
            efcom := m_file_EF_COM,
    		efsod := m_file_EF_SOD,
    		dg1 := m_file_DG1,
    		dg2 := m_file_DG2,
    		dg3 := m_file_DG3,
    		dg4 := m_file_DG4,
    		dg14 := m_file_DG14,
            efcom := m_fileCOM,
    		efsod := m_fileSOD,
    		dg1 := m_fileDG1,
    		dg2 := m_fileDG2,
    		dg3 := m_fileDG3,
    		dg4 := m_fileDG4,
    		dg14 := m_fileDG14,
    		dg15 := omit,
    		efcvca := omit,
    		fileslist := "EF.COM,EF.SOD,DG1,DG2,DG3,DG4,DG14",
@@ -309,14 +215,14 @@ module ePassport_Templates {
    
    
    	template (value) ConfigurationSet m_cfg_eac_aa := {
            efcom := m_file_EF_COM,
    		efsod := m_file_EF_SOD,
    		dg1 := m_file_DG1,
    		dg2 := m_file_DG2,
    		dg3 := m_file_DG3,
    		dg4 := m_file_DG4,
    		dg14 := m_file_DG14,
    		dg15 := m_file_DG15,
            efcom := m_fileCOM,
    		efsod := m_fileSOD,
    		dg1 := m_fileDG1,
    		dg2 := m_fileDG2,
    		dg3 := m_fileDG3,
    		dg4 := m_fileDG4,
    		dg14 := m_fileDG14,
    		dg15 := m_fileDG15,
    		efcvca := omit,
    		fileslist := "EF.COM,EF.SOD,DG1,DG2,DG3,DG4,DG14,DG15",
     		docNumber := "C11T002JM4",
@@ -348,7 +254,7 @@ module ePassport_Templates {
        }

		//SELECT TEMPLATES 00 a4 02 0c 02 01 1e                           
        template Command mw_selectByFileID (Oct2 v_fileID) := {
        template Command mw_selectByFileID (LongFileId v_fileID) := {
		    class := mw_class_00,
			ins := e_select, //'a4'O,
			p1 := '000000??'B,
@@ -356,6 +262,14 @@ module ePassport_Templates {
			payload := mw_payload(v_fileID, omit)
        }
        
        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,
@@ -390,7 +304,7 @@ module ePassport_Templates {
  			payload := mw_payload(omit, ?)
         }

        template Command mw_readShortEF (Oct1 v_shortFID) := {
        template Command mw_readShortEF (ShortFileId v_shortFID) := {
            class := mw_class_00,
            ins := e_readBinary, //'b0'O,
            p1 := (oct2bit(v_shortFID) or4b '10000000'B),    // '100?????'B,
@@ -398,6 +312,14 @@ module ePassport_Templates {
            payload := mw_payload(omit, ?)
        }
        
        template Command mw_readAnyShortEF := {
        	class := mw_class_00,
            ins := e_readBinary, //'b0'O,
            p1 := '100?????'B,
            p2 := ?,
            payload := mw_payload(omit, ?)	
        }
        
        template Command mw_readCurrentEF := {
            class := mw_class_00,
            ins := e_readBinary, //'b0'O,
+6 −1
Original line number Diff line number Diff line
@@ -47,8 +47,13 @@ module ePassport_TestSystem {
	** @desc	Test Component Variables are defined here  
	*
	*/
	type record SimuParams {
	type LongFileId CurrentFile;
	type record of CurrentFile CurrentFiles;
	
	type record SimuParams {
		SecurityStatus securityStatus,
		PassportProtection passportProtection,
		CurrentFiles currentFiles
	}
/*
	type component TestAdapter {
+22 −38
Original line number Diff line number Diff line
@@ -32,12 +32,12 @@ module ePassport_Testcases {
        testcase TC_ISO7816_A02() runs on MRTD system MRTD_System {
        	
        	f_cfUp();
        	f_initializeMRTD(e_cfgDfltBac);
        	f_initializeMRTD("CFG.DFLT.BAC");
        	f_initializeIS();  
        	
        	t_wait.start;
        	alt {
        		[] a_standardInspectionProcedure;
        		[] a_standardInspectionProcedure();
        		
        		[] mgmt.receive(mw_report(c_aisNoFailure)) {
        			t_wait.stop;
@@ -70,12 +70,12 @@ module ePassport_Testcases {
        testcase TC_ISO7816_D02() runs on MRTD system MRTD_System {
        		
        	f_cfUp();
        	f_initializeMRTD(e_cfgDfltEac);
        	f_initializeMRTD("CFG.DFLT.EAC");
        	f_initializeIS();  
        	    	
        	t_wait.start;
        	alt {
        		[] a_advancedInspectionProcedure;
        		[] a_advancedInspectionProcedure();
        		
        		[] mgmt.receive(mw_report(c_aisNoFailure)) {
        			t_wait.stop;
@@ -108,14 +108,12 @@ module ePassport_Testcases {
        testcase TC_ISO7816_E06() runs on MRTD system MRTD_System {
    		
        	f_cfUp();
        	f_initializeMRTD(e_cfgDfltEac);
        	//TODO: Modify SOD; was: v_cfg.efsod:=valueof(m_file_EF_SOD_E06);
        	
        	f_initializeMRTD("CFG.EAC.ISO7816.E06");        	
        	f_initializeIS(); 
    
    		t_wait.start;
    		alt {
        		[] a_advancedInspectionProcedure;
        		[] a_advancedInspectionProcedure();
        		
        		[] mgmt.receive(mw_report(c_aisNoFailure)) {
        			t_wait.stop;
@@ -143,16 +141,12 @@ module ePassport_Testcases {
        testcase TC_ISO7816_E08() runs on MRTD system MRTD_System {
    
    	   	f_cfUp();
        	f_initializeMRTD(e_cfgDfltEac);
        	//TODO: Modify EF.CVCA + SOD; 
        	//	was: 	v_cfg.efcvca:=valueof(m_file_EF_CVCA_E08);
    		//			v_cfg.efsod:=valueof(m_file_EF_SOD_E08);
        	
        	f_initializeMRTD("CFG.EAC.ISO7816.E08");        	
        	f_initializeIS(); 
        		
        	t_wait.start;
        	alt {
        		[] a_advancedInspectionProcedure;
        		[] a_advancedInspectionProcedure();
        		
        		[] mgmt.receive(mw_report(c_aisTerminalAuthenticationFailure)) {
        			t_wait.stop;
@@ -185,7 +179,7 @@ module ePassport_Testcases {
        testcase TC_ISO7816_E11() runs on MRTD system MRTD_System {
    	
    	   	f_cfUp();
        	f_initializeMRTD(e_cfgDfltEac);
        	f_initializeMRTD("CFG.EAC.ISO7816.E11");
        	//TODO: Modify Document number; 
        	//	was: 	v_cfg.docNumber :="M11T002JM";
        	
@@ -193,7 +187,7 @@ module ePassport_Testcases {
    	
    		t_wait.start;
        	alt {
        		[] a_advancedInspectionProcedure;
        		[] a_advancedInspectionProcedure();
        		
        		[] mgmt.receive(mw_report(c_aisTerminalAuthenticationFailure)) {
        			t_wait.stop;
@@ -227,14 +221,14 @@ module ePassport_Testcases {
        testcase TC_ISO7816_E18() runs on MRTD system MRTD_System {
    
    	   	f_cfUp();
        	f_initializeMRTD(e_cfgDfltEac);
        	f_initializeMRTD("CFG.DFLT.EAC");
        	
        	//TODO: add a wrong certificate to the IS (IS_Cert_01);
        	f_initializeIS(); 
    	
    		t_wait.start;
        	alt {
        		[] a_advancedInspectionProcedure;
        		[] a_advancedInspectionProcedure();
        		
        		[] mgmt.receive(mw_report(c_aisTerminalAuthenticationFailure)) {
        			t_wait.stop;
@@ -272,17 +266,15 @@ module ePassport_Testcases {
        testcase TC_LDS_B25() runs on MRTD system MRTD_System {
    
        	f_cfUp();
        	f_initializeMRTD(e_cfgDfltEac);
        	//TODO: Modify DG1 and MRZ; 
        	//	was: 	v_cfg.dg1:=valueof(m_file_DG1_LDS_B25);
    		//			v_cfg.efsod:=valueof(m_file_EF_SOD_LDS_B25);
        	//			v_cfg.mrz:=PXT_MRZ_LDS_B25;
        	f_initializeMRTD("CFG.BAC.LDS.B25");
        	//TODO: ModifyMRZ; 
        	//	was:	v_cfg.mrz:=PXT_MRZ_LDS_B25;
        	
        	f_initializeIS();  
        	
        	t_wait.start;
        	alt {
        		[] a_advancedInspectionProcedure;
        		[] a_advancedInspectionProcedure();
        		
        		[] mgmt.receive(mw_report(c_aisNoFailure)) {
        			t_wait.stop;
@@ -315,16 +307,13 @@ module ePassport_Testcases {
        testcase TC_LDS_D12() runs on MRTD system MRTD_System {
        	
            f_cfUp();
        	f_initializeMRTD(e_cfgDfltEac);
        	//TODO: Modify DG3; 
        	//	was: 	v_cfg.dg3:=valueof(m_file_DG3_LDS_D12);
        	//			v_cfg.efsod:=valueof(m_file_EF_SOD_LDS_D12);
        	f_initializeMRTD("CFG.EAC.LDS.D12");
        	
        	f_initializeIS(); 
    
    		t_wait.start;
    		alt {
        		[] a_advancedInspectionProcedure;
        		[] a_advancedInspectionProcedure();
        		
        		[] mgmt.receive(mw_report(c_aisFailureInDG3)) {
        			t_wait.stop;
@@ -363,16 +352,13 @@ module ePassport_Testcases {
        testcase TC_LDS_F04() runs on MRTD system MRTD_System {
        	
            f_cfUp();
        	f_initializeMRTD(e_cfgDfltEac);
        	//TODO: Modify DG3; 
        	//	was: 	v_cfg.dg14:=valueof(m_file_DG14_LDS_F04);
			//			v_cfg.efsod:=valueof(m_file_EF_SOD_LDS_F04);
        	f_initializeMRTD("CFG.EAC.LDS.F04");
        	
        	f_initializeIS(); 
    
    		t_wait.start;
    		alt {
        		[] a_advancedInspectionProcedure;
        		[] a_advancedInspectionProcedure();
        		
        		[] mgmt.receive(mw_report(c_aisFailureInDG14)) {
        			t_wait.stop;
@@ -410,15 +396,13 @@ module ePassport_Testcases {
        testcase TC_LDS_H37() runs on MRTD system MRTD_System {
        	
            f_cfUp();
        	f_initializeMRTD(e_cfgDfltEac);
        	//TODO: Modify DG3; 
        	//	was: 	v_cfg.efsod:=valueof(m_file_EF_SOD_LDS_H37);
        	f_initializeMRTD("CFG.EAC.LDS.H37");
        	
        	f_initializeIS(); 
    
    		t_wait.start;
    		alt {
        		[] a_advancedInspectionProcedure;
        		[] a_advancedInspectionProcedure();
        		
        		[] mgmt.receive(mw_report(c_aisFailureInEFSOD)) {
        			t_wait.stop;
Loading