Commit a95eb3b5 authored by mullers's avatar mullers
Browse files

trans prototype TCs validated

parent 405929f1
Loading
Loading
Loading
Loading
+37 −24
Original line number Original line Diff line number Diff line
@@ -21,6 +21,33 @@


	group calcPrefixFns {
	group calcPrefixFns {
	
	
		function f_createUniqueInterfaceId ( 	
			in 	Oct6to15 p_macAddr
		)
		return Oct8 {
			var UInt8 i;
			var Oct3 v_leftPartMac := int2oct(0,3);
			var Oct3 v_rightPartMac := int2oct(0,3);
			var Bit24 v_leftPartBits := int2bit(0,24);
			var Bit24 v_leftPartBitMask := oct2bit('020000'O);
			
			//get leftPart
			for (i:=0; i<lengthof(p_macAddr)-3; i:=i+1) {
				v_leftPartMac[i] := p_macAddr[i];
			}
			//get rightPart
			for (i:=3; i<lengthof(p_macAddr); i:=i+1) {
				v_rightPartMac[i-3] := p_macAddr[i];
			}
			//flipBit universalBit of leftPart
			v_leftPartBits :=  oct2bit(v_leftPartMac);
			v_leftPartBits := v_leftPartBits xor4b v_leftPartBitMask;
			v_leftPartMac := bit2oct(v_leftPartBits);
			//build InterfaceId
			return v_leftPartMac & 'FFFE'O & v_rightPartMac;
			
		}
	
		function f_createIpAddresses( in Oct6to15 p_macAddr,
		function f_createIpAddresses( in Oct6to15 p_macAddr,
									in Oct16 /*Prefix*/ p_prefix,//Type changed so that NbrDsc moduel does not need to be imported 
									in Oct16 /*Prefix*/ p_prefix,//Type changed so that NbrDsc moduel does not need to be imported 
									in UInt8 p_prefixLen,
									in UInt8 p_prefixLen,
@@ -35,10 +62,7 @@
			var Bit64 v_prefixReadyBits := oct2bit('0000000000000000'O);
			var Bit64 v_prefixReadyBits := oct2bit('0000000000000000'O);
			var Oct8 v_prefixReady := int2oct(0,8);
			var Oct8 v_prefixReady := int2oct(0,8);
			var Oct8 v_interfaceIdReady := int2oct(0,8);
			var Oct8 v_interfaceIdReady := int2oct(0,8);
			var Oct3 v_leftPartMac := int2oct(0,3);
			var Oct3 v_rightPartMac := int2oct(0,3);			
			var Oct3 v_rightPartMac := int2oct(0,3);			
			var Bit24 v_leftPartBits := int2bit(0,24);
			var Bit24 v_leftPartBitMask := oct2bit('020000'O);
//			var Ipv6Address v_gla := int2oct(0,16);
//			var Ipv6Address v_gla := int2oct(0,16);
			
			
			if (p_prefixLen > 64) {
			if (p_prefixLen > 64) {
@@ -56,27 +80,19 @@
				}
				}
				v_prefixReady := bit2oct(v_prefixReadyBits);
				v_prefixReady := bit2oct(v_prefixReadyBits);
			}
			}
			//get leftPart
			// compute interface ID
			for (i:=0; i<lengthof(p_macAddr)-3; i:=i+1) {
			v_interfaceIdReady := f_createUniqueInterfaceId (p_macAddr);
				v_leftPartMac[i] := p_macAddr[i];
			}
			//get rightPart
  			for (i:=3; i<lengthof(p_macAddr); i:=i+1) {
	  			v_rightPartMac[i-3] := p_macAddr[i];
  			}
  			//flipBit universalBit of leftPart
			v_leftPartBits :=  oct2bit(v_leftPartMac);
			v_leftPartBits := v_leftPartBits xor4b v_leftPartBitMask;
			v_leftPartMac := bit2oct(v_leftPartBits);
			//build InterfaceId
			v_interfaceIdReady := v_leftPartMac & 'FFFE'O & v_rightPartMac;
			
			
			//LLA
			//LLA
			p_lla := 'FE80000000000000'O & v_interfaceIdReady;
			p_lla := 'FE80000000000000'O & v_interfaceIdReady;
			
			
			//GLA
			//GLA
			p_gla := v_prefixReady & v_interfaceIdReady;
			p_gla := v_prefixReady & v_interfaceIdReady;
			//LLA
			
			//get rightPart
			for (i:=3; i<lengthof(p_macAddr); i:=i+1) {
				v_rightPartMac[i-3] := p_macAddr[i];
			}
			
			
			//SOL_NODE_MCA
			//SOL_NODE_MCA
			p_solNodeMca := 'FF0200000000000000000001FF'O & v_rightPartMac;
			p_solNodeMca := 'FF0200000000000000000001FF'O & v_rightPartMac;
@@ -738,11 +754,9 @@ group ipSecFns {
		v_espEncrBlockSize := f_getEncrBlockSize(PX_ENCRYPTION_ALGO);
		v_espEncrBlockSize := f_getEncrBlockSize(PX_ENCRYPTION_ALGO);
		v_espIntegrBlockSize := f_getIntegrBlockSize(PX_INTEGRITY_ALGO);
		v_espIntegrBlockSize := f_getIntegrBlockSize(PX_INTEGRITY_ALGO);
		
		
		//TODO v_ahIntegrBlockSize
		
		// SAD for ESP and AH Tests
		// SAD for ESP and AH Tests
		vc_sad[c_saIni] := {
		vc_sad[c_saIni] := {
			spi := PX_SPI/*f_createSpi()*/,
			spi := f_createSpi(),
			seqNr := c_uInt32Zero,
			seqNr := c_uInt32Zero,
			// AH Integrity
			// AH Integrity
			ahIntegrityAlgo := PX_INTEGRITY_ALGO,
			ahIntegrityAlgo := PX_INTEGRITY_ALGO,
@@ -769,7 +783,7 @@ group ipSecFns {
		}
		}


		vc_sad[c_saRes] := {
		vc_sad[c_saRes] := {
			spi := PX_SPI/*f_createSpi()*/,
			spi := f_createSpi(),
			seqNr := c_uInt32Zero,
			seqNr := c_uInt32Zero,
			// AH Integrity
			// AH Integrity
			ahIntegrityAlgo := PX_INTEGRITY_ALGO,
			ahIntegrityAlgo := PX_INTEGRITY_ALGO,
@@ -947,7 +961,6 @@ group ipSecFns {
	return UInt8 {
	return UInt8 {
		var UInt8 v_len := 0;
		var UInt8 v_len := 0;


//FIXME		
		if ( match(p_saTransformAttributeList, SaTransformAttributeList:omit)) {
		if ( match(p_saTransformAttributeList, SaTransformAttributeList:omit)) {
			log("**** SaTransformAttributeList omitted ****");
			log("**** SaTransformAttributeList omitted ****");
		}
		}
+0 −1
Original line number Original line Diff line number Diff line
@@ -1070,7 +1070,6 @@ group rfc4303Esp_ExtHdrFunctions {
		}
		}


		// is a tunneledIpv6Hdr in the extHdrList? If yes, then it becomes the Ipv6Hdr of the original packet
		// is a tunneledIpv6Hdr in the extHdrList? If yes, then it becomes the Ipv6Hdr of the original packet
		// FIXME: check only the first extHdr
		if (ispresent(p_espHeader.espPayload.espIpDatagram.extHdrList)) {
		if (ispresent(p_espHeader.espPayload.espIpDatagram.extHdrList)) {
			for (i:=0; i<sizeof(p_espHeader.espPayload.espIpDatagram.extHdrList) and v_loop ;i:=i+1) {
			for (i:=0; i<sizeof(p_espHeader.espPayload.espIpDatagram.extHdrList) and v_loop ;i:=i+1) {
				if (ischosen(p_espHeader.espPayload.espIpDatagram.extHdrList[i].tunneledIpv6)) {
				if (ischosen(p_espHeader.espPayload.espIpDatagram.extHdrList[i].tunneledIpv6)) {
+3 −2
Original line number Original line Diff line number Diff line
@@ -69,7 +69,8 @@ module LibIpv6_Interface_TypesAndValues {
			PrefixLength 	prefixLength optional,
			PrefixLength 	prefixLength optional,
			//IPv4 Information
			//IPv4 Information
			Ipv4Address		ipv4Addr optional,
			Ipv4Address		ipv4Addr optional,
			Oct2			subnetId optional
			//Oct2			subnetId optional,
			Ipv4Address		relRtAca optional //relayRouterAnycast Address
		}
		}


		type port Ipv6Port message {
		type port Ipv6Port message {
@@ -410,7 +411,7 @@ module LibIpv6_Interface_TypesAndValues {
			HomeAgentAddressDiscoveryReplyMsg		homeAgentAddrDiscReplyMsg,
			HomeAgentAddressDiscoveryReplyMsg		homeAgentAddrDiscReplyMsg,
			MobilePrefixSolicitationMsg				mobilePrefixSolMsg,
			MobilePrefixSolicitationMsg				mobilePrefixSolMsg,
			MobilePrefixAdvertisementMsg			mobilePrefixAdvMsg,
			MobilePrefixAdvertisementMsg			mobilePrefixAdvMsg,
			MobileRouterAdvertisementMsg			mobileRouterAdvMsg,//TODO check this
			MobileRouterAdvertisementMsg			mobileRouterAdvMsg,
			//Imported from Rfc 4068
			//Imported from Rfc 4068
			RouterSolicitationForProxyRtAdvMsg		routerSolPrRtAdvMsg,
			RouterSolicitationForProxyRtAdvMsg		routerSolPrRtAdvMsg,
			ProxyRouterAdvertisementMsg				proxyRtAdvMsg,
			ProxyRouterAdvertisementMsg				proxyRtAdvMsg,
+0 −5
Original line number Original line Diff line number Diff line
@@ -51,11 +51,6 @@ group security {
	*/
	*/
	modulepar { IntegrityAlgo PX_INTEGRITY_ALGO := e_auth_hmacSha1_96 }
	modulepar { IntegrityAlgo PX_INTEGRITY_ALGO := e_auth_hmacSha1_96 }
	
	
	/*
	 * @desc Which SPI shall be used for testing?
	*/
	modulepar {UInt32 PX_SPI := 1}
	
	/*
	/*
	 * @desc Key for integrity vc_sad[c_saRes]
	 * @desc Key for integrity vc_sad[c_saRes]
	*/
	*/
+7 −217
Original line number Original line Diff line number Diff line
@@ -401,59 +401,6 @@ module LibIpv6_Rfc3775Mipv6_Functions {
																vc_sad[c_saIni].seqNr,
																vc_sad[c_saIni].seqNr,
																v_espIpDatagram,
																v_espIpDatagram,
																c_mobileHdr))));
																c_mobileHdr))));
	
/*		if ( v_ret != e_success ) {return v_ret;}
		tc_ac.start;
		alt {
			//the test adapter process consists of decrypt and integrity check
			//TODO SMU replace vc_sad[c_saIni] with vc_sad[vc_sad.secParamsIndex]
			[]	ipPort.receive(mw_bindingAck_noData(
									c_routeHdr,
									p_haGlaNut,
									p_mnCoaTn,
									m_extHdrList_2Elem(
										mw_extHdr_routingHeader(	
											c_espHdr,
											c_routeHdrLen2,
											c_routeHdrType2,
											c_routeHdrSegmentsLeft1,
											m_routingHeaderData_homeAddress(p_mnHoaTn)),
										mw_extHdr_espHeader(
											vc_sad[c_saIni].securityParametersIndex,
											vc_sad[c_saIni].sequenceNumber + 1,
											m_plaintextData(
												m_extHdrList_1Elem(
													mw_extHdr_mobileHeader(
														c_noNextHdr,
														c_bindingAck,
														mw_bindingAckMsg(p_seqNr) ) ),
												omit),
											c_mobileHdr ) ) ) )-> value  v_ipv6Packet {
					tc_ac.stop;	
					v_ret := e_success ;
				}
			[]	ipPort.receive(mw_bindingAck_noData(	c_routeHdr,
													p_haGlaNut,
													p_mnCoaTn,
													m_extHdrList_2Elem(
													mw_extHdr_routingHeader(	c_mobileHdr,
																				c_routeHdrLen2,
																				c_routeHdrType2,
																				c_routeHdrSegmentsLeft1,
																				m_routingHeaderData_homeAddress(p_mnHoaTn)),
													mw_extHdr_mobileHeader (	c_noNextHdr,
																			c_bindingAck,
																			mw_bindingAckMsg(p_seqNr))))) {
					tc_ac.stop;	
					v_ret := e_error ;
					log("**** f_sendBindUpAndWaitForBindAckOffHome_espTunnelMode: ERROR: No encrypted message received **** ");
				}
			[]	tc_ac.timeout{
					v_ret :=  e_timeout;
					log("**** f_sendBindUpAndWaitForBindAckOffHome_espTunnelMode: ERROR: tc_ac.timeout **** ");
				}		
		} // end alt
*/
		return v_ret;
		return v_ret;


	}//end f_mnSendBindUpToHaAndWaitForBindAckOffHome_espTransportMode
	}//end f_mnSendBindUpToHaAndWaitForBindAckOffHome_espTransportMode
@@ -464,161 +411,7 @@ module LibIpv6_Rfc3775Mipv6_Functions {
	 * @param p_mnHoaTn Mobile Node Home Address of test node
	 * @param p_mnHoaTn Mobile Node Home Address of test node
	 * @param p_haGlaNut Home Agent Address of node under test
	 * @param p_haGlaNut Home Agent Address of node under test
	 * @param p_seqNr Seq Nr of Binding Update
	 * @param p_seqNr Seq Nr of Binding Update
 	 * @param p_timeUnits Lifetiem of Binding Update
 	 * @param p_timeUnits Lifetime of Binding Update
	*/
/*	function f_sendBindUpAndWaitForBindAckOffHome_espTransportMode(	in template Ipv6Address p_mnCoaTn,
													in template Ipv6Address p_mnHoaTn,
													in template Ipv6Address p_haGlaNut,
													in UInt16 p_seqNr,
													in UInt16 p_timeUnits)
	runs on LibIpv6Node
	return FncRetCode {
		var FncRetCode v_ret;
		var Ipv6Packet v_ipv6Packet;

		//Build espPayloadData
		var ModularIpv6Packet v_modularIpv6Packet := {
			ipv6Hdr := omit,
			extHdrList  := valueof(
				m_extHdrList_1Elem(
					m_extHdr_mobileHeader (
						c_noNextHdr,
						c_bindingUpdate,
						m_bindingUpdateMsg(
							p_seqNr,
							c_aFlag1,
							c_hFlag1,
							c_lFlag0,
							c_kFlag0,
							p_timeUnits,
							m_mobileOptList_2Elem(
								m_mobileOpt_padN(m_optPad2),
								m_mobileOpt_altCoa(m_mobileOptAltCoA(p_mnCoaTn)))))) ),
			ipv6Payload := omit
		}

		var EncryptResult v_encryptResult := fx_encryptModularIpPacket(
												e_transportMode,
												vc_sad[c_saIni].espEncryptionAlgo,
												vc_sad[c_saIni].espEncryptionKey,
												v_modularIpv6Packet);
		

		//Fill EspExtHdr
		var EspHeader_snd v_espHeader_snd :=  {
			// Header
			securityParametersIndex := vc_sad[c_saIni].securityParametersIndex,
			sequenceNumber := vc_sad[c_saIni].sequenceNumber,		
			// Payload
			iv := v_encryptResult.iv,
			espPayloadData := v_encryptResult.espPayloadData,
			tfcPadding := v_encryptResult.tfcPadding,
			// Trailer
			padding := omit,
			padLength := c_uInt8Zero,
			nextHdr := c_mobileHdr,
			icv := omit
		}

		var ExtensionHeader v_extHdr_espHeader := {espHeader_snd := v_espHeader_snd};

		v_espHeader_snd.icv := fx_integrityExtHdr(
									vc_sad[c_saIni].espIntegrityAlgo,
									vc_sad[c_saIni].espIntegrityKey,
									v_extHdr_espHeader);


		v_ret := f_sendGeneralIpv6(m_generalIpv6_extHdr(c_dstHdr,
														p_mnCoaTn,
														p_haGlaNut,
														m_extHdrList_2Elem(
															m_extHdr_dstOptHeader(	c_espHdr,
																					c_optLen2,
																					m_dstOptList_2Elem(
																						m_dstOpt_padN(m_optPad4),
																						m_dstOpt_homeAddr(p_mnHoaTn))),
															v_extHdr_espHeader)));
	
		if ( v_ret != e_success ) {return v_ret;}
		tc_ac.start;
		alt {
			[]	ipPort.receive(mw_generalIpv6_extHdr_noData(	c_routeHdr,
													p_haGlaNut,
													p_mnCoaTn,
													m_extHdrList_2Elem(
													mw_extHdr_routingHeader(	c_mobileHdr,
																				c_routeHdrLen2,
																				c_routeHdrType2,
																				c_routeHdrSegmentsLeft1,
																				m_routingHeaderData_homeAddress(p_mnHoaTn)),
													mw_extHdr_espHeader))) -> value  v_ipv6Packet {

					
				
														var DecryptedEspHeaderData v_decryptedEspHeaderData := fx_decryptEspPayload(
																			1,
																			2,
																			e_transportMode,
																			vc_sad[c_saIni].espEncryptionAlgo,
																			vc_sad[c_saIni].espEncryptionKey,
																			v_ipv6Packet.extHdrList[1].espHeader_rcv.espHeaderData );
				//	fx_match( valueof(mw_extHdr_mobileHeader(
				//							c_noNextHdr,
				//							c_bindingAck,
				//							mw_bindingAckMsg(p_seqNr))),
				//			v_decryptedEspHeaderData.espPayloadData) ;
				//Check concept: encode (message), then compare with received octetstring
					
					tc_ac.stop;	
					v_ret := e_success ;
				}
			[]	ipPort.receive(mw_bindingAck_noData(	c_routeHdr,
													p_haGlaNut,
													p_mnCoaTn,
													m_extHdrList_2Elem(
													mw_extHdr_routingHeader(	c_mobileHdr,
																				c_routeHdrLen2,
																				c_routeHdrType2,
																				c_routeHdrSegmentsLeft1,
																				m_routingHeaderData_homeAddress(p_mnHoaTn)),
													mw_extHdr_mobileHeader (	c_noNextHdr,
																			c_bindingAck,
																			mw_bindingAckMsg(p_seqNr))))) {
					tc_ac.stop;	
					v_ret := e_success ;
				}
			[]	tc_ac.timeout{
					v_ret :=  e_timeout;
					log("**** f_sendBindUpAndWaitForBindAckOffHome_espTunnelMode: ERROR: tc_ac.timeout **** ");
				}		
		} // end alt

		return v_ret;


		//Test trial with payload to encrypt
		var Ipv6Packet v_dhaadReq := valueof(m_dhaadReq(c_16ZeroBytes,c_16ZeroBytes,c_uInt16Zero));
		var Ipv6Payload v_dhaadReqMsg := v_dhaadReq.ipv6Payload;

		//Build espPayloadData
		v_modularIpv6Packet := {
			ipv6Hdr := omit,
			extHdrList  := omit,
			ipv6Payload := v_dhaadReqMsg
		}

	}//end f_sendBindUpAndWaitForBindAckOffHome_espTunnelMode

	*/


	/*
	 * @desc  Test Node is Off Home and sends BindUpdate and waits for Binding Ack
	 * @param p_mnCoaTn Mobile Node Care Of Address of test node
	 * @param p_mnHoaTn Mobile Node Home Address of test node
	 * @param p_haGlaNut Home Agent Address of node under test
	 * @param p_seqNr Seq Nr of Binding Update
 	 * @param p_timeUnits Lifetiem of Binding Update
	*/
	*/
	function f_mnSendBindUpToCnAndWaitForBindAckOffHome(
	function f_mnSendBindUpToCnAndWaitForBindAckOffHome(
				in template Ipv6Address p_mnCoaTn,
				in template Ipv6Address p_mnCoaTn,
@@ -668,7 +461,6 @@ module LibIpv6_Rfc3775Mipv6_Functions {
													mw_extHdr_mobileHeader (	c_noNextHdr,
													mw_extHdr_mobileHeader (	c_noNextHdr,
																			c_bindingAck,
																			c_bindingAck,
																			mw_bindingAckMsg(p_seqNr))))) {
																			mw_bindingAckMsg(p_seqNr))))) {
					//TODO SMU check on authenticator
					tc_ac.stop;	
					tc_ac.stop;	
					v_ret := e_success ;
					v_ret := e_success ;
				}
				}
@@ -713,7 +505,7 @@ module LibIpv6_Rfc3775Mipv6_Functions {
																								m_mobileOptList_5Elem(
																								m_mobileOptList_5Elem(
																									m_mobileOpt_padN(m_optPad2),
																									m_mobileOpt_padN(m_optPad2),
																									m_mobileOpt_altCoa(m_altCoA(p_mnHoaTn)),
																									m_mobileOpt_altCoa(m_altCoA(p_mnHoaTn)),
																									m_mobileOpt_nonceIndices(m_mobileOptNonceIndices_dummy), //TODO SMU+AB validate byte boundary. padding should not be needed here
																									m_mobileOpt_nonceIndices(m_mobileOptNonceIndices_dummy),
																									m_mobileOpt_padN(m_optPad4),
																									m_mobileOpt_padN(m_optPad4),
																									m_mobileOpt_bindingAuth(m_bindingAuthData_dummy)))))));
																									m_mobileOpt_bindingAuth(m_bindingAuthData_dummy)))))));
		if ( v_ret != e_success ) {return v_ret;}
		if ( v_ret != e_success ) {return v_ret;}
@@ -1177,7 +969,7 @@ module LibIpv6_Rfc3775Mipv6_Functions {


group mobileSecurityFns {
group mobileSecurityFns {


	function f_createKbm(out Oct20 p_kbm) //TODO SMU should be creatMnSimuKbm
	function f_createKbm(out Oct20 p_kbm)
	runs on LibIpv6Node
	runs on LibIpv6Node
	return FncRetCode {
	return FncRetCode {


@@ -1187,11 +979,10 @@ group mobileSecurityFns {
		}
		}


		p_kbm := fx_mac(
		p_kbm := fx_mac(
					e_auth_sha1_96/*e_sha1_96*/,
					e_auth_sha1_96,
					c_1ZeroByte,
					c_1ZeroByte,
					bit2oct(vc_mobileSec.mnSimuParams.receivedHomeKeygenToken)
					bit2oct(vc_mobileSec.mnSimuParams.receivedHomeKeygenToken)
					& bit2oct(vc_mobileSec.mnSimuParams.receivedCareOfKeygenToken) ) ;
					& bit2oct(vc_mobileSec.mnSimuParams.receivedCareOfKeygenToken) ) ;
       //TODO SMU+ DTE check if truncate to 20 octet is needed
       return e_success;
       return e_success;


	}//end function f_createKbm
	}//end function f_createKbm
@@ -2313,7 +2104,6 @@ group mobileSecurityFns {
		var HomeAgentAddressDiscoveryRequest v_dhaadReq;
		var HomeAgentAddressDiscoveryRequest v_dhaadReq;
		var Ipv6Packet v_ipv6Packet ;
		var Ipv6Packet v_ipv6Packet ;


		//TODO: remove this
		[]	ipPort.receive(mw_dhaadReq(?, ?)) -> value v_dhaadReq {
		[]	ipPort.receive(mw_dhaadReq(?, ?)) -> value v_dhaadReq {
			f_sendHaAddrDrep(
			f_sendHaAddrDrep(
				m_dhaadRep(p_paramsHa.gla, p_paramsIut.mnCoa, v_dhaadReq.ipv6Payload.homeAgentAddrDiscRequestMsg.identifier));
				m_dhaadRep(p_paramsHa.gla, p_paramsIut.mnCoa, v_dhaadReq.ipv6Payload.homeAgentAddrDiscRequestMsg.identifier));
@@ -2941,8 +2731,8 @@ group mobileSecurityFns {
				p_paramsHa.gla,
				p_paramsHa.gla,
				m_extHdrList_1Elem (					
				m_extHdrList_1Elem (					
					mw_extHdr_espHeader(
					mw_extHdr_espHeader(
						vc_sad[c_saRrpIn].spi,//vc_sad[c_saIni].spi, //FIXME
						vc_sad[c_saRrpIn].spi,
						?,//vc_sad[c_saIni].seqNr + 1, //FIXME
						?,
						m_espIpDatagram (
						m_espIpDatagram (
							m_extHdrList_2Elem(
							m_extHdrList_2Elem(
								mw_extHdr_tunneledHeader (
								mw_extHdr_tunneledHeader (
Loading