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
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
|
/* 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:
let pk = 'g'^~sk
in
[ Fr(~sk) ]
--[ UserSecretKey($U, ~sk) ]->
[ !ConfiguredUser($U, pk), !UserSecret($U, ~sk), Out(pk), ValidPK(pk) ]
/* User with an identity element as a certificate. Will render the
* authentication meaningless as the shared secrets will also be identities.
* It doesn't even matter what the user secret is.
*/
rule SetupBad:
[]
-->
[ !ConfiguredUser($U, DH_neutral) ]
/* 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.
*
* - Public key was valid, in particular, it wasn't the identity element.
*/
rule ServerAuthFinish:
let challenge = 'g'^ck
response = h(<pk^ck, challenge, pk, username>)
in
[ In(response)
, ServerPending(username, ck)
, !ConfiguredUser(username, pk)
, ValidPK(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
|
