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

[Hugo Krawczyk <[e-mail]>]

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]>
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]
> https://www.irtf.org/mailman/listinfo/cfrg
>