Open AccessSimulation and Formal Verification of SIP/ZRTP Protocol using UPPAAL
Author(s) -
Arvind Raghavan,
P. P. Amritha,
M. Sethumadhavan
Publication year - 2019
Publication title -
international journal of recent technology and engineering
Language(s) - English
Resource type - Journals
ISSN - 2277-3878
DOI - 10.35940/ijrte.b1029.0982s1119
Subject(s) - computer science , correctness , key (lock) , protocol (science) , session key , network packet , session (web analytics) , universal composability , computer network , session initiation protocol , voice over ip , cryptographic protocol , encryption , computer security , the internet , cryptography , operating system , server , medicine , alternative medicine , pathology , world wide web , programming language
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.