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

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

Dear Hugo, dear PAKE enthusiasts,

I can confirm the AMAZING work of Björn Tackamm and I also would like to
thank
very much Julia Hesse for her help. I would also like to stress that my
impression is
that most people involved in this PAKE selection process seem really be
dedicated
to the work of trying to improve security and not primarily to push
their favorite
pet.

Similarly to OPAQUE, I will soon again be publishing a revised and more
comprehensive
version of the security proofs for AuCPace and CPace. Anybody
interrested in the preliminary
version could give a note. (Target deadline for the revised AuCPace
proof: This weekend.)

Since both, AuCPace and OPAQUE
have much in common due to the same ideal functionalities, I would like
to come up
with a possible issue that I observed when re-working AuCPace and CPace
which I believe to
be shared with OPAQUE.

Thank's to Julia's review we realized that also in the case of AuCPace
and CPace we needed
an adaption to the ideal functionalities very much in the same style as
for the "relaxed"
version of SaPWKE in OPAQUE. In my opinion this "relaxed" functionality
somewhat
captures the difference between "perfect forward security" in a protocol
with mutual
explicit authentication and "weak forward security" in case of implicit
authentication.
(As Hugo has pointed out in his HQMV paper).

In this context I realized that the current formulation of relaxed
SaPWKE in the OPAQUE
paper un-intentionally allows the adversary for two (!) password guesses
per session.

In the OPAQUE paper it currently reads

On (TestPwd,sid,ssid,S,pw∗) fromA∗, if there is a
record〈ssid,S,U,pw〉markedcompletedwith session keySK, and this is the
firstTestPwdmessage for ssid and S, do: if pw∗=pw, returnSK to A∗; else
return “wrongguess.”

The problem is, that the adversary might run the protocol honestly using
NewSession and NewKey queries using a controlled
party P_j, testing one password and use a "late" TestPwd query in
addition. The "relaxed" query in its current form from the OPAQUE paper
seemingly also allows for a passwort guess for a protocol run between
two honest parties.?

I think that one should rule out "late" TestPwd queries for the password
of P_i in a session between a "completed" P_i and a P_j also in the case
that the session of party P_j has entered state "completed". I.e. one
would have the wording "if there is a
record <ssid,P_i,P_j,pw> with session key S and this is the first
TestPwd message for ssid and S and there is no record for
<ssid,P_j,P_i,pw*> marked completed."

Maybe this is something you (OPAQUE-People) could fix in the very same step.

Yours,

Björn.

Am 17.09.2019 um 07:30 schrieb Hugo Krawczyk:
> Dear PAKE enthusiasts,
>
> We want to thank Bjorn Tackmann for an AMAZING work in verifying the
> OPAQUE
> proofs. In his report below he has identified two issues where there
> are gaps in
> the proof. One of them is mostly formal in our view and has to do with the
> mechanics of the UC model. The other is more substantial and indeed
> requires
> an adjustment of the proof and a restriction in the modeling of the
> Authenticated
> Encryption piece in OPAQUE (but does not entail any change to the
> protocol).
> We are going to check carefully that this indeed addresses Bjorn's
> finding and
> we will report back to this list. We want to point out that in
> addition to his
> report to cfrg, Bjorn provided us (privately) with important comments
> that will
> help improving the paper's formalism and presentation considerably..
>
> We have also received super useful comments from Julia Hesse that helped
> improving several aspects of the paper, including the OPRF formalization.
>
> Note: The version of OPAQUE in eprint has a hard-to-read (sketchy) proof.
> We have a better version that we will post shortly but we first want
> to make
> sure we are resolving correctly Bjorn's and Julia's comments. If anyone is
> interested to read the proofs directly, please write to us (e.g., my
> email here)
> and we'll send the paper in its current form.
>
> Stas, Hugo and Jiayu
>
> On Sun, Sep 15, 2019 at 11:11 AM Bjoern Tackmann
> <[e-mail] <mailto:[e-mail]>> wrote:
>
>     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).
>
>
>
>     _______________________________________________
>     Cfrg mailing list
>     [e-mail] <mailto:[e-mail]>
>     https://www.irtf.org/mailman/listinfo/cfrg
>
>
> _______________________________________________
> Cfrg mailing list
> [e-mail]
> https://www.irtf.org/mailman/listinfo/cfrg