Analysing protocol implementations

Abstract

Many protocols running over the Internet are neither formalised, nor formally analysed. The amount of documentation for tele- communication protocols used in real-life applications is huge, while the available analysis methods and tools require precise and clear-cut protocol clauses. A manual formalisation of the Session Initiation Protocol (SIP) used in Voice over IP (VoIP) applications is not feasible. Therefore, by combining the information retrieved from the specification documents published by the IETF, and traces of real world SIP traffic we craft a formal specification of the protocol in addition to an implementation of the protocol. In the course of our work we detected several weaknesses, both of SIP call setup and in the Asterisk implementation of the protocol. These weaknesses could be exploited and pose as a threat for authentication and non-repudiation of VoIP calls. © 2009 Springer Berlin Heidelberg.