The Session Initiation Protocol (SIP) is one of the
leading protocols for multimedia control over the Internet, including initiating, maintaining and terminating multimedia sessions. The protocol uses transactions to complete the control tasks. In this paper we
focus on the INVITE transaction of SIP, which is used
to initiate a session. SIP is designed to operate over a
transport protocol that can be reliable or unreliable.
Our previous work has veri ed the functional properties of the INVITE transaction over a reliable transport medium, using Coloured Petri Nets (CPNs). In
this paper, we use CPNs to model and analyse SIP
INVITE transaction when the medium is unreliable.
The veri cation reveals similar problem as that in the
case of a reliable medium, i.e. the transaction may
terminate in an undesirable state while one communication party is still waiting for a response from its
peer. Additionally with an unreliable medium, the
transaction has undesirable terminal states in which
retransmitted requests may lead to erroneous operation. This result provides theoretical evidence and
timely support for the Internet Draft that has been
recently submitted to the Internet Engineering Task
Force to propose updates to SIP INVITE transaction.