diff options
| -rw-r--r-- | LICENSES/MIT.txt | 20 | ||||
| -rw-r--r-- | README.md | 107 | ||||
| -rw-r--r-- | sof-dhcr.spthy | 119 |
3 files changed, 246 insertions, 0 deletions
diff --git a/LICENSES/MIT.txt b/LICENSES/MIT.txt new file mode 100644 index 0000000..fe74569 --- /dev/null +++ b/LICENSES/MIT.txt @@ -0,0 +1,20 @@ +Copyright (c) <year> <copyright holders> + +Permission is hereby granted, free of charge, to any person obtaining a +copy of this software and associated documentation files (the +"Software"), to deal in the Software without restriction, including +without limitation the rights to use, copy, modify, merge, publish, +distribute, sublicense, and/or sell copies of the Software, and to +permit persons to whom the Software is furnished to do so, subject to +the following conditions: + +The above copyright notice and this permission notice shall be included +in all copies or substantial portions of the Software. + +THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS +OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF +MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. +IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY +CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, +TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE +SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. diff --git a/README.md b/README.md new file mode 100644 index 0000000..5dd3644 --- /dev/null +++ b/README.md @@ -0,0 +1,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. diff --git a/sof-dhcr.spthy b/sof-dhcr.spthy new file mode 100644 index 0000000..8d4d141 --- /dev/null +++ b/sof-dhcr.spthy @@ -0,0 +1,119 @@ +/* Copyright 2026 Osmium Sorcerer + * SPDX-License-Identifier: MIT + */ + +theory DHCR +begin + +builtins: hashing, diffie-hellman + +/* Configuration of a username-certificate pair on the server. This sets up + * the identity of a user prior to authentication. Client knows the secret key + * for its username, and the server uses the corresponding certificate (public + * key) to authenticate the client. + * + * ~sk is a randomly generated secret key bound to the username. + * 'g'^~sk is the public key derived from the secret key ~sk. + * + * The public key is deliberately exposed at this step, as the security model + * assumes both usernames and public keys to be nonsecret. + */ +rule Setup: + [ Fr(~sk) ] +--[ UserSecretKey($U, ~sk) ]-> + [ !ConfiguredUser($U, 'g'^~sk), !UserSecret($U, ~sk), Out('g'^~sk) ] + +/* Client begins the authentication flow by sending the username. + * Honest participants know the secret key they must use for this. + */ +rule ClientAuthStart: + [ !UserSecret($U, sk) ] +--> + [ Out($U), ClientPending($U, sk) ] + +/* Server generates a fresh ephemeral secret key ~ck, computes the public key + * 'g'^~ck (challenge), and sends it to the client. + * + * Unlike the client's preconfigured, long-term identity key pair, server's + * key is freshly randomly generated for every new authentication attempt and is + * never reused. + */ +rule ServerChallenge: + [ In(U), Fr(~ck) ] +--> + [ Out('g'^~ck), ServerPending(U, ~ck) ] + +/* Client mixes his secret key into the challenge to derive the shared secret. + * To construct a response, it hashes it together with the entire transcript: + * challenge (ensuring freshness and binding to this session), public key and + * username (binding to the identity). + */ +rule ClientResponse: + let response = h(<challenge^sk, challenge, 'g'^sk, username>) + in + [ In(challenge), ClientPending(username, sk) ] +--[ Responded(username, 'g'^sk, challenge) ]-> + [ Out(response) ] + +/* Server accepts the response if: + * + * - The username and public key are configured on the server. + * + * - Server ends up deriving the same shared secret as the client, namely + * pk^ck = challenge^sk. This holds if the client possesses the secret key + * sk corresponding to its public key pk. + * + * - Client and server agree on the rest of the parameters: challenge, pk, + * username, exactly as they've been transmitted and seen. + */ +rule ServerAuthFinish: + let challenge = 'g'^ck + response = h(<pk^ck, challenge, pk, username>) + in + [ In(response), ServerPending(username, ck), !ConfiguredUser(username, pk) ] +--[ Accepted(username, pk, challenge) ]-> + [] + +/* The event of a key compromise. The environment may leak a key at any time + * (stolen or mismanaged), which is outside of the protocol's control, and the + * proofs must be aware of this. + */ +rule LeakUserKey: + [ !UserSecret(u, sk) ] +--[ Leaked(u) ]-> + [ Out(sk) ] + +/* Properties */ + +/* The user's secret key is never revealed in honest protocol runs. */ +lemma KeySecrecy: + "All u sk #i. UserSecretKey(u, sk) @ i & not (Ex #j. Leaked(u) @ j) + ==> not (Ex #k. K(sk) @ k)" + +/* Correct authentication is possible: client's response precedes successful + * authenticaton with the same parameters, and the key doesn't get leaked. + */ +lemma HonestSessionExists: + exists-trace "Ex u pk ch #i #j. Accepted(u, pk, ch) @ i + & Responded(u, pk, ch) @ j + & #j < #i + & not (Ex #r. Leaked(u) @ r)" + +/* Main lemma of the protocol. + * + * Server authenticates the user's identity with configured username u and + * public key pk, with challenge ch. The user hasn't been compromised. + * + * Then, the client ran the protocol with the same parameters and previously + * produced the matching response. + * + * "Injective" here means that each authentication session is unique. The server + * won't accept multiple sessions using the same challenge. + */ +lemma InjectiveAgreement: + "All u pk ch #i. Accepted(u, pk, ch) @ i & not (Ex #r. Leaked(u) @ r) + ==> + (Ex #j. Responded(u, pk, ch) @ j & #j < #i) + & not (Ex u2 pk2 #i2. Accepted(u2, pk2, ch) @ i2 & not (#i = #i2))" + +end |