Commit 630c94a5 authored by berge's avatar berge
Browse files

Huge changes in types (part2)

parent 4de11e53
Loading
Loading
Loading
Loading
+40 −29
Original line number Diff line number Diff line
@@ -106,12 +106,14 @@
		
    	altstep a_activeAuthentication () runs on MRTD {
    		
    		var Command v_command;
    		var CommandInternalAuthenticate v_command;
    		var octetstring v_rndIfd;
    		var octetstring v_response;
    
			[] mrtdport.receive(mw_intAuthenticate) -> value v_command {
   				v_rndIfd := v_command.payload.plainText.commandData;
   				v_rndIfd := v_command.msg
    						.internalAuthenticateMsg.payload
    						.internalAuthenticateData.challenge;
				v_response := f_activeAuthentication(v_rndIfd);
				mrtdport.send(m_responseRead(v_response));
			}
@@ -120,11 +122,14 @@
    	altstep a_chipAuthentication () runs on MRTD {

    		//var EFfile v_file:=valueof(p_file);
    		var Command v_command;
    		var CommandManageSecurityEnvironment v_command;
    		var octetstring v_publicKeyPcd;

			[] mrtdport.receive(mw_mseSetKAT) -> value v_command {
				v_publicKeyPcd := v_command.payload.plainText.commandData;
				v_publicKeyPcd := v_command.msg
    						.manageSecurityEnvironmentMsg.payload
    						.manageSecurityEnvironmentData.crtKAT
    						.crtReferenceOfSecretOrPublicKey.tlvValue;
				f_chipAuthentication(v_publicKeyPcd);
				mrtdport.send(m_responseOK);
				vc_simu.securityStatus := e_chipAuthenticated;
@@ -134,14 +139,17 @@
    	// Terminal Authentication triggered by reading of EF.CVCA
    	altstep a_terminalAuthentication () runs on MRTD {

    		var Command v_command;
    		var CommandManageSecurityEnvironment v_command;
    		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.payload.plainText.commandData;
				v_dstCAR := v_command.msg
    						.manageSecurityEnvironmentMsg.payload
    						.manageSecurityEnvironmentData.crtDST
    						.crtReferenceOfSecretOrPublicKey.tlvValue;
				// TODO: check CAR exists
				
				mrtdport.send(m_responseOK);
@@ -157,8 +165,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.payload.plainText.commandData); 
				v_signature := f_getSignature(v_command.payload.plainText.commandData);
				v_certificate := f_getCertificate(v_command.msg.genericMsg.payload.genericData.data); // FIXME 
				v_signature := f_getSignature(v_command.msg.genericMsg.payload.genericData.data); // FIXME 
				if (f_verifySignature(v_signature, v_dstCAR)) {
					//TODO store certificate and CAR						
		 			mrtdport.send(m_responseOK);
@@ -171,7 +179,9 @@

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

@@ -183,7 +193,9 @@

			// 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.payload.plainText.commandData;
				v_signature := v_command.msg.externalOrMutualAuthenticateMsg
						.payload.externalOrMutualAuthenticateData
						.challengeResponse;
				if(f_verifySignature(v_signature, v_atCAR)) {
					mrtdport.send(m_responseOK);
				}
@@ -215,8 +227,7 @@
    			
    	altstep a_bac() runs on MRTD {
	
        	var Command v_command;
        	var CommandData v_data;
        	var CommandExternalOrMutualAuthenticate v_command;
        	var octetstring v_rndIcc;
        	var octetstring v_response;
        	var octetstring v_challengeResponse;
@@ -228,7 +239,10 @@
        	}
        	
    		[] mrtdport.receive(mw_extAuthenticate) -> value v_command {
    			v_challengeResponse := v_command.payload.plainText.commandData;
    			        				
    			v_challengeResponse := v_command.msg
    									.externalOrMutualAuthenticateMsg.payload
    									.externalOrMutualAuthenticateData.challengeResponse ;
        		
        		v_response := f_basicAccessControl(v_rndIcc, v_challengeResponse);
        		mrtdport.send(m_responseRead(v_response));
@@ -242,8 +256,6 @@
	
    		var Command v_command;
    		var integer v_logicalChannel;
    		var LongFileId v_longFileId;
    		var ShortFileId v_shortFileId;
    		var octetstring v_data := ''O;
    		var integer v_dataLength;
    		var integer v_offset;
@@ -254,8 +266,8 @@
        		
        		// set current file for logical channel
        		v_logicalChannel := f_getLogicalChannel(v_command.class);
        		v_longFileId := v_command.payload.plainText.commandData;
        		vc_simu.currentFiles[v_logicalChannel] := getFileByLongId(v_longFileId);
        		
        		vc_simu.currentFiles[v_logicalChannel] := getFileByLongId(p_file.longFileId);
        				
        		mrtdport.send(m_responseOK);
        		repeat;
@@ -266,11 +278,10 @@
    
    			// set current file for logical channel
        		v_logicalChannel := f_getLogicalChannel(v_command.class);
        		v_shortFileId := v_command.payload.plainText.commandData;
        		vc_simu.currentFiles[v_logicalChannel] :=  getFileByShortId(v_shortFileId);
        		vc_simu.currentFiles[v_logicalChannel] := getFileByShortId(p_file.shortFileId);
        					
    			v_offset := bit2int(v_command.p2);
    			v_dataLength := v_command.payload.plainText.lengthE;
    			v_offset := v_command.msg.readBinaryMsg.params.fileIdAndOffset.offset;
    			v_dataLength := v_command.msg.readBinaryMsg.payload.readBinaryData.lengthE;
      		
        		v_result := f_readFileData(vc_simu.currentFiles[v_logicalChannel], 
        			v_offset, v_dataLength, v_data);
@@ -290,7 +301,7 @@
    				repeat;
    			}
    		
    			v_offset := bit2int(v_command.p1 & v_command.p2);
    			v_offset := v_command.msg.readBinaryMsg.params.longOffset.offset;
    			
    			v_result := f_readFileData(vc_simu.currentFiles[v_logicalChannel],
    			 	v_offset, v_dataLength, v_data);
@@ -307,7 +318,7 @@
		//FIXME: duplicated code
		altstep a_readAnyFile() runs on MRTD {
	
    		var Command v_command;
    		var CommandSelect v_command;
    		var integer v_logicalChannel;
    		var LongFileId v_longFileId;
    		var ShortFileId v_shortFileId;
@@ -321,7 +332,7 @@
        		
        		// set current file for logical channel
        		v_logicalChannel := f_getLogicalChannel(v_command.class);
        		v_longFileId := v_command.payload.plainText.commandData;
        		v_longFileId := v_command.msg.selectMsg.payload.selectData.fileId;
        		vc_simu.currentFiles[v_logicalChannel] := getFileByLongId(v_longFileId);
        				
        		mrtdport.send(m_responseOK);
@@ -333,11 +344,11 @@
    
    			// set current file for logical channel
        		v_logicalChannel := f_getLogicalChannel(v_command.class);
				v_shortFileId := v_command.payload.plainText.commandData;
				v_shortFileId := bit2oct(v_command.msg.readBinaryMsg.params.fileIdAndOffset.fileId);
        		vc_simu.currentFiles[v_logicalChannel] :=  getFileByShortId(v_shortFileId);
        		       					
    			v_offset := bit2int(v_command.p2);
    			v_dataLength := v_command.payload.plainText.lengthE;
    			v_offset := v_command.msg.readBinaryMsg.params.fileIdAndOffset.offset;
    			v_dataLength := v_command.msg.readBinaryMsg.payload.readBinaryData.lengthE;
      		
        		v_result := f_readFileData(vc_simu.currentFiles[v_logicalChannel], 
        			v_offset, v_dataLength, v_data);
@@ -357,7 +368,7 @@
    				repeat;
    			}
    		
    			v_offset := bit2int(v_command.p1 & v_command.p2);
    			v_offset := v_command.msg.readBinaryMsg.params.longOffset.offset;
    			
    			v_result := f_readFileData(vc_simu.currentFiles[v_logicalChannel], 
    				v_offset, v_dataLength, v_data);
+284 −81
Original line number Diff line number Diff line
@@ -31,18 +31,36 @@ module ePassport_Templates {
    	template Command mw_getdata_cert := {
    		class := mw_class_01,		
    		ins := e_getData,	
    		msg := {
		  		genericMsg := {
					p1 := '00000001'B,   		// values for Certificate reference ID
		  			p2 := '11110001'B,
    		payload := mw_payload(omit, 0)
		  			payload := {
		  				genericData := {
		  					data := omit,
		  					lengthE := 0	
		  				}	
		  			}
		  		}	
		  	}
    	}    	
    	
    	// TEMPLATES m_get_data_MRZ
        template Command mw_getdata_mrz := {
            class := mw_class_01,		
            ins := e_getData,
            msg := {
		  		genericMsg := {
					p1 := '00000001'B,   		
		  			p2 := '11110010'B,
            payload := mw_payload(omit, 0)
		  			payload := {
		  				genericData := {
		  					data := omit,
		  					lengthE := 0	
		  				}	
		  			}
		  		}	
		  	}			
    	}
    	
    	// TEMPLATES m_setdata_cert
@@ -65,16 +83,6 @@ module ePassport_Templates {
	} // 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,
@@ -105,120 +113,315 @@ module ePassport_Templates {
        template Command mw_report(template Oct2 v_failCode) := {
    	   	class := mw_class_01,	
    	  	ins := e_putDataWithDataBytes, //'da'O,		
    	  	msg := {
		  		genericMsg := {
					p1 := '00001111'B,    		
		  			p2 := ?,
    	  	payload := mw_payload(v_failCode, 0)
		  			payload := {
		  				genericData := {
		  					data := v_failCode,
		  					lengthE := 0	
		  				}	
		  			}
		  		}	
		  	}		
    	}
	} // end managementTemplates

    group commandTemplates {
    	
		//SELECT TEMPLATES : Send APDU to the passport 00 a4 04 0c 07 a0 00 00 02 47 10 01                      
        template Command mw_selectApplication := {
        template CommandSelect mw_selectApplication := {
		    class := mw_class_00,
			ins := e_select, 
			p1 := '00000100'B, // FIXME
			p2 := '00001100'B, // FIXME
			payload := mw_payload('a0000002471001'O, omit) // FIXME
			msg := {
				selectMsg := {
        			p1 := {
        				reserved := c_4ZeroBits,	
        				selectionMethod := e_selectByDFName
        			},
        			p2 := { 
        				reserved := c_4ZeroBits,
        				fileControlInformation := e_noResponseOrProprietary,
        				fileOccurrence := e_firstOrOnlyOccurrence
        			},
        			payload := { 
        				selectData := {
        					fileId := 'a0000002471001'O, // FIXME
        					lengthE :=  omit 	
        				}
        			}					
				}	
			}
         }

		//SELECT TEMPLATES 00 a4 02 0c 02 01 1e                           
        template Command mw_selectByFileId (LongFileId v_fileID) := {
        template CommandSelect mw_selectByFileId (LongFileId v_fileID) := {
		    class := mw_class_00,
			ins := e_select, 
			p1 := '000000??'B,
			p2 := '000011??'B,
			payload := mw_payload(v_fileID, omit)
			msg := {
				selectMsg := {
        			p1 := {
        				reserved := c_4ZeroBits,	
        				selectionMethod := e_selectByFileId
        			},
        			p2 := { 
        				reserved := c_4ZeroBits,
        				fileControlInformation := e_noResponseOrProprietary,
        				fileOccurrence := e_firstOrOnlyOccurrence
        			},
        			payload := { 
        				selectData := {
        					fileId := v_fileID,
        					lengthE :=  omit 	
        				}
        			}					
				}	
			}
        }
        
        template Command mw_selectAnyFile := {
        template CommandSelect mw_selectAnyFile := {
		    class := mw_class_00,
			ins := e_select, 
			p1 := '000000??'B, // FIXME
			p2 := '000011??'B, // FIXME
			payload := mw_payload(?, omit)
			msg := {
				selectMsg := {
        			p1 := {
        				reserved := c_4ZeroBits,	
        				selectionMethod := e_selectByFileId
        			},
        			p2 := { 
        				reserved := c_4ZeroBits,
        				fileControlInformation := e_noResponseOrProprietary,
        				fileOccurrence := e_firstOrOnlyOccurrence
        			},
        			payload := { 
        				selectData := {
        					fileId := ?,
        					lengthE :=  omit 	
        				}
        			}					
				}	
			}
        }

        template Command mw_readShortEF (ShortFileId p_shortFileId) := {
        template CommandReadBinary mw_readShortEF (ShortFileId p_shortFileId) := {
            class := mw_class_00,
            ins := e_readBinary, 
            p1 := (oct2bit(p_shortFileId) or4b '10000000'B),    // '100?????'B,  // FIXME
            p2 := ?,
            payload := mw_payload(omit, ?)
            msg := {
            	readBinaryMsg := {
            		params := {
            			fileIdAndOffset := {
            				fileIdPresent := e_fileIdAndOffset, 
							rfu := c_2ZeroBits,
							fileId := substr(oct2bit(p_shortFileId),3,5),
							offset := ?
            			}
					},
					payload := {
						readBinaryData := {
							lengthE := ?
						}
					}
            	}
            }
        }
         
        template Command mw_readAnyShortEF := {
        template CommandReadBinary mw_readAnyShortEF := {
        	class := mw_class_00,
            ins := e_readBinary, 
            p1 := '100?????'B,  // FIXME
            p2 := ?,
            payload := mw_payload(omit, ?)	
            msg := {
            	readBinaryMsg := {
            		params := {
            			fileIdAndOffset := {
            				fileIdPresent := e_fileIdAndOffset, 
							rfu := c_2ZeroBits,
							fileId := ?,
							offset := ?
            			}
					},
					payload := {
						readBinaryData := {
							lengthE := ?
						}
					}
            	}
            }
        }
        
        template Command mw_readCurrentEF := {
        template CommandReadBinary mw_readCurrentEF := {
            class := mw_class_00,
            ins := e_readBinary, 
            p1 := '0???????'B,  // FIXME
            p2 := ?,
            payload := mw_payload(omit, ?)
            msg := {
            	readBinaryMsg := {
            		params := {
            			longOffset := {
            				fileIdPresent := e_longOffset, 
							offset := ?
            			}
					},
					payload := {
						readBinaryData := {
							lengthE := ?
						}
					}
            	}
            }
         }
 
		template Command mw_getChallenge := {
		template CommandGetChallenge mw_getChallenge := {
	      	class := mw_class_00,
		  	ins := e_getChallenge, 
		  	p1 := '00000000'B,  // FIXME
		  	p2 := '00000000'B,  // FIXME
		  	payload := mw_payload(omit, ?) //8? // FIXME
		  	msg := {
		  		getChallengeMsg := {
		  			algorithm := ?,
					reserved := c_1ZeroByte,
					payload := {
						getChallengeData := {
							lengthE := ?	
						}
					}	
		  		}	
		  	}
        }

		template Command mw_extAuthenticate := {
		template CommandExternalOrMutualAuthenticate mw_extAuthenticate := {
	    	class := mw_class_00,
			ins := e_externalOrMutualAuthenticate,
			p1 := '00000000'B,  // FIXME
			p2 := '00000000'B,  // FIXME
			payload := mw_payload(?, ?)
			msg := {
				externalOrMutualAuthenticateMsg := {
					algorithm := ?,
					referenceData := ?,
					payload := ?
				}	
			} 
        }
        
		template Command mw_intAuthenticate := {   ////// to modify : wrong template
		template CommandInternalAuthenticate mw_intAuthenticate := { 
	      	class := mw_class_00,
		  	ins := e_externalOrMutualAuthenticate, // FIXME
			p1 := '00000000'B,  // FIXME
		  	p2 := '00000000'B,  // FIXME
		  	payload := mw_payload(?, ?)
		  	ins := e_internalAuthenticate, 
			msg := {
				internalAuthenticateMsg := {
					algorithm := ?,
					referenceData := ?,
					payload := ?
				}	
			} 
        }

		template Command mw_mseSetDST := {
		template CommandManageSecurityEnvironment mw_mseSetDST := {
	      	class := mw_class_00,
		  	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(?, ?)
		  	msg := { 
		  		manageSecurityEnvironmentMsg := {
		  			p1 := {
		  				 mseSecureMessagingInCommandDataField := ?,
						 mseSecureMessagingInResponseDataField := ?,
						 mseComputationDeciphermentIntAuthKeyAgreement := ?,
						 mseVerificationEnciphermentExtAuthKeyAgreement := ?,
						 mseFunction := e_mseFunctionSet
		  			},
		  			p2 := e_crtDST,
		  			payload := {
		  				manageSecurityEnvironmentData := {
		  					crtDST := {
		  						crtCryptographicMechanismReference := *,
            					crtFileReference := *,
            					crtDfName := *,
            					crtReferenceOfSecretOrPublicKey := ?,
            					crtReferenceOfSessionOrPrivateKey := *,
            					crtKeyUsageTemplate := *,
            					crtAuxRandomNumber := *,
            					crtUsageQualifierByte := *
		  					}
		  				}
		  			}		
		  		}
		  	}
        }

		template Command mw_mseSetKAT := {
		template CommandManageSecurityEnvironment mw_mseSetKAT := {
	      	class := mw_class_00,
		  	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_mseSetAT := {
		  	msg := { 
		  		manageSecurityEnvironmentMsg := {
		  			p1 := {
		  				 mseSecureMessagingInCommandDataField := ?,
						 mseSecureMessagingInResponseDataField := ?,
						 mseComputationDeciphermentIntAuthKeyAgreement := ?,
						 mseVerificationEnciphermentExtAuthKeyAgreement := ?,
						 mseFunction := e_mseFunctionSet
		  			},
		  			p2 := e_crtKAT,
		  			payload := {
		  				manageSecurityEnvironmentData := {
		  					crtKAT := {
            					crtCryptographicMechanismReference := *,
            					crtFileReference := *,
            					crtDfName := *,
            					crtReferenceOfSecretOrPublicKey := ?,
            					crtReferenceOfSessionOrPrivateKey := *,
            					crtKeyUsageTemplate	:= *,
            					crtAuxPreviousExchangedChallengePlusOne	:= *,
            					crtAuxHashCodeProvidedByCard := *,
            					crtAuxRandomNumberProvidedByCard := *,
            					crtAuxRandomNumber := *,
            					crtAuxTimestampProvidedByCard := *,
            					crtAuxTimestamp := *,
            					crtAuxPreviousDigitalSignatureCounterPlusOne := *,
            					crtAuxDigitalSignatureCounter := *,
            					crtUsageQualifierByte := *
		  					}
		  				}
		  			}		
		  		}
		  	}        }

		template CommandManageSecurityEnvironment mw_mseSetAT := {
	      	class := mw_class_00,
		  	ins := e_manageSecurityEnvironment, 
		  	p1 := '10000001'B,  // FIXME
		  	p2 := '10100100'B, // FIXME
		  	payload := mw_payload(?, ?)
		  	msg := { 
		  		manageSecurityEnvironmentMsg := {
		  			p1 := {
		  				 mseSecureMessagingInCommandDataField := ?,
						 mseSecureMessagingInResponseDataField := ?,
						 mseComputationDeciphermentIntAuthKeyAgreement := ?,
						 mseVerificationEnciphermentExtAuthKeyAgreement := ?,
						 mseFunction := e_mseFunctionSet
		  			},
		  			p2 := e_crtAT,
		  			payload := {
		  				manageSecurityEnvironmentData := {
		  					crtAT := {
								crtCryptographicMechanismReference := *,
            					crtFileReference := *,
            					crtDfName := *,
            					crtReferenceOfSecretOrPublicKey := ?,
            					crtReferenceOfSessionOrPrivateKey := *,
            					crtKeyUsageTemplate	:= *,
            					crtAuxChallengeOrDataElementForDerivingKey := *,
            					crtUsageQualifierByte := *
		  					}
		  				}
		  			}		
		  		}
		  	}
        }

		template Command mw_psoVerifyCertificate := {
		template CommandPerformSecurityOperation mw_psoVerifyCertificate := {
	      	class := mw_class_00,
		  	ins := e_performSecurityOperation, 
		  	msg := {
		  		genericMsg := {
					p1 := '00000000'B,  // FIXME
		  			p2 := '10111110'B,  // FIXME
		  	payload := mw_payload(?, ?)
		  			payload := {
		  				genericData := {
		  					data := ?,
		  					lengthE := *	
		  				}	
		  			}
		  		}	
		  	}
        }
	} // end commandTemplates

+20 −20

File changed.

Preview size limit exceeded, changes collapsed.

+143 −75

File changed.

Preview size limit exceeded, changes collapsed.