[CFRG] Re: DHKEM binding properties

[Cas Cremers <[e-mail]>]

Hi Peter,

while you directed the email to Deirdre, we think it may be a good point to
chime in here as the original authors of https://eprint.iacr.org/2023/1933:

TL;DR: Yes, DH-KEM is probably not MAL secure. This is not because of an
API mismatch but because it does not explicitly check for well-formed key
material. Our API models real-world KEM usage. The ‘trivial attacks’ we
‘block’ in our paper are degenerate cases in our properties, we will update
the wording.

Let us first address some points, before going to the API.
1. Deirdre's Slides: Checking Deirdre's backup slides, there seem to be
some relics from earlier talks. We no longer conjecture MAL properties but
provide a proof for LEAK in the ROM (for DH-KEM and other KEMs).
2. Previous Paper Versions: We've checked, and the previous versions of the
paper are available to us on IACR as expected:
https://eprint.iacr.org/archive/versions/2023/1933

MAL-Binding and API Choices
We agree that MAL claims need careful interpretation. As mentioned, we no
longer conjecture these properties for any KEM implementation. This change
is not due to our API choice differing from the real-world API, but because
these properties can only be achieved if the KEM implementation verifies
the well-formedness of the supplied key material. For example, a KEM
implementation might check whether the hash of the public key stored inside
the secret key is correct. Without these checks, a MAL adversary could
alter the stored hash to break binding. More details can be found in
Section 3 of [this paper](https://eprint.iacr.org/2024/523.pdf).

Next, we will elaborate on our API choices, why they differ from the
real-world API, and why we believe this is necessary.

Let’s recall the intuition behind our binding properties:
Given a shared secret, a public key, or a ciphertext, two KEM operations
which use (or result in) this value, should with overwhelming probability
also produce equal values for one (or more) of the other parameters. Note,
that we did not include the private key here, as during a KEM exchange,
only one of the parties knows the private key.
As an example, given a shared secret, any two KEM operations that result in
this shared secret must also agree on the used public key. In our paper,
this property is called X-K-PK, where X can be different threat models.

If we now want to formally write down such a property, we have to refer to
the public key of a KEM. However, the previous KEM.Decaps API does not
allow us to do this because the public key does not appear in it – even
though KEM.Decaps uses the public key internally. This is only possible
because in the real-world the public key (or a hash of it) is usually
stored inside of the secret key.
To allow us to formally state properties which include the public key over
KEM.Decaps, we thus added the public key to the KEM.Decaps API. We want to
stress that this is only a syntactic change which we believe to be
necessary to state our properties.

First, we acknowledge that 'trivial attacks' was a poor word choice
(originating in crypto literature tradition). The ‘trivial attacks’ we
‘block’ are not actual attacks, but ‘degenerate’ cases in our property
definition that would lead to a property which is not achievable for any
KEM. Any changes we made to the real-world API, and assumptions we placed
on it were only made to formally write down our properties. We believe our
API models real-world KEM usage and we will update the eprint with better
wording.
Additionally, our API changes alone do not 'block' any behavior. The
behavior is 'blocked' by our assumption that the KEM.Decaps algorithm uses
the explicitly supplied public key instead of extracting it from the secret
key. This assumption is necessary; without it, our binding properties
depend on a parameter that might never be used, resulting in a useless,
unachievable property for any KEM.

Dismissing X-BIND-PK, CT-K
You correctly note that our dismissal X-BIND-PK, CT-K is not justified for
implicitly rejecting KEMs in the context of MAL. This is an artifact of an
earlier version, as pointed out to us previously by Dennis Jackson. Our
next eprint update will fix this.

Of course, ideally, our binding properties would be independent of the API
choice. If we were to redesign the KEM API from scratch, we would probably
neither use the academic definitions nor the current real-world APIs, all
of which have their drawbacks. Also, if we were to redesign KEMs with what
we know now, we would probably only recommend explicitly rejecting KEMs.

Best regards,

Niklas, Alex, and Cas


On Mon, Jul 29, 2024 at 3:51 PM Peter C <Peter.C=
[e-mail]> wrote:

> Deirdre,
>
>
>
> > > DHKEM is MAL-BIND-K-CT and MAL-BIND-K-PK secure as analyzed
>
> > > in the symbolic model” and cite Cremers et al (https://ia.cr/2023/1933
> ).
>
>
>
> > This was an error from previous slide decks, those properties are
> modelled
>
> > in Tamarin and tested with several protocols to see if attacks showed up
>
> > when the KEMs used in protocols such as Kyber-AKE have varying binding
>
> > properties. The eprint version seems to be weird (all the previous
> versions
>
> > are 404'ing?) so I've attached the version I have in my archive as it
> has lots
>
> > more material, case studies, and short proofs for different KEMs about
> their
>
> > binding properties (as written, vs as in practice, but still)
>
>
>
> Thanks for the clarification and a copy of the earlier version.
>
>
>
> > > As specified in RFC 9180, DHKEM is not MAL-BIND-K-PK secure because
>
> > > DHKEM.Decaps recomputes the public key from the private key.  To
> achieve
>
> > > MAL-BIND-K-PK, I think the public key needs to be provided as input to
>
> > > DHKEM.Decaps and used in the KDF instead of the recomputed
>
>
>
> > Fair enough. Either way, we get much stronger BIND properties from the
>
> > default HPKE construction DH-KEM than swapping DH-KEM out for say
>
> > Classic McEliece, which is IND-CCA secure but gets us zero binding to the
>
> > PK, not even HON, and which earlier drafts of HPKE would have protected
>
> > against, but no longer does.
>
>
>
> Classic McEliece is not HON-BIND-CT-K or HON-BIND-CT-PK since it is
>
> implicitly rejecting.  It is not HON -BIND-K-PK or HON -BIND-K, CT-PK by
>
> Grubbs et al (https://ia.cr/2021/708)  For one of the parameter sets, it
> is
>
> not even HON-BIND-K-CT or HON-BIND-K, PK-CT if the implementation
>
> does not check the ciphertext padding bits (see “IND-CCA2 for encodings”
> in https://classic.mceliece.org/mceliece-rationale-20221023.pdf)
>
>
>
> > Relatedly, depending on how thing like Kyber/ML-KEM are implemented and
>
> > used in practice, we may rarely get MAL-BIND security in practice if the
> encaps
>
> > keys are only partially used in the interior KDF, or other shenanigans
> (see the
>
> > 'Kemmy Schmidt' note for more fun: https://eprint.iacr.org/2024/523.pdf)
> We
> > may cover ourselves by including everything in the higher protocol key
> schedule
> > anyway (like TLS 1.3) but in HPKE we don't do that. LEAK-BIND may be
> sufficient
> > and achievable in practice for general KEM usages but since HPKE is
> supposed
> > to be a pretty bulletproof building block (and basically is for DH-KEM)
> it would be
>
> > even nicer to change HPKE to be as bulletproof for other KEM cipher
> suites, or
>
> > whatever action actually results in users getting security in
> deployments without
> > having to do this bespoke analyst themselves every time.
>
>
>
> Again, I think any MAL-BIND-P-Q claims need to be interpreted very
> carefully as
>
> they can work in a very different way to their HON- or LEAK-
> counterparts.  For
>
> example, Cremers et al dismiss X-BIND-PK, CT-K on the basis that “if
> Decaps is
>
> deterministic, this is trivally true”, but that only holds for HON- and
> LEAK-.  An
>
> implicitly rejecting KEM will not be MAL-BIND-PK, CT-K if malformed public
> keys
>
> can be used to cause decapsulation failures.
>
>
>
> Peter
>
>
>
>
>
> _______________________________________________
> CFRG mailing list -- [e-mail]
> To unsubscribe send an email to [e-mail]
>