This paper investigates the feature negotiation procedure of the Datagram Congestion Control Protocol (DCCP) in RFC 4340 using Coloured Petri Nets (CPNs). After obtaining a formal executable CPN model of DCCP feature negotiation, we analyse it using state space analysis. The experimental result reveals that simultaneous negotiation could be broken on even a simple lossless FIFO channel. In the undesired terminal states, the confirmed feature values of Client and Server do not match.
1.1
Unlike TCP, DCCP does not impose flow control on data transfer. But state
information such as the sequence number sent and received is still required in order
to trace packet loss which is crucial for congestion control. From the sequence
number variables, a sequence number validity window is set up [
Formal methods [
The contribution of this paper is three fold. Firstly, as far as we are aware of this paper presents the first formal executable model of DCCP feature negotiation. Secondly the formal analysis helps us identify an error in the specification. Thirdly, investigating the state space analysis provides us insight what causes the error.
This paper is organised as follows. Section 2 provides an overview of the protocol and packet format. Section 3 briefly describes DCCP feature negotiation procedure. The description of the CPN model of DCCP feature negotiation is described in section 4, which starts with modelling assumptions and specification interpretation. Section 5 discusses analysis result and insight. Section 6 presents the conclusion of this paper and future work. DCCP Header 0 1 2 3 4 5 6 7 8 9 0 1 2 3 4 5 6 7 8 9 0 1 2 3 4 5 6 7 8 9 0 1
Source Port
Destination Port Generic Header
Data Offset CcVal CsCov
Checksum
Packet X Res Type = Reserved Sequence Number (high bits) 1
Sequence Number (low bits) Reserved
Acknowledge Number
(high bits)
Acknowledge Number (low bits) Option Type Length
Feature No. Values . . . . . .
Application Data
The Internet protocol architecture is organized into five layers known as the
TCP/IP reference model. While TCP is a transport protocol that provide the
reliable delivery of a byte stream, DCCP is a transport protocol for the timely but
unreliable delivery of datagrams. DCCP can be viewed as an upgraded version
of UDP equipped with new facilities for connection management;
acknowledgement; feature negotiation and congestion control.
DCCPs exchange packets over the Internet Protocol between a client and a
server. The protocol uses 11 packets to setup and release connections and transfer
data. RFC 4340 [
The DCCP header contains 16 bit source and destination port numbers, and
a 16 bit checksum. An 8 bit data offset indicates the length in 32-bit words from
the beginning of the Header to the beginning of the Application data. CCVal, a
4 bit field, is a value used by the congestion control mechanisms [
The Options field contains state information or commands for applications
to negotiate various features such as the Congestion Control Identifier (CCID)
and the width of the Sequence Number validity window [
The options field is a multiple of 32-bit words which may contain more than
one option. Because each option consists of a multiple of 8 bits, the field may
need to be padded to the word boundary. Options are classified into two groups:
single byte and multi-byte. A single byte option has a value from 0 to 31 which
represents an option type. An Option type is a 8-bit integer which represents the
meaning of the option, such as 1 meaning mandatory, 2 meaning slow receiver
[
DCCP allows both the client and server to change their parameters called features using feature negotiation procedures. The negotiation can happen at any time but typically during connection establishment. Each entity can initiate the negotiation of two kinds of features: local features (L)-the initiator’s features and remote features (R)-the other side’s features. Four particular options are dedicated to feature negotiations; Change L, Confirm L, Change R and Confirm R. The option types have values of 32 to 35 respectively. The format of Confirm or Change Options including feature numbers and feature values are shown in a) b) c)
Option Length Feature Type Number
Feature values Fig. 2. Option format in DCCP header and an example of a Change L option. Fig 2 a). Fig 2 b) shows six of 8-bit values representing a Change L option when negotiating CCID. The meaning of each 8-bit values is shown in Fig 2 c).
The feature number identifies the feature. For instance, 1 refers to CCID and
2 means short sequence numbers are allowed. The complete list of features is
given in [
1. The server priority rule: This rule is applied when the feature value is a fixed-length byte string. During negotiation DCCP entity keeps an ordered preference list of the feature values. The initiator sends a Change option containing its preference list. The receiver responds with the Confirm option containing an agreed value followed by its preference list. Thus the agree value will appear twice in the Confirm option. The agreed value is defined as the first element in the server’s list that matches any element in the client’s list. If there is no match, the agreed value remains the existing feature value.
For example, the client sends 32,6,1,2,3,4 corresponding to Change L(32), length(6), CCID(1), the client’s preference list(2,3,4). This means the client proposes to change its CCID and the preferred CCIDs are CCID#2, CCID#3 and CCID#4 respectively. The server responds 35,7,1,3,3,4,2 corresponding to Confirm R(35), length(7), CCID (1), agreed value (3) and the server’s preference list (3,4,2). According to the Client’s and Server’s preference lists in this example, the client must use CCID#3.
2. Non-negotiable rule: The Change and Confirm options under this rule contain only one feature value which is a byte string. After receiving the Change L from the feature local, the feature remote must accept the valid value and reply with Confirm R containing this value. If the received feature value is invalid, the feature remote must send an empty Confirm R. This non-negotiable rule must not be used with Change R and Confirm L options.
For example the client sends 32,9,3,0,0,0,0,4,0 corresponding to Change L(32), length(9), Sequence number window (3), value of window size(1024). The server replies with 35,9,3,0,0,0,0,4,0. 3.1
The feature negotiation procedures are represented by state diagrams. Figure 3 shows the state diagram for feature local. It comprises three states: STABLE; CHANGING; and UNSTABLE. The entity in the STABLE state always knows its feature value and expects the other end agrees with the same value. When the local receives Change R, it calculates a new agreed value and replies Confirm L. On the other hand the Confirm R received will be discarded.
After the entity in STABLE sends the first Change L command, it enters the CHANGING state and goes back to the STABLE state upon receiving a Confirm R or a empty Confirm R. When the local in CHANGING does not get reply from the other side, it keeps retransmit the Change L option. time out or rcv non-ack packet retransmit Change L rcv Confirm R rcv Change R calculate a new feature value snd Confirm L
When the preference list is changed by its user while the entity is in the CHANGING state, it enters the UNSTABLE state. Here it ignores the on-going negotiation but starts a new negotiation by sending a Change command with the new preference list before going back to the CHANGING state.
The state diagram for feature remote can be obtained by interchanging Ls and Rs in Fig. 3. Thus each entity consists of three state machines working together: connection management, feature local and feature remote. It is possible that one side initiates Change L while the other side initiates Change R of the same feature. According to Fig. 3 when the local in CHANGING receives Change R, it computes a new agree value and replies Confirm L. This situation is called simultaneous negotiation. The specification also allows the preferences to be changed at any time. 3.2
Although the feature negotiation procedures explained in the previous section sound simple, the real situation could be very complex when packets are reordered and lost. Moreover the negotiation for the same feature could be simultaneously initiated by both sides and the preference lists can be changed at any time. To cope with this, the RFC specifies some rules intended to provide reliable signalling so that both sides reach agreement with the same feature value.
Change and Confirm options in packets that do not arrive in strictly increasing order must be ignored. According to the related pseudo code and algorithms, the strictly increasing order rule is only enforced for packets that contain the Change and Confirm options. An ordered packet with the Change and/or Confirm options may have a sequence number less than GSR if the later packets do not contain any Change or Confirm options.
In order to check the order of arrival, the RFC specifies another two variables: Feature Greatest Sequence Number Received (FGSR) and Feature Greatest Sequence Number Sent (FGSS). If the received packet’s sequence number is less than or equal to FGSR, Change or Confirm options received must be ignored. If the acknowledgement Number is less than FGSS or the packet contains no acknowledgement, the Confirm option received must be ignored.
Because DCCP-Data with short sequence numbers is vulnerable to be attacked, any option attached to DCCP-Data that might cause the connection to be reset shall be ignore. Thus both Change and Confirm options received in DCCP-Data must be ignored in all circumstances. A sequence number valid packet received that contains non-reordered Change or Confirm options updates FGSR while FGSS is updated when the entity sends a Change Option during a transition from STABLE or UNSTABLE to CHANGING.
Retransmission Because the reordered options are ignored or the packet can be lost, Change options must be retransmitted when the sender does not receive a non-reordered Confirm option within a specific period. The Confirm option must be generated only when a non-reordered Change option is received. Retransmission of options may be achieved by either generating a new packet (DCCP-Ack or DCCP-Sync) or by including the appropriate option field in a packet that is about to be transmitted. Retransmission continues until a non-reordered Confirm option is received or the connection is closed down. 4 4.1
We make the following assumptions regarding DCCP feature negotiation when creating our model.
1. This paper assumes the medium to be First-in First-out (FIFO) channels with no loss. There are three reasons supporting this assumption. Firstly, according to RFC 4340 the Change and Confirm Options must arrive in strictly increasing order otherwise it will be ignored. This requirement implies that actually DCCP feature negotiation protocol operates over FIFO channels. Secondly, reordered and/or lossy channels can mask out inherent errors such as unspecified receptions which could appear when protocol operates over FIFO channels with no loss. Thus protocol validation shall be started from operating over the FIFO channels with no loss. Thirdly, the assumption of FIFO channel makes the model simpler. We can abstract away irrelevant details such as sequence number, acknowledgement number, state variables FGSS and FGSR.
2. Although we agree with [
3. A DCCP packet is modelled by an option type and a list of feature values (preference list). Other fields such as packet type and sequence-acknowledgement numbers are omitted because they do not affect the operation of the feature negotiation.
4. RFC4340 allows many options to be sent in one packet and many
features to be negotiated at the same time. Following an incremental approach [
5. Our model does not include the mandatory options, invalid options and unknown feature numbers.
6. RFC 4340 specifies that the preference list can be changed at any time. It
is unclear what should be happened if the preference list is changed while the
endpoint in STABLE. However according to [
Our model structure is inspired by [
FN_Local FN_Remote
Stable_Local Changing_Local Unstable_Local Stable_Remote Changing_Remote
Unstable_Remote 1: (* Feature Negotiations *) 2: colset E = with e; 3: colset CCID = int with 2..255; 4: colset Confirmed_Value = CCID; 5: colset Preference_List = list CCID; 6: colset Option_Type = with ChangeL | ConfirmL 7: | ChangeR | ConfirmR; 8: colset Option_Field = product Option_Type 9: * Preference_List; 10: colset List_Option_Field = list Option_Field; 11: colset FN_State = with STABLE | CHANGING | UNSTABLE; 12: colset FN_CB = product FN_State * Confirmed_Value 13: * Preference_List;
Remote2Local List_Option_Field
Local2Remote List_Option_Field
FN_CB Remote
FN_Remote
Fig. 6. The Main_FN overview page.
FN_CB In/Out
FN_CB
In/Out Output
List_Option_Field STABLE_Local ApplicationEvent lopt2 lopt2 lopt1 Preference_List
Fusion 1
New
Preference
Fig. 8. The STABLE_Local page. by double-line rectangles), four places (represented by ellipses) and arcs connecting between places and transitions. The substitution transition on the left models the Client (Local) and another on the right models the Server (Remote). Both communicate via two places named Remote2Local and Local2Remote in the middle of Fig. 6. Each place models a unidirectional and First-in First-out channel typed by List_Option_Field. List_Option_Field is a list of product sets named Option_Field defined in Fig. 5. Option_Field comprises Option_Type and Preference_List sets also defined in Fig. 5. Through these places, tokens (which are values taken from the type of the place) are transferred between Local and Remote.
Places FN_State_Local and FN_State_Remote, typed by FN_CB, model the states of the feature negotiation procedure. The FN_CB is defined as a product comprising colour sets FN_State, Confirmed_Value and Preference_List.
The substitution transitions Local and Remote in Fig. 6 are linked to the second level pages named FN_Local (Fig. 7) and FN_Remote. Each of the second level CPN diagrams comprises further three substitute transitions, named by the feature negotiation states (Fig. 7) and linked to the CPN diagrams in the third level. Because these CPN diagrams of FN_Remote are very similar to those of FN_Local, this paper illustrates only the CPN diagrams of FN_Local. (UNSTABLE, cnf, newPrefLS) (CHANGING, cnf, prefLS) (CHANGING, cnf, prefLS) (CHANGING, cnf, prefLS)
Fusion 1 1`[
Preference_List [n > 0] Retrans n n-1 lopt2^^ lopt2 [(ChangeL, prefLS)]
RCNT 0
INT List_Option_Field
Output In/Out
lopt2^^ lopt2 [(ConfirmL, (pphSrrdeeT(ffmALLBSSaL))tcE),h,(prefLPkt, Rcv_Chan^mg^aetpRcrhe(fpLSre)f]:(L:CPlhokapt,nt1pgreeRf,LSp)refLPkt) (cCnfH,ApNreGfILNSG), lo(pCt1onfirmR, []) In/Out (cCnHf,ApNreGfILNSG), Rcv_EmptyComfirmR lopt1
::lopt1 FN_CB
FN_CB (cSnTf,ApBrLeEfL,S) (STABLE, ckLocal(prefLS, cnf_p::prefLPkt), prefLS)
In/Out Input
List_Option_Field Rcv_ComfirmR (ConfirmR, cnf_p ::prefLPkt)::lopt1 lopt1 (CHANGING, cnf_s, prefLS)
Fig. 9. The CHANGING_Local page.
In/Out Output List_Option_Field lopt2^^ [(ChangeL, newPrefLS)]
lopt2 (UNSTABLE, cnf, newPrefLS) (CHANGING, cnf, newPrefLS) In/Out FN_CB FN_CB (UNSTABLE, cnf, prefLS) (UNSTABLE, cnf, prefLS) (ChangeR, prefLPkt) ::lopt1
In/Out Input List_Option_Field (ConfirmR, prefLPkt)::lopt1 (UNSTABLE, cnf, prefLS) (UNSTABLE, cnf, prefLS)
Our DCCP feature negotiation model is analysed using CPN Tools [
We choose to model and analyse the negotiation of the feature CCID. This
feature uses the reconciliation rule: server priority. The default feature value is 2
which represents TCP-like congestion control. Although currently the standard
specifies only CCID2 (RFC4341), CCID3 (RFC4342) and CCID4 (RFC5622),
we make up CCID numbers in each preference list for the purpose of validating
the feature negotiation procedure. Table 1 shows the values in preference lists we
used in our experiment before and after the preference has been changed. The
resolved values before and after the preference changed under the server-priority
reconciliation rule are shown in Table 1 as well. According to [
Table 2 shows the initial configurations of twelve possible scenarios. They are classified according to which sides are allowed to initiate the negotiation and which sides change their preference lists. Our CPN model allows simultaneous negotiation and both sides can change their preference lists (Case 12). 5.2
The analysis results of DCCP feature negotiation CPN model using the initial configurations described in the previous subsection are shown in Table 3. The total number of states, arcs in each case are shown in the second and third columns. Column 4, 5 and 6 show the terminal markings of each scenario. All terminal markings have both sides in STABLE and no packets left in the channels and hence there is no unspecified reception. The terminal markings are classified into 3 types. Type-I is the desired terminal state where both Client and Server reach the same feature value. Type-II is the undesired terminal state where both
Terminal Markings sides reach the different feature values but an endpoint knows that the agreed value is wrong. Type-III is also the the undesired terminal state where both sides reach the different feature values and both endpoints do not know that their feature values do not match. Figure 11 shows a scenario leading to a Type-II terminal state. Referring Fig. 11, after sending the first Change L Option, Client changes its preference list in UNSTABLE and sends the second Change L. When receiving the Confirm R of the first Change L in the CHANGING state, Client enters the STABLE state and then ignores the Confirm R of the second Change L. The agreed feature value in the first Confirm R is outdated and different from the feature value in Server. However when comparing the preference list in the first Confirm R option with the preference list in Client’s state information, Client is able to know that the agreed value is wrong. Obviously in this case the Client should resend the Change option or reset the connection.
Figure 12 illustrates a scenario leading to an undesired Type-III terminal state. This is the center of our attention in this paper. This scenario could happen when both sides initiate the negotiation simultaneously and both sides change their preference list (Case 12). We notice that all Confirm options in Fig. 12 are discarded. It becomes one way communication with no acknowledgement. Figure 12 can be viewed as three attempts of negotiation. Two attempts are initiated simultaneously from both sides. This could be happened during DCCP simultaneous open procedure. Preference list changed in CHANGING
(STABLE, 2, [
(STABLE, 2, [
(STABLE, 2, [
(STABLE, 2, [
Type-III terminal state is worse than type-II because both entities are not aware that their agreed feature values are different. In our opinion the main objective of the DCCP feature negotiation protocol is to exchange the preference lists. After the preference list of the other side is known, the agreed feature value can be correctly computed. We suggest a solution when the preference list is changed (either major or minor change), the endpoint shall send Change option to inform the other side. If the preference list is changed in the STABLE state, the endpoint shall send Change option and enter CHANGING state. Another solution could be that the endpoint does not discard Confirm option in STABLE state. 6
This paper presents Coloured Petri Net model and analysis of DCCP feature negotiation procedure operating over FIFO with no loss channels. The analysis result shows that the protocol could fail to an undesired state (Type-III) where the feature values of both sides do not match and both sides are not aware of the mismatch.
Usually when the protocol operates over reordering and/or lossy channels, it is possible that the protocol could fail due to the channel imperfection. However if the protocol operates over the ideal channels (FIFO with no loss), the error indicates the flaw in the protocol itself.
The terminal state (Type-III) occurs when both sides change their preference lists during the simultaneous feature negotiation. Although the odds of this scenario is low, given the large number of potential connection in the Internet, we consider that this defect could be a serious threat.
The model development begins with a lot of assumptions. In the future we would like to relax these assumptions and refine the model. In particular we are interested to include connection management procedures together with Network Address Translators (NATs) into the model.
Acknowledgments This work is supported by Research Grant from the Thai Network Information Center Foundation and the Thailand Research Fund. The author is thankful to anonymous reviewers. Their constructive feedback has helped the author improve the quality of this paper.