Add MKRAND RBG

[mknight-tag]

No description provided.

[kiniry]

Reflections @TomMD ?

[TomMD]

It's great to see a RBG being contributed but I'm curious about the motivation behind this generator, the intended use cases, and how we expect other Cryptol users to benefit. These questions concern me largely because 1) the text would greatly mislead the uninitiated and 2) this isn't a secure RBG.

I'm sure you know this isn't a secure generator, but for posterity sake I'll elaborate. Ideally there would be a proof of reduction to a hard problem, or it would be based on a public standard or cited publication. Lots of published papers exist detailing DRBGs with many trade-offs so it isn't an unexplored space that warrants arbitrary implementations.

This is actually a really fun and cool example for showing how Cryptol can aid analysis of the security of an algorithm. In this case we run the generator for a little and feed the output into a SAT solver to extract the "secret" seed. That is, given just the output random bytes from a generator we can discover the seed and thus know any prior or future random data:

> :set prover=boolector
> :sat (\seed -> take (randBytes seed) == 
                                                        [108, 78, 89, 137, 178, 143
                                                        , 203, 235, 160, 49, 161, 115
                                                        , 120, 96, 17, 54, 82, 242, 0
                                                        , 156, 205, 68, 55, 60, 156
                                                        , 116, 131, 121, 69, 8, 66, 19])
(\seed -> take (randBytes seed) == [108, 78, 89, 137, 178, 143
                                                        , 203, 235, 160, 49, 161, 115
                                                        , 120, 96, 17, 54, 82, 242, 0
                                                        , 156, 205, 68, 55, 60, 156
                                                        , 116, 131, 121, 69, 8, 66, 19])               
           0x00000000000000010000000000000000 = True
     // Notice the result 0x00...010..00 is the `seedUnit` variable
    // which I used to generated the array of random numbers.

For example, this could be used to take one cryptographic key generated via this generator and discover any prior or later generated key.

The misleading part of the text all are due to the security implications. For examples it A) mentions cryptographic uses B) calls out time as an entropy source C) claims the generator can provide an infinite stream of bits even though all DRBGs have a useful limit.

[acfoltzer]

@TomMD, your comments make me feel that this could be merged, but only after some substantial editing to the documentation. @mknight-tag, would you be up for doing this, or would you prefer we handle the changes?

[acfoltzer]

Bumped this to the next milestone as we are hitting our feature freeze for 2.1

[TomMD]

I see the code has been updated since our earlier comments. I no longer have an objection to the text but am left with the broader question of what constitutes something that belongs in the Cryptol repository? Anything written in Cryptol (hello bloat!)? Need it be cryptographic (good bye n-queens!)? Need it be educational (good bye AES, maybe)?

[acfoltzer]

@TomMD, for the moment we are happily accepting examples, both cryptographic and not, in the /examples/contrib subtree. At some point it might be worth splitting that out into a separate repository, and having a smaller core here, but for now I don't see any problems.