1 files changed, 119 insertions, 0 deletions
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