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

From: Bjoern Tackmann <[email-masked]>
Date: Sun, 15 Sep 2019 17:11:23 +0200

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

---

From: Hugo Krawczyk <[email-masked]>
Date: Tue, 17 Sep 2019 01:30:13 -0400

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

---

From: Björn Haase <[email-masked]>
Date: Tue, 17 Sep 2019 09:00:06 +0200

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:
> proofs. In his report below he has identified two issues where there
> are gaps in
> 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..
>
> interested to read the proofs directly, please write to us (e.g., my
> email here)
> On Sun, Sep 15, 2019 at 11:11 AM Bjoern Tackmann
> <[email-masked] <mailto:[email-masked]>> 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..
>
>     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.
>
>     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.
>
>     - 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
>     - 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
>
>     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
>     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).
>
>
>
>     [email-masked] <mailto:[email-masked]>

---

From: Björn Haase <[email-masked]>
Date: Sun, 22 Sep 2019 22:26:01 +0200

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 mo…

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.

> - 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 larg…
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…

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.

> - 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 no…
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 verifyin…

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.