1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
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
|
