Added CN deregistration in postamble (b21932e1) · Commits · TTCN-3 Libraries / LibIPv6

ttcn3/EtsiLibrary/LibIpv6/LibMobility/LibIpv6_Rfc3775Mipv6_Functions.ttcn

+433 −187

Original line number	Diff line number	Diff line
		@@ -848,7 +848,7 @@ module LibIpv6_Rfc3775Mipv6_Functions {
		var Ipv6Address v_receivedTargetAddr := c_16ZeroBytes;
		var Ipv6Address v_receivedSrcAddr := c_16ZeroBytes;
		var NeighborSolicitation v_nbrSol ;
		//var default localDef := activate(a_receiveBindingUpdateAndReplyAtHome(p_paramsHa, p_paramsIut));
		var default localDef := activate(a_receiveBindingUpdateAndReplyAtHome(p_paramsHa, p_paramsIut));

		tc_loop.start;
		//tc_ac.start;
		@@ -867,12 +867,233 @@ module LibIpv6_Rfc3775Mipv6_Functions {
		}
		}

		//1st alternative: m_optPad2 + Coa
		[] ipPort.receive (
		// //1st alternative: m_optPad2 + Coa
		// [] ipPort.receive (
		// mw_bindingUpdate_srcDst (
		// c_dstHdr,
		// p_paramsIut.mnHoa,
		// p_paramsHa.gla,
		// m_extHdrList_2Elem (
		// m_extHdr_dstOptHeader (
		// c_mobileHdr,
		// c_optLen2,
		// m_dstOptList_2Elem (
		// m_dstOpt_padN(m_optPad4),
		// mw_dstOpt_homeAddr)),
		// mw_extHdr_mobileHeader (
		// c_noNextHdr,
		// c_bindingUpdate,
		// mw_bindingUpdateMsg (
		// c_aFlag1,
		// c_hFlag1,
		// ?, //c_lFlag0,
		// c_kFlag0,
		// m_mobileOptList_2Elem (
		// m_mobileOpt_padN(m_optPad2),
		// m_mobileOpt_altCoa(
		// m_altCoA(
		// p_paramsIut.mnHoa)))))))) -> value v_ipv6Packet {
		// //Get SeqNr
		// v_seqNr := v_ipv6Packet.extHdrList[1].mobileHeader.mobileMessage.bindingUpdateMsg.sequenceNumber;
		// //Get Lifetime
		// v_lifetime := v_ipv6Packet.extHdrList[1].mobileHeader.mobileMessage.bindingUpdateMsg.lifeTime;
		// v_ret := e_success;
		//
		// v_ret := f_sendBA (
		// m_bindingAck (
		// c_routeHdr,
		// p_paramsHa.gla,
		// p_paramsIut.mnHoa,
		// m_extHdrList_2Elem (
		// m_extHdr_routingHeader (
		// c_mobileHdr,
		// c_routeHdrLen2,
		// c_routeHdrType2,
		// c_routeHdrSegmentsLeft1,
		// m_routingHeaderData_homeAddress(p_paramsIut.mnHoa)),
		// m_extHdr_mobileHeader (
		// c_noNextHdr,
		// c_bindingAck,
		// m_bindingAckMsg(
		// v_seqNr,
		// v_lifetime,
		// m_mobileOptList_1Elem (
		// m_mobileOpt_padN(m_optPad4)))))));
		//
		// repeat;
		// }
		// //2nd alternative: m_optPad4
		// [] ipPort.receive (
		// mw_bindingUpdate_srcDst (
		// c_dstHdr,
		// p_paramsIut.mnHoa,
		// p_paramsHa.gla,
		// m_extHdrList_2Elem (
		// m_extHdr_dstOptHeader (
		// c_mobileHdr,
		// c_optLen2,
		// m_dstOptList_2Elem(
		// m_dstOpt_padN(m_optPad4),
		// mw_dstOpt_homeAddr)),
		// mw_extHdr_mobileHeader (
		// c_noNextHdr,
		// c_bindingUpdate,
		// mw_bindingUpdateMsg(
		// c_aFlag1,
		// c_hFlag1,
		// ?, //c_lFlag0,
		// c_kFlag0,
		// m_mobileOptList_1Elem(
		// m_mobileOpt_padN(m_optPad4))))))) -> value v_ipv6Packet {
		// //Get SeqNr
		// v_seqNr := v_ipv6Packet.extHdrList[1].mobileHeader.mobileMessage.bindingUpdateMsg.sequenceNumber;
		// //Get Lifetime
		// v_lifetime := v_ipv6Packet.extHdrList[1].mobileHeader.mobileMessage.bindingUpdateMsg.lifeTime;
		// v_ret := e_success;
		//
		// v_ret := f_sendBA (
		// m_bindingAck (
		// c_routeHdr,
		// p_paramsHa.gla,
		// p_paramsIut.mnHoa,
		// m_extHdrList_2Elem (
		// m_extHdr_routingHeader (
		// c_mobileHdr,
		// c_routeHdrLen2,
		// c_routeHdrType2,
		// c_routeHdrSegmentsLeft1,
		// m_routingHeaderData_homeAddress(p_paramsIut.mnHoa)),
		// m_extHdr_mobileHeader (
		// c_noNextHdr,
		// c_bindingAck,
		// m_bindingAckMsg(
		// v_seqNr,
		// v_lifetime,
		// m_mobileOptList_1Elem (
		// m_mobileOpt_padN(m_optPad4)))))));
		//
		// repeat;
		// }

		[] ipPort.receive(mw_nbrSol) -> value v_nbrSol{
		v_receivedSrcAddr := v_nbrSol.ipv6Hdr.sourceAddress ;
		v_receivedTargetAddr := v_nbrSol.ipv6Payload.nbrSolMsg.targetAddr ;
		if ( v_receivedTargetAddr == p_paramsIut.mnHoa
		or v_receivedTargetAddr == p_paramsIut.lla) {
		f_sendNbrAdv (m_nbrAdv_noExtHdr( p_paramsHa.lla,
		c_allNodesMca,
		c_rFlag0,
		c_sFlag0,
		c_oFlag0,
		v_receivedTargetAddr,
		m_nbrAdvOpt_tllaOpt(p_paramsHa.macUca) )) ;
		}
		else {
		if ( v_receivedTargetAddr == p_paramsHa.gla
		or v_receivedTargetAddr == p_paramsHa.lla) {
		f_sendNbrAdv (m_nbrAdv_noExtHdr( p_paramsHa.lla,
		c_allNodesMca,
		c_rFlag1,
		c_sFlag0,
		c_oFlag0,
		v_receivedTargetAddr,
		m_nbrAdvOpt_tllaOpt(p_paramsHa.macUca) )) ;
		}
		}

		repeat;
		}

		// TODO DTE add when TT compiler fix
		// [] a_receiveBindingUpdateAndReply(p_paramsHa.gla);
		// [] tc_ac.timeout {//Guard timer
		// v_ret:= e_timeout;
		// }
		}
		deactivate(localDef);
		return v_ret;
		}//end function f_sendRtAdvAndReplyBindUpAtHome


		/*
		* @desc Test Node is At Home and sends RtAdvertisements and waits for Binding Update
		* @param p_paramsHa All IPv6 parameters of Home Agent
		* @param p_paramsIut All IPv6 parameters of Node Under Test
		* @param p_paramsHa All IPv6 parameters of Correspondent Node
		* @param p_nrOfRtAdv Nr of RTadv to be sent by the Test Node
		*/
		function f_sendRtAdvAndReplyBindUpAtHomeAndUnbindCn( template Ipv6NodeParams p_paramsHa,
		template Ipv6NodeParams p_paramsIut,
		template Ipv6NodeParams p_paramsCn,
		UInt8 p_nrOfRtAdv)
		runs on Ipv6Node
		return FncRetCode {
		//Variables
		var FncRetCode v_ret := e_error;
		var UInt8 v_count := 0;
		var Ipv6Packet v_ipv6Packet;
		var UInt16 v_seqNr := 0;
		var UInt16 v_lifetime := 0;
		var Ipv6Address v_receivedTargetAddr := c_16ZeroBytes;
		var Ipv6Address v_receivedSrcAddr := c_16ZeroBytes;
		var NeighborSolicitation v_nbrSol ;
		var boolean v_hoaDeregistered := false;
		var boolean v_cnDeregistered := false;
		//var default localDef := activate(a_receiveBindingUpdateAndReplyAtHome(p_paramsHa, p_paramsIut));

		tc_loop.start;
		tc_ac.start;
		alt {
		[] tc_loop.timeout {
		f_sendMipRtAdvWithPrefix( p_paramsHa.lla,
		c_allNodesMca,
		p_paramsHa.prefixLength,
		p_paramsHa.gla,
		p_paramsHa.macUca ) ;
		tc_loop.stop;
		v_count := v_count + 1;
		if (v_count <= p_nrOfRtAdv) {
		tc_loop.start;
		}
		repeat;
		}


		[] ipPort.receive(mw_nbrSol) -> value v_nbrSol{
		v_receivedSrcAddr := v_nbrSol.ipv6Hdr.sourceAddress ;
		v_receivedTargetAddr := v_nbrSol.ipv6Payload.nbrSolMsg.targetAddr ;
		if ( v_receivedTargetAddr == p_paramsIut.mnHoa
		or v_receivedTargetAddr == p_paramsIut.lla) {
		f_sendNbrAdv (m_nbrAdv_noExtHdr( p_paramsHa.lla,
		c_allNodesMca,
		c_rFlag0,
		c_sFlag0,
		c_oFlag0,
		v_receivedTargetAddr,
		m_nbrAdvOpt_tllaOpt(p_paramsHa.macUca) )) ;
		}
		else {
		if ( v_receivedTargetAddr == p_paramsHa.gla
		or v_receivedTargetAddr == p_paramsHa.lla) {
		f_sendNbrAdv (m_nbrAdv_noExtHdr( p_paramsHa.lla,
		c_allNodesMca,
		c_rFlag1,
		c_sFlag0,
		c_oFlag0,
		v_receivedTargetAddr,
		m_nbrAdvOpt_tllaOpt(p_paramsHa.macUca) )) ;
		}
		}

		repeat;
		}

		// Standalone CN BU : m_optPad2 + AltCoa
		[v_hoaDeregistered == true] ipPort.receive (
		mw_bindingUpdate_srcDst (
		c_dstHdr,
		p_paramsIut.mnHoa,
		p_paramsHa.gla,
		p_paramsCn.gla,
		m_extHdrList_2Elem (
		m_extHdr_dstOptHeader (
		c_mobileHdr,
		@@ -884,50 +1105,33 @@ module LibIpv6_Rfc3775Mipv6_Functions {
		c_noNextHdr,
		c_bindingUpdate,
		mw_bindingUpdateMsg (
		c_aFlag1,
		c_hFlag1,
		?, //c_aFlag1,
		c_hFlag0,
		?, //c_lFlag0,
		c_kFlag0,
		m_mobileOptList_2Elem (
		m_mobileOptList_6Elem (
		m_mobileOpt_padN(m_optPad2),
		m_mobileOpt_altCoa(
		m_altCoA(
		p_paramsIut.mnHoa)))))))) -> value v_ipv6Packet {
		//Get SeqNr
		v_seqNr := v_ipv6Packet.extHdrList[1].mobileHeader.mobileMessage.bindingUpdateMsg.sequenceNumber;
		//Get Lifetime
		v_lifetime := v_ipv6Packet.extHdrList[1].mobileHeader.mobileMessage.bindingUpdateMsg.lifeTime;
		m_mobileOpt_altCoa(mw_altCoA_any),
		m_mobileOpt_padN(m_optPad2),
		m_mobileOpt_nonceIndices (
		m_mobileOptNonceIndices(
		vc_mobileSec.cnSimuParams.nonceIndex,//vc_mobileSec.mnSimuParams.receivedHomeNonceIndex,
		vc_mobileSec.cnSimuParams.nonceIndex)),//vc_mobileSec.mnSimuParams.receivedCareOfNonceIndex)),
		m_mobileOpt_padN(m_optPad2),
		m_mobileOpt_bindingAuth (
		mw_bindingAuthData))))))) -> value v_ipv6Packet {
		tc_ac.stop;
		tc_loop.stop;
		v_cnDeregistered := true;
		v_ret := e_success;

		v_ret := f_sendBA (
		m_bindingAck (
		c_routeHdr,
		p_paramsHa.gla,
		p_paramsIut.mnHoa,
		m_extHdrList_2Elem (
		m_extHdr_routingHeader (
		c_mobileHdr,
		c_routeHdrLen2,
		c_routeHdrType2,
		c_routeHdrSegmentsLeft1,
		m_routingHeaderData_homeAddress(p_paramsIut.mnHoa)),
		m_extHdr_mobileHeader (
		c_noNextHdr,
		c_bindingAck,
		m_bindingAckMsg(
		v_seqNr,
		v_lifetime,
		m_mobileOptList_1Elem (
		m_mobileOpt_padN(m_optPad4)))))));

		repeat;
		}
		//2nd alternative: m_optPad4
		[] ipPort.receive (

		//Standalone CN BU: no AltCoa
		[v_hoaDeregistered == true] ipPort.receive (
		mw_bindingUpdate_srcDst (
		c_dstHdr,
		p_paramsIut.mnHoa,
		p_paramsHa.gla,
		p_paramsCn.gla,
		m_extHdrList_2Elem (
		m_extHdr_dstOptHeader (
		c_mobileHdr,
		@@ -939,80 +1143,84 @@ module LibIpv6_Rfc3775Mipv6_Functions {
		c_noNextHdr,
		c_bindingUpdate,
		mw_bindingUpdateMsg(
		c_aFlag1,
		c_hFlag1,
		?, //c_aFlag1,
		c_hFlag0,
		?, //c_lFlag0,
		c_kFlag0,
		m_mobileOptList_1Elem(
		m_mobileOpt_padN(m_optPad4))))))) -> value v_ipv6Packet {
		//Get SeqNr
		v_seqNr := v_ipv6Packet.extHdrList[1].mobileHeader.mobileMessage.bindingUpdateMsg.sequenceNumber;
		//Get Lifetime
		v_lifetime := v_ipv6Packet.extHdrList[1].mobileHeader.mobileMessage.bindingUpdateMsg.lifeTime;
		m_mobileOptList_2Elem(
		m_mobileOpt_nonceIndices (
		m_mobileOptNonceIndices(
		vc_mobileSec.cnSimuParams.nonceIndex,//vc_mobileSec.mnSimuParams.receivedHomeNonceIndex,
		vc_mobileSec.cnSimuParams.nonceIndex)),//vc_mobileSec.mnSimuParams.receivedCareOfNonceIndex)),
		m_mobileOpt_bindingAuth (
		mw_bindingAuthData))))))) -> value v_ipv6Packet {
		tc_ac.stop;
		tc_loop.stop;
		v_cnDeregistered := true;
		v_ret := e_success;
		}

		v_ret := f_sendBA (
		m_bindingAck (
		c_routeHdr,
		p_paramsHa.gla,
		// HoTI
		[v_hoaDeregistered == true] ipPort.receive (
		mw_homeTestInit_noData (
		c_mobileHdr,
		p_paramsIut.mnHoa,
		m_extHdrList_2Elem (
		m_extHdr_routingHeader (
		p_paramsCn.gla,
		m_extHdrList_1Elem (
		mw_extHdr_mobileHeader (
		c_noNextHdr,
		c_homeTestInit,
		mw_hoti) ) ) ) -> value v_ipv6Packet {
		vc_mobileSec.cnSimuParams.receivedHomeInitCookie :=
		v_ipv6Packet.extHdrList[0].mobileHeader.mobileMessage.homeTestInitMsg.homeInitCookie;
		vc_mobileSec.cnSimuParams.homeKeygenToken :=
		f_createHomeKeygenToken(
		vc_mobileSec.cnSimuParams.kcnList[vc_mobileSec.cnSimuParams.nonceIndex],
		valueof(p_paramsIut.mnHoa),
		vc_mobileSec.cnSimuParams.nonceList[vc_mobileSec.cnSimuParams.nonceIndex]);

		v_ret := f_sendHot (
		m_homeTest (
		c_mobileHdr,
		c_routeHdrLen2,
		c_routeHdrType2,
		c_routeHdrSegmentsLeft1,
		m_routingHeaderData_homeAddress(p_paramsIut.mnHoa)),
		p_paramsCn.gla,
		p_paramsIut.mnHoa,
		m_extHdrList_1Elem (
		m_extHdr_mobileHeader (
		c_noNextHdr,
		c_bindingAck,
		m_bindingAckMsg(
		v_seqNr,
		v_lifetime,
		m_mobileOptList_1Elem (
		m_mobileOpt_padN(m_optPad4)))))));

		c_homeTest,
		m_hot (
		vc_mobileSec.cnSimuParams.nonceIndex,
		vc_mobileSec.cnSimuParams.receivedHomeInitCookie,
		vc_mobileSec.cnSimuParams.homeKeygenToken ) ) ) ) );
		repeat;
		}

		[] ipPort.receive(mw_nbrSol) -> value v_nbrSol{
		v_receivedSrcAddr := v_nbrSol.ipv6Hdr.sourceAddress ;
		v_receivedTargetAddr := v_nbrSol.ipv6Payload.nbrSolMsg.targetAddr ;
		if ( v_receivedTargetAddr == p_paramsIut.mnHoa
		or v_receivedTargetAddr == p_paramsIut.lla) {
		f_sendNbrAdv (m_nbrAdv_noExtHdr( p_paramsHa.lla,
		c_allNodesMca,
		c_rFlag0,
		c_sFlag0,
		c_oFlag0,
		v_receivedTargetAddr,
		m_nbrAdvOpt_tllaOpt(p_paramsHa.macUca) )) ;
		// TODO DTE add when TT compiler fix
		[] a_receiveBindingUpdateAndReplyAtHome(p_paramsHa, p_paramsIut){
		tc_ac.stop;
		v_hoaDeregistered := true;
		tc_ac.start;
		repeat;
		}
		else {
		if ( v_receivedTargetAddr == p_paramsHa.gla
		or v_receivedTargetAddr == p_paramsHa.lla) {
		f_sendNbrAdv (m_nbrAdv_noExtHdr( p_paramsHa.lla,
		c_allNodesMca,
		c_rFlag1,
		c_sFlag0,
		c_oFlag0,
		v_receivedTargetAddr,
		m_nbrAdvOpt_tllaOpt(p_paramsHa.macUca) )) ;
		[] tc_ac.timeout {//Guard timer
		v_ret:= e_timeout;
		}

		}

		repeat;
		if(v_hoaDeregistered == false) {
		log("** f_sendRtAdvAndReplyBindUpAtHomeAndUnbindCn: ERROR: Home Address not correctly deregistered ** ");
		v_ret := e_error;
		}

		// TODO DTE add when TT compiler fix
		// [] a_receiveBindingUpdateAndReply(p_paramsHa.gla);
		// [] tc_ac.timeout {//Guard timer
		// v_ret:= e_timeout;
		// }
		if(v_cnDeregistered == false) {
		log("** f_sendRtAdvAndReplyBindUpAtHomeAndUnbindCn: WARNING: Correspondent Node not correctly deregistered ** ");
		v_ret := e_error;
		}

		// deactivate(localDef);
		return v_ret;
		}//end function f_sendRtAdvAndReplyBindUpAtHome
		}//end function f_sendRtAdvAndReplyBindUpAtHomeAndUnbindCn


		}//end group bindingFns
		@@ -1839,9 +2047,8 @@ group mobileSecurityFns {
		* @param p_paramsTn All IP params of test node
		* @param p_paramsIut All IP params of node under test
		*/
		altstep a_receiveBindingUpdateAndReplyAtHome( in template Ipv6NodeParams p_paramsTn,
		altstep a_receiveBindingUpdateAndReplyAtHome( in template Ipv6NodeParams p_paramsHa,
		in template Ipv6NodeParams p_paramsIut
		//in template Ipv6Address p_haGlaTn
		)
		runs on Ipv6Node {
		//Variables
		@@ -1856,40 +2063,60 @@ group mobileSecurityFns {
		[] ipPort.receive(mw_nbrSol_addressDetermination(p_paramsIut.solNodeMca, ?)) -> value v_nbrSol{
		v_receivedTargetAddr := v_nbrSol.ipv6Payload.nbrSolMsg.targetAddr ;

		f_sendNbrAdv (m_nbrAdv_noExtHdr( p_paramsTn.lla,
		f_sendNbrAdv (m_nbrAdv_noExtHdr( p_paramsHa.lla,
		c_allNodesMca,
		c_rFlag0,
		c_sFlag0,
		c_oFlag0,
		v_receivedTargetAddr,
		m_nbrAdvOpt_tllaOpt(p_paramsTn.macUca) )) ;
		m_nbrAdvOpt_tllaOpt(p_paramsHa.macUca) )) ;
		repeat;
		}

		//1st alternative: m_optPad2 + Coa
		[] ipPort.receive(mw_bindingUpdate_dst( c_mobileHdr,
		p_paramsTn.gla,//p_haGlaTn,
		m_extHdrList_1Elem(
		mw_extHdr_mobileHeader (c_noNextHdr,
		[] ipPort.receive (
		mw_bindingUpdate_srcDst (
		c_dstHdr,
		p_paramsIut.mnHoa,
		p_paramsHa.gla,
		m_extHdrList_2Elem (
		m_extHdr_dstOptHeader (
		c_mobileHdr,
		c_optLen2,
		m_dstOptList_2Elem (
		m_dstOpt_padN(m_optPad4),
		mw_dstOpt_homeAddr)),
		mw_extHdr_mobileHeader (
		c_noNextHdr,
		c_bindingUpdate,
		mw_bindingUpdateMsg(c_aFlag1,
		mw_bindingUpdateMsg (
		c_aFlag1,
		c_hFlag1,
		c_lFlag0,
		?, //c_lFlag0,
		c_kFlag0,
		m_mobileOptList_2Elem (
		m_mobileOpt_padN(m_optPad2),
		m_mobileOpt_altCoa(mw_altCoA_any))))))) -> value v_ipv6Packet {
		m_mobileOpt_altCoa(
		m_altCoA(
		p_paramsIut.mnHoa)))))))) -> value v_ipv6Packet {
		//Get SeqNr
		v_seqNr := v_ipv6Packet.extHdrList[0].mobileHeader.mobileMessage.bindingUpdateMsg.sequenceNumber;
		v_seqNr := v_ipv6Packet.extHdrList[1].mobileHeader.mobileMessage.bindingUpdateMsg.sequenceNumber;
		//Get Lifetime
		v_lifetime := v_ipv6Packet.extHdrList[0].mobileHeader.mobileMessage.bindingUpdateMsg.lifeTime;
		//Get HomeAddress
		v_mnHomeAddr := v_ipv6Packet.ipv6Hdr.sourceAddress;
		//TODO SMU read v_mnCareOfAddr from MobileOptions
		v_lifetime := v_ipv6Packet.extHdrList[1].mobileHeader.mobileMessage.bindingUpdateMsg.lifeTime;
		v_ret := e_success;
		v_ret := f_sendBA(m_bindingAck( c_mobileHdr,
		p_paramsTn.gla,//p_haGlaTn,
		v_mnHomeAddr,
		m_extHdrList_1Elem(

		v_ret := f_sendBA (
		m_bindingAck (
		c_routeHdr,
		p_paramsHa.gla,
		p_paramsIut.mnHoa,
		m_extHdrList_2Elem (
		m_extHdr_routingHeader (
		c_mobileHdr,
		c_routeHdrLen2,
		c_routeHdrType2,
		c_routeHdrSegmentsLeft1,
		m_routingHeaderData_homeAddress(p_paramsIut.mnHoa)),
		m_extHdr_mobileHeader (
		c_noNextHdr,
		c_bindingAck,
		@@ -1898,31 +2125,50 @@ group mobileSecurityFns {
		v_lifetime,
		m_mobileOptList_1Elem (
		m_mobileOpt_padN(m_optPad4)))))));
		repeat;
		//repeat;
		}

		//2nd alternative: m_optPad4
		[] ipPort.receive(mw_bindingUpdate_dst( c_mobileHdr,
		p_paramsTn.gla,//p_haGlaTn,
		m_extHdrList_1Elem(
		mw_extHdr_mobileHeader (c_noNextHdr,
		[] ipPort.receive (
		mw_bindingUpdate_srcDst (
		c_dstHdr,
		p_paramsIut.mnHoa,
		p_paramsHa.gla,
		m_extHdrList_2Elem (
		m_extHdr_dstOptHeader (
		c_mobileHdr,
		c_optLen2,
		m_dstOptList_2Elem(
		m_dstOpt_padN(m_optPad4),
		mw_dstOpt_homeAddr)),
		mw_extHdr_mobileHeader (
		c_noNextHdr,
		c_bindingUpdate,
		mw_bindingUpdateMsg(c_aFlag1,
		mw_bindingUpdateMsg(
		c_aFlag1,
		c_hFlag1,
		c_lFlag0,
		?, //c_lFlag0,
		c_kFlag0,
		m_mobileOptList_1Elem(
		m_mobileOpt_padN(m_optPad4))))))) -> value v_ipv6Packet {
		//Get SeqNr
		v_seqNr := v_ipv6Packet.extHdrList[0].mobileHeader.mobileMessage.bindingUpdateMsg.sequenceNumber;
		v_seqNr := v_ipv6Packet.extHdrList[1].mobileHeader.mobileMessage.bindingUpdateMsg.sequenceNumber;
		//Get Lifetime
		v_lifetime := v_ipv6Packet.extHdrList[0].mobileHeader.mobileMessage.bindingUpdateMsg.lifeTime;
		//Get HomeAddress
		v_mnHomeAddr := v_ipv6Packet.ipv6Hdr.sourceAddress;
		v_lifetime := v_ipv6Packet.extHdrList[1].mobileHeader.mobileMessage.bindingUpdateMsg.lifeTime;
		v_ret := e_success;
		v_ret := f_sendBA(m_bindingAck( c_mobileHdr,
		p_paramsTn.gla,//p_haGlaTn,
		v_mnHomeAddr,
		m_extHdrList_1Elem(

		v_ret := f_sendBA (
		m_bindingAck (
		c_routeHdr,
		p_paramsHa.gla,
		p_paramsIut.mnHoa,
		m_extHdrList_2Elem (
		m_extHdr_routingHeader (
		c_mobileHdr,
		c_routeHdrLen2,
		c_routeHdrType2,
		c_routeHdrSegmentsLeft1,
		m_routingHeaderData_homeAddress(p_paramsIut.mnHoa)),
		m_extHdr_mobileHeader (
		c_noNextHdr,
		c_bindingAck,
		@@ -1931,9 +2177,10 @@ group mobileSecurityFns {
		v_lifetime,
		m_mobileOptList_1Elem (
		m_mobileOpt_padN(m_optPad4)))))));
		repeat;
		//repeat;
		}


		}//end a_receiveBindingUpdateAndReplyAtHome

		/*
		@@ -1941,9 +2188,8 @@ group mobileSecurityFns {
		* @param p_paramsTn All IP params of test node
		* @param p_paramsIut All IP params of node under test
		*/
		altstep a_receiveBindingUpdateAndReplyOffHome(in template Ipv6NodeParams p_paramsTn,
		altstep a_receiveBindingUpdateAndReplyOffHome(in template Ipv6NodeParams p_paramsHa,
		template Ipv6NodeParams p_paramsIut
		//in template Ipv6Address p_haGlaTn
		)
		runs on Ipv6Node {
		//Variables
		@@ -1971,7 +2217,7 @@ group mobileSecurityFns {
		// }
		//1st alternative : m_optPad2 + Coa
		[] ipPort.receive(mw_bindingUpdate_dst( c_dstHdr,
		p_paramsTn.haGlas[0],//p_haGlaTn,
		p_paramsHa.gla,
		m_extHdrList_2Elem(
		m_extHdr_dstOptHeader(
		c_mobileHdr,
		@@ -2002,7 +2248,7 @@ group mobileSecurityFns {
		v_mnHomeAddr := v_ipv6Packet.extHdrList[0].destinationOptionHeader.destOptionList[1].homeAddressOption.homeAddress;
		v_ret := e_success ;
		v_ret := f_sendBA(m_bindingAck( c_routeHdr,
		p_paramsTn.haGlas[0],//p_haGlaTn,
		p_paramsHa.gla,
		v_mnCareOfAddr1,
		m_extHdrList_2Elem(
		m_extHdr_routingHeader(
		@@ -2023,7 +2269,7 @@ group mobileSecurityFns {
		}
		//2nd alternative : m_optPad4
		[] ipPort.receive(mw_bindingUpdate_dst( c_dstHdr,
		p_paramsTn.haGlas[0],//p_haGlaTn,
		p_paramsHa.gla,
		m_extHdrList_2Elem(
		m_extHdr_dstOptHeader(
		c_mobileHdr,
		@@ -2052,7 +2298,7 @@ group mobileSecurityFns {
		v_ret := e_success ;
		v_ret := f_sendBA(m_bindingAck(
		c_routeHdr,
		p_paramsTn.haGlas[0],//p_haGlaTn,
		p_paramsHa.gla,
		v_mnCareOfAddr1,
		m_extHdrList_2Elem(
		m_extHdr_routingHeader(