enacl_eqc.erl 20.5 KB
Newer Older
Jesper Louis Andersen's avatar
Jesper Louis Andersen committed
1
2
3
4
-module(enacl_eqc).
-include_lib("eqc/include/eqc.hrl").
-compile(export_all).

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
non_byte_int() ->
    oneof([
        ?LET(N, nat(), -(N+1)),
        ?LET(N, nat(), N+256)
    ]).

g_iolist() ->
    ?SIZED(Sz, g_iolist(Sz)).
    
g_iolist(0) ->
    fault(
        oneof([
          elements([a,b,c]),
          real(),
          non_byte_int()
        ]),
        return([]));
g_iolist(N) ->
    fault(
        oneof([
          elements([a,b,c]),
          real(),
          non_byte_int()
        ]),
        frequency([
            {1, g_iolist(0)},
            {N, ?LAZY(list(oneof([char(), binary(), g_iolist(N div 4)])))}
        ])).
                    
g_iodata() ->
    fault(
      oneof([elements([a,b,c]), real()]),
      oneof([binary(), g_iolist()])).

v_iolist([]) -> true;
v_iolist([B|Xs]) when is_binary(B) -> v_iolist(Xs);
v_iolist([C|Xs]) when is_integer(C), C >= 0, C < 256 -> v_iolist(Xs);
v_iolist([L|Xs]) when is_list(L) ->
    v_iolist(L) andalso v_iolist(Xs);
v_iolist(_) -> false.

v_iodata(B) when is_binary(B) -> true;
v_iodata(Structure) -> v_iolist(Structure).

Jesper Louis Andersen's avatar
Jesper Louis Andersen committed
49
50
51
%% Generator for binaries of a given size with different properties and fault injection:
g_binary(Sz) ->
    fault(g_binary_bad(Sz), g_binary_good(Sz)).
Jesper Louis Andersen's avatar
Jesper Louis Andersen committed
52

Jesper Louis Andersen's avatar
Jesper Louis Andersen committed
53
54
g_binary_good(Sz) when Sz =< 32 -> binary(Sz);
g_binary_good(Sz) -> eqc_gen:largebinary(Sz).
55

Jesper Louis Andersen's avatar
Jesper Louis Andersen committed
56
57
58
59
g_binary_bad(Sz) ->
    frequency([
        {5, ?SUCHTHAT(B, binary(), byte_size(B) /= Sz)},
        {1, elements([a, b])},
60
61
        {1, int()},
        {1, g_iodata()}
Jesper Louis Andersen's avatar
Jesper Louis Andersen committed
62
63
64
    ]).
    
v_binary(Sz, N) when is_binary(N) ->
65
    byte_size(N) == Sz;
Jesper Louis Andersen's avatar
Jesper Louis Andersen committed
66
v_binary(_, _) -> false.
67

68
                  
69
%% Typical generators based on the binaries
Jesper Louis Andersen's avatar
Jesper Louis Andersen committed
70
71
nonce() -> g_binary(enacl:box_nonce_size()).
nonce_valid(N) -> v_binary(enacl:box_nonce_size(), N).
72

73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
%% Generator of natural numbers
g_nat() ->
    fault(g_nat_bad(), nat()).
    
g_nat_bad() ->
    oneof([
        elements([a,b,c]),
        real(),
        binary(),
        ?LET(X, nat(), -X)
    ]).

is_nat(N) when is_integer(N), N >= 0 -> true;
is_nat(_) -> false.

88
keypair_good() ->
89
    #{ public := PK, secret := SK} = enacl:box_keypair(),
90
91
92
93
94
    {PK, SK}.

keypair_bad() ->
    ?LET(X, elements([pk, sk]),
      begin
95
        #{ public := PK, secret := SK} = enacl:box_keypair(),
96
97
98
99
100
101
102
103
104
105
106
107
        case X of
            pk ->
              PKBytes = enacl:box_public_key_bytes(),
              {oneof([return(a), nat(), ?SUCHTHAT(B, binary(), byte_size(B) /= PKBytes)]), SK};
            sk ->
              SKBytes = enacl:box_secret_key_bytes(),
              {PK, oneof([return(a), nat(), ?SUCHTHAT(B, binary(), byte_size(B) /= SKBytes)])}
        end
      end).

keypair() ->
    fault(keypair_bad(), keypair_good()).
108

109
110
111
%% CRYPTO BOX
%% ---------------------------

112
113
114
115
116
117
keypair_valid(PK, SK) when is_binary(PK), is_binary(SK) ->
    PKBytes = enacl:box_public_key_bytes(),
    SKBytes = enacl:box_secret_key_bytes(),
    byte_size(PK) == PKBytes andalso byte_size(SK) == SKBytes;
keypair_valid(_PK, _SK) -> false.

Jesper Louis Andersen's avatar
Jesper Louis Andersen committed
118
119
prop_box_keypair() ->
    ?FORALL(_X, return(dummy),
120
        ok_box_keypair(enacl:box_keypair())).
Jesper Louis Andersen's avatar
Jesper Louis Andersen committed
121

122
ok_box_keypair(#{ public := _, secret := _}) -> true;
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
ok_box_keypair(_) -> false.

box(Msg, Nonce , PK, SK) ->
    try
        enacl:box(Msg, Nonce, PK, SK)
    catch
        error:badarg -> badarg
    end.

box_open(CphText, Nonce, PK, SK) ->
    try
        enacl:box_open(CphText, Nonce, PK, SK)
    catch
         error:badarg -> badarg
    end.

failure(badarg) -> true;
failure(_) -> false.
Jesper Louis Andersen's avatar
Jesper Louis Andersen committed
141

142
prop_box_correct() ->
143
    ?FORALL({Msg, Nonce, {PK1, SK1}, {PK2, SK2}},
144
            {fault_rate(1, 40, g_iodata()),
145
146
147
             fault_rate(1, 40, nonce()),
             fault_rate(1, 40, keypair()),
             fault_rate(1, 40, keypair())},
148
        begin
149
            case v_iodata(Msg) andalso nonce_valid(Nonce) andalso keypair_valid(PK1, SK1) andalso keypair_valid(PK2, SK2) of
150
                true ->
151
152
                    Key = enacl:box_beforenm(PK2, SK1),
                    Key = enacl:box_beforenm(PK1, SK2),
153
                    CipherText = enacl:box(Msg, Nonce, PK2, SK1),
154
                    CipherText = enacl:box_afternm(Msg, Nonce, Key),
155
                    {ok, DecodedMsg} = enacl:box_open(CipherText, Nonce, PK1, SK2),
156
                    {ok, DecodedMsg} = enacl:box_open_afternm(CipherText, Nonce, Key),
157
                    equals(iolist_to_binary(Msg), DecodedMsg);
158
159
160
161
162
163
                false ->
                    case box(Msg, Nonce, PK2, SK1) of
                        badarg -> true;
                        Res -> failure(box_open(Res, Nonce, PK1, SK2))
                    end
            end
164
165
166
        end).

prop_box_failure_integrity() ->
167
    ?FORALL({Msg, Nonce, {PK1, SK1}, {PK2, SK2}},
168
            {fault_rate(1, 40, g_iodata()),
169
170
171
             fault_rate(1, 40, nonce()),
             fault_rate(1, 40, keypair()),
             fault_rate(1, 40, keypair())},
172
        begin
173
174
            case v_iodata(Msg)
                 andalso nonce_valid(Nonce)
175
176
177
                 andalso keypair_valid(PK1, SK1)
                 andalso keypair_valid(PK2, SK2) of
                true ->
178
                    Key = enacl:box_beforenm(PK2, SK1),
179
180
                    CipherText = enacl:box(Msg, Nonce, PK2, SK1),
                    Err = enacl:box_open([<<"x">>, CipherText], Nonce, PK1, SK2),
181
                    Err = enacl:box_open_afternm([<<"x">>, CipherText], Nonce, Key),
182
183
                    equals(Err, {error, failed_verification});
                false ->
184
                    case box(Msg, Nonce, PK2, SK1) of
185
186
187
188
189
                      badarg -> true;
                      Res ->
                        failure(box_open(Res, Nonce, PK1, SK2))
                    end
            end
190
        end).
Jesper Louis Andersen's avatar
Jesper Louis Andersen committed
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
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
%% PRECOMPUTATIONS
beforenm_key() ->
    ?LET([{PK1, SK1}, {PK2, SK2}], [fault_rate(1, 40, keypair()), fault_rate(1, 40, keypair())],
        case keypair_valid(PK1, SK1) andalso keypair_valid(PK2, SK2) of
            true ->
                enacl:box_beforenm(PK1, SK2);
            false ->
                oneof([
                  elements([a,b,c]),
                  real(),
                  ?SUCHTHAT(X, binary(), byte_size(X) /= enacl:box_beforenm_bytes())
                  ])
        end).

v_key(K) when is_binary(K) -> byte_size(K) == enacl:box_beforenm_bytes();
v_key(_) -> false.

prop_beforenm_correct() ->
    ?FORALL([{PK1, SK1}, {PK2, SK2}], [fault_rate(1, 40, keypair()), fault_rate(1, 40, keypair())],
        case keypair_valid(PK1, SK1) andalso keypair_valid(PK2, SK2) of
            true ->
                equals(enacl:box_beforenm(PK1, SK2), enacl:box_beforenm(PK2, SK1));
            false ->
                badargs(fun() ->
                	K = enacl:box_beforenm(PK1, SK2),
                	K = enacl:box_beforenm(PK2, SK1)
                end)
        end).

prop_afternm_correct() ->
    ?FORALL([Msg, Nonce, Key],
        [fault_rate(1, 40, g_iodata()),
         fault_rate(1, 40, nonce()),
         fault_rate(1, 40, beforenm_key())],
      begin
          case v_iodata(Msg) andalso nonce_valid(Nonce) andalso v_key(Key) of
              true ->
                  CipherText = enacl:box_afternm(Msg, Nonce, Key),
                  equals({ok, iolist_to_binary(Msg)}, enacl:box_open_afternm(CipherText, Nonce, Key));
              false ->
                  try enacl:box_afternm(Msg, Nonce, Key) of
                      CipherText ->
                          try enacl:box_open_afternm(Msg, Nonce, Key) of
                              {ok, _M} -> false;
                              {error, failed_validation} -> false
                          catch
                              error:badarg -> true
                          end
                  catch
                      error:badarg -> true
                  end
          end
      end).
                  
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
%% SIGNATURES
%% ----------

prop_sign_keypair() ->
    ?FORALL(_D, return(dummy),
      begin
        #{ public := _, secret := _ } = enacl:sign_keypair(),
        true
      end).

sign_keypair_bad() ->
  ?LET(X, elements([pk, sk]),
    begin
      KP = enacl:sign_keypair(),
      case X of
        pk ->
          Sz = enacl:sign_keypair_public_size(),
          ?LET(Wrong, oneof([a, int(), ?SUCHTHAT(B, binary(), byte_size(B) /= Sz)]),
            KP#{ public := Wrong });
        sk ->
          Sz = enacl:sign_keypair_secret_size(),
          ?LET(Wrong, oneof([a, int(), ?SUCHTHAT(B, binary(), byte_size(B) /= Sz)]),
            KP#{ secret := Wrong })
      end
    end).

sign_keypair_good() ->
  return(enacl:sign_keypair()).

sign_keypair() ->
  fault(sign_keypair_bad(), sign_keypair_good()).

sign_keypair_public_valid(#{ public := Public })
  when is_binary(Public) ->
    byte_size(Public) == enacl:sign_keypair_public_size();
sign_keypair_public_valid(_) -> false.
    
sign_keypair_secret_valid(#{ secret := Secret })
  when is_binary(Secret) ->
    byte_size(Secret) == enacl:sign_keypair_secret_size();
sign_keypair_secret_valid(_) -> false.
    
sign_keypair_valid(KP) ->
  sign_keypair_public_valid(KP) andalso sign_keypair_secret_valid(KP).

prop_sign() ->
292
293
294
    ?FORALL({Msg, KeyPair},
          {fault_rate(1, 40, g_iodata()),
           fault_rate(1, 40, sign_keypair())},
295
      begin
296
        case v_iodata(Msg) andalso sign_keypair_secret_valid(KeyPair) of
297
298
299
300
301
302
303
304
305
306
          true ->
            #{ secret := Secret } = KeyPair,
            enacl:sign(Msg, Secret),
            true;
          false ->
            #{ secret := Secret } = KeyPair,
            badargs(fun() -> enacl:sign(Msg, Secret) end)
        end
      end).

307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
signed_message_good(M) ->
    #{ public := PK, secret := SK} = enacl:sign_keypair(),
    SM = enacl:sign(M, SK),
    frequency([
        {3, return({{valid, SM}, PK})},
        {1, ?LET(X, elements([sm, pk]),
               case X of
                 sm -> {{invalid, binary(byte_size(SM))}, PK};
                 pk -> {{invalid, SM}, binary(byte_size(PK))}
               end)}]).

signed_message_bad() ->
    Sz = enacl:sign_keypair_public_size(),
    {binary(), oneof([a, int(), ?SUCHTHAT(B, binary(Sz), byte_size(B) /= Sz)])}.

signed_message(M) ->
    fault(signed_message_bad(), signed_message_good(M)).

signed_message_valid({valid, _}, _) -> true;
signed_message_valid({invalid, _}, _) -> true;
signed_message_valid(_, _) -> false.

329
prop_sign_open() ->
330
    ?FORALL(Msg, g_iodata(),
331
      ?FORALL({SignMsg, PK}, signed_message(Msg),
332
          case v_iodata(Msg) andalso signed_message_valid(SignMsg, PK) of
333
334
335
              true ->
                  case SignMsg of
                    {valid, SM} ->
336
                        equals({ok, iolist_to_binary(Msg)}, enacl:sign_open(SM, PK));
337
338
339
340
341
342
343
                    {invalid, SM} ->
                        equals({error, failed_verification}, enacl:sign_open(SM, PK))
                  end;
              false ->
                  badargs(fun() -> enacl:sign_open(SignMsg, PK) end)
          end)).
     
344
345
346
%% CRYPTO SECRET BOX
%% -------------------------------

Jesper Louis Andersen's avatar
Jesper Louis Andersen committed
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
%% Note: key sizes are the same in a lot of situations, so we can use the same generator
%% for keys in many locations.

key_sz(Sz) ->
  equals(enacl:secretbox_key_size(), Sz).

prop_key_sizes() ->
    conjunction([{secret, key_sz(enacl:secretbox_key_size())},
                 {stream, key_sz(enacl:stream_key_size())},
                 {auth, key_sz(enacl:auth_key_size())},
                 {onetimeauth, key_sz(enacl:onetime_auth_key_size())}]).

nonce_sz(Sz) ->
  equals(enacl:secretbox_nonce_size(), Sz).

prop_nonce_sizes() ->
    conjunction([{secret, nonce_sz(enacl:secretbox_nonce_size())},
                 {stream, nonce_sz(enacl:stream_nonce_size())}]).

366
367
368
secret_key_good() ->
	Sz = enacl:secretbox_key_size(),
	binary(Sz).
Jesper Louis Andersen's avatar
Jesper Louis Andersen committed
369

370
371
372
373
secret_key_bad() ->
	oneof([return(a),
	       nat(),
	       ?SUCHTHAT(B, binary(), byte_size(B) /= enacl:secretbox_key_size())]).
Jesper Louis Andersen's avatar
Jesper Louis Andersen committed
374

375
secret_key() ->
376
377
378
379
380
381
382
383
384
385
386
387
388
	fault(secret_key_bad(), secret_key_good()).

secret_key_valid(SK) when is_binary(SK) ->
	Sz = enacl:secretbox_key_size(),
	byte_size(SK) == Sz;
secret_key_valid(_SK) -> false.

secretbox(Msg, Nonce, Key) ->
  try
    enacl:secretbox(Msg, Nonce, Key)
  catch
    error:badarg -> badarg
  end.
Jesper Louis Andersen's avatar
Jesper Louis Andersen committed
389

390
391
392
393
394
395
secretbox_open(Msg, Nonce, Key) ->
  try
    enacl:secretbox_open(Msg, Nonce, Key)
  catch
    error:badarg -> badarg
  end.
396
397

prop_secretbox_correct() ->
398
    ?FORALL({Msg, Nonce, Key},
399
            {fault_rate(1, 40, g_iodata()),
400
401
             fault_rate(1, 40, nonce()),
             fault_rate(1, 40, secret_key())},
402
      begin
403
        case v_iodata(Msg) andalso nonce_valid(Nonce) andalso secret_key_valid(Key) of
404
405
406
          true ->
             CipherText = enacl:secretbox(Msg, Nonce, Key),
             {ok, DecodedMsg} = enacl:secretbox_open(CipherText, Nonce, Key),
407
             equals(iolist_to_binary(Msg), DecodedMsg);
408
409
410
411
412
413
414
          false ->
             case secretbox(Msg, Nonce, Key) of
               badarg -> true;
               Res ->
                 failure(secretbox_open(Res, Nonce, Key))
             end
        end
415
      end).
Jesper Louis Andersen's avatar
Jesper Louis Andersen committed
416

417
prop_secretbox_failure_integrity() ->
418
    ?FORALL({Msg, Nonce, Key}, {g_iodata(), nonce(), secret_key()},
419
420
421
422
423
424
      begin
        CipherText = enacl:secretbox(Msg, Nonce, Key),
        Err = enacl:secretbox_open([<<"x">>, CipherText], Nonce, Key),
        equals(Err, {error, failed_verification})
      end).

Jesper Louis Andersen's avatar
Jesper Louis Andersen committed
425
%% CRYPTO STREAM
426
427
428
429
430
431
432
433
434
435
prop_stream_correct() ->
    ?FORALL({Len, Nonce, Key},
            {int(),
             fault_rate(1, 40, nonce()),
             fault_rate(1, 40, secret_key())},
        case Len >= 0 andalso nonce_valid(Nonce) andalso secret_key_valid(Key) of
          true ->
              CipherStream = enacl:stream(Len, Nonce, Key),
              equals(Len, byte_size(CipherStream));
          false ->
Jesper Louis Andersen's avatar
Jesper Louis Andersen committed
436
              badargs(fun() -> enacl:stream(Len, Nonce, Key) end)
437
438
        end).

439
440
441
442
xor_bytes(<<A, As/binary>>, <<B, Bs/binary>>) ->
    [A bxor B | xor_bytes(As, Bs)];
xor_bytes(<<>>, <<>>) -> [].

443
444
prop_stream_xor_correct() ->
    ?FORALL({Msg, Nonce, Key},
445
            {fault_rate(1, 40, g_iodata()),
446
447
             fault_rate(1, 40, nonce()),
             fault_rate(1, 40, secret_key())},
448
        case v_iodata(Msg) andalso nonce_valid(Nonce) andalso secret_key_valid(Key) of
449
            true ->
450
                Stream = enacl:stream(iolist_size(Msg), Nonce, Key),
451
                CipherText = enacl:stream_xor(Msg, Nonce, Key),
452
453
454
455
456
                StreamXor = enacl:stream_xor(CipherText, Nonce, Key),
                conjunction([
                    {'xor', equals(iolist_to_binary(Msg), StreamXor)},
                    {stream, equals(iolist_to_binary(xor_bytes(Stream, iolist_to_binary(Msg))), CipherText)}
                ]);
457
            false ->
Jesper Louis Andersen's avatar
Jesper Louis Andersen committed
458
                badargs(fun() -> enacl:stream_xor(Msg, Nonce, Key) end)
459
        end).
Jesper Louis Andersen's avatar
Jesper Louis Andersen committed
460
461
462
463

%% CRYPTO AUTH
prop_auth_correct() ->
    ?FORALL({Msg, Key},
464
            {fault_rate(1, 40, g_iodata()),
Jesper Louis Andersen's avatar
Jesper Louis Andersen committed
465
             fault_rate(1, 40, secret_key())},
466
       case v_iodata(Msg) andalso secret_key_valid(Key) of
Jesper Louis Andersen's avatar
Jesper Louis Andersen committed
467
468
469
470
471
472
473
         true ->
           Authenticator = enacl:auth(Msg, Key),
           equals(Authenticator, enacl:auth(Msg, Key));
         false ->
           badargs(fun() -> enacl:auth(Msg, Key) end)
       end).

474
475
476
477
478
authenticator_bad() ->
    oneof([a, int(), ?SUCHTHAT(X, binary(), byte_size(X) /= enacl:auth_size())]).

authenticator_good(Msg, Key) when is_binary(Key) ->
    Sz = enacl:secretbox_key_size(),
479
    case v_iodata(Msg) andalso byte_size(Key) == Sz of
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
      true ->
        frequency([{1, ?LAZY({invalid, binary(enacl:auth_size())})},
                   {3, return({valid, enacl:auth(Msg, Key)})}]);
      false ->
        binary(enacl:auth_size())
    end;
authenticator_good(_Msg, _Key) ->
    binary(enacl:auth_size()).

authenticator(Msg, Key) ->
  fault(authenticator_bad(), authenticator_good(Msg, Key)).

authenticator_valid({valid, _}) -> true;
authenticator_valid({invalid, _}) -> true;
authenticator_valid(_) -> false.

prop_auth_verify_correct() ->
    ?FORALL({Msg, Key},
498
            {fault_rate(1, 40, g_iodata()),
499
500
             fault_rate(1, 40, secret_key())},
      ?FORALL(Authenticator, authenticator(Msg, Key),
501
        case v_iodata(Msg) andalso secret_key_valid(Key) andalso authenticator_valid(Authenticator) of
502
503
504
505
506
507
508
509
510
511
512
          true ->
            case Authenticator of
              {valid, A} ->
                equals(true, enacl:auth_verify(A, Msg, Key));
              {invalid, A} ->
                equals(false, enacl:auth_verify(A, Msg, Key))
            end;
          false ->
            badargs(fun() -> enacl:auth_verify(Authenticator, Msg, Key) end)
        end)).

Jesper Louis Andersen's avatar
Jesper Louis Andersen committed
513
514
515
%% CRYPTO ONETIME AUTH
prop_onetimeauth_correct() ->
    ?FORALL({Msg, Key},
516
            {fault_rate(1, 40, g_iodata()),
Jesper Louis Andersen's avatar
Jesper Louis Andersen committed
517
             fault_rate(1, 40, secret_key())},
518
       case v_iodata(Msg) andalso secret_key_valid(Key) of
Jesper Louis Andersen's avatar
Jesper Louis Andersen committed
519
520
521
522
523
524
525
         true ->
           Authenticator = enacl:onetime_auth(Msg, Key),
           equals(Authenticator, enacl:onetime_auth(Msg, Key));
         false ->
           badargs(fun() -> enacl:onetime_auth(Msg, Key) end)
       end).

526
527
528
529
530
ot_authenticator_bad() ->
    oneof([a, int(), ?SUCHTHAT(X, binary(), byte_size(X) /= enacl:onetime_auth_size())]).

ot_authenticator_good(Msg, Key) when is_binary(Key) ->
    Sz = enacl:secretbox_key_size(),
531
    case v_iodata(Msg) andalso byte_size(Key) == Sz of
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
      true ->
        frequency([{1, ?LAZY({invalid, binary(enacl:onetime_auth_size())})},
                   {3, return({valid, enacl:onetime_auth(Msg, Key)})}]);
      false ->
        binary(enacl:onetime_auth_size())
    end;
ot_authenticator_good(_Msg, _Key) ->
    binary(enacl:auth_size()).

ot_authenticator(Msg, Key) ->
  fault(ot_authenticator_bad(), ot_authenticator_good(Msg, Key)).

ot_authenticator_valid({valid, _}) -> true;
ot_authenticator_valid({invalid, _}) -> true;
ot_authenticator_valid(_) -> false.

prop_onetime_auth_verify_correct() ->
    ?FORALL({Msg, Key},
550
            {fault_rate(1, 40, g_iodata()),
551
552
             fault_rate(1, 40, secret_key())},
      ?FORALL(Authenticator, ot_authenticator(Msg, Key),
553
        case v_iodata(Msg) andalso secret_key_valid(Key) andalso ot_authenticator_valid(Authenticator) of
554
555
556
557
558
559
560
561
562
563
564
          true ->
            case Authenticator of
              {valid, A} ->
                equals(true, enacl:onetime_auth_verify(A, Msg, Key));
              {invalid, A} ->
                equals(false, enacl:onetime_auth_verify(A, Msg, Key))
            end;
          false ->
            badargs(fun() -> enacl:onetime_auth_verify(Authenticator, Msg, Key) end)
        end)).

Jesper Louis Andersen's avatar
Jesper Louis Andersen committed
565
566
%% HASHING
%% ---------------------------
567
568
569
diff_pair() ->
    ?SUCHTHAT({X, Y}, {g_iodata(), g_iodata()},
        iolist_to_binary(X) /= iolist_to_binary(Y)).
Jesper Louis Andersen's avatar
Jesper Louis Andersen committed
570
571

prop_crypto_hash_eq() ->
572
573
    ?FORALL(X, g_iodata(),
        case v_iodata(X) of
574
575
576
577
578
579
580
581
582
          true -> equals(enacl:hash(X), enacl:hash(X));
          false ->
            try
              enacl:hash(X),
              false
            catch
              error:badarg -> true
            end
        end
583
    ).
Jesper Louis Andersen's avatar
Jesper Louis Andersen committed
584

Jesper Louis Andersen's avatar
Jesper Louis Andersen committed
585
prop_crypto_hash_neq() ->
586
    ?FORALL({X, Y}, diff_pair(),
Jesper Louis Andersen's avatar
Jesper Louis Andersen committed
587
        enacl:hash(X) /= enacl:hash(Y)
588
    ).
Jesper Louis Andersen's avatar
Jesper Louis Andersen committed
589

590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
%% STRING COMPARISON
%% -------------------------

verify_pair_bad(Sz) ->
  ?LET(X, elements([fst, snd]),
    case X of
      fst ->
        {?SUCHTHAT(B, binary(), byte_size(B) /= Sz), binary(Sz)};
      snd ->
        {binary(Sz), ?SUCHTHAT(B, binary(), byte_size(B) /= Sz)}
    end).

verify_pair_good(Sz) ->
  oneof([
    ?LET(Bin, binary(Sz), {Bin, Bin}),
    ?SUCHTHAT({X, Y}, {binary(Sz), binary(Sz)}, X /= Y)]).
Jesper Louis Andersen's avatar
Jesper Louis Andersen committed
606

607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
verify_pair(Sz) ->
  fault(verify_pair_bad(Sz), verify_pair_good(Sz)).

verify_pair_valid(Sz, X, Y) ->
    byte_size(X) == Sz andalso byte_size(Y) == Sz.

prop_verify_16() ->
    ?FORALL({X, Y}, verify_pair(16),
      case verify_pair_valid(16, X, Y) of
          true ->
              equals(X == Y, enacl:verify_16(X, Y));
          false ->
              try
                 enacl:verify_16(X, Y),
                 false
              catch
                  error:badarg -> true
              end
      end).
Jesper Louis Andersen's avatar
Jesper Louis Andersen committed
626

627
628
629
630
631
632
633
634
635
636
637
638
prop_verify_32() ->
    ?FORALL({X, Y}, verify_pair(32),
      case verify_pair_valid(32, X, Y) of
          true ->
              equals(X == Y, enacl:verify_32(X, Y));
          false ->
              try
                 enacl:verify_32(X, Y),
                 false
              catch
                  error:badarg -> true
              end
Jesper Louis Andersen's avatar
Jesper Louis Andersen committed
639
640
      end).

641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
%% RANDOMBYTES
prop_randombytes() ->
    ?FORALL(X, g_nat(),
        case is_nat(X) of
            true ->
                is_binary(enacl:randombytes(X));
            false ->
                try
                    enacl:randombytes(X),
                    false
                catch
                    error:badarg ->
                       true
                end
       end).

%% SCRAMBLING
prop_scramble_block() ->
    ?FORALL({Block, Key}, {binary(16), eqc_gen:largebinary(32)},
        is_binary(enacl_ext:scramble_block_16(Block, Key))).

Jesper Louis Andersen's avatar
Jesper Louis Andersen committed
662
663
664
665
666
667
668
669
%% HELPERS
badargs(Thunk) ->
  try
    Thunk(),
    false
  catch
    error:badarg -> true
  end.