1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
|
<!--
Copyright 2026 Osmium Sorcerer
SPDX-License-Identifier: MIT
-->
# Diffie-Hellman challenge-response authentication (symbolic model)
Symbolic model of an authentication protocol used at Serenade of Flames,
formally proven using [Tamarin prover](https://tamarin-prover.com).
## 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](https://www.rfc-editor.org/rfc/rfc9180.html#name-dh-based-kem-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.
|
