Commit f25b144f authored by berge's avatar berge
Browse files

Huge changes in types (part3)

parent 630c94a5
Loading
Loading
Loading
Loading
+42 −44
Original line number Diff line number Diff line
@@ -111,8 +111,7 @@
    		var octetstring v_response;
    
			[] mrtdport.receive(mw_intAuthenticate) -> value v_command {
   				v_rndIfd := v_command.msg
    						.internalAuthenticateMsg.payload
   				v_rndIfd := v_command.payload
    						.internalAuthenticateData.challenge;
				v_response := f_activeAuthentication(v_rndIfd);
				mrtdport.send(m_responseRead(v_response));
@@ -126,8 +125,7 @@
    		var octetstring v_publicKeyPcd;

			[] mrtdport.receive(mw_mseSetKAT) -> value v_command {
				v_publicKeyPcd := v_command.msg
    						.manageSecurityEnvironmentMsg.payload
				v_publicKeyPcd := v_command.payload
    						.manageSecurityEnvironmentData.crtKAT
    						.crtReferenceOfSecretOrPublicKey.tlvValue;
				f_chipAuthentication(v_publicKeyPcd);
@@ -139,15 +137,16 @@
    	// Terminal Authentication triggered by reading of EF.CVCA
    	altstep a_terminalAuthentication () runs on MRTD {

    		var CommandManageSecurityEnvironment v_command;
    		var CommandManageSecurityEnvironment v_mseCommand;
    		var CommandPerformSecurityOperation v_psoCommand;
    		var CommandExternalOrMutualAuthenticate v_extAuthcommand;
    		var octetstring v_rndIcc;
    		var octetstring v_dstCAR, v_atCAR;
    		var octetstring v_certificate, v_signature;

           	// reading of the certificate chain
			[] mrtdport.receive(mw_mseSetDST) -> value v_command {
				v_dstCAR := v_command.msg
    						.manageSecurityEnvironmentMsg.payload
			[] mrtdport.receive(mw_mseSetDST) -> value v_mseCommand {
				v_dstCAR := v_mseCommand.payload
    						.manageSecurityEnvironmentData.crtDST
    						.crtReferenceOfSecretOrPublicKey.tlvValue;
				// TODO: check CAR exists
@@ -157,7 +156,7 @@
			}

			// The MRTD is waiting for a PSO:Verify Certificate
			[] mrtdport.receive(mw_psoVerifyCertificate) -> value v_command {
			[] mrtdport.receive(mw_psoVerifyCertificate) -> value v_psoCommand {
						 
				// if the Certificate Body and the Signature are OK then the certificate was successfully validated
				// and the public key has been imported
@@ -165,8 +164,8 @@
					
				// the correct Certificate must be passed as parameter in the external function
				// in order to verify IS and DV and link CAVA certificates.
				v_certificate := f_getCertificate(v_command.msg.genericMsg.payload.genericData.data); // FIXME 
				v_signature := f_getSignature(v_command.msg.genericMsg.payload.genericData.data); // FIXME 
				v_certificate := f_getCertificate(v_psoCommand.payload.genericData.data); // FIXME 
				v_signature := f_getSignature(v_psoCommand.payload.genericData.data); // FIXME 
				if (f_verifySignature(v_signature, v_dstCAR)) {
					//TODO store certificate and CAR						
		 			mrtdport.send(m_responseOK);
@@ -178,24 +177,22 @@
			}

			// The MRTD is waiting a MSE:SetAT message with a key reference
			[] mrtdport.receive(mw_mseSetAT) -> value v_command {
				v_atCAR := v_command.msg.manageSecurityEnvironmentMsg
						.payload.manageSecurityEnvironmentData
			[] mrtdport.receive(mw_mseSetAT) -> value v_mseCommand {
				v_atCAR := v_mseCommand.payload.manageSecurityEnvironmentData
						.crtAT.crtReferenceOfSecretOrPublicKey.tlvValue;
				mrtdport.send(m_responseOK);
			}

			// 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 {
			[] mrtdport.receive(mw_getChallenge) {
				v_rndIcc := f_generateRandomOctetstring(c_atNonceSize); 
				mrtdport.send(m_responseRead(v_rndIcc));		
			}

			// The MRTD is waiting an External Authenticate message including the signature of the IS
			[] mrtdport.receive(mw_extAuthenticate) -> value v_command { 
				v_signature := v_command.msg.externalOrMutualAuthenticateMsg
						.payload.externalOrMutualAuthenticateData
						.challengeResponse;
			[] mrtdport.receive(mw_extAuthenticate) -> value v_extAuthcommand { 
				v_signature := v_extAuthcommand.payload
						.externalOrMutualAuthenticateData.challengeResponse;
				if(f_verifySignature(v_signature, v_atCAR)) {
					mrtdport.send(m_responseOK);
				}
@@ -240,8 +237,7 @@
        	
    		[] mrtdport.receive(mw_extAuthenticate) -> value v_command {
    			        				
    			v_challengeResponse := v_command.msg
    									.externalOrMutualAuthenticateMsg.payload
    			v_challengeResponse := v_command.payload
						.externalOrMutualAuthenticateData.challengeResponse ;
        		
        		v_response := f_basicAccessControl(v_rndIcc, v_challengeResponse);
@@ -254,7 +250,8 @@
		
		altstep a_readFile(in FileInfo p_file) runs on MRTD {
	
    		var Command v_command;
    		var CommandSelect v_selectCommand;
    		var CommandReadBinary v_readCommand;
    		var integer v_logicalChannel;
    		var octetstring v_data := ''O;
    		var integer v_dataLength;
@@ -262,10 +259,10 @@
    		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_selectCommand {
        		
        		// set current file for logical channel
        		v_logicalChannel := f_getLogicalChannel(v_command.class);
        		v_logicalChannel := f_getLogicalChannel(v_selectCommand.class);
        		
        		vc_simu.currentFiles[v_logicalChannel] := getFileByLongId(p_file.longFileId);
        				
@@ -274,14 +271,14 @@
        	}
        		
        	// READ Command with short EF
    		[] mrtdport.receive(mw_readShortEF(p_file.shortFileId)) -> value v_command {
    		[] mrtdport.receive(mw_readShortEF(p_file.shortFileId)) -> value v_readCommand {
    
    			// set current file for logical channel
        		v_logicalChannel := f_getLogicalChannel(v_command.class);
        		v_logicalChannel := f_getLogicalChannel(v_readCommand.class);
        		vc_simu.currentFiles[v_logicalChannel] := getFileByShortId(p_file.shortFileId);
        					
    			v_offset := v_command.msg.readBinaryMsg.params.fileIdAndOffset.offset;
    			v_dataLength := v_command.msg.readBinaryMsg.payload.readBinaryData.lengthE;
    			v_offset := v_readCommand.params.fileIdAndOffset.offset;
    			v_dataLength := v_readCommand.payload.readBinaryData.lengthE;
      		
        		v_result := f_readFileData(vc_simu.currentFiles[v_logicalChannel], 
        			v_offset, v_dataLength, v_data);
@@ -291,17 +288,17 @@
    		}
    
    		// READ Command (using current EF)
    		[] mrtdport.receive(mw_readCurrentEF) -> value v_command {
    		[] mrtdport.receive(mw_readCurrentEF) -> value v_readCommand {
    		
    			// Check current file
    			v_logicalChannel := f_getLogicalChannel(v_command.class);
    			v_logicalChannel := f_getLogicalChannel(v_readCommand.class);
    			if(vc_simu.currentFiles[v_logicalChannel] == c_noFileInfo) {
    				log(""); //TODO
    				mrtdport.send(m_responseNOK(c_w1w2NoCurrentEF));
    				repeat;
    			}
    		
    			v_offset := v_command.msg.readBinaryMsg.params.longOffset.offset;
    			v_offset := v_readCommand.params.longOffset.offset;
    			
    			v_result := f_readFileData(vc_simu.currentFiles[v_logicalChannel],
    			 	v_offset, v_dataLength, v_data);
@@ -318,7 +315,8 @@
		//FIXME: duplicated code
		altstep a_readAnyFile() runs on MRTD {
	
    		var CommandSelect v_command;
    		var CommandSelect v_selectCommand;
    		var CommandReadBinary v_readCommand;
    		var integer v_logicalChannel;
    		var LongFileId v_longFileId;
    		var ShortFileId v_shortFileId;
@@ -328,11 +326,11 @@
    		var W1W2Status v_result;
    		
    		// SELECT Command
        	[] mrtdport.receive(mw_selectAnyFile) -> value v_command {
        	[] mrtdport.receive(mw_selectAnyFile) -> value v_selectCommand {
        		
        		// set current file for logical channel
        		v_logicalChannel := f_getLogicalChannel(v_command.class);
        		v_longFileId := v_command.msg.selectMsg.payload.selectData.fileId;
        		v_logicalChannel := f_getLogicalChannel(v_selectCommand.class);
        		v_longFileId := v_selectCommand.payload.selectData.fileId;
        		vc_simu.currentFiles[v_logicalChannel] := getFileByLongId(v_longFileId);
        				
        		mrtdport.send(m_responseOK);
@@ -340,15 +338,15 @@
        	}
        		
        	// READ Command with short EF
    		[] mrtdport.receive(mw_readAnyShortEF) -> value v_command {
    		[] mrtdport.receive(mw_readAnyShortEF) -> value v_readCommand {
    
    			// set current file for logical channel
        		v_logicalChannel := f_getLogicalChannel(v_command.class);
				v_shortFileId := bit2oct(v_command.msg.readBinaryMsg.params.fileIdAndOffset.fileId);
        		v_logicalChannel := f_getLogicalChannel(v_readCommand.class);
				v_shortFileId := bit2oct(v_readCommand.params.fileIdAndOffset.fileId);
        		vc_simu.currentFiles[v_logicalChannel] :=  getFileByShortId(v_shortFileId);
        		       					
    			v_offset := v_command.msg.readBinaryMsg.params.fileIdAndOffset.offset;
    			v_dataLength := v_command.msg.readBinaryMsg.payload.readBinaryData.lengthE;
    			v_offset := v_readCommand.params.fileIdAndOffset.offset;
    			v_dataLength := v_readCommand.payload.readBinaryData.lengthE;
      		
        		v_result := f_readFileData(vc_simu.currentFiles[v_logicalChannel], 
        			v_offset, v_dataLength, v_data);
@@ -358,17 +356,17 @@
    		}
    
    		// READ Command (using current EF)
    		[] mrtdport.receive(mw_readCurrentEF) -> value v_command {
    		[] mrtdport.receive(mw_readCurrentEF) -> value v_readCommand {
    		
    			// Check current file
    			v_logicalChannel := f_getLogicalChannel(v_command.class);
    			v_logicalChannel := f_getLogicalChannel(v_readCommand.class);
    			if(vc_simu.currentFiles[v_logicalChannel] == c_noFileInfo) {
    				log(""); //TODO
    				mrtdport.send(m_responseNOK(c_w1w2NoCurrentEF));
    				repeat;
    			}
    		
    			v_offset := v_command.msg.readBinaryMsg.params.longOffset.offset;
    			v_offset := v_readCommand.params.longOffset.offset;
    			
    			v_result := f_readFileData(vc_simu.currentFiles[v_logicalChannel], 
    				v_offset, v_dataLength, v_data);
+214 −268
Original line number Diff line number Diff line
@@ -28,13 +28,13 @@ module ePassport_Templates {
    	}	
    	
    	// TEMPLATES m_get_data_certificate see Automatic Interface Proposal
    	template Command mw_getdata_cert := {
    	template CommandGeneric mw_getdata_cert := {
    		class := mw_class_01,		
    		ins := e_getData,	
    		msg := {
		  		genericMsg := {
			params := {
				p1 := '00000001'B,   		// values for Certificate reference ID
		  			p2 := '11110001'B,
	  			p2 := '11110001'B
    		},
  			payload := {
  				genericData := {
  					data := omit,
@@ -42,17 +42,15 @@ module ePassport_Templates {
  				}	
  			}
    	}    	
		  	}
    	}    	
    	
    	// TEMPLATES m_get_data_MRZ
        template Command mw_getdata_mrz := {
        template CommandGeneric mw_getdata_mrz := {
            class := mw_class_01,		
            ins := e_getData,
            msg := {
		  		genericMsg := {
            params := {
	  			p1 := '00000001'B,   		
		  			p2 := '11110010'B,
	  			p2 := '11110010'B
            },
  			payload := {
  				genericData := {
  					data := omit,
@@ -60,8 +58,6 @@ module ePassport_Templates {
  				}	
		  	}			
    	}
		  	}			
    	}
    	
    	// 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 !!!
@@ -110,13 +106,13 @@ module ePassport_Templates {
	group managementTemplates {

    	// TEMPLATES mw_report
        template Command mw_report(template Oct2 v_failCode) := {
        template CommandGeneric mw_report(template Oct2 v_failCode) := {
    	   	class := mw_class_01,	
    	  	ins := e_putDataWithDataBytes, //'da'O,		
    	  	msg := {
		  		genericMsg := {
    	  	params := {
				p1 := '00001111'B,    		
		  			p2 := ?,
	  			p2 := ?
	  		},
  			payload := {
  				genericData := {
  					data := v_failCode,
@@ -124,8 +120,6 @@ module ePassport_Templates {
  				}	
  			}
    	}
		  	}		
    	}
	} // end managementTemplates

    group commandTemplates {
@@ -134,14 +128,10 @@ module ePassport_Templates {
        template CommandSelect mw_selectApplication := {
		    class := mw_class_00,
			ins := e_select, 
			msg := {
				selectMsg := {
        			p1 := {
        				reserved := c_4ZeroBits,	
        				selectionMethod := e_selectByDFName
        			},
        			p2 := { 
        				reserved := c_4ZeroBits,
			params := {
				reservedP1 := c_4ZeroBits,	
				selectionMethod := e_selectByDFName,
				reservedP2 := c_4ZeroBits,
				fileControlInformation := e_noResponseOrProprietary,
				fileOccurrence := e_firstOrOnlyOccurrence
   			},
@@ -152,21 +142,15 @@ module ePassport_Templates {
				}
			}					
         }
			}
         }

		//SELECT TEMPLATES 00 a4 02 0c 02 01 1e                           
        template CommandSelect mw_selectByFileId (LongFileId v_fileID) := {
		    class := mw_class_00,
			ins := e_select, 
			msg := {
				selectMsg := {
        			p1 := {
        				reserved := c_4ZeroBits,	
        				selectionMethod := e_selectByFileId
        			},
        			p2 := { 
        				reserved := c_4ZeroBits,
			params := {
				reservedP1 := c_4ZeroBits,	
				selectionMethod := e_selectByFileId,
				reservedP2 := c_4ZeroBits,
				fileControlInformation := e_noResponseOrProprietary,
				fileOccurrence := e_firstOrOnlyOccurrence
			},
@@ -177,20 +161,14 @@ module ePassport_Templates {
				}
			}					
        }
			}
        }
        
        template CommandSelect mw_selectAnyFile := {
		    class := mw_class_00,
			ins := e_select, 
			msg := {
				selectMsg := {
        			p1 := {
        				reserved := c_4ZeroBits,	
        				selectionMethod := e_selectByFileId
        			},
        			p2 := { 
        				reserved := c_4ZeroBits,
			params := {
				reservedP1 := c_4ZeroBits,	
				selectionMethod := e_selectByFileId,
				reservedP2 := c_4ZeroBits,
				fileControlInformation := e_noResponseOrProprietary,
				fileOccurrence := e_firstOrOnlyOccurrence
			},
@@ -201,14 +179,10 @@ module ePassport_Templates {
				}
			}					
        }
			}
        }

        template CommandReadBinary mw_readShortEF (ShortFileId p_shortFileId) := {
            class := mw_class_00,
            ins := e_readBinary, 
            msg := {
            	readBinaryMsg := {
    		params := {
    			fileIdAndOffset := {
    				fileIdPresent := e_fileIdAndOffset, 
@@ -223,14 +197,10 @@ module ePassport_Templates {
				}
			}
        }
            }
        }
         
        template CommandReadBinary mw_readAnyShortEF := {
        	class := mw_class_00,
            ins := e_readBinary, 
            msg := {
            	readBinaryMsg := {
    		params := {
    			fileIdAndOffset := {
    				fileIdPresent := e_fileIdAndOffset, 
@@ -245,14 +215,10 @@ module ePassport_Templates {
				}
			}
        }
            }
        }
        
        template CommandReadBinary mw_readCurrentEF := {
            class := mw_class_00,
            ins := e_readBinary, 
            msg := {
            	readBinaryMsg := {
    		params := {
    			longOffset := {
    				fileIdPresent := e_longOffset, 
@@ -264,63 +230,53 @@ module ePassport_Templates {
					lengthE := ?
				}
			}
            	}
            }
        }
 
		template CommandGetChallenge mw_getChallenge := {
	      	class := mw_class_00,
		  	ins := e_getChallenge, 
		  	msg := {
		  		getChallengeMsg := {
	  		params := {
	  			algorithm := ?,
					reserved := c_1ZeroByte,
				reserved := c_1ZeroByte
	  		},
			payload := {
				getChallengeData := {
					lengthE := ?	
				}
			}	
        }
		  	}
        }

		template CommandExternalOrMutualAuthenticate mw_extAuthenticate := {
	    	class := mw_class_00,
			ins := e_externalOrMutualAuthenticate,
			msg := {
				externalOrMutualAuthenticateMsg := {
			params := {
				algorithm := ?,
					referenceData := ?,
				referenceData := ?
			},
			payload := ?
        }
			} 
        }
        
		template CommandInternalAuthenticate mw_intAuthenticate := { 
	      	class := mw_class_00,
		  	ins := e_internalAuthenticate, 
			msg := {
				internalAuthenticateMsg := {
			params := {
				algorithm := ?,
					referenceData := ?,
				referenceData := ?
			},
			payload := ?
        }
			} 
        }

		template CommandManageSecurityEnvironment mw_mseSetDST := {
	      	class := mw_class_00,
		  	ins := e_manageSecurityEnvironment, 
		  	msg := { 
		  		manageSecurityEnvironmentMsg := {
		  			p1 := {
  			params := {
  				 mseSecureMessagingInCommandDataField := ?,
				 mseSecureMessagingInResponseDataField := ?,
				 mseComputationDeciphermentIntAuthKeyAgreement := ?,
				 mseVerificationEnciphermentExtAuthKeyAgreement := ?,
						 mseFunction := e_mseFunctionSet
				 mseFunction := e_mseFunctionSet,
  				crtTag := e_crtDST
  			},
		  			p2 := e_crtDST,
  			payload := {
  				manageSecurityEnvironmentData := {
  					crtDST := {
@@ -336,22 +292,18 @@ module ePassport_Templates {
  				}
  			}		
        }
		  	}
        }

		template CommandManageSecurityEnvironment mw_mseSetKAT := {
	      	class := mw_class_00,
		  	ins := e_manageSecurityEnvironment, 
		  	msg := { 
		  		manageSecurityEnvironmentMsg := {
		  			p1 := {
  			params := {
  				 mseSecureMessagingInCommandDataField := ?,
				 mseSecureMessagingInResponseDataField := ?,
				 mseComputationDeciphermentIntAuthKeyAgreement := ?,
				 mseVerificationEnciphermentExtAuthKeyAgreement := ?,
						 mseFunction := e_mseFunctionSet
				 mseFunction := e_mseFunctionSet,
				 crtTag := e_crtKAT
  			},		  			
		  			p2 := e_crtKAT,
  			payload := {
  				manageSecurityEnvironmentData := {
  					crtKAT := {
@@ -374,21 +326,18 @@ module ePassport_Templates {
  				}
  			}		
		}
		  	}        }
		
		template CommandManageSecurityEnvironment mw_mseSetAT := {
	      	class := mw_class_00,
		  	ins := e_manageSecurityEnvironment, 
		  	msg := { 
		  		manageSecurityEnvironmentMsg := {
		  			p1 := {
  			params := {
  				 mseSecureMessagingInCommandDataField := ?,
				 mseSecureMessagingInResponseDataField := ?,
				 mseComputationDeciphermentIntAuthKeyAgreement := ?,
				 mseVerificationEnciphermentExtAuthKeyAgreement := ?,
						 mseFunction := e_mseFunctionSet
				 mseFunction := e_mseFunctionSet,
  				 crtTag := e_crtAT
  			},
		  			p2 := e_crtAT,
  			payload := {
  				manageSecurityEnvironmentData := {
  					crtAT := {
@@ -404,16 +353,14 @@ module ePassport_Templates {
  				}
  			}		
        }
		  	}
        }

		template CommandPerformSecurityOperation mw_psoVerifyCertificate := {
	      	class := mw_class_00,
		  	ins := e_performSecurityOperation, 
		  	msg := {
		  		genericMsg := {
	  		params := {
				p1 := '00000000'B,  // FIXME
		  			p2 := '10111110'B,  // FIXME
	  			p2 := '10111110'B  // FIXME
	  		},
  			payload := {
  				genericData := {
  					data := ?,
@@ -421,8 +368,7 @@ module ePassport_Templates {
  				}	
  			}		  		
        }
		  	}
        }
        
	} // end commandTemplates

    group responseTemplates {
+2 −2
Original line number Diff line number Diff line
@@ -107,13 +107,13 @@ group portDefs {
    		CommandDeleteFile,
    		CommandTerminateDF,
    		CommandTerminateCardUsage,
    		Command; 
    		CommandGeneric;
		out 
			Response;
	};
	
	type port Mgmt message {
		in Command;
		in CommandGeneric;
		out Response;
	};
	
+334 −312

File changed.

Preview size limit exceeded, changes collapsed.