Diffie-Hellman challenge-response authentication (symbolic model)

Symbolic model of an authentication protocol used at Serenade of Flames, formally proven using Tamarin prover.

Protocol description

An interactive identification protocol that authenticates a client to a server using a Diffie-Hellman challenge-response tied to the client's public key.

Let G be a cyclic group of prime order with generator g, where ^ denotes group exponentiation. h() denotes a cryptographic hash function. We write h(x1, ..., xN) as hashing an encoding of the tuple (x1, ..., xN).

Server sets up a (username, certificate) pair out of band in a trusted config. User has a secret key key corresponding to its public key certificate = g^key.

The flow:

1. Client sends username.
2. Server generates a random verification secret v, computes challenge = g^v, and sends challenge.
3. Client responds with h(challenge^key, challenge, certificate, username).
4. Server computes h(certificate^v, challenge, certificate, username). If it matches the client's response, the server accepts.

Properties

The following properties are proven in the Dolev-Yao model. In this model, the adversary controls the entire network and can arbitrarily delete, inject, modify and intercept messages exchanged between participants. Cryptographic operations constrain the attacker's capabilities.

1. Authentication with injective agreement. If the server accepts an authentication for the user, then the client must've previously produced the corresponding response with matching parameters (challenge, certificate, username). Furthermore, each acceptance corresponds to a distinct client authentication session.
2. User's secret key remains secret. Not even the server learns it.

As a sanity check, a lemma establishing that the protocol is executable is included. An honest client possessing the correct secret key can successfully authenticate to the server if the username and the corresponding certificate are configured. This whole design is pointless if this isn't the case.

Running the prover

tamarin-prover --prove sof-dhcr.spthy

Tested with version 1.10.0.

Note on symbolic model

Symbolic model is deeply magical. We assume all cryptography to be ideal, and formally conclude that the properties defined in the model hold. In practice, one must consider poor environments, such as low-quality random number generators or erroneous primitives. The protocol itself might be implemented poorly even if the individual primitives are correct. Security properties might also be underspecified.

The abstract primitives for hashing and Diffie-Hellman have to be concretely instantiated.

h must be a cryptographic hash function, domain-separated for this specific instance. Unambiguous encoding must be used to avoid canonicalization issues, for example, by prefixing lengths to each field. In SoF, BLAKE2b is used with a domain separation string and simple concatenation: BLAKE2b-256("Einsof-Auth-DHCR" || shared_secret || challenge || certificate || username). BLAKE2 is invulnerable to length extension attacks, and due to all but last fields being of fixed length, there's no encoding ambiguity.

For Diffie-Hellman operations, SoF uses X25519. The construction relies on a computational Diffie-Hellman problem in the underlying group. Interestingly, the construction resembles a Key Encapsulation Mechanism (KEM), similar to DHKEM. This suggests that the model could potentially be generalized to use any (IND-CCA secure?) KEM instead of Diffie-Hellman.

Authentication assumes username is strictly paired to a certificate for any protocol run. If an adversary sends a username which is not configured on the server, the protocol will immediately fail. In a symbolic model, it's exactly what we want: server accepts if everything's correct, and rejects otherwise. In practice, such direct behavior reveals which valid users exist on a server. To mitigate this, SoF uses randomly generated bogus public key to "verify" any nonexistent username, always resulting in a rejection indistinguishable from a failed login attempt with a valid username.

The protocol only authenticates the client to the server. Clients are assumed to know the server they're connected to. Server impersonation is thus theoretically possible, but the impact of it is unclear: a malicious server will either copy a valid config and let the victim authenticate without learning anything, or the authentication will automatically fail. This could further be formalized.

While the protocol itself is secure in a fully attacker-controlled network, it only authenticates the client but doesn't protect the channel afterward. After a successful authentication, an adversary could still inject and modify arbitrary messages in the session, including now privileged commands. Therefore, the protocol should be used within an established secure channel, such as TLS.