mirror of
https://github.com/GaloisInc/cryptol.git
synced 2024-11-29 10:13:29 +03:00
Add MKRAND RBG
This commit is contained in:
parent
bede37a436
commit
502816fbd3
121
examples/contrib/mkrand.cry
Normal file
121
examples/contrib/mkrand.cry
Normal file
@ -0,0 +1,121 @@
|
||||
/*
|
||||
|
||||
MKRAND - A non-deterministic Digital Random Bit Generator
|
||||
|
||||
The MIT License (MIT)
|
||||
|
||||
Copyright (c) 2014, TAG Universal Machine.
|
||||
|
||||
Permission is hereby granted, free of charge, to any person obtaining a copy
|
||||
of this software and associated documentation files (the "Software"), to deal
|
||||
in the Software without restriction, including without limitation the rights
|
||||
to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
|
||||
copies of the Software, and to permit persons to whom the Software is
|
||||
furnished to do so, subject to the following conditions:
|
||||
|
||||
The above copyright notice and this permission notice shall be included in
|
||||
all copies or substantial portions of the Software.
|
||||
|
||||
THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
|
||||
IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
|
||||
FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
|
||||
AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
|
||||
LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
|
||||
OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN
|
||||
THE SOFTWARE.
|
||||
|
||||
--
|
||||
|
||||
USAGE
|
||||
|
||||
The non-deterministic component of this process is the precise time of invocation.
|
||||
When implementing, since most system clocks provide less than 128 bits, apply
|
||||
the hash function to amplify the time-dependent bits:
|
||||
|
||||
seed = sha30 (<time_bits>)
|
||||
|
||||
Once the seed is created, you may use it to generate an infinite stream of bits:
|
||||
|
||||
take `{100} (randBytes seed)
|
||||
|
||||
The seed created from a hashed time-stamp is non-deterministic, since the precise
|
||||
time of invocation was chosen by the individual. Once the seed is created, all
|
||||
subsequently generated bits are deterministically random, as a function of that seed.
|
||||
The precise invocation time is the only secret, as far as the computation is concerned.
|
||||
|
||||
Depending on your application, this distinction is important, as when generating
|
||||
a block of keys, for example:
|
||||
|
||||
take `{3} (rands seed)
|
||||
|
||||
The three keys will be cryptographically unique with respect to each other,
|
||||
however they are all a function of the same seed and therefore can all be regenerated
|
||||
(or verified) knowing the seed.
|
||||
|
||||
Here we encode a string with seedUnit, using the deterministic random stream as a
|
||||
one-time pad against which to XOR the string:
|
||||
|
||||
Encode:
|
||||
randXOR seedUnit "Deus Ex Machina"
|
||||
[0x28, 0x2b, 0x2c, 0xfa, 0x92, 0xca, 0xb3, 0xcb, 0xed, 0x50, 0xc2,v0x1b, 0x11, 0x0e, 0x70]
|
||||
|
||||
Decode:
|
||||
:set ascii=on
|
||||
randXOR seedUnit [0x28, 0x2b, 0x2c, 0xfa, 0x92, 0xca, 0xb3, 0xcb, 0xed, 0x50, 0xc2,0x1b, 0x11, 0x0e, 0x70]
|
||||
"Deus Ex Machina"
|
||||
|
||||
Therefore, when non-determinism is desired, create the seed at the point of use,
|
||||
and discard after using it.
|
||||
|
||||
*/
|
||||
|
||||
module MKRAND where
|
||||
|
||||
type Seg = [0x80]
|
||||
type Field = [0x80]Seg
|
||||
|
||||
/* Canonical seed - a segment with a single True bit in the center */
|
||||
seedUnit:Seg
|
||||
seedUnit = (0 :[63]) # (1:[1]) # (0:[64])
|
||||
|
||||
|
||||
/*
|
||||
* Field - Unfold an application of Rule 30 to a seed
|
||||
*/
|
||||
field: Seg -> [inf]Seg
|
||||
field s = new
|
||||
where
|
||||
new = [s] # [ rule30 row | row <- new]
|
||||
rule30 r = [ a ^ (b || c) | a <- r >>> 1
|
||||
| b <- r
|
||||
| c <- r <<< 1
|
||||
]
|
||||
|
||||
|
||||
/* SHA30 - Use the input segment as the seed, generate two square fields,
|
||||
* keep the center column of the second.
|
||||
*/
|
||||
sha30: Seg -> Seg
|
||||
sha30 s = take`{0x80} (drop`{0x80} [ r @ ((((width r) / 2)-1):[8]) | r <- field s])
|
||||
|
||||
|
||||
/*
|
||||
* RAND - Seed XOR (SHA30 Seed)
|
||||
*/
|
||||
rands : Seg -> [inf]Seg
|
||||
rands s = rest
|
||||
where
|
||||
rand p = p ^ (sha30 p)
|
||||
rest = [rand s] # [rand x | x <- rest]
|
||||
|
||||
|
||||
/* Break segments into bytes */
|
||||
randBytes : Seg -> [inf][8]
|
||||
randBytes s = groupBy`{8} (join (rands s))
|
||||
|
||||
|
||||
/* XOR a byte string into a random byte string, using the given seed */
|
||||
randXOR : {n} Seg -> String n -> String n
|
||||
randXOR seed src = [s ^ r | s <- src
|
||||
| r <- randBytes seed
|
||||
]
|
Loading…
Reference in New Issue
Block a user