Formal Analysis of the Real-time Multimedia Network Protocol ZRTP

Title:Formal Analysis of the Real-time Multimedia Network Protocol ZRTP

Volume: 8 Issue: 1

Author(s): Siqi Lu, Wenbo Wang and Qingfeng Cheng

Affiliation:

Keywords: Formal analysis, real-time transport protocol, scyther, tamarin, ZRTP protocol.

Abstract: As the multimedia social network develops rapidly, protocols protecting the security of realtime multimedia are becoming very significant. The ZRTP protocol, one of Real-time Transport Protocols (RTPs) for real-time multimedia applications, has many advantages compared with others. Though the calculation cost is relatively high, the ZRTP protocol provides perfect forward secrecy and authentication against man-in-the-middle attack. As so many formal verification tools were proposed recently, formal method has become one of the main methods of security protocol analysis. However, the formal verification tools are rarely used for the Real-time Transport Protocols. In this paper, we innovatively utilize the formal verification tool Scyther- Compromise and Tamarin to analyse the ZRTP protocol. According to the results, we find that the ZRTP protocol is insecure under the eCK model though it provides the perfect forward secrecy property. The adversary can impersonate the endpoint when the shared secrets are revealed. Besides, the experiments of this paper show that the formal method can perform perfectly and play an important role in protocol analysis.

Cite this article as:

Lu Siqi, Wang Wenbo and Cheng Qingfeng, Formal Analysis of the Real-time Multimedia Network Protocol ZRTP, Recent Advances in Electrical & Electronic Engineering 2015; 8 (1) . https://dx.doi.org/10.2174/2352096508666150317234447

DOI https://dx.doi.org/10.2174/2352096508666150317234447	Print ISSN 2352-0965
Publisher Name Bentham Science Publisher	Online ISSN 2352-0973