upstream: https://github.com/mirage/mirage-crypto
ocaml-crypto: enable MDX on lib/crypto.mli, fix broken doc examples
Run mdx on lib/crypto.mli so the {[ ... ]} odoc blocks now type-check.
Three blocks under abstract module types CBC and CTR were algebraic
identities written in pseudo-OCaml (|| for concatenation, == for
semantic equivalence). Rewrote each as a self-contained example
instantiated against Crypto.AES.CBC / AES.CTR with concrete keys, IVs,
and counters, and added an assert (chained = single) check so the
identity is documented and verifiable rather than asserted in prose.
+43
-12
+39
-12
lib/crypto.mli
+39
-12
lib/crypto.mli
···
386
386
the next message.
387
387
388
388
It is either [iv], when [String.length ciphertext - off = 0], or the
389
-
last block of [ciphertext]. Note that
389
+
last block of [ciphertext]. For example, with AES the following holds:
390
390
391
391
{[
392
-
encrypt ~iv msg1
393
-
|| encrypt ~iv:(next_iv ~iv (encrypt ~iv msg1)) msg2
394
-
== encrypt ~iv (msg1 || msg2)
392
+
let chain_cbc () =
393
+
let module M = Crypto.AES.CBC in
394
+
let key = M.of_secret (String.make 16 '\x00') in
395
+
let iv = String.make 16 '\x00' in
396
+
let msg1 = String.make 16 'a' in
397
+
let msg2 = String.make 16 'b' in
398
+
let chained =
399
+
let c1 = M.encrypt ~key ~iv msg1 in
400
+
c1 ^ M.encrypt ~key ~iv:(M.next_iv ~iv c1) msg2
401
+
in
402
+
let single = M.encrypt ~key ~iv (msg1 ^ msg2) in
403
+
assert (chained = single)
395
404
]}
396
405
397
406
@raise Invalid_argument if the length of [iv] is not [block_size].
···
516
525
For protocols which perform inter-message chaining, this is the counter
517
526
for the next message.
518
527
519
-
It is computed as [C.add ctr (ceil (len msg / block_size))]. Note that
520
-
if [len msg1 = k * block_size],
528
+
It is computed as [C.add ctr (ceil (len msg / block_size))]. For
529
+
example, with AES and [msg1] aligned on a block boundary:
521
530
522
531
{[
523
-
encrypt ~ctr msg1
524
-
|| encrypt ~ctr:(next_ctr ~ctr msg1) msg2 == encrypt ~ctr (msg1 || msg2)
532
+
let chain_ctr () =
533
+
let module M = Crypto.AES.CTR in
534
+
let key = M.of_secret (String.make 16 '\x00') in
535
+
let ctr = (0L, 0L) in
536
+
let msg1 = String.make 16 'a' in
537
+
let msg2 = String.make 16 'b' in
538
+
let chained =
539
+
M.encrypt ~key ~ctr msg1
540
+
^ M.encrypt ~key ~ctr:(M.next_ctr ~ctr msg1) msg2
541
+
in
542
+
let single = M.encrypt ~key ~ctr (msg1 ^ msg2) in
543
+
assert (chained = single)
525
544
]} *)
526
545
527
546
val ctr_of_octets : string -> ctr
···
535
554
is the first [n] bytes of
536
555
[E(ctr) || E(add ctr 1) || E(add ctr 2) || ...].
537
556
538
-
Note that
557
+
For example, restarting an AES keystream at a block boundary:
539
558
540
559
{[
541
-
stream ~key ~ctr (k * block_size)
542
-
|| stream ~key ~ctr:(add ctr k) x
543
-
== stream ~key ~ctr ((k * block_size) + x)
560
+
let restart_stream () =
561
+
let module M = Crypto.AES.CTR in
562
+
let key = M.of_secret (String.make 16 '\x00') in
563
+
let ctr = (0L, 0L) in
564
+
let k = 2 and x = 5 in
565
+
let restarted =
566
+
M.stream ~key ~ctr (k * M.block_size)
567
+
^ M.stream ~key ~ctr:(M.add_ctr ctr (Int64.of_int k)) x
568
+
in
569
+
let single = M.stream ~key ~ctr ((k * M.block_size) + x) in
570
+
assert (restarted = single)
544
571
]}
545
572
546
573
In other words, it is possible to restart a keystream at [block_size]