ProVerif Analysis of the ZRTP Protocol

Abstract

When some agents want to communicate through a media stream (for example voice or video), the Real Time Protocol (RTP) is used. This protocol does not provide en-cryption, so it is necessary to use Secure RTP (SRTP) to secure the communication. In order for this to work, the agents need to agree on key material and ZRTP provides them with a procedure to perform this task: it is a key agreement protocol, which relies on a Diffie-Hellman exchange to generate SRTP session parameters, providing confidentiality and protecting against Man-in-the-Middle attacks even without a public key infrastructure or endpoint certificates. This is an analysis of the ZRTP protocol performed with ProVerif, which tests security properties; in order to perform the analysis, the protocol has been modeled in the applied π-calculus.