This paper describes the formal approach to modeling IETF Session Initiation Protocol (SIP) and its services in SDL. The main objective is to discover the advantages and shortcomings of using a formal language such as SDL to model an IETF application signaling protocol: SIP. Evaluating the feasibility of using CASE tools such as Telelogic Tau in modeling a protocol as complex as SIP is also the interest of this study. By creating an “Abstract User” interface, we discover the importance of use case analysis in specifying SIP services more precisely. In addition, the object-oriented extension in SDL-96 has been applied to some extent in the modeling process; we create an SDL framework that allows us to reuse and to add SIP services to the core protocol more easily by applying SDL type inheritance in our model. Furthermore, we discuss enhancements that may be made to the SDL language and Tau tools to improve the modeling experience of IETF protocols.