Subject: [Cfrg] some notes on OPAQUE and AuCPace

From: Hugo Krawczyk <[email-masked]>
Date: Mon, 18 Nov 2019 12:23:50 -0500

I would like to address some questions that we received off-list from
several people and may be of more general interest, this includes some
comments on the proof of AuCPace.

3-message OPAQUE: In a previous email I said that OPAQUE must provide full
forward secrecy (i.e., forward secrecy against active attackers) and this
implies that OPAQUE must have 3 messages. This is a property of any aPAKE
protocols where the first message from the client can be produced without
knowledge of the password (which is the case for OPAQUE). In principle,
aPAKE protocols where the first message depends on the password may use
just two messages. This clarification may be important since my observation
in the HMQV paper that implicitly authenticated protocols (i.e., where the
messages of the protocol do not depend on the parties' private keys) cannot
ensure full forward secrecy with only two messages, was misinterpreted to
say that NO forward-secure AKE protocol can use two messages (even though
in the same paper I gave examples of full AKEs with two messages). I hope
this clarification will help avoiding such misunderstanding in the aPAKE
setting.

Equivocable encryption: The proof of OPAQUE models the encryption that
produces the envelope EnvU as equivocable encryption. This means that there
exists a simulator (of the type used in cryptographic proofs) that can
generate a ciphertext before it knows the corresponding plaintext. This is
an abstract property needed in the proof but IT DOES NOT MEAN that the
encryption has such property in the real world. This is similar to the use
of "rewinding" in zero-knowledge proofs - no one expects to rewind proofs
in the real world, it's just a proof technique. In particular, equivocable
encryption can be modeled via programmable random oracles or ideal ciphers.
Moreover, the proof of OPAQUE can work with regular semantically secure
encryption assuming  "non-information oracles" as used for proving UC
secure channels in https://eprint.iacr.org/2002/059.  See also the next
paragraph for an encryption-less variant.

Optimizing EnvU and server state size: OPAQUE can be built so that the
envelope EnvU only contains the server's public key and a MAC value on it,
and  the server's state only contains the user's public key and a MAC on it
(in addition to protocol-independent user account information). The current
OPAQUE internet draft (v 03) contains a note on this. An additional
property of such OPAQUE variant is that it completely dispenses with the
above issue of equivocable encryption.

Adaptive security of OPAQUE: The current proof of the DH-OPRF function
works for non-adaptive adversaries only (we do not know of any adaptive
attack but the existing proof works for static adversaries). This
translates into non-adaptiveness in the proof of OPAQUE.

Adaptive security of AuCPace. The AuCPace presents a proof against adaptive
adversaries. We have no reason to believe the protocol is not secure
against such adversaries but we do believe that an adaptive proof would
need much more detail and completeness than the current proof to be
convincing (these proofs are very delicate and adaptiveness makes them more
so). Regardless, note that when one considers Strong AuCPace, the proof is
already non-adaptive because of the same reason as above, namely, the proof
of DH-OPRF on which Strong AuCPace would be based is non-adaptive.

On cryptographic assumptions (OPAQUE and AuCPace). Currently the proof of
OPAQUE depends on the Gap One-More DH (G-OMDH) Assumption on which DH-OPRF
builds plus any assumption the specific AKE in use requires. The current
AuCPace security claim only assumes CDH. However, this seems too optimistic
as CPace itself requires a stronger assumption (*). Moreover, Strong
AuCPace also requires G-OMDH as this comes from the DH-OPRF function that
Strong AuCPace uses. We also believe that the UC modeling of aPAKE in
AuCPace needs to be updated along the lines of the updates in the latest
eprint version of OPAQUE eprint.iacr.org/2018/163. The AuCPace proofs would
need to be updated and expanded accordingly.

(*) CPace requires the following 2-CDH assumption (if the attacker can
break the assumption, it can actually break the security of the protocol).
Assumption 2-CDH: Given input (G1,G2,X) of random group elements, output
values (Y,K1,K2) such that Y is a group element other than 1 and
K1=DH(G1,X,Y) and K2=DH(G2,X,Y). The DH function is defined as
DH(G,G^x,Y)=Y^x.
Clearly, solving CDH solves 2-CDH. Showing the other direction (to prove
equivalence with CDH) would be very surprising. Has this assumption been
used/analyzed earlier?