[Cfrg] Review of (security of) remaining candidates

[Julia Hesse <[e-mail]>]

Apologies for the lengthy and late review. I looked at security aspects 
of the four remaining candidates, and the recommendations are not taking 
other properties such as efficiency or integration into standards into 
account.

To summarize, security-wise I (conditionally) recommend SPAKE2 and OPAQUE.

SPAKE2
======
I reviewed the following documents: the candidate's specification as 
described in draft-irtf-cfrg-spake2-09, and proofs of (what they call) 
SPAKE2 in https://www.di.ens.fr/~mabdalla/papers/AbPo05a-letter.pdf 
(passive and MITM security) and https://eprint.iacr.org/2019/1194 
(adaptive corruption and forward secrecy).

Security pro's and con's:
+ Existing security proofs require one programmable global RO and Gap-DH 
(needed for forward secrecy, passive/mitm proof requires CDH instead of 
Gap-DH)
+ SPAKE2 has forward secrecy
+ None of the proofs require key confirmation (draft-irtf-cfrg-spake2-09 
puts it as MUST = absolute requirement)
+ Security proofs cover multi-party & multi-session setting (including 
re-use of passwords)
+ Security proofs are tight (i.e., guarantees do not degrade with the 
number of users)
+ Security proof for passive/MITM security was published already in 2005 
and since today no issues have been found (see also notes on Scott's 
review below)
- Security proofs cover only executions where users use passwords chosen 
uniformly random from the dictionary
- draft-irtf-cfrg-spake2-09 adds a cofactor h to the protocol, but no 
security analysis exists for that
- No quantum preparedness, no option to switch to it, limited crypto 
agility since not a modular protocol
- No quantum annoyance if M,N generated system-wide

Notes on SPAKE2's reliance on parameters M,N (both group elements):
If the dlog of M or N is known, then SPAKE2 is offline attackable 
(meaning that attacking only one run of the protocol allows the attacker 
to later test arbitrarily many passwords). However, the protocol's 
security does not rely on M != N

Notes regarding other reviews:
Scott Fluhrer mentions an issue in the proof of passive and MITM 
security, which to me is not a concern. Namely, he indicates that there 
exists a distinguisher between Ext2 and Ext3. In this game hop, random 
self-reducibility of CDH is exploited to plant a CDH problem instance 
into hashed outputs of participants, such that any hash query of a 
distinguisher would contain a CDH solution. Scott's concern is that 
parts of the CDH problem instances could be adversarially generated (and 
thus self-reducibility does not help in replacing MITM-attacked 
instances). However, Ext3 only replaces outputs of sessions that are 
*not* attacked by a MITM (indicated by "for all sessions generated via 
an Execute oracle query"). Instead, those sessions are handled only in 
Ext4 where the analysis correctly concludes that the attacker can only 
distinguish replacement of the RO in case he guesses the correct 
password. Therefor I don't see any issue with the proof.

Comments:
Both security proofs seem sound to me. If possible, 
draft-irtf-cfrg-spake2-09 should demand a gap-DH group instead of a CDH 
group such that SPAKE2 is guaranteed to achieve forward secrecy. Since 
all variants discussed on the list of generating M,N will leave the 
proofs valid, security-wise the only concern is that system-wide M,N 
would hinder quantum annoyance, which seems already well-known to everybody.
Clearly, a strong point in favor of SPAKE2 is that proofs show that only 
one RO suffices to obtain strong guarantees.
My main concern is that the protocol in the RFC is not the one analyzed 
in the papers. Some modifications seem to add to its security (e.g., 
using w=MHF(pw) mod p instead of pw partly mitigates the fact that 
security is only analysed wrt randomly distributed passwords), but for 
others it is less clear (e.g., usage of cofactor h, cf also Karthik's 
review) and more analysis needs to be carried out. I am also slightly 
worried that the authors of draft-irtf-cfrg-spake2-09 say that key 
confirmation is mandatory while security analysis clearly shows that it 
is not necessary. I am not an expert in implementing crypto protocols, 
but to me it seems desireable to state SPAKE2 without key confirmation 
and leave it up to the application protocol if/how key confirmation is 
implemented.

CPace
=====
I reviewed the updated security analysis 
https://github.com/BjoernMHaase/AuCPace/blob/master/aucpace_security_analysis_20200208.pdf 
and the specification https://tools.ietf.org/html/draft-haase-cpace-01. 
For details on how to implement Map2Point I looked at the most recent 
version of the original CPace publication at 
https://eprint.iacr.org/2018/286.

Security pro's and con's:
+ Strong security notion with adversarially-chosen passwords, 
composability, adaptive corruptions and forward secrecy
+ Security properties do not rely on key confirmation
+ CPace is quantum annoying
+ Security proof covers multi-party & multi-session setting (including 
re-use of passwords)
- Security proof does not analyze distinguishing advantage, thus I also 
cannot say whether the proof is tight
- Trusted setup required for Map2Point
- Heavy use of random oracles (2, both are programmed)
- Proof posted only in 2019 with several issues already discovered (and 
probably containing more, see below)
- No quantum preparedness, no option to switch to it, limited crypto 
agility since not a modular protocol

Note on sid handling:
As clarified by Ran Canetti, the sid can be chosen by the initiator and 
transmitted to the responder. Security-wise let me note that the sid 
does *not* have to be randomly distributed, and it does *not* have to be 
kept secret. It only has to be unique system-wide (e.g., contains a 
nonce or counter and some addressing information of both initiator and 
responder, which needs to be unique anyway to correctly route the 
message). CPace is thus a 1-round protocol assuming that the application 
protocols allows transmitting the sid along with the initiator's first 
message.

Comments:
Even though the author(s) continuously improve the security analysis of 
CPace, I am still not able to follow. One reason is that it is a 
simulation-based proof without any formal indistinguishability 
arguments. Another reason is that, while the proof is written as a 
sequence of games, most non-trivial changes happen in the step Exp2 to 
Exp3. In this step it is shown how to simulate a CPace execution without 
knowledge of passwords. However, all possible corruption scenarios 
(corrupted initiator, corrupted sender, and different times where these 
corruptions can each happen) are handled simultaneously, resulting in so 
many different cases that, at least to me, it is impossible to say 
whether the simulation is complete.
While the security definition in the UC framework originates from a 
paper of 2005 by Canetti et al, it had to be adapted to allow for proofs 
of implicit authenticated CPace. On the plus side, adaptation has been 
done in coordination with, among others, authors of OPAQUE who face the 
same problem since they use also the UC framework. However, it still 
seems to me that the changes made are not sufficient for CPace to 
realize the current version, called F_ipwKE. An attacker leaving both 
parties uncorrupted but injecting a self-chosen Y_b will observe the 
hashed output of the initiator (obtained from F_ipwKE, oblivious to the 
simulator). If he then afterwards queries the random oracle on the 
shared secret Y_a^y_b, the simulator can use the newly introduced 
DelayedTestPwd query to learn whether the attacker and the initiator 
used the same password. However, to program the random oracle H_2 
according to this answer, the simulator needs to learn the output given 
towards the honest initiator. This is not possible with F_ipwKE.
This might seem nit-picky, and indeed I do not have any doubts that 
CPace UC-emulates a slightly revised but not crucially weakened version 
of F_ipwKE. However, the proof relies on heavy tools: two programmable 
random oracles and several properties of Map2Point (efficiently 
invertible such that dlogs of images can be chosen by the simulator 
etc.) which additionally require availability of a shared trusted setup 
among all protocol participants (called CRS in the paper). Let me stress 
that a UC secure balanced (!) PAKE protocol can be obtained *without* 
any idealized assumptions, although such a protocol would be less 
efficient than CPace. Still, the question remains what the current proof 
is worth: due to the heavy usage of idealized assumptions it is only a 
rudimentary sanity check of the protocol and it does not rule out a very 
large class of attacks exploiting properties of instantiations of any of 
the idealized building blocks.

Recommendation balanced PAKE
============================
While the proven guarantees for SPAKE2 are a bit weaker than for CPace, 
I do believe that they are sufficient for a widely deployed SPAKE2 not 
to have any serious security issues. For CPace, I unfortunately cannot 
state the same. Upon deployment and instantiation of Map2Point and the 
programmable random oracles, there are just too many things which could 
go wrong due to the strong/idealized assumptions on all of these 
components. In that sense, the analyzed protocol is too far away from 
what will be actually deployed. Security-wise I thus recommend SPAKE2, 
conditioned on a thorough analysis on usage of cofactors.

AuCPace
=======
I reviewed the updated security analysis in 
https://github.com/BjoernMHaase/AuCPace/blob/master/aucpace_security_analysis_20200208.pdf.

Security pro's and con's:
+ Strong security notion with adversarially-chosen passwords, 
composability, adaptive corruptions and forward secrecy
+ Security properties do not rely on key confirmation
+ Modular: AuCPace can be instantiated with any (implicit) UC-secure 
balanced PAKE
+ Minimal usage of idealized assumptions (1 programmable RO)
- Proof not convincing without further analysis

Comments:
After thoroughly checking the proof of the implicit (not strongly 
secure) AuCPace I am unfortunately not convinced that AuCPace can be 
proven UC secure (i.e., to emulate F_aipwKE as stated in the paper). 
While the authors give a simulator for AuCPace, they do not give any 
arguments why this simulation is sufficient. Such arguments should be 
intelligible from the sequence of games they provide. Below is an 
incomplete list of issues with this sequence.
* The first game is the real execution without F_aipwKE, and none of the 
games introduce (any part of) this ITI. But then, the last game suddenly 
contains F_aipwKE.
* Games G_2,G_3(1),G_3(2) do not say how to formally change the 
execution, nor do they contain formal reductions to, e.g., CDH.
* Game G_4 contains no indistinguishability arguments despite the fact 
that almost all changes happen from G_3(2) to G_4
* The newly introduced interfaces are analyzed only rudimentary: G_4 
lets the simulator relay Interrupt and DelayedTestPwd queries towards 
F_ipwKE to F_aipwKE. According to the text, this should work because the 
interfaces in both functionalities are equal. However, whether F_aipwKE 
gives an answer that can be used to simulate F_ipwKE depends on the 
*values* set in the functionalities. To say the least, one has to prove 
that dPT=1 in F_aipwKE whenever dPT=1 in F_ipwKE.

OPAQUE
======
I reviewed the security analysis in https://eprint.iacr.org/2018/163.pdf 
(rev of Oct 22) and the specification in 
https://tools.ietf.org/html/draft-krawczyk-cfrg-opaque-03.

Security pro's and con's:
+ Strong security notion with adversarially-chosen passwords, 
composability, adaptive corruptions and forward secrecy
+ Security properties do not rely on key confirmation
+ Modular, good crypto agility
+ Security proof covers multi-party & multi-session setting (including 
re-use of passwords)
+ No idealized assumptions outside of building blocks required
- No quantum preparedness and not quantum annoying

Comments:
OPAQUE's security proof is wrt the same strong model as AuCPace. OPAQUE 
is modular, using KCI-secure AKE and an OPRF as building blocks. OPAQUE 
is nowhere close to quantum prepared since it is a long way towards a 
quantum-safe OPRF that is efficient enough. The protocol comes with an 
impressive security analysis that does not leave a lot of wiggle room. 
Obvious downsides are the complexity of the current proof (~20 pages in 
the OPAQUE paper, plus one has to assemble the HMQV security proof from 
few other papers) and the fact that it is relatively new and thus 
presumably not checked by many people.
I checked the (evolving) proof of OPAQUE already few times, and with the 
current version I find only one issue I could not (trivially) solve 
myself: the non-modular way in which HMQV is used. Namely, HMQV's 
security proof is wrt a protocol-internal key generation algorithm 
setting up a key pair for each user. When using HMQV modularly, those 
keys would never "leave" honest parties. However, in OPAQUE the keys are 
generated and used outside HMQV (they form the password file and are 
send, encrypted with the OPRFed password, from the server to the user). 
Still, the OPAQUE proof uses the HMQV simulator as a sub-algorithm. I am 
not convinced that this simulator can be run on externally-chosen keys. 
For example, in an honest execution the saPAKE adversary can, after a 
successful key exchange, try a late password guess by decrypting any 
ciphertext sent by the server. The adversary then learns the HMQV keys 
*without corrupting any party* and can compute the shared HMQV secret of 
those parties. It seems to me that this is not simulatable by the saPAKE 
simulator without learning the session key generated by honest protocol 
participants. (Note: this is a similar issue as described for CPace above.)

Recommendation augmented PAKE
=============================
Both proofs come with similar pro's. The conducted analysis of OPAQUE is 
clearly superior to the one of AuCPace. Conditioned on me being wrong 
about the issue with HMQV's keys, or the authors being able to fix it, I 
thus recommend OPAQUE.