Re: [Cfrg] Comments on the CPace proof and the CFRG PAKE selection process

[Manuel Barbosa <[e-mail]>]

Hi,

Just a short note to follow up on Michel’s email, which I agree with.

It was the first time I followed a CFRG selection process closely and it is a bit disappointing to see that, rather than discussing whether we should go for stronger mechanisms to ensure verifiability such as formal verification of proofs and reference implementations, we are still discussing the importance of a fully checked security proof.

Regards,
Manuel

PS - Hopefully this will not be delivered more than once; I had some trouble getting the message through.

> On 1 Jun 2020, at 23:41, Michel Abdalla <[e-mail]> wrote:
> 
> Hi everybody,
> 
> Given that CPace has been selected as the balanced PAKE option, I believe it is important to make a few comments about its security as well as the CFRG PAKE selection process.  
> 
> 1) Inclusion of the protocol transcript in the key derivation function
> 
> Although the latest RFC for CPace (link) includes the protocol transcript in the key derivation function (suggested by Bjoern Tackmann), the security analysis in the corresponding paper (link) does not clearly state the reasons for it. In particular, when examining the proof, the inclusion of the transcript during the computation of ISK has not been applied consistently throughout the paper and the analysis does not seem to make use of this fact.  
> 
> Here I would like to point out that this requirement is a hard one. Without it, the protocol would be insecure. To see why, just consider the following man-in-the-middle attack during an execution between a server and a client having the same password.
> 
> (a) When the server sends Y_a, the attacker forwards Y_a^2 = G^{2 y_a c_j} to the client
> (b) When the client sends Y_b, the attacker forwards Y_b^2 = G^{2 y_b c_j} to the server
> (c) The client and the server would compute the same ISK despite seeing different messages, since the key used to derive it would be the same: G^{2 y_a y_b c_j^2}.
> 
> 2) Trivial malleability attacks
> 
> When introducing the protocol transcript in the key derivation function, the current RFC for CPace does not use the actual values of Y_a and Y_b to compute ISK. Instead, the input of the key derivation function uses strip_sign_information(Y_a) and strip_sign_information(Y_b).
> 
> One problem with this is that trivial modifications of the messages (for instance by changing Y_a to -Y_a) by a MITM attacker would not be detected by honest parties since the final key derivation does not properly bind the session keys to the transcript.
> 
> Although such an issue can be easily fixed by avoiding the use of strip_sign_information(), it clearly shows an important gap in the current proof.   
> 
> 3) Reduction to SDH
> 
> The reduction to the SDH problem in the latest version of the Haase’s paper is still not given explicitly. Hence, right now, the security analysis only shows that the SDH is a necessary assumption but not necessarily sufficient.  Though such a reduction might be possible, I still don’t see exactly how it can be done so it would be nice if the Haase and Labrique could address this gap in the proof.  
> 
> In a separate paper currently available on ePrint (link), we provide proofs in the UC model for SPAKE2, TBPEKE, and SPEKE. Our results for TBPEKE and SPEKE can also be extended to CPace but only in the case where the key derivation includes the transcript of the communication (which is required) and the password (we may be able to remove this requirement with further analysis).
> 
> As stated in the paper, our proofs for SPAKE2 and TBPEKE rely on the gap versions of the CDH and SDH assumptions. In particular, the Decision Diffie-Hellman oracle is used throughout these proofs to maintain consistency of answers to RO queries, and that this is needed even to deal with sessions in which the adversary is passive: the reduction still needs to be able to consistently deal with the sessions where the attacker is active and the attacker may adaptively decide to launch an active attack after seeing one of the protocol messages. In the case of SPAKE2, removing the need of a gap assumption might be possible given the recent result by Shoup (link).  
> 
> 
> 4) Static versus adaptive UC security
> 
> Our proofs of security for SPAKE2, TBPEKE, and SPEKE in https://eprint.iacr.org/2020/320 only assume static corruptions and it would be interesting to extend them to deal with adaptive corruptions, but doing so does not seem straightforward.
> 
> The current security claim for CPace in https://github.com/BjoernMHaase/AuCPace/blob/master/aucpace_security_analysis_20200208.pdf still claims adaptive security. Unfortunately, since the reductions to the SDH problem are not explicitly given, one cannot verify how corruptions can be handled during these reductions. Note that, when reducing to the SDH problem, the reduction would not know the discrete log of some of the values being exchanged and, hence, it might be hard to know how to properly answer adaptive corruption queries.
> 
> 
> 5) Perfect forward secrecy vs weak forward secrecy
> 
> The UC relaxations used in the proofs of security of CPace, TBPEKE, SPEKE, and SPAKE2 are not known to imply perfect forward secrecy without an additional key confirmation step. In particular, the notion of lazy-extraction UC PAKE in https://eprint.iacr.org/2020/320 is only known to imply weak forward secrecy. Interestingly, proving perfect forward secrecy without the key confirmation step seems to be significantly harder. In the case of SPAKE2, we were able to provide a game-based proof for it under gap CDH (see https://eprint.iacr.org/2019/1194), but the reduction is not tight and requires an intermediate assumption previously used in the proof of SPAKE1. A similar result is currently not known for CPace, TBPEKE, and SPEKE.
> 
> 
> 6) Comment on the CFRG PAKE selection process
> 
> Since the selection process is now over and I no longer have a conflict of interest, I would like to end this email by commenting on the CFRG PAKE selection process.
> 
> On the one hand, the selection process highlighted several important security aspects for real-world PAKE schemes, such as side-channel resistance and quantum annoyance. The notion of quantum annoyance is actually quite interesting and something which we never considered when designing SPAKE2 back in 2005. Nevertheless, I also find it hard to argue that a protocol can satisfy it, since this property was never formally defined, let alone formally proved to hold for any of the candidates.
> 
> On the other hand, I was a bit surprised to see that concerns about security proofs were often ignored in the process. Among the 4 candidates for balanced PAKE, CPace seems to be the one for which nobody was ever able to verify its proofs. Yet, its theorems and strong security claims were mostly taken for granted because people seemed to believe that a correct proof for it could be given (me included) and this seemed to have played an important role in the process. However, what the different MITM attacks given above show is that the security of CPace is still not very well understood. In particular, the current version of CPace still lacks appropriate verifiable proofs and all the versions of the CPace scheme in https://eprint.iacr.org/2018/286 and TCHES are insecure.
> 
> As a result, moving forward, I would strongly recommend against taking security statements for granted if they cannot be verified. Moreover, I also believe that the issues with the security proof of CPace should be fully addressed before proceeding with any formal specification of the latter. 
> 
> Regards,
> Michel
> 
> PS: I would like to acknowledge the help of Manuel Barbosa with whom I discussed the security issues mentioned above.
> 
> _______________________________________________
> Cfrg mailing list
> [e-mail]
> https://www.irtf.org/mailman/listinfo/cfrg