Re: [Cfrg] Comments on the CPace proof and the CFRG PAKE selection process

Dear Michael,

so far the CFRG PAKE selection process since finalization of RFC8125 has
been governed
in my perception with a serious attitude of all participants, despite
the fact that any
contributor also feels some emotional attachment to his own work.

Your last post, in contrast, does remind me earlier PAKE mail cascades
that predate the
structured process in that it does not seem to contribute a constructive
feedback
suitable for advancing the CFRG process.

For instance, you seem to complain without concrete suggestions
regarding how to
proceed and move things forward constructively.

You forced me to rectify things from my vacation (on a borrowed smart
phone with a strange
german "typing correction" feature, sorry for that) and you now force me
to write an overly
long response which in my opinion might largely stem from the fact that
you might have
just overlooked an important section in the proof papers. (I concede
that important parts
of the paper that relate to your mail could have been written better.)

It's not at all about keeping "things under the table", but with a first
direct personal
communication to people that might feel criticized, you might have
reduced the risk of
emotional injuries that could be highly detrimental.

As mentioned in my earlier preliminary response, I believe that apart of
an important
aspect of the CPace proof that you seemingly have overlooked, the main
topic that you
would like to bring up seems to relate to the form of collaboration
contract between
different expert security domains, such as "security proof expertise",
"side-channel
expertise", and "speed/security tradeoffs".

It is my conviction that in order to get the best feasible security in
real-world settings
(as considered by the IETF) needs adequate consideration of all
subdomains. In my opinion,
on the protocol proof level this includes, for instance, the need to
consider the practical
security advantages of "x-coordinate-only" Diffie-Hellmann. This
requires a certain level
of flexibility in the protocol specifications. On the other hand, most
security people
will agree on the assumption excessive flexibility is harmful.

Me with my background in secure implementation on extremely constrained
targets am obviously
taking a very different initial approach from you with your background
on academic security
proofs. For instance, I believe that the protocol designer should really
allow for
a sufficient flexibility in the protocol construction, e.g. for
optimizing for side-channel
resistance or suitability with existing encoding standards, while you
might have the
tendency to leave no flexibility at all (e.g. by ruling out
x-coordinate-only style algorithms
such as X25519 by the protocol design in the first place).

Similarly, I believe that known aspects such as resilience with respect
to quantum computers
should be considered by protocol designs, even if formalized theoretical
models are not yet
available or even feasible, while you seem to advocate for the opposite
position.

For the larger CFRG audience, I apologize for the possibly excessive
length of my answers
in this mail, but I would like to respond to your mail in all points and
would finally come
up with a suggestion on how to proceed.

1.) Adaptive security and reduction to the SDH problem:

The main difference between the CPace protocol on one side and TBPEKE
and SPAKE2 on the other
side is the use of a mapping primitive that converts bit strings to
group elements.
Mostly, e.g. in the discussion of the "Hash to curve" draft, the aspect
of conversion from
strings to group elements is highlighted. Still also the other way
round, i.e. conversion from
group elements to strings, has an important field of applications, e.g.
regarding privacy and
censorship circumvention (Note the corresponding questions came up
specifically regarding this
point during Riad's CHES2019 presentation.).

This conversion from a curve point to a string indistinguishable from a
random string plays
a crucial role in the security proof of CPace and allows for a proof of
security without having
to rely on the "GAP" variants of the underlying problems.

For the following discussion I will mainly refer to the security proof
as shown in
https://github.com/BjoernMHaase/AuCPace/blob/master/aucpace_security_analysis_20200208.pdf.
(Michael note, that I did not place this paper on the IACR eprint server
specifically because
I saw the need to add proper reference to your recent UC PAKE paper
previously. Unfortunately
in these Covid-19 times I did not yet find the time to spend on this work.)

The availability of the "inverse" direction of the Map2Point operation
is detailed in assumption
A2 in section 5.4.. This assumption A2 allows the simulator to simulate
the hash function H_1 such that for any string ST the descrete log x of
the point
X = B^x = Map2Point(H_1(ST)) is known to the simulator. (game G_1,
Section 5.4.2.)

This feature makes the difference with what is possible with
constructions that don't use
a Map2Point primitive such as Elligator2. For TBPEKE and SPAKE2 versions
that don't use such
a mapping the simulator does not have access to the discrete log.
As you have pointed out correctly, availability of the discrete log of
Map2Point-generated points
for the simulator is mandatory for adaptive security and for a proof
that does not rely on
"GAP" variants of the hard problems.

As such, it is natural, that the UC security analysis for TBPEKE and
SPAKE2 need availability
of a DDH oracles later on in the proof as means for solving the
computational DH (computional
SDH) problems. Your need for adding the password and the transcript also
to input string for
the final hash operation that generates the session key also shows up in
the very same
context (because it gives you the exact candidate inputs to pass to the
DDH oracle).

Note also that use of a Map2Point primitive also is at the core of the
resilience of CPace
against quantum-computer assisted attack strategies ("quantum annoying
property" as intruduced
by Steve Thomas in the course of the PAKE selection process.).

In the proof (transition from game G_2, G3), the direct link between
indistinguishability of
the two games and the capability of the environment algorithm to solve
the SDH problem shows
up in the context of a setting where one honest party (whose password is
not available to the
simulator) interacts with the environment algorithm. The passive case of
two honest parties
directly reduces to the CDH problem.

Please let me thank Stanislav Jarecki for his analysis and guidance from
December 2019 regarding
the aspects that I will be writing below:

The honest party in game G_2 will follow the protocol and query sk =
H_2(K) for the result point
K of a Diffie-Hellmann group operation. The environment will be given
this "sk" result of this
calculation and could query H_2 himself for own inputs.

The difficulty for the simulator in G_3 arises because it needs to
convert environment-generated
queries to H_2 into TestPwd queries for the ideal functionality for the
honest party. More
specifically, the problem for the simulator is, that exactly one such
TestPwd query is available
and the password needs to be guessed by the simulator.

For the UC proofs for SPAKE2 and TBPEKE, the simulator has no way for
guessing the password
and needs to be given it as included input to the H_2 query. There the
oracle for the decisional
problem enters the procedure (for SPAKE2 and TBPEKE) and identifies the
case that the
environment also did follow the protocol. If this condition is observed,
the simulator did learn
the password and could issue the TestPwd query for the ideal
functionality and possibly
program the H_2 RO output values to possibly match a value that
previously might have been
passed to the honest party.

In contrast, for CPace, the availability of an inverse Map2Point allows
the simulator to identify
the condition and learn the password used by the environment (Section
5.4.5, last paragraph on
page 18) *without* needing an oracle for the decisional problem. The
simulator will ask the
TestPwd query at the ideal functionality and possibly program the H_2
output (just as in the case
of SPAKE2 and TBPEKE). The simulator algorithm will fail if and only if
the environment in G_3
is able to come up with *two* of such suitable candidate points because
otherwise the H_2 outputs
of G_2 and G_3 would be indistinguishable because the simulator strategy
fails. In all other
conditions, the H_2 outputs would be indistiguishable for the
environment in G_2 and G_3:
- If the input points to H_2 were not generated by a Diffie-Hellmann
calculation, the honest party
and the simulator get different results with overwhelming probability in
both games.
- If the input points were generated with a Diffie-Hellman calculation
with a password-generated
base point and matching passwords, the same results will be given in
both games.

I.e. if the environment was able to distinguish G_2 and G_3 by the
generated H_2 outputs it
has been able to solve an instance of the SDH problem.

As mentioned in my preliminary response, I am against adding the
clear-text password
again to the final hash as you did seem to suggest in your mail. In my
opinion we should
treat hash operations with great care with respect to side-channel
leakage, since these are
typicall *very* difficult to protect against power analysis.

2.) Regarding implicit and explicit mutual authentication:

Througout the CFRG selection process, in my opinion significant advances
in research have been
made regarding appropriate formulation of the ideal PAKE
functionalities. Here Julia Hesse's
paper and the reworked OPAQUE proof paper in addition to your UC-PAKE
paper for SPAKE2 and
TBPEKE have provided significant input. As a consequence, for protocols
without explicit
authentication a "relaxed" functionality has to be used in the security
proof which includes
the capability of the adversary to add "delayed" test password queries
even if a player has
already received his session key. (We both seem to agree that this
feature decides upon
"weak forward security" vs. "perfect forward security" properties.)

The original ideal functionality that has been used by GMR06, the
Eurocrypt version of the
OPAQUE paper and the TCHES version of AuCPace / CPace did aim at
allowing the flexibility
to allow for both, implicit and explicit authentication. Both teams
aimed at deviating from
the GMR06 verion as little as possible. As pointed out by Julia Hesse in
here
recent paper, the GMR06 formulation of the ideal functionality with its
"test Abort" query
was clearly un-satisfactory.
The reason for adding the flexibility with respect to explicit or
implicit authentication
has been the fact, that some applications might need the explicit mutual
authentication, while
for other applications this might result in unnecessary overhead.

As a consequence, specifically of the insights after Julia Hesse's
analysis, both the OPAQUE and
the CPace and AuCPace security proofs have seen a major rework. In the
latest analysis of the CPace
and AuCPace protocol, I have concentrated in the implicitly
authenticated version which provides
weak forward security.
As your own work demonstrates, the most suitable UC formulation of PAKE
functionality now seems
to have stabilized. Note that your relaxed ideal functionality from your
March 15th paper is
(virtually) identical to the one used in the latest CPace proof from
February, so your results
carry over to CPace.

Your own https://eprint.iacr.org/2020/320.pdf paper shows the principle
how explicit authentication
can added, as shown in section 4.

Also in the https://eprint.iacr.org/2018/286.pdf the augmented
AuCPace protocol includes an implicitly authenticated CPace as a
building block and as a
consequence the "relaxed" delayed password tests vanish.

Regarding the decision of explicit or implicit authentication, I would
like to advocate to leave
it to the application by allowing both. I think that this captures the
real-world needs best.

3.) Regarding the need of inclusion of the full transcripts for CPace

The "interrupt" (in your paper "RegisterTest") query captures the
capability of the adversary
to act destructively such that two honest party won't successfully
authenticate. If the
full transcripts are not included, the
adversary is given the capability to change his mind and "undo" his
earlier interaction with
two honest parties, such that two honest parties with the same password
successfully authenticate
again in the real world. The only way to achieve this is to replace both
exchanged points by
arbitrary multiples of the originally transmitted points of the honest
parties.
(The corresponding discussion is found in section 4.3 of
https://eprint.iacr.org/2018/286.pdf) .
This actually does not modify the real-world security picture in any
meaningful way. Still
parties only authenticate iff the passwords match and the adversary does
not learn anything
on the password with or without transcripts.

I.e. protocols both, with and without included transcripts are secure in
the real world meaning
of security: The adversary is not given any power that is useful.

In the latest version of the proof (february github version of the
paper), I decided to
follow Björn Tackmann's suggestion of avoiding the need of an additional
"undo interrupt"
query in the ideal functionalities. Specifically, for the augmented
AuCPace proofs, the
augmented functionalities would no longer have fit on one page.
In the earlier papers, I still aimed at avoiding the amount of RAM
required for storing the full
transcript for tiny embedded targets. Note that such a consideration is
certainly completely
irrelevant for PCs or smart phones but could provide difficulties on
very small targets. My
personal feeling was that one should probably make the full transcripts
an optional feature,
but as you know, I did follow Björn Tackmann in the latest revision of
the paper.

This is one aspect, where I'd advocate to leave this flexibility to the
application, while you
obviously consider it mandatory that no flexibility at all must be
given. Also note, that seeing,
that the impact on the security properties was negible in my perception,
I did give the aspect
of the transcripts little room in the paper.

I am having a problem with the fact that you use the terminus "insecure"
in this context, since
this implies that you suggest, that the authors and CFRG reviewers would
have overlooked a
crucially important aspect, which leads to a practically exploitable attack.
In fact all of the aspects for which you declare the protocols in the
TCHES paper "insecure"
in your mail are extensively discussed in the respective papers and
don't have any impact on
the security guarantees regarding authentication checks.
As you know the terminus "insecure" is commonly used for protocols that
claim security features
that are broken by demonstrated attacks, what is clearly not the case here!

Similarly, demonstrating an attack rendering CPace "insecure" in the
light of an adversary which
exchanges Y_a with -Y_a for a protocol which declares in its definition,
that it does
treat Y_a and -Y_a as identical from the very beginning, could be
considered as misleading
nit-picking. Making it mandatory that any binary representation is
completely un-ambigous
is likely to prevent that any re-use of existing encoding standards is
possible.

Again this aspect touches the "contract" between the implementer's needs
and the "protocol
designer's" duties. Considering the concept of "groups modulo negation"
or "x-coordinate-only"
Diffie-Hellmann adds complexity for the proof analysis. You seem to be
reluctant to take into
account as part of the duty of the protocol designer.
On the other hand if this complexity is considered (as in the CPace
proof), this opens significant
opportunities for the implementer for getting better results in the
speed/implementation security
tradeoff. For instance, you could constrain invalid curve attacks to the
curve and it's quadratic
twist. For this reason, the CPace draft requests that the sign
information SHALL be removed.

On the other hand, there might be applications, such as the recent CPace
prototype implementations
on ristretto255 where this mandatory removal of the sign should probably
be made optional. For this
purpose the "contract" form between the designer of the protocol and the
user would need to be
even more flexible than I originally suggested. In the Ristretto
framework, the sign information
should not be removed, while for conventional Short-Weierstrass and
Montgomery curves the sign
should be disregarded. One of the Ristretto advantages is to provide a
clear form of
protocol-designer/implementer "contract" and any protocol design for
this eco-system should be
in line with these assumptions.

Summary and suggestion for moving things further:

Summing up, I don't want to blame you for excessive nit-picking.
Security largely *is* about
nit-picking and your input here is valuable and appreciated.

Still I'd like to keep in mind that there *is* a need for a secure PAKE
protocol for various
applications and that we don't improve security by delaying the process
inadequately or by
spreading fear and doubt. CFRG is also but not exclusively a forum of
security proof experts
that directly grasp all the nuances of the meaning of your wording.
I'd kindly ask you to keep this in mind.

The topics regarding SDH reduction and adaptive security are resolved
IMO by the features that
come with the requirement that Map2Point comes with an inverse Map2Point
whose result
is required to be indistinguishable from a random string.

The remaining topics that you did bring up are, IMO, mainly related to
different understandings
on the form of the "protocol designer" and "implementator" contract
which I suggest to be
discussed in the process of the CFRG guidance document.

This topic might also justify wider discussion in the CFRG community and
should IMO involve
people with a strong background in secure implementation and expertise
in the speed/security
tradeoff domain.

Please feel also free to contact me directly in order to clearify
aspects. You might recall that
I explicitly tried to get your expertise involved when I had sent early
preprints of the AuCPace
paper to people like you.

Yours,

Björn

Am 02.06.2020 um 00:41 schrieb Michel Abdalla:
> Hi everybody,
>
> Given that CPace has been selected as the balanced PAKE option, I
> believe it is important to make a few comments about its security as
> well as the CFRG PAKE selection process.
>
> 1) Inclusion of the protocol transcript in the key derivation function
>
> Although the latest RFC for CPace (link
> <https://datatracker.ietf.org/doc/draft-haase-cpace/>) includes the
> protocol transcript in the key derivation function (suggested by
> Bjoern Tackmann), the security analysis in the corresponding paper
> (link
> <https://github.com/BjoernMHaase/AuCPace/blob/master/aucpace_security_analysis_20200208.pdf>)
> does not clearly state the reasons for it. In particular, when
> examining the proof, the inclusion of the transcript during the
> computation of ISK has not been applied consistently throughout the
> paper and the analysis does not seem to make use of this fact.
>
> Here I would like to point out that this requirement is a hard one.
> Without it, the protocol would be insecure. To see why, just consider
> the following man-in-the-middle attack during an execution between a
> server and a client having the same password.
>
> (a) When the server sends Y_a, the attacker forwards Y_a^2 = G^{2 y_a
> c_j} to the client
> (b) When the client sends Y_b, the attacker forwards Y_b^2 = G^{2 y_b
> c_j} to the server
> (c) The client and the server would compute the same ISK despite
> seeing different messages, since the key used to derive it would be
> the same: G^{2 y_a y_b c_j^2}.
>
> 2) Trivial malleability attacks
>
> When introducing the protocol transcript in the key derivation
> function, the current RFC for CPace does not use the actual values of
> Y_a and Y_b to compute ISK. Instead, the input of the key derivation
> function uses strip_sign_information(Y_a) and strip_sign_information(Y_b).
>
> One problem with this is that trivial modifications of the messages
> (for instance by changing Y_a to -Y_a) by a MITM attacker would not be
> detected by honest parties since the final key derivation does not
> properly bind the session keys to the transcript.
>
> Although such an issue can be easily fixed by avoiding the use of
> strip_sign_information(), it clearly shows an important gap in the
> current proof.
>
> 3) Reduction to SDH
>
> The reduction to the SDH problem in the latest version of the Haase’s
> paper is still not given explicitly. Hence, right now, the security
> analysis only shows that the SDH is a necessary assumption but not
> necessarily sufficient.  Though such a reduction might be possible, I
> still don’t see exactly how it can be done so it would be nice if the
> Haase and Labrique could address this gap in the proof.
>
> In a separate paper currently available on ePrint (link
> <https://eprint.iacr.org/2020/320>), we provide proofs in the UC model
> for SPAKE2, TBPEKE, and SPEKE. Our results for TBPEKE and SPEKE can
> also be extended to CPace but only in the case where the key
> derivation includes the transcript of the communication (which is
> required) and the password (we may be able to remove this requirement
> with further analysis).
>
> As stated in the paper, our proofs for SPAKE2 and TBPEKE rely on the
> gap versions of the CDH and SDH assumptions. In particular, the
> Decision Diffie-Hellman oracle is used throughout these proofs to
> maintain consistency of answers to RO queries, and that this is needed
> even to deal with sessions in which the adversary is passive: the
> reduction still needs to be able to consistently deal with the
> sessions where the attacker is active and the attacker may adaptively
> decide to launch an active attack after seeing one of the protocol
> messages. In the case of SPAKE2, removing the need of a gap assumption
> might be possible given the recent result by Shoup (link
> <https://eprint.iacr.org/2020/313>).
>
>
> 4) Static versus adaptive UC security
>
> Our proofs of security for SPAKE2, TBPEKE, and SPEKE in
> https://eprint.iacr.org/2020/320 only assume static corruptions and it
> would be interesting to extend them to deal with adaptive corruptions,
> but doing so does not seem straightforward.
>
> The current security claim for CPace in
> https://github.com/BjoernMHaase/AuCPace/blob/master/aucpace_security_analysis_20200208.pdf still
> claims adaptive security. Unfortunately, since the reductions to the
> SDH problem are not explicitly given, one cannot verify how
> corruptions can be handled during these reductions. Note that, when
> reducing to the SDH problem, the reduction would not know the discrete
> log of some of the values being exchanged and, hence, it might be hard
> to know how to properly answer adaptive corruption queries.
>
>
> 5) Perfect forward secrecy vs weak forward secrecy
>
> The UC relaxations used in the proofs of security of CPace, TBPEKE,
> SPEKE, and SPAKE2 are not known to imply perfect forward secrecy
> without an additional key confirmation step. In particular, the notion
> of lazy-extraction UC PAKE in https://eprint.iacr.org/2020/320 is only
> known to imply weak forward secrecy. Interestingly, proving perfect
> forward secrecy without the key confirmation step seems to be
> significantly harder. In the case of SPAKE2, we were able to provide a
> game-based proof for it under gap CDH (see
> https://eprint.iacr.org/2019/1194) but the reduction is not tight and
> requires an intermediate assumption previously used in the proof of
> SPAKE1. A similar result is currently not known for CPace, TBPEKE, and
> SPEKE.
>
>
> 6) Comment on the CFRG PAKE selection process
>
> Since the selection process is now over and I no longer have a
> conflict of interest, I would like to end this email by commenting on
> the CFRG PAKE selection process.
>
> On the one hand, the selection process highlighted several important
> security aspects for real-world PAKE schemes, such as side-channel
> resistance and quantum annoyance. The notion of quantum annoyance is
> actually quite interesting and something which we never considered
> when designing SPAKE2 back in 2005. Nevertheless, I also find it hard
> to argue that a protocol can satisfy it, since this property was never
> formally defined, let alone formally proved to hold for any of the
> candidates.
>
> On the other hand, I was a bit surprised to see that concerns about
> security proofs were often ignored in the process. Among the 4
> candidates for balanced PAKE, CPace seems to be the one for which
> nobody was ever able to verify its proofs. Yet, its theorems and
> strong security claims were mostly taken for granted because people
> seemed to believe that a correct proof for it could be given (me
> included) and this seemed to have played an important role in the
> process. However, what the different MITM attacks given above show is
> that the security of CPace is still not very well understood. In
> particular, the current version of CPace still lacks appropriate
> verifiable proofs and all the versions of the CPace scheme in
> https://eprint.iacr.org/2018/286 and TCHES are insecure.
>
> As a result, moving forward, I would strongly recommend against taking
> security statements for granted if they cannot be verified. Moreover,
> I also believe that the issues with the security proof of CPace should
> be fully addressed before proceeding with any formal specification of
> the latter.
>
> Regards,
> Michel
>
> PS: I would like to acknowledge the help of Manuel Barbosa with whom I
> discussed the security issues mentioned above.
>
>
> _______________________________________________
> Cfrg mailing list
> Cfrg@irtf.org
> https://www.irtf.org/mailman/listinfo/cfrg