Loading ttcn3/EtsiLibrary/LibIpv6/LibCommonRfcs/LibIpv6_Interface_Functions.ttcn +2 −0 Original line number Diff line number Diff line Loading @@ -168,6 +168,8 @@ group rfc2460Root_Functions { v_activeIpv6Packet, v_activeIpv6Packet.extHdrList[i].espHeader, v_pseudoIpv6Packet); v_pseudoIpv6Packet.ipv6Hdr.destinationAddress := v_pseudoDstAddr; v_pseudoIpv6Packet.ipv6Hdr.sourceAddress := v_pseudoSrcAddr; if (v_ret == e_success) { f_setExtensionHeaders( v_pseudoIpv6Packet, v_pseudoIpv6Packet.ipv6Hdr.sourceAddress, Loading ttcn3/EtsiLibrary/LibIpv6/LibMobility/LibIpv6_Rfc3775Mipv6_Functions.ttcn +396 −11 Original line number Diff line number Diff line Loading @@ -1712,7 +1712,7 @@ group mobileSecurityFns { } //1st alternative: m_optPad2 + Coa [] ipPort.receive ( [PX_IP_SEC == e_securityOff] ipPort.receive ( mw_bindingUpdate_srcDst ( c_mobileHdr, p_paramsIut.mnHoa, Loading Loading @@ -1753,8 +1753,8 @@ group mobileSecurityFns { m_mobileOpt_padN(m_optPad4))))))); } //1st alternative: m_optPad2 + Coa [] ipPort.receive ( //1st alternative bis: m_optPad2 + Coa + HoADestOpt [PX_IP_SEC == e_securityOff] ipPort.receive ( mw_bindingUpdate_srcDst ( c_dstHdr, p_paramsIut.mnHoa, Loading Loading @@ -1808,7 +1808,7 @@ group mobileSecurityFns { } //2nd alternative: m_optPad4 [] ipPort.receive ( [PX_IP_SEC == e_securityOff] ipPort.receive ( mw_bindingUpdate_srcDst ( c_mobileHdr, p_paramsIut.mnHoa, Loading Loading @@ -1847,8 +1847,8 @@ group mobileSecurityFns { } //2nd alternative: m_optPad4 [] ipPort.receive ( //2nd alternative bis: m_optPad4 + HoADestOpt [PX_IP_SEC == e_securityOff] ipPort.receive ( mw_bindingUpdate_srcDst ( c_dstHdr, p_paramsIut.mnHoa, Loading Loading @@ -1898,6 +1898,248 @@ group mobileSecurityFns { m_mobileOpt_padN(m_optPad4))))))); } //1st alternative : m_optPad2 + Coa [PX_IP_SEC == e_securityOn] ipPort.receive ( mw_bindingUpdate_srcDst ( c_espHdr, p_paramsIut.mnHoa, p_paramsHa.gla, m_extHdrList_1Elem ( mw_extHdr_espHeader( vc_sad[c_saIn].spi, ?, //vc_sad[c_saIn].seqNr + 1, m_espIpDatagram ( m_extHdrList_1Elem( 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)))))), omit), c_mobileHdr)))) -> value v_ipv6Packet { //Get SeqNr v_seqNr := v_ipv6Packet.extHdrList[0].espHeader.espPayload.espIpDatagram.extHdrList[0].mobileHeader.mobileMessage.bindingUpdateMsg.sequenceNumber; //Get Lifetime v_lifetime := v_ipv6Packet.extHdrList[0].espHeader.espPayload.espIpDatagram.extHdrList[0].mobileHeader.mobileMessage.bindingUpdateMsg.lifeTime; v_ret := e_success; v_ret := f_sendBA ( m_bindingAck ( c_espHdr, p_paramsHa.gla, p_paramsIut.mnHoa, m_extHdrList_1Elem ( m_extHdr_espHeader( vc_sad[c_saOut].spi, vc_sad[c_saOut].seqNr + 1, m_espIpDatagram ( m_extHdrList_1Elem ( m_extHdr_mobileHeader ( c_noNextHdr, c_bindingAck, m_bindingAckMsg( v_seqNr, v_lifetime, m_mobileOptList_1Elem ( m_mobileOpt_padN(m_optPad4))))), omit), c_mobileHdr)))); } //1st alternative bis: m_optPad2 + Coa + HoADestOpt [PX_IP_SEC == e_securityOn] ipPort.receive ( mw_bindingUpdate_srcDst ( c_dstHdr, p_paramsIut.mnHoa, p_paramsHa.gla, m_extHdrList_2Elem ( m_extHdr_dstOptHeader ( c_espHdr, c_optLen2, m_dstOptList_2Elem( m_dstOpt_padN(m_optPad4), mw_dstOpt_homeAddr)), mw_extHdr_espHeader( vc_sad[c_saIn].spi, ?, //vc_sad[c_saIn].seqNr + 1, m_espIpDatagram ( m_extHdrList_1Elem( 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)))))), omit), c_mobileHdr)))) -> value v_ipv6Packet { //Get SeqNr v_seqNr := v_ipv6Packet.extHdrList[1].espHeader.espPayload.espIpDatagram.extHdrList[0].mobileHeader.mobileMessage.bindingUpdateMsg.sequenceNumber; //Get Lifetime v_lifetime := v_ipv6Packet.extHdrList[1].espHeader.espPayload.espIpDatagram.extHdrList[0].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_espHdr, c_routeHdrLen2, c_routeHdrType2, c_routeHdrSegmentsLeft1, m_routingHeaderData_homeAddress(p_paramsIut.mnHoa)), m_extHdr_espHeader( vc_sad[c_saOut].spi, vc_sad[c_saOut].seqNr + 1, m_espIpDatagram ( m_extHdrList_1Elem ( m_extHdr_mobileHeader ( c_noNextHdr, c_bindingAck, m_bindingAckMsg( v_seqNr, v_lifetime, m_mobileOptList_1Elem ( m_mobileOpt_padN(m_optPad4))))), omit), c_mobileHdr)))); } //2nd alternative : m_optPad4 [PX_IP_SEC == e_securityOn] ipPort.receive ( mw_bindingUpdate_srcDst ( c_espHdr, p_paramsIut.mnHoa, p_paramsHa.gla, m_extHdrList_1Elem ( mw_extHdr_espHeader( vc_sad[c_saIn].spi, ?, //vc_sad[c_saIn].seqNr + 1, m_espIpDatagram ( m_extHdrList_1Elem( 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))))), omit), c_mobileHdr)))) -> value v_ipv6Packet { //Get SeqNr v_seqNr := v_ipv6Packet.extHdrList[0].espHeader.espPayload.espIpDatagram.extHdrList[0].mobileHeader.mobileMessage.bindingUpdateMsg.sequenceNumber; //Get Lifetime v_lifetime := v_ipv6Packet.extHdrList[0].espHeader.espPayload.espIpDatagram.extHdrList[0].mobileHeader.mobileMessage.bindingUpdateMsg.lifeTime; v_ret := e_success; v_ret := f_sendBA ( m_bindingAck ( c_espHdr, p_paramsHa.gla, p_paramsIut.mnHoa, m_extHdrList_1Elem ( m_extHdr_espHeader( vc_sad[c_saOut].spi, vc_sad[c_saOut].seqNr + 1, m_espIpDatagram ( m_extHdrList_1Elem ( m_extHdr_mobileHeader ( c_noNextHdr, c_bindingAck, m_bindingAckMsg( v_seqNr, v_lifetime, m_mobileOptList_1Elem ( m_mobileOpt_padN(m_optPad4))))), omit), c_mobileHdr)))); } //2nd alternative bis: m_optPad4 + HoADestOpt [PX_IP_SEC == e_securityOn] ipPort.receive ( mw_bindingUpdate_srcDst ( c_dstHdr, p_paramsIut.mnHoa, p_paramsHa.gla, m_extHdrList_2Elem ( m_extHdr_dstOptHeader ( c_espHdr, c_optLen2, m_dstOptList_2Elem( m_dstOpt_padN(m_optPad4), mw_dstOpt_homeAddr)), mw_extHdr_espHeader( vc_sad[c_saIn].spi, ?, //vc_sad[c_saIn].seqNr + 1, m_espIpDatagram ( m_extHdrList_1Elem( 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))))), omit), c_mobileHdr)))) -> value v_ipv6Packet { //Get SeqNr v_seqNr := v_ipv6Packet.extHdrList[1].espHeader.espPayload.espIpDatagram.extHdrList[0].mobileHeader.mobileMessage.bindingUpdateMsg.sequenceNumber; //Get Lifetime v_lifetime := v_ipv6Packet.extHdrList[1].espHeader.espPayload.espIpDatagram.extHdrList[0].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_espHdr, c_routeHdrLen2, c_routeHdrType2, c_routeHdrSegmentsLeft1, m_routingHeaderData_homeAddress(p_paramsIut.mnHoa)), m_extHdr_espHeader( vc_sad[c_saOut].spi, vc_sad[c_saOut].seqNr + 1, m_espIpDatagram ( m_extHdrList_1Elem ( m_extHdr_mobileHeader ( c_noNextHdr, c_bindingAck, m_bindingAckMsg( v_seqNr, v_lifetime, m_mobileOptList_1Elem ( m_mobileOpt_padN(m_optPad4))))), omit), c_mobileHdr)))); } }//end a_haReceiveBindingUpdateAndReplyAtHome Loading Loading @@ -1928,7 +2170,7 @@ group mobileSecurityFns { } //1st alternative: m_optPad2 + Coa [] ipPort.receive ( [PX_IP_SEC == e_securityOff] ipPort.receive ( mw_bindingUpdate_dst ( c_dstHdr, p_paramsHa.gla, Loading Loading @@ -1984,7 +2226,7 @@ group mobileSecurityFns { } //2nd alternative: m_optPad4 [] ipPort.receive ( [PX_IP_SEC == e_securityOff] ipPort.receive ( mw_bindingUpdate_dst ( c_dstHdr, p_paramsHa.gla, Loading Loading @@ -2038,6 +2280,147 @@ group mobileSecurityFns { m_mobileOpt_padN(m_optPad4))))))); } //1st alternative: m_optPad2 + Coa [PX_IP_SEC == e_securityOn] ipPort.receive ( mw_bindingUpdate_dst ( c_dstHdr, p_paramsHa.gla, m_extHdrList_2Elem ( m_extHdr_dstOptHeader ( c_espHdr, c_optLen2, m_dstOptList_2Elem( m_dstOpt_padN(m_optPad4), mw_dstOpt_homeAddr)), mw_extHdr_espHeader( vc_sad[c_saIn].spi, ?, //vc_sad[c_saIn].seqNr + 1, m_espIpDatagram ( m_extHdrList_1Elem( 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(mw_altCoA_any))))), omit), c_mobileHdr)))) -> value v_ipv6Packet { //Get SeqNr v_seqNr := v_ipv6Packet.extHdrList[1].espHeader.espPayload.espIpDatagram.extHdrList[0].mobileHeader.mobileMessage.bindingUpdateMsg.sequenceNumber; //Get Lifetime v_lifetime := v_ipv6Packet.extHdrList[1].espHeader.espPayload.espIpDatagram.extHdrList[0].mobileHeader.mobileMessage.bindingUpdateMsg.lifeTime; //Get CareOfAddress v_mnCareOfAddr := v_ipv6Packet.ipv6Hdr.sourceAddress; //GetHomeAddress v_mnHomeAddr := v_ipv6Packet.extHdrList[0].destinationOptionHeader.destOptionList[1].homeAddressOption.homeAddress; v_ret := e_success; v_ret := f_sendBA ( m_bindingAck ( c_routeHdr, p_paramsHa.gla, v_mnCareOfAddr, m_extHdrList_2Elem ( m_extHdr_routingHeader ( c_espHdr, c_routeHdrLen2, c_routeHdrType2, c_routeHdrSegmentsLeft1, m_routingHeaderData_homeAddress(v_mnHomeAddr)), m_extHdr_espHeader( vc_sad[c_saOut].spi, vc_sad[c_saOut].seqNr + 1, m_espIpDatagram ( m_extHdrList_1Elem ( m_extHdr_mobileHeader ( c_noNextHdr, c_bindingAck, m_bindingAckMsg_status( p_status, v_seqNr, v_lifetime, m_mobileOptList_1Elem ( m_mobileOpt_padN(m_optPad4))))), omit), c_mobileHdr)))); } // 2nd alternative: m_optPad4 [PX_IP_SEC == e_securityOn] ipPort.receive ( mw_bindingUpdate_dst ( c_dstHdr, p_paramsHa.gla, m_extHdrList_2Elem ( m_extHdr_dstOptHeader ( c_espHdr, c_optLen2, m_dstOptList_2Elem( m_dstOpt_padN(m_optPad4), mw_dstOpt_homeAddr)), mw_extHdr_espHeader( vc_sad[c_saIn].spi, ?, //vc_sad[c_saIn].seqNr + 1, m_espIpDatagram ( m_extHdrList_1Elem( 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))))), omit), c_mobileHdr)))) -> value v_ipv6Packet { //Get SeqNr v_seqNr := v_ipv6Packet.extHdrList[1].espHeader.espPayload.espIpDatagram.extHdrList[0].mobileHeader.mobileMessage.bindingUpdateMsg.sequenceNumber; //Get Lifetime v_lifetime := v_ipv6Packet.extHdrList[1].espHeader.espPayload.espIpDatagram.extHdrList[0].mobileHeader.mobileMessage.bindingUpdateMsg.lifeTime; //Get CareOfAddress v_mnCareOfAddr := v_ipv6Packet.ipv6Hdr.sourceAddress; //GetHomeAddress v_mnHomeAddr := v_ipv6Packet.extHdrList[0].destinationOptionHeader.destOptionList[1].homeAddressOption.homeAddress; v_ret := e_success; v_ret := f_sendBA ( m_bindingAck ( c_routeHdr, p_paramsHa.gla, v_mnCareOfAddr, m_extHdrList_2Elem ( m_extHdr_routingHeader ( c_espHdr, c_routeHdrLen2, c_routeHdrType2, c_routeHdrSegmentsLeft1, m_routingHeaderData_homeAddress(v_mnHomeAddr)), m_extHdr_espHeader( vc_sad[c_saOut].spi, vc_sad[c_saOut].seqNr + 1, m_espIpDatagram ( m_extHdrList_1Elem ( m_extHdr_mobileHeader ( c_noNextHdr, c_bindingAck, m_bindingAckMsg_status( p_status, v_seqNr, v_lifetime, m_mobileOptList_1Elem ( m_mobileOpt_padN(m_optPad4))))), omit), c_mobileHdr)))); } }//end a_haReceiveBindingUpdateAndReplyOffHome /* Loading Loading @@ -2400,7 +2783,8 @@ group mobileSecurityFns { //Variables var Ipv6Packet v_ipv6Packet; [PX_IP_SEC == e_securityOn] ipPort.receive ( // FIXME Alex [/*PX_IP_SEC == e_securityOn*/] ipPort.receive ( mw_homeTestInit_noData ( c_tunneledIpHdr, p_paramsIut.mnCoa, Loading Loading @@ -2431,7 +2815,8 @@ group mobileSecurityFns { } [PX_IP_SEC == e_securityOff] ipPort.receive ( // FIXME Alex [/*PX_IP_SEC == e_securityOff*/] ipPort.receive ( mw_homeTestInit_noData ( c_tunneledIpHdr, p_paramsIut.mnCoa, Loading Loading
ttcn3/EtsiLibrary/LibIpv6/LibCommonRfcs/LibIpv6_Interface_Functions.ttcn +2 −0 Original line number Diff line number Diff line Loading @@ -168,6 +168,8 @@ group rfc2460Root_Functions { v_activeIpv6Packet, v_activeIpv6Packet.extHdrList[i].espHeader, v_pseudoIpv6Packet); v_pseudoIpv6Packet.ipv6Hdr.destinationAddress := v_pseudoDstAddr; v_pseudoIpv6Packet.ipv6Hdr.sourceAddress := v_pseudoSrcAddr; if (v_ret == e_success) { f_setExtensionHeaders( v_pseudoIpv6Packet, v_pseudoIpv6Packet.ipv6Hdr.sourceAddress, Loading
ttcn3/EtsiLibrary/LibIpv6/LibMobility/LibIpv6_Rfc3775Mipv6_Functions.ttcn +396 −11 Original line number Diff line number Diff line Loading @@ -1712,7 +1712,7 @@ group mobileSecurityFns { } //1st alternative: m_optPad2 + Coa [] ipPort.receive ( [PX_IP_SEC == e_securityOff] ipPort.receive ( mw_bindingUpdate_srcDst ( c_mobileHdr, p_paramsIut.mnHoa, Loading Loading @@ -1753,8 +1753,8 @@ group mobileSecurityFns { m_mobileOpt_padN(m_optPad4))))))); } //1st alternative: m_optPad2 + Coa [] ipPort.receive ( //1st alternative bis: m_optPad2 + Coa + HoADestOpt [PX_IP_SEC == e_securityOff] ipPort.receive ( mw_bindingUpdate_srcDst ( c_dstHdr, p_paramsIut.mnHoa, Loading Loading @@ -1808,7 +1808,7 @@ group mobileSecurityFns { } //2nd alternative: m_optPad4 [] ipPort.receive ( [PX_IP_SEC == e_securityOff] ipPort.receive ( mw_bindingUpdate_srcDst ( c_mobileHdr, p_paramsIut.mnHoa, Loading Loading @@ -1847,8 +1847,8 @@ group mobileSecurityFns { } //2nd alternative: m_optPad4 [] ipPort.receive ( //2nd alternative bis: m_optPad4 + HoADestOpt [PX_IP_SEC == e_securityOff] ipPort.receive ( mw_bindingUpdate_srcDst ( c_dstHdr, p_paramsIut.mnHoa, Loading Loading @@ -1898,6 +1898,248 @@ group mobileSecurityFns { m_mobileOpt_padN(m_optPad4))))))); } //1st alternative : m_optPad2 + Coa [PX_IP_SEC == e_securityOn] ipPort.receive ( mw_bindingUpdate_srcDst ( c_espHdr, p_paramsIut.mnHoa, p_paramsHa.gla, m_extHdrList_1Elem ( mw_extHdr_espHeader( vc_sad[c_saIn].spi, ?, //vc_sad[c_saIn].seqNr + 1, m_espIpDatagram ( m_extHdrList_1Elem( 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)))))), omit), c_mobileHdr)))) -> value v_ipv6Packet { //Get SeqNr v_seqNr := v_ipv6Packet.extHdrList[0].espHeader.espPayload.espIpDatagram.extHdrList[0].mobileHeader.mobileMessage.bindingUpdateMsg.sequenceNumber; //Get Lifetime v_lifetime := v_ipv6Packet.extHdrList[0].espHeader.espPayload.espIpDatagram.extHdrList[0].mobileHeader.mobileMessage.bindingUpdateMsg.lifeTime; v_ret := e_success; v_ret := f_sendBA ( m_bindingAck ( c_espHdr, p_paramsHa.gla, p_paramsIut.mnHoa, m_extHdrList_1Elem ( m_extHdr_espHeader( vc_sad[c_saOut].spi, vc_sad[c_saOut].seqNr + 1, m_espIpDatagram ( m_extHdrList_1Elem ( m_extHdr_mobileHeader ( c_noNextHdr, c_bindingAck, m_bindingAckMsg( v_seqNr, v_lifetime, m_mobileOptList_1Elem ( m_mobileOpt_padN(m_optPad4))))), omit), c_mobileHdr)))); } //1st alternative bis: m_optPad2 + Coa + HoADestOpt [PX_IP_SEC == e_securityOn] ipPort.receive ( mw_bindingUpdate_srcDst ( c_dstHdr, p_paramsIut.mnHoa, p_paramsHa.gla, m_extHdrList_2Elem ( m_extHdr_dstOptHeader ( c_espHdr, c_optLen2, m_dstOptList_2Elem( m_dstOpt_padN(m_optPad4), mw_dstOpt_homeAddr)), mw_extHdr_espHeader( vc_sad[c_saIn].spi, ?, //vc_sad[c_saIn].seqNr + 1, m_espIpDatagram ( m_extHdrList_1Elem( 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)))))), omit), c_mobileHdr)))) -> value v_ipv6Packet { //Get SeqNr v_seqNr := v_ipv6Packet.extHdrList[1].espHeader.espPayload.espIpDatagram.extHdrList[0].mobileHeader.mobileMessage.bindingUpdateMsg.sequenceNumber; //Get Lifetime v_lifetime := v_ipv6Packet.extHdrList[1].espHeader.espPayload.espIpDatagram.extHdrList[0].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_espHdr, c_routeHdrLen2, c_routeHdrType2, c_routeHdrSegmentsLeft1, m_routingHeaderData_homeAddress(p_paramsIut.mnHoa)), m_extHdr_espHeader( vc_sad[c_saOut].spi, vc_sad[c_saOut].seqNr + 1, m_espIpDatagram ( m_extHdrList_1Elem ( m_extHdr_mobileHeader ( c_noNextHdr, c_bindingAck, m_bindingAckMsg( v_seqNr, v_lifetime, m_mobileOptList_1Elem ( m_mobileOpt_padN(m_optPad4))))), omit), c_mobileHdr)))); } //2nd alternative : m_optPad4 [PX_IP_SEC == e_securityOn] ipPort.receive ( mw_bindingUpdate_srcDst ( c_espHdr, p_paramsIut.mnHoa, p_paramsHa.gla, m_extHdrList_1Elem ( mw_extHdr_espHeader( vc_sad[c_saIn].spi, ?, //vc_sad[c_saIn].seqNr + 1, m_espIpDatagram ( m_extHdrList_1Elem( 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))))), omit), c_mobileHdr)))) -> value v_ipv6Packet { //Get SeqNr v_seqNr := v_ipv6Packet.extHdrList[0].espHeader.espPayload.espIpDatagram.extHdrList[0].mobileHeader.mobileMessage.bindingUpdateMsg.sequenceNumber; //Get Lifetime v_lifetime := v_ipv6Packet.extHdrList[0].espHeader.espPayload.espIpDatagram.extHdrList[0].mobileHeader.mobileMessage.bindingUpdateMsg.lifeTime; v_ret := e_success; v_ret := f_sendBA ( m_bindingAck ( c_espHdr, p_paramsHa.gla, p_paramsIut.mnHoa, m_extHdrList_1Elem ( m_extHdr_espHeader( vc_sad[c_saOut].spi, vc_sad[c_saOut].seqNr + 1, m_espIpDatagram ( m_extHdrList_1Elem ( m_extHdr_mobileHeader ( c_noNextHdr, c_bindingAck, m_bindingAckMsg( v_seqNr, v_lifetime, m_mobileOptList_1Elem ( m_mobileOpt_padN(m_optPad4))))), omit), c_mobileHdr)))); } //2nd alternative bis: m_optPad4 + HoADestOpt [PX_IP_SEC == e_securityOn] ipPort.receive ( mw_bindingUpdate_srcDst ( c_dstHdr, p_paramsIut.mnHoa, p_paramsHa.gla, m_extHdrList_2Elem ( m_extHdr_dstOptHeader ( c_espHdr, c_optLen2, m_dstOptList_2Elem( m_dstOpt_padN(m_optPad4), mw_dstOpt_homeAddr)), mw_extHdr_espHeader( vc_sad[c_saIn].spi, ?, //vc_sad[c_saIn].seqNr + 1, m_espIpDatagram ( m_extHdrList_1Elem( 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))))), omit), c_mobileHdr)))) -> value v_ipv6Packet { //Get SeqNr v_seqNr := v_ipv6Packet.extHdrList[1].espHeader.espPayload.espIpDatagram.extHdrList[0].mobileHeader.mobileMessage.bindingUpdateMsg.sequenceNumber; //Get Lifetime v_lifetime := v_ipv6Packet.extHdrList[1].espHeader.espPayload.espIpDatagram.extHdrList[0].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_espHdr, c_routeHdrLen2, c_routeHdrType2, c_routeHdrSegmentsLeft1, m_routingHeaderData_homeAddress(p_paramsIut.mnHoa)), m_extHdr_espHeader( vc_sad[c_saOut].spi, vc_sad[c_saOut].seqNr + 1, m_espIpDatagram ( m_extHdrList_1Elem ( m_extHdr_mobileHeader ( c_noNextHdr, c_bindingAck, m_bindingAckMsg( v_seqNr, v_lifetime, m_mobileOptList_1Elem ( m_mobileOpt_padN(m_optPad4))))), omit), c_mobileHdr)))); } }//end a_haReceiveBindingUpdateAndReplyAtHome Loading Loading @@ -1928,7 +2170,7 @@ group mobileSecurityFns { } //1st alternative: m_optPad2 + Coa [] ipPort.receive ( [PX_IP_SEC == e_securityOff] ipPort.receive ( mw_bindingUpdate_dst ( c_dstHdr, p_paramsHa.gla, Loading Loading @@ -1984,7 +2226,7 @@ group mobileSecurityFns { } //2nd alternative: m_optPad4 [] ipPort.receive ( [PX_IP_SEC == e_securityOff] ipPort.receive ( mw_bindingUpdate_dst ( c_dstHdr, p_paramsHa.gla, Loading Loading @@ -2038,6 +2280,147 @@ group mobileSecurityFns { m_mobileOpt_padN(m_optPad4))))))); } //1st alternative: m_optPad2 + Coa [PX_IP_SEC == e_securityOn] ipPort.receive ( mw_bindingUpdate_dst ( c_dstHdr, p_paramsHa.gla, m_extHdrList_2Elem ( m_extHdr_dstOptHeader ( c_espHdr, c_optLen2, m_dstOptList_2Elem( m_dstOpt_padN(m_optPad4), mw_dstOpt_homeAddr)), mw_extHdr_espHeader( vc_sad[c_saIn].spi, ?, //vc_sad[c_saIn].seqNr + 1, m_espIpDatagram ( m_extHdrList_1Elem( 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(mw_altCoA_any))))), omit), c_mobileHdr)))) -> value v_ipv6Packet { //Get SeqNr v_seqNr := v_ipv6Packet.extHdrList[1].espHeader.espPayload.espIpDatagram.extHdrList[0].mobileHeader.mobileMessage.bindingUpdateMsg.sequenceNumber; //Get Lifetime v_lifetime := v_ipv6Packet.extHdrList[1].espHeader.espPayload.espIpDatagram.extHdrList[0].mobileHeader.mobileMessage.bindingUpdateMsg.lifeTime; //Get CareOfAddress v_mnCareOfAddr := v_ipv6Packet.ipv6Hdr.sourceAddress; //GetHomeAddress v_mnHomeAddr := v_ipv6Packet.extHdrList[0].destinationOptionHeader.destOptionList[1].homeAddressOption.homeAddress; v_ret := e_success; v_ret := f_sendBA ( m_bindingAck ( c_routeHdr, p_paramsHa.gla, v_mnCareOfAddr, m_extHdrList_2Elem ( m_extHdr_routingHeader ( c_espHdr, c_routeHdrLen2, c_routeHdrType2, c_routeHdrSegmentsLeft1, m_routingHeaderData_homeAddress(v_mnHomeAddr)), m_extHdr_espHeader( vc_sad[c_saOut].spi, vc_sad[c_saOut].seqNr + 1, m_espIpDatagram ( m_extHdrList_1Elem ( m_extHdr_mobileHeader ( c_noNextHdr, c_bindingAck, m_bindingAckMsg_status( p_status, v_seqNr, v_lifetime, m_mobileOptList_1Elem ( m_mobileOpt_padN(m_optPad4))))), omit), c_mobileHdr)))); } // 2nd alternative: m_optPad4 [PX_IP_SEC == e_securityOn] ipPort.receive ( mw_bindingUpdate_dst ( c_dstHdr, p_paramsHa.gla, m_extHdrList_2Elem ( m_extHdr_dstOptHeader ( c_espHdr, c_optLen2, m_dstOptList_2Elem( m_dstOpt_padN(m_optPad4), mw_dstOpt_homeAddr)), mw_extHdr_espHeader( vc_sad[c_saIn].spi, ?, //vc_sad[c_saIn].seqNr + 1, m_espIpDatagram ( m_extHdrList_1Elem( 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))))), omit), c_mobileHdr)))) -> value v_ipv6Packet { //Get SeqNr v_seqNr := v_ipv6Packet.extHdrList[1].espHeader.espPayload.espIpDatagram.extHdrList[0].mobileHeader.mobileMessage.bindingUpdateMsg.sequenceNumber; //Get Lifetime v_lifetime := v_ipv6Packet.extHdrList[1].espHeader.espPayload.espIpDatagram.extHdrList[0].mobileHeader.mobileMessage.bindingUpdateMsg.lifeTime; //Get CareOfAddress v_mnCareOfAddr := v_ipv6Packet.ipv6Hdr.sourceAddress; //GetHomeAddress v_mnHomeAddr := v_ipv6Packet.extHdrList[0].destinationOptionHeader.destOptionList[1].homeAddressOption.homeAddress; v_ret := e_success; v_ret := f_sendBA ( m_bindingAck ( c_routeHdr, p_paramsHa.gla, v_mnCareOfAddr, m_extHdrList_2Elem ( m_extHdr_routingHeader ( c_espHdr, c_routeHdrLen2, c_routeHdrType2, c_routeHdrSegmentsLeft1, m_routingHeaderData_homeAddress(v_mnHomeAddr)), m_extHdr_espHeader( vc_sad[c_saOut].spi, vc_sad[c_saOut].seqNr + 1, m_espIpDatagram ( m_extHdrList_1Elem ( m_extHdr_mobileHeader ( c_noNextHdr, c_bindingAck, m_bindingAckMsg_status( p_status, v_seqNr, v_lifetime, m_mobileOptList_1Elem ( m_mobileOpt_padN(m_optPad4))))), omit), c_mobileHdr)))); } }//end a_haReceiveBindingUpdateAndReplyOffHome /* Loading Loading @@ -2400,7 +2783,8 @@ group mobileSecurityFns { //Variables var Ipv6Packet v_ipv6Packet; [PX_IP_SEC == e_securityOn] ipPort.receive ( // FIXME Alex [/*PX_IP_SEC == e_securityOn*/] ipPort.receive ( mw_homeTestInit_noData ( c_tunneledIpHdr, p_paramsIut.mnCoa, Loading Loading @@ -2431,7 +2815,8 @@ group mobileSecurityFns { } [PX_IP_SEC == e_securityOff] ipPort.receive ( // FIXME Alex [/*PX_IP_SEC == e_securityOff*/] ipPort.receive ( mw_homeTestInit_noData ( c_tunneledIpHdr, p_paramsIut.mnCoa, Loading