Validating DCCP Simultaneous-Open and Feature Negotiation Procedures


IEICE TRANSACTIONS on Information and Systems   Vol.E100-D   No.6   pp.1190-1199
Publication Date: 2017/06/01
Online ISSN: 1745-1361
Type of Manuscript: Special Section PAPER (Special Section on Formal Approach)
Category: Formal techniques
coloured Petri nets,  state space analysis,  prioritized transitions,  pseudo-code,  RFC 4340,  RFC 5596,  

Full Text: PDF(1MB)
>>Buy this Article

This paper presents the formal analysis of the feature negotiation and connection management procedures of the Datagram Congestion Control Protocol (DCCP). Using state space analysis we discover an error in the DCCP specification, that result in both ends of the connection having different agreed feature values. The error occurs when the client ignores an unexpected Response packet in the OPEN state that carries a valid Confirm option. This provides an evidence that the connection management procedure and feature negotiation procedures interact. We also propose solutions to rectify the problem.