Initialize

1 files changed, 107 insertions, 0 deletions

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.