[Cfrg] (Preliminary) review of augmented PAKEs

[Bjoern Tackmann <[e-mail]>]

Hi all,

I had a look on the augmented PAKE candidates from a proof perspective. My results for AuCPace and OPAQUE are still a bit preliminary, in both cases I still see open issues. I am also trying to sort these things out with the authors.

Note that I did not judge the schemes in terms of their suitability or applicability, I really just looked at the security statements and proofs. I’ll be happy to give my take on the other aspects later in the process.

Please find details in my report below.

Best regards,
Björn


=====

GENERAL REMARKS

Two candidates (AuCPace and OPAQUE) have a security analysis in the UC framework. VTBPEKE has a security analysis in a game-based model. There is no security analysis of the full BSPAKE protocol; as the purpose of this report is to check security proofs, it will therefore not consider BSPAKE further.

While I don't know of a formal relationship between the security models considered here, it seems fair to say that the UC models are stricter in major aspects: (i) the distribution of passwords can be arbitrary whereas the security game assumes a uniform distribution over a given dictionary, and the same for each user, (ii) the adaptive-corruption guarantees are stronger; game-based adaptive “corruptions" are much more similar to UC static “corruptions" than they are to UC adaptive “corruptions", (iii) the security bound proven in the game-based version informally states that "the adversary will break the protocol with a probability that is only slightly larger than expected by password guessing". I expect that for real-life parameters on the Internet scale this bound will be trivial. (There is a leading term q_s/N, where q_s is the number of overall sessions actively involving the adversary and N is the size of the dictionary that the passwords are chosen from. Over time, q_s will be huge — it’s the number of all connection attempts that any adversary ever made.) In contrast, the UC formulations better model "a particular session is broken only if the password _of that session_ is guessed".

High-level remarks on AuCPace. There were several flaws in the security analysis, the authors addressed most in a recent revision. I re-checked the latest revision and still found few gaps, at this point I think I would suggest one change to the CPace protocol. Generally, I found it hard to verify the proofs.

High-level remarks on OPAQUE. The security analysis of OPAQUE linked in the submission material is incomplete. The authors pointed me to an updated analysis; yet, I currently still think there is a gap in the proof. My intuition is that the security statement may hold, but significant changes to the proof will be needed.

High-level remarks on VTBPEKE. I reviewed the proof and found it to be sound.

As far as I can tell, the security analyses of AuCPace and OPAQUE require a programmable random oracle, while this is not the case for VTBPEKE. This appears closely related to the stronger/weaker adaptiveness in corruptions. The analyses of OPAQUE and VTBPEKE appear to lend themselves quite well to estimating parameters such as key length. VTBPEKE even has a concrete security statement, while for OPAQUE the reductions appear pretty tight. AuCPace is analyzed in a purely asymptotic manner and does not allow for any such conclusions.


MORE DETAILS ON AUCPACE

I have reviewed the proofs for both CPace and AuCPace, as the latter builds on the former. Generally, the proofs in the paper are rather sketchy, and omit several formal steps (such as reductions, or even the full description of the simulator). I have first reviewed a version mid August and one mid September. (I will skip the parts where the authors addressed early feedback in the current version.)

One difference in modeling with OPAQUE is in user registration: AuCPace has an explicit user registration sub-protocol in which the user inputs the password and interacts with the server. OPAQUE models the cleartext password to be input by the server. The AuCPace modeling seems to better capture real deployments, but the modeling of this step in the analysis is inconsistent and evades the formal model. So at this point I’m not really happy with either.

Concrete issues in the current proofs:

CPace:
- In G1, the authors use Assumption 2 to argue that the image of Map2Point is large. This argument fails (the reduction does not work out), but as this property of Map2Point (that its image is large in J) should hold unconditionally for interesting candidates, it seems preferable to simply state and use this fact. (It fixes and simplifies the proof.)
- In G3, the flag DHFails is set if the adversary interacted with the Diffie-Hellman values "in a destructive way". However, one should note that the basis used in the original protocol and the one used in the simulation are not the same, it’s not a priori clear that "destructive” would be the same (or at least that would require proof). One fix for this is a modification of the protocol, namely computing sk = H2(sid || K || Ya || Yb) instead of sk = H2(sid || K) as done now; then any modification by the adversary will be destructive.

AuCPace:
- The protocol has an input (contimueAfterHashingParams, sid, ssid, P_i) [sic] that is never sent, which formally makes the server halt. It does not seem to be an input from Z, since Fawpke does not have it. It could also be a message from the client, but the protocol does not specify that either. (I think it should be an input of Fawpke.)

Overall, although I am not explicitly aware of further flaws and believe the protocol is secure, I found it impossible to be fully convinced by the proofs of CPace and AuCPace. (Especially verifying the completeness, meaning that all cases are covered, mostly due to the write-up.)

On tightness. The security statements are asymptotic, and cannot easily be turned into concrete security ones with good bounds (see, e.g., the step Game0 -> Game1 of the CPace proof).


MORE DETAILS ON OPAQUE

My review focuses on the proofs in Section 5 of the paper, as the AKE-based auPAKE with SIGMA as AKE seems to be the preferred variant. As with AuCPace, the authors have addressed some feedback and I list only current issues.

One first observes that the protocol in Figure 7 is not a well-formed ITM in the sense of the UC framework. In step 2 of the Login phase, the protocol is supposed to take two actions: send the ciphertext c to U, which activates A, and send (SndrComplete, ...) to F_OPRF, which in turn leads to an activation of A. If the AKE protocol is initiated by the server, this adds a third output to A. In consequence, those two/three actions cannot be performed within the same activation. This of course renders the security proof formally void, but tried to follow the main arguments nevertheless.

There is currently one major issue with the proof strategy that I am checking with the authors. Game 2 in the proof does not seem well-defined -- steps of the challenger in the game depend on future actions of the adversary. The underlying problem here is that outputting a value c = AE_rw(pc,Pc,Ps) in some session is committing the simulator to (pc,Pc,Ps). Informally: AE does not deal gracefully with the fact that the key may become public, which however happens when a password is guessed.


MORE DETAILS ON VTBPEKE

I found the proof to be sound. The only minor comment I have is that to me it seems that in Game 11, in the Send3 queries, the secret key in case 1 should be set consistently with the corresponding client session (since both may be affected by a Test query).