-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathotrv4_nidake_deniable.pv
226 lines (183 loc) · 8.52 KB
/
otrv4_nidake_deniable.pv
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
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
(* Model of OTRv4
* Sebastian R. Verschoor
*
* Here we prove offline deniability for OTRv4 when running in non-interactive
* mode. That means that a communicating party is not able to provide
* convincing evidence that a conversation took part. Whatever
* transcript/evidence is given, the honest parties can always successful argue
* that the entire transcript was simulated by a third party (with access to
* only the public keys of the honest parties).
*
* In Proverif we model this by modelling the above simulator. We run the
* interactive handshake for the honest parties and for the simulator. If the
* adversary cannot distinguish between honest and simulated, then the protocol
* is offline deniable.
*
* # Inaccuracies of the model
*
* Proverif is based on the pi-calculus and can only do so much to accurately
* model the protocol and cryptographic primitives as specified (let alone
* implemented). In particular, Proverif assumes perfect cryptographic
* primitives and cannot handle associativity, but for a more complete
* discussion of the matter see the [Proverif manual][Proverif]. This is
* relevant for OTRv4 in at least the following ways:
* - Diffie-Hellman is only defined relative to the base element.
* - Hashes (also MAC and KDF) are essentialy random oracles.
*
* Besides the above unavoidable sources of incompleteness, there are also some
* diversions from the protocol as [currently specified][OTRv4]:
* - Each party is assumed to have just one signed prekey.
* - protocol negotiation/modes: it is assumed that Alice and Bob have agreed
* on this beforehand. Downgrade attacks, for example, are not covered.
* - nested KDF calls are avoided
* - I modelled [this proposal](https://github.com/otrv4/otrv4/issues/205)
* (since I have only modelled the handshake, that means that I simply did
* not include additional ephemeral keys)
* FIXME: this should be done differently
* - Fingerprint comparison must be modelled at a particular point in time,
* here done just after the regular protocol completes. In reality, it
* can be done at any time (preferably beforehand). The alternative (SMP) has
* not been modelled.
*
* Some things may look strange but they should not affect the results:
* - public data (Client-/Prekey-Profiles) are outputted only once
* - new values are generated as early as possible, this helps Proverif
* resolve the model quicker. In general the order of operations does not
* matter, only the order of sent/received messages.
* - prekey management is more complicated then is modelled here. However, from
* the protocol perspective all the server is doing is caching the messages.
* - signatures are implemented with message recovery directly from the signature.
* This should improve Proverif performance and does not affect the model since
* signatures are always computed over publicly known values.
* - SSID values can be compared, but this is not required to be confidential,
* this is modelled by simply outputting the value (but actual comparison is
* considered out of scope).
*
* # References
*
* [DAKES]: https://www.petsymposium.org/2018/files/papers/issue1/paper12-2018-1-source.pdf
* [Proverif]: http://prosecco.gforge.inria.fr/personal/bblanche/proverif/manual.pdf
* [OTRv4]: https://github.com/otrv4/otrv4/blob/master/otrv4.md
*)
(* The specification makes sure types cannot be mixed *)
set ignoreTypes = false.
(* Public communication channel *)
channel c.
(* ECDH: key exchange *)
type ec_point.
type ec_scalar.
const ec_base: ec_point [data].
fun ec_point_as_bits(ec_point): bitstring [data, typeConverter].
fun ec_mul(ec_scalar, ec_point): ec_point.
equation forall x: ec_scalar, y: ec_scalar;
ec_mul(x, ec_mul(y, ec_base)) = ec_mul(y, ec_mul(x, ec_base)).
(* EdDSA: digital signatures *)
type eddsa_private_key.
type eddsa_signature.
fun eddsa_scalar(eddsa_private_key): ec_scalar.
letfun eddsa_public_key(x: eddsa_private_key) = ec_mul(eddsa_scalar(x), ec_base).
fun eddsa_sign(eddsa_private_key, bitstring): eddsa_signature.
reduc forall k: eddsa_private_key, m: bitstring;
eddsa_get_msg(eddsa_sign(k, m)) = m.
reduc forall k: eddsa_private_key, m: bitstring;
eddsa_verify(eddsa_sign(k, m), ec_mul(eddsa_scalar(k), ec_base)) = m.
(* Elliptic curve ring signatures (three public keys) *)
type ring_signature.
type coins.
fun internal_ring_sign(ec_scalar, ec_point, ec_point, bitstring, coins): ring_signature.
letfun ring_sign(k: ec_scalar, a: ec_point, b: ec_point, m: bitstring) =
new r: coins; internal_ring_sign(k, a, b, m, r).
reduc forall k: ec_scalar, a: ec_point, b: ec_point, m: bitstring, r: coins;
ring_get_msg(internal_ring_sign(k, a, b, m, r)) = m.
reduc
forall k: ec_scalar, a: ec_point, b: ec_point, m: bitstring, r: coins;
ring_verify(internal_ring_sign(k, a, b, m, r), ec_mul(k, ec_base), a, b) = m;
forall k: ec_scalar, a: ec_point, b: ec_point, m: bitstring, r: coins;
ring_verify(internal_ring_sign(k, a, b, m, r), ec_mul(k, ec_base), b, a) = m;
forall k: ec_scalar, a: ec_point, b: ec_point, m: bitstring, r: coins;
ring_verify(internal_ring_sign(k, a, b, m, r), a, ec_mul(k, ec_base), b) = m;
forall k: ec_scalar, a: ec_point, b: ec_point, m: bitstring, r: coins;
ring_verify(internal_ring_sign(k, a, b, m, r), a, b, ec_mul(k, ec_base)) = m;
forall k: ec_scalar, a: ec_point, b: ec_point, m: bitstring, r: coins;
ring_verify(internal_ring_sign(k, a, b, m, r), b, ec_mul(k, ec_base), a) = m;
forall k: ec_scalar, a: ec_point, b: ec_point, m: bitstring, r: coins;
ring_verify(internal_ring_sign(k, a, b, m, r), b, a, ec_mul(k, ec_base)) = m.
(* KDF *)
type tag.
fun kdf(tag, bitstring): bitstring.
(* Domain seperating tags *)
(* usageID variables, superfluous ones are commented out *)
const usageFingerprint: tag [data].
const usageSharedSecret: tag [data].
const usageSSID: tag [data].
const usageTmpKey: tag [data].
const usageAuthMACKey: tag [data].
const usageAuthMAC: tag [data].
const usageMACKey: tag [data].
const usageAuthenticator: tag [data].
const usageSMPSecret: tag [data].
(* Other constants *)
const zero: tag [data].
const one: tag [data].
const fp_idake_alice: tag [data].
const fp_idake_bob: tag [data].
const fp_nidake_alice: tag [data].
const fp_nidake_bob: tag [data].
(* Identity of the honest parties (e.g. bare JID) *)
type identity.
free id1, id2: identity.
(* Fingerprint calculation *)
letfun fingerprint(client_profile: eddsa_signature) =
kdf(usageFingerprint, eddsa_get_msg(client_profile)).
(* The main process. The idea is that we run an interactive handshake
* between Alice and Bob, or a simulated conversation by a third party.
* If the adversary cannot distinguish between them, then the handshake
* is *offline deniable*.
*)
process
(* Generate the honest parties *)
new h1: eddsa_private_key;
new f1: ec_scalar;
let H1 = eddsa_public_key(h1) in
let F1 = ec_mul(f1, ec_base) in
let cp1 = eddsa_sign(h1, (H1, F1)) in
new h2: eddsa_private_key;
new f2: ec_scalar;
let H2 = eddsa_public_key(h2) in
let F2 = ec_mul(f2, ec_base) in
let cp2 = eddsa_sign(h2, (H2, F2)) in
(* Bob's prekey profile *)
new d: ec_scalar;
let D = ec_mul(d, ec_base) in
let pkp = eddsa_sign(h2, ec_point_as_bits(D)) in
out(c, (cp1, cp2, pkp));
(
(!(
(* Bob, prekey part, cached by the Prekey server *)
new y: ec_scalar;
let Y = ec_mul(y, ec_base) in
out(c, Y);
(* Alice *)
new x: ec_scalar;
let X = ec_mul(x, ec_base) in
let tmpk = kdf(usageTmpKey, (ec_mul(x, Y), ec_mul(x, D), ec_mul(x, H2))) in
let t = (cp2, cp1, Y, X, D, id2, id1) in
let k = kdf(usageSharedSecret, tmpk) in
let ssid = kdf(usageSSID, k) in out(c, ssid);
let priv = choice[eddsa_scalar(h1), y] in
let pub = choice[Y, H1] in
let sigma = ring_sign(priv, F2, pub, t) in
let xzdh_mac_key = kdf(usageAuthMACKey, tmpk) in
let xzdh_mac = kdf(usageAuthMAC, (xzdh_mac_key, t)) in
let msg_mac_key = kdf(usageMACKey, k) in
new z: ec_scalar;
let Z = ec_mul(z, ec_base) in
let Z_mac = kdf(usageAuthenticator, (msg_mac_key, ec_point_as_bits(Z))) in
out(c, (sigma, xzdh_mac, Z, Z_mac));
(* Bob (has no further output) *)
(* Reveal the session key *)
out(c, k)
)) |
(* Reveal all secret values *)
(phase 1; out(c, (h1, f1, h2, f2)))
)