Simulation and Formal Verification of SIP/ZRTP Protocol Using UPPAAL
Aishwarya Raghavan1, P. P. Amritha2, M. Sethumadhavan3
1Aishwarya Raghavan, TIFAC-Core Cyber Security, Amrita School of Engineering, Coimbatore (Tamil Nadu), India.
2P. P, Amritha, TIFAC-Core Cyber Security, Amrita School of Engineering, Coimbatore (Tamil Nadu), India.
3M. Sethumadhavan, TIFAC-Core Cyber Security, Amrita School of Engineering, Coimbatore (Tamil Nadu), India.
Manuscript received on 10 October 2019 | Revised Manuscript received on 19 October 2019 | Manuscript Published on 02 November 2019 | PP: 177-181 | Volume-8 Issue-2S11 September 2019 | Retrieval Number: B10290982S1119/2019©BEIESP | DOI: 10.35940/ijrte.B1029.0982S1119
Open Access | Editorial and Publishing Policies | Cite | Mendeley | Indexing and Abstracting
© The Authors. Blue Eyes Intelligence Engineering and Sciences Publication (BEIESP). This is an open access article under the CC-BY-NC-ND license (http://creativecommons.org/licenses/by-nc-nd/4.0/)
Abstract: The security of voice communication over the Internet Protocol is a continuously growing research area due to the rapid rise in its usage among consumers. With the advent of Voice-over-IP Protocols, the Real Time Protocol (RTP) was used to facilitate VoIP communications. To secure this communication, Secure Real Time Protocol (SRTP) was implemented to encrypt these voice packets. The SRTP requires a session key to be shared between the communicating entities. The challenging task of establishing a new, unused session key to secure each SRTP session was overcome by the key agreement protocol, Zimmermann Real-time Transport Protocol (ZRTP) which ensures confidentiality as well as a shield against Man-in-the-Middle attack. We firstly analyze the security properties of this protocol. Formal analysis is a mathematical technique that can be used to verify the correctness of the system. We simulated the complete ZRTP Protocol with the well-known formal analysis tool, Uppaal, and verified the existing security properties such as Deadlock Prevention, Liveliness, Safety and other protocol parameters mismatch detection using the Uppaal model checker engine. Temporal logic was used to design the queries to verify the properties.
Keywords: Temporal Logic, Timed Automata, UPPAAL, ZRTP.
Scope of the Article: Network Protocols & Wireless Networks