Initialize

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