/* 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