The ZRTP Protocol Security Considerations
Riccardo Bresciani
Scuola Superiore Sant'Anna, Pisa (I)
École Normale Supérieure de Cachan, Cachan (F)
bresciani@sssup.it
Abstract
ZRTP is draft of key agreement protocol by Phil Zimmer-mann, which relies on a Diffie-Hellman exchange to gener-ate 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 protocol performed with AVISP A and ProVerif, which tests security properties of ZRTP; in order to perform the analysis, the protocol has been modeled in HLPSL (for AVISP A) and in the applied π-calculus (for Proverif). An improvement to gather some extra resistance against Man-in-the-Middle attacks is also proposed. PROTOCOL OVERVIEW
ZRTP is a protocol1for media path Diffie-Hellman ex-change to agree on a session key and parameters for estab-lishing SRTP sessions2.
This protocol does not rely on a public key infrastructure or on certification authorities, in fact ephimeral Diffie-Hell-man keys are generated on each session establishment: this allows to bypass the complexity of creating and mantaining a complex third trusted party.
These keys will contribute to the generation of the session key and parameters for SRTP sessions, along with previous-ly shared secrets: this gives protection against Man-in-the-Middle attacks, assuming the attacker was not present in the first session between the two endpoints.
To ensure that the attacker is indeed not present in the first session (when no shared secrets exist), the Short Authenti-cation String method is used: the two endpoint compare a value by reading it aloud.
In case the two values match, then no Man-in-the-Middle attack has been performed.
Call Flow
In the call flow of the protocol, two roles can be identified: initiator (Alice) and responder (Bob).
The parties exchange ZRTP messages, which are enclosed in a frame that makes ZRTP packets clearly distinguishable from RTP ones, thus maintaining backward compatibility with clients which do not support ZRTP.
1Actually, at the time of this writing, ZRTP is still a draft of protocol.
2SRTP has not been projected to perform this task, so it has to rely on external key management protocols.The CRC included in the frame is more reliable than the one built-in in UDP, thus reducing the chances of mistaking a transmission error for an attack.
Each message starts with a preamble containing information about the message length(including preamble length,1 word).
RTP Session Establishment
The key agreement is performed via an RTP session, which is established through a signaling protocol such as SIP.
The signaling protocol passes the signaling secret (sigs), which is the hash of the concatenation of Call-ID, to tag and from tag: this is a secret because Call-ID is random-generat-ed, but only if the SIP
session is secure (usually data is transmitted through a TLS channel).
The signaling also provides the SRTP secret (srtps), which is the hash of SRTP master key and salt.
Key Agreement – Diffie-Hellman Mode
The key agreement algorithm can be divided into 4 steps:
●discovery;
●hash committment;
●Diffie-Hellman exchange;
●switch to SRTP and confirmation.
These steps are showed in the following scheme:
In the Diffie-Hellman mode the authentication relies on a
Diffie-Hellman exchange and on previously shared secrets.
There can be also a Preshared mode, where authentication relies only on previously shared secrets: this mode will not be discussed in this paper.
Discovery
During the discovery phase Alice and Bob exchange their ZRTP identifiers (ZID). Besides, they gather information about each other's capabilities, in terms of supported ZRTP versions, hash functions, ciphers, authorization tag lengths, key agreement types, and SAS algorithms.
The messages exchanged during this phase are called Hello messages,to which each party replies with a HelloACK message (optional for Bob, who could simply reply with a Commit message).
The ZID is used to retrieve information on retained shared secrets rs1, rs2. Additional other secrets (os) may exist.
If a secret of a given type does not exist a random value is generated, so an eavesdropper can't get to know the number of secrets shared between the two parties: the random value will be discarded when the DHPart1and DHPart2mes-sages are exchanged3.
Hash Committment
After the discovery phase, Bob performs the hash commit-ment, by choosing – among the ones supported by both end-points–which hash function,cipher,authorization tag length, key agreement type and SAS algorithm should be used: his choice is sent via the Commit message.
Bob generates a fresh Diffie-Hellman key pair (secret value svB and public value pvB,svB being twice as long as the AES key length):
pvB≡g svB[p]
where [M] denotes a modulo M operation, and g and p are determined by the key agreement type value.
Bob calculates hvB as the hash of his DHPart2message concatenated with the information of Alice's Hello mes-sage4.
Because of the simmetry of the discovery phase, it can hap-pen that Alice tries to act as the initiator, therefore sending her own Commit message upon receipt of Bob's HelloACK 3An user should be careful when accepting a session where there is no retained shared secret match (for example the first session): an attacker could successfully perform an attack by causing mismatches in all the secrets, thus being able to establish an SRTP session with both parties. In this case the solution is the SAS: it is a short string generated from the previously exchanged messages – therefore it is not secret – that has to be compared from the two endpoints, usually by having each user to read aloud his string. It is necessary when all secrets mismatch to ensure that no Man-in-the-Middle attack has been performed.
4This is a precaution against bid-down attacks, which aim to make the authentication procedure rely on weaker mechanisms even when stronger ones ssage:Alice's message is discarded if hvA<hvB, other-wise the protocol lets her be the initiator.
Diffie-Hellman Exchange
By means of the Diffie-Hellman exchange,Alice and Bob aim to generate a new shared secret s0, from which later will derive the new retained shared secret rs0.
When Alice gets the Commit message, she generates her own fresh Diffie-Hellman key pair (svA and pvA).
Alice gathers the retained secrets shared with Bob(rs1, rs2): she will be able to generate a new secret s0 by hashing the concatenation of the Diffie-Hellman result (dhr, which she will be able to compute upon receipt of the DHPart2 message from Bob), the shared secrets (the retained ones, sigs, srtps and os) and the message hash (mh, hash of the concatenation of her Hello message, Commit, DHPart1 and DHPart2)5:
Alice and Bob could have their retained shared secrets sort-ed in a different order (or even have different secrets or none at all) and that would compromise the calculation of s0: to avoid this Alice sorts hers following Bob's order, as-signing to sX the correct secret (in case of mismatch sX will be assigned a null value). To achieve this goal Alice calcu-lates a sequence of HMACs truncated to the leftmost 64 bit, using the string “responder” as key.
She then sends these values to Bob in the DHPart1mes-sage: first he checks that pvA≠1 and pvA≠(p-1), case in which the exchange is terminated (an active intruder could inject a false DHPart1 message to weaken the final Diffie-Hellman result). After this check, he gathers the secret asso-ciated with Alice: he will calculate s0in the same way as Alice does and sends the HMACs of his secrets, already computed when sending the Commit message using the string “initiator” as key. Afterwards he calculates the ex-pected HMACs from Alice and compares them with the ones in the DHPart1message: the matching secrets are kept, the others are replaced by a null value.
He then assigns to each sX the corresponding value, thus defining the sorting of the secrets6.
Bob calculates the Diffie-Hellman result (dhr):
dhr≡pvA svB[p]≡g svA⋅svB[p]≡pvB svA[p]
After this, Bob is actually able to compute s0.
He then sends Alice the DHPart2 message: upon receipt she performs the usual check on pvB and then calculates the hash of the DHPart2 message concatenated with her Hello 5Actually some other parameters are also concatened in this hash, fol-lowing the requirements listed in NIST SP800-56A: these extra parame-ters are omitted for the sake of simplicity and can be found in [1].
6As the non-matching secrets have been replaced by a null value, they have no effect on the cancatenation.
message: if it is different a Man-in-the-Middle attack is tak-ing place and the exchange is aborted.
After these checks Alice calculates dhr and finally calcu-lates s0, after sorting her shared secrets in the same order as Bob.
A further remark: since a Diffie-Hellman exchange affects the state of the retained shared secret cache, it is possible for only one exchange to occur at a time. In case multiple exchanges are needed – this is the case of multiple media streams7 to be established in parallel – the subsequent one can run only after the Conf2ACK message relative to the preceding exchange has been received.
Switch to SRTP and Confirmation
Alice and Bob can now use s0to generate SRTP master keys SRTP-mkey and salts SRTP-msalt– separate in each direction for each media stream – using an HMAC function and truncating the obtained values to the length required by the chosen SRTP algorithm
Next they compute their HMAC keys (ZRTP-key), which are used only by ZRTP, not by SRTP, and the new retained secret rs0.
After this,Alice and Bob generate the ZRTP keys, which will be destroyed only at the end of the call signaling ses-sion: this will allow ZRTP Preshared mode to generate new SRTP key-salt pairs for new concurrent media streams be-tween Alice and Bob, within the limit of the call signaling session.水陆两栖车
After this s0 is deleted, all other key material will be delet-ed as soon as it is no longer used, in any case no later than the end of the session.
They also compute the SAS value as the leftmost 32 bits of mh.
At this point Alice and Bob can send the confirmation mes-sages Confirm1 and Confirm2, which are exchanged essen-tially for two reasons:they confirm that the whole key agreement procedure was successful and encryption is working, and they enable automatic detection of Man-in-the-Middle attacks; they allow the CFB-encrypted transmis-sion of the SAS Verified flag, so that no passive observer can learn wheter Alice and Bob have the good habit to veri-fy the SAS.
Confirmation messages in fact contain a ciphered part com-posed by the cache expiration interval for
窦房结
rs0, an optional signature and an 8 bit unsigned integer (flagoctet), which contains the Disclosure flag, the Allow clear, and the SAS Verified flag.
This part is ciphered via CFB algorithm, using ZRTP-key as key: its initialization vector is sent in the message, along with an HMAC covering the encrypted part.
7Except when ZRTP runs in Preshared mode.The Conf2ACK message is a confirmation sent by Alice upon receipt of Confirm2 message.
After the confirmation procedure, both parties discard the rs2 secret and replace it by rs1 secret and rs1 by rs0. AVISPA MODEL
AVISPA (Automated Validation of Internet Security Proto-cols and Applications) is a cryptographic protocol verifier, developed by Artificial Intelligence Laboratory (DIST, Uni-versity of Genova,Italy),Eidgenössische Technische Hochschule Zürich (Information Security Group,Depart-ment of Computer Science, Zürich, Switzerland), CASSIS (joint INRIA team from LORIA Nancy and LIFC Be-sançon, France) and Siemens Aktiengesellschaft (Munich, Germany).
The tool processes input files in IF format or in HLPSL for-mat: the latter is a higher level format (in f
act it has to be translated into IF format before the protocol can actually be analyzed) and therefore is the one used to model the proto-col – the code can be find in [2].
The AVISPA analysis relies on four different back-ends: On-the-fly Model-Checker(OFMC),CL-based Attack Searcher(CL-AtSe),SAT-based Model-Checker (SATMC),and Tree Automata-based Protocol Analyser (TA4SP): only the first two back-ends have been used here, as the others do not support exponentiation.
OFMC is a tool performing protocol verification through the exploration of the transition system described in the protocol specification on a bounded number of session.
CL-AtSe translates the protocol specification into con-straints and runs it over a finite number of iterations, after reducing it by means of simplification heuristics and redun-dancy elimination techniques.
The Model
The protocol has been modeled in the case when no secret mismatch is detected (a constant secretsab, unknown to the intruder, is passed to both Alice and Bob).
Moreover,Bob does not choose the hash function(and therefore the HMAC) depending on Alice's Hello message, as strings and secrets are joined into cumulative dummy constants8: the hash function is instead fixed and publicly known.
The requested goals are secrecy9 of the encrypted texts ex-changed in the confirmation messages and secrecy of s0 (anyway this is redundant as the encrypted texts can be se-cret only if s0 is also secret).
8It would make no sense giving them a meaning, as they will have to be processed by the program using ZRTP that runs on the endpoints' ma-chines.
9Secrecy is accomplished when an attacker cannot get to know a secret value.
Moreover Alice authenticates10Bob on s0and viceversa (this is also redundant as it can be inferred from the fact that only Alice and Bob know the shared secrects).
Results
None of the two back-ends succeded in finding an attack on the protocol.
By slightly modifying the HLPSL code,secretsab can be added to the intruder knowledge: this happens, for example, when all the secrets mismatch and all of them are discarded. Obviously, in this case the back-ends find that a Man-in-the-Middle attack is possible: that is why the SAS is needed whenever the endpoints cannot rely on the shared secrets. PROVERIF MODEL
ProVerif is a cryptographic protocol verifier, developed by Bruno Blanchet.
The tool processes input files formatted as a sequence of Horn clauses or as a process in the applied π-calculus11, which will be translated into Horn clauses before being run: the latter is the format used to model the protocol – the code can be find in [2].
The Model
The protocol has been modeled almost in the same way as for AVISPA: no secret mismatch is detected (a new name secrets, unknown to the attacker, is used by each couple of Alice and Bob processes),Bob does not choose the hash function depending on Alice's Hello message (it is instead fixed and publicly known) and strings and secrets are joined into cumulative public variables.
A different channel is used for each message, so that the in-formation of the Message Type Block is contained in the channel used.
The queries involve the secrecy of the encrypted blocks ex-changed in the confirmation messages (and therefore the se-crecy of the key material used to encrypt them).
For completeness, also strong secrecy12 is queried for these encrypted blocks. To prove strong secrecy, these blocks are given a set of possible values each: if these blocks contain the optional signature suggested in the latest ZRTP protocol draft as an alternative to SAS, they are unlikely to assume the same values, so the intersection of the possible values is an empty set; if the optional signature is not used, this inter-section may not be empty as these blocks contain only two 10Authentication is accomplished when an attacker cannot pretend to be the authenticated user.
11The applied π-calculus is an extension of the original π-calculus by Robin Milner, which has been developed by Martìn Abadi and Cédric Fournet.
12Strong secrecy is accomplished when two processes holding a secret cannot be distinguished if the value of the secret changes (the processes are observationally equivalent), i.e. an attacker knowing a possible val-ue of secret data cannot tell if that data is the one actually sent.parameters (plus the signature length, which is zero) that are not unlikely to be the same.
Results
The queries confirmed that the secrecy of the encrypted data exchanged during the protocol run is preserved.
In addition the queries confirmed that strong secrecy is ac-complished when signatures are exchanged in the secret blocks, so even an attacker having a pool of possible valid blocks cannot tell which block is the one actually sent. Viceversa, if the endpoints do not exchange signatures in the confirmation messages, the ciphered blocks are only made of Signature Length(null value),Cache Expiration Interval and flagoctet so there is a high probability for the endpoints to send the same block. In this case the proof fails: the attacker in fact can see when the two blocks are identical, though he still cannot understand which block among the possible ones appearing in both lists – if more than one – is the one actually sent.
CONCLUSION
Nor AVISPA, neither ProVerif have succeeded in finding possible attacks on the protocol model, which has proven to be robust and not vulnerable to attacks throughout its run, under the hypothesis that the endpoints share the secrets needed to generate the key.
In case this hypothesis is removed, the protocol is still se-cure under the assumption that SAS provid
es the means to detect a Man-in-the-Middle.
This assumption holds if the attacker has no voice-forgery capabilities: a Man-in-the-Middle could attack the protocol if he were able to generate a collision on sasvalue (the first 64 bits of the message hash mh), but this is not possible as neither party can deterministically influence sasvalue.In fact the initiator chooses his public value and sends a “hint” of it in the Commit message and therefore he cannot change it upon receipt of the responder's public value – being able to do so would imply being able to choose a different public value which would result in the same “hint”, thus being able to find a collision in the hash function and this is assumed to be computationally infeasible.
For the same reason, security against bid-down attacks is provided by including the initiator's Hello message in the “hint”, which is sent upon the hash commitment, and again when generating the secret s0.
Analysis with AVISPA and with ProVerif
监狱法全文Both tools use the Dolev-Yao model for channels, in which the intruder can do whatever he pleases with the exchanged messages, including altering them, preventing them to reach their destination or replaying them whenever he wants: a way to see this is to think of a net modeled as a star, with the intruder in the central node.
In both tools each single ZRTP protocol run has been mod-eled as two concurrent processes that synchronize by means
of message exchange: the arrival of an awaited message lets a process get to the following state; in both cases the under-lying hypotheses are that there is no shared secret mismatch and that the hash function is chosen a priori.
Here are the differences between performing the analysis with AVISPA and Proverif:
●endpoint authentication and key secrecy have been
proven only in AVISPA, as these are redundant proves (authentication is given because only the two endpoints can have the secrets; if the encrypted data is secret also key secrecy must be accomplished);
●in AVISPA the endpoints communicate through the
same channel and the message type is identified by a string, in ProVerif each message is sent on a different channel;
●ProVerif allows analysing the protocol on an unbound-
ed number of session, as the instantiation of the end-points has been made with the (infinite) replication op-erator “!”, in AVISPA the used back-ends are limited to a bounded number of sessions.
SAS: the Achilles' heel of ZRTP
If the assumption that SAS provides the means to detect a Man-in-the-Middle is removed – and this is the case of a voice-forgery capable attacker, which in not unreasonable though it requires him to be really skilled, powerful and re-sourceful – some possible attacks have been found through an analysis in the Murphi model checker carried out by An-drew Schwartz and Jeremy Robin on a pre-realease version of ZRTP.
It is worth spending a few words to present the attacks found.
The Voice Forgery Attack can be performed when an at-tacker is able to imitate the voices of Alice and Bob: at the SAS phase he authenticates with each party using different SAS strings which are re
ad with the other party's voice. The Bill Clinton Attack is based on the assumption that a celebrity will not remember the voice of a random person such as Alice,while Alice will remember the celebrity's voice:an attacker can therefore execute SAS with the celebrity with his own voice to create a false shared secret and when Alice will later try to contact the celebrity, the at-tacker will authenticate to Alice by imitating the celebrity's voice. This schema can work for each random person with-out knowing in advance who this random person will be, the attacke only needs the celebrity to forget voices.
The 6 Month Attack is based on the assumption that Alice and Bob will not remember for a long time their voices, as they are unfamiliar and they do not happen to talk very of-ten: in this case an attacker can establish false shared se-crets with each party – as made with the celebrity in the Bill Clinton attack– so they will not execute SAS on the fol-lowing sessions and the attacker will be able to listen to the traffic and simply relay it.The Court Reporter Attack can be performed if Alice and Bob do not know each other's voice: an attacker establishes a session with each one of them and, after performing SAS with his own voice, he has to relay the traffic in both direc-tions in his own voice. It is easier to perform this attack with two court reporters and two talkers, because delay margins are slightly less restrictive.
The Hybrid Clinton-Court Reporter Attack is a mix of Court Reporter and Bill Clinton attacks and can be per-formed when an attacker can forge Alice's voice and Alice does not know Bob's voice, but Bob knows Alice's: Marvin do not need to be a court reporter if he is able to imitate Al-ice's voice.
A trusted server for SAS
The Achilles' heel of ZRTP protocol is SAS authentication, as no protocol can provide protection against an active at-tacker to both initiator and responder.
A possible solution to this problem could be the one pro-posed in the latest ZRTP protocol draft, that consists in sending a signature in the encrypted part of the confirma-tion messages: this is a solution that anyway requires some kind of underlying Public-Key Infrastructure.
Another possible solution, that still does not require a Pub-lic-Key Infrastructure, could be accepting to rely on a third trusted party only when no secret shared between the end-points is available.
This solution could be implemented through a protocol which allows only to verify that the trusted party is not be-ing emulated by the attacker (this is quite an easy require-ment to accomplish, as the trusted server would be publicly known).
Here is the possible scheme: Alice sends Trent (the trusted server) the SAS value she has computed (for additional se-curity she could send the entire message hash mh) along with her and Bob's ZID s; Bob then sends Trent the SAS val-ue he has computed (or mh) along with his and Alice's ZID s. Trent verifies that the same task was not performed in the preceding 60 seconds (an attacke should perform this pro-cedure with one endpoint at a time, but this would introduce a great delay which would prevent him from passing unde-tected) and that the values associated to the (ZIDA,ZIDB) pair match:Trent returns the result of the comparison to both Alice and Bob.
In this way one of the following cases happens: Alice and Bob manage to talk; Alice talks to the attacker pretending to be Bob, and Bob gets an error from Trent; Bob talks to the attacker pretending to be Alice, and Alice gets an error from Trent; both Alice and Bob get an error from Trent.
The actual messages exchanged from each client to Trent could be a simple concatenation of the strings ZIDA, ZIDB and sasvalue
After Trent has received the authentication request mes-sages, he only has to make an almost unexpensive operation
such as comparison, after checking that the same couple of ZID s has not requested authentication i
n the preceding minute.
Only if the check is positive and the comparison succeeds13, Trent sends back a signature (for example the hash of the authorization request encrypted with his private key), other-wise he sends a bunch of zeros (or a random value) to noti-fy the authentication failure.
Upon receipt of the result,Alice and Bob decrypt it with Trent's public key and check the hash correctness, thus be-ing able to validate or reject the key exchange.
In the authentication request messages one coud also send the hash of the concatenation of ZID s and sasvalue along with a string indentifing the ZID pair14 in order to transmit less data, thus leaving to Trent only the operation of signing the hash and sending the signature: this does not compro-mise the authentication in principle, although this may re-sult in an increase in the probability of a collision, especial-ly if Trent has many clients to authenticate.
This way of authenticating, though requiring a trusted serv-er, has the following benefits:
●it does not require the user to interact with the proto-
col;
● a Man-in-the-Middle has no chances to pass undetect-
ed;
●the protocol is immune to the Voice Forgery attack;
电子设计
工程>
气体保护焊丝
●the protocol is immune to the Court Reporter attack;
●the protocol is immune to the Hybrid Clinton-Court
Reporter attack;
●it still does not need a public key infrastucture;
●the trusted server is rather simple, as it does not need to
keep big databases or perform expensive computations;
●from a more practical point of view, the server load is
unlikely to be too heavy, as it is limited to a few pack-ets to transmit and receive, a hashing operation and an encryption for each couple.
To ensure immunity – or at least to be more resistant – to 6 Month and Bill Clinton attacks, the cache expiration inter-val should be lowered or set to 0, though in this last case this implies that Trent will be required to authenticate the endpoints each time they want to connect.
As the user is not required to interact with the protocol, the task of authenticating the endpoints can be performed more often, without annoying the users.
13This makes the server resistant to Denial of Service Attacks, both memo-ry-exhausting and computational. If the same couple or the same IP(s) tries to authenticate an excessive number of times – even at minute inter-vals – this could be an attack, and the server may decide to blacklist the couple or the IP(s).
14This can be the first bytes of each ZID, the hash of their concatenation or any string derived from the ZID s that is long enough to have a low probability to collide with the one of another couple of endpoints.ACKNOWLEDGMENTS
The author wants to thank Mr. Steve Kremer, who has tutored him during his stage at LSV (ENS Cachan) in spring 2007: this stage has resulted in Research Report LSV-07-20, a work on a pre-vious draft of ZRTP, from which this paper is derived.
REFERENCES
[1]Phil Zimmermann, ZRTP: Extension to RTP for Diffie-
Hellman Key Agreement for SRTP, 2007
</>
[2]Riccardo Bresciani, The ZRTP Protocol (Research Re-
port LSV-07-20), 2007 <s-
cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2007-
20.pdf>
[3] A. Schwartz, J. Robin, Analysis of ZRTP, 2006
<www.stanford.edu/class/cs259/projects/projec-
t05>
[4]AVISPA v1.1 User Manual, 2006 <www.avispa-
[5]David Basin, Sebastian Mödersheim, Luca Viganò,
OFMC: A symbolic model checker for security proto-
cols, Springer-Verlag, 2004 <www.avispa-
[6]Mathieu Turuani, The CL-Atse Protocol Analyser,
Springer, 2006
<hal.inria.fr/docs/00/10/35/73/PDF/RTA06_16_
Turuani.pdf>
[7]Bruno Blanchet, ProVerif, Automatic Cryptographic
Protocol Verifier User Manual, 2007 <www.-
the π-calculus, Cambridge University Press, 1999 [9]Martín Abadi, Cédric Fournet, Mobile Values, New
Names, and Secure Communication, 2001
<www.soe.ucsc.edu/~abadi/Papers/popl01-abadi-fournet.ps>
[10]Martín Abadi, Bruno Blanchet, Analyzing Security
Protocols with Secrecy Types and Logic Programs,
2005
<s.fr/~blanchet/publications/Abadi-
BlanchetJACM7037.pdf>
[11]Martín Abadi, Bruno Blanchet, Cédric Fournet, Just
Fast Keying in the Pi Calculus, 2007 <www.-
netTISSEC07.pdf>
[12]Bruno Blanchet, Automatic Proof of Strong Secrecy
for Security Protocols, 2004
<s.fr/~blanchet/publications/Blanchet
>
豫公网安备41160202000603
站长QQ:729038198
关于我们
投诉建议