Re: [Cfrg] (Preliminary) review of augmented PAKEs

[Björn Haase <[e-mail]>]

Dear Björn (Tackmann),

I have just uploaded a revised version of the security paper for AuCPace
and CPace on the eprints

https://eprint.iacr.org/2018/286

The most significant change with respect to the previous paper version
is the corrction with respect to perfect and weak forward secrecy
regarding protocol variants with and without explicit key confirmation.

> 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.

I have re-worked the modeling of password registration. I now have
modified the ideal functionality F_apwKE such that it allows for
registering the password on the server P_j by a query of the client P_i.

Also I have reworked the formal procedure of password registration by
introducing a F_tunnel functionality for the confidential and
authenticated channel which is assumed to be used for password change
and password registering.

> 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.)
I have now added this requirement as additional statement for assumption
A1 for the CPace theorem. (Since both parties, client and Server, "halt"
after issuing the NewSession query to F_pwKE and F_pwKE already sends a
message to the adversary as reaction on the client and server'S
NewSession queries, the only way to make the protocol proceed seems to
be a message from the adversary.)
> - 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.

I agree with you that hashing full transcripts simplifies security
analysis a lot and doing so is kind of the "gold standard" for this type
of protocol. We were aware of this when designing the protocol.

However as AuCPace was explicitly designed to be tailored for smallest
targets, even the 64 or 128 bytes of additional RAM requirement for the
transcript were considered to be an issue. I agree that your suggestion
is also a safe choice and simplifies the security proofs. However, I am
still convinced that all of the security guarantees are maintained also
without "full transcripts". I have added a corresponding section 4.3
that considers this topic in more detail. Actually for subsystems like
TLS I would also advocate for "full transcripts", however for other
constructions that aim to be less resource-hungry, I'd like to keep the
option without full transcripts.

> 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.)
In fact, we need the external trigger from the adversary in order to
make the server party continue. We have added a corresponding statement
in the description.
> 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.)

I agree that the write-up would benefit from a complete rework from
scratch. (With my present knowledge I would have addressed the topic
completely differently). However we did not see to manage this re-work
within our target deadline of end of september latest. Thank you for
your patience and care.

One problem for us was, that we aimed at covering all of the different
possible combinations of "partial/full augmentation", "with / without
explicit key confirmation" and "with / without pre-computation attack
resistance" in one proof paper in addition to the complexity of adaptive
adversaries ...

In order to make the differences in the functionalities, assumptions and
protocol variants more transparent, we now have added an appendix E.

> 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).
Yes, I agree.