[Cfrg] proofs for augmented PAKEs

[Hugo Krawczyk <[e-mail]>]

In Stanislav's excellent presentation today there was a slide about whether
the mentioned schemes have proofs.

In the cases of augmented schemes SPAKE2+, AugPAKE, VTBPEKE, Stanislav had
quotes from me regarding the existence of proofs.

I want to note that this is not a personal/subjective opinion. So let me
elaborate.

SPAKE2+ has given a design rationale in Section 9 of
https://eprint.iacr.org/2008/067.pdf

but no proof or model, or any form of formal argument was presented (or
intended). The protocol is presented as a potential application of
techniques in that paper whose main subject is not PAKEs.
I asked one of the authors and there is no other publication they have (or
that they know about) with such a proof.
I have no particular reason to believe the protocol is insecure but proofs
of augmented PAKEs are very tricky, including the theoretical modeling. So
a proof will be very welcome but not available now.
Let me stress that this applies to augmented SPAKE2+. The balanced version
SPAKE2 has a proof of security.

AugPAKE has an analysis in
https://eprint.iacr.org/2010/334.pdf

However the analysis is only in the balanced model. That paper does not
present a proof or model for the augmented case.

VTBPEKE has a proof  of security in a augmented PAKE model that allows for
pre-computation attacks.

Vulnerability to pre-computation attacks  (due to the need to send salt
over unprotected channel) is common to all the above protocols. As far as I
know OPAQUE is the first to be secure against such attacks. This is
significant since resistance to pre-computation attacks is what motivates
the notion of Augmented PAKE in the first place.

If anyone knows of information that changes the above description, please
let us know.

Hugo