GaloisInc/cryptol
1
1
Fork 0
mirror of https://github.com/GaloisInc/cryptol.git synced 2024-11-30 23:45:23 +03:00
Code Issues Projects Releases Wiki Activity

Note: NIST 180-4 has an inconsistency in section 4.1.1 - the prose

Browse Source 
says 0<=t<=80, but the formula says 0<=t<=79. Later, they refer to
80 elements, so we're going with the formula's specification
This commit is contained in:
Dylan McNamee 2014-04-21 13:50:00 -07:00
parent 744808f67f
commit a04a2444a5
1 changed files with 2 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
examples/SHA1.cry
View File

@ -3,7 +3,7 @@
* Distributed under the terms of the BSD3 license (see LICENSE file)
*/
// Description of SHA1 at http://www.itl.nist.gov/fipspubs/fip180-1.htm
// Description of SHA1 at http://www.itl.nist.gov/fipspubs/fip180-4.htm
sha1 msg = sha1' pmsg
where
@ -42,7 +42,7 @@ f (t, x, y, z) =
if (0 <= t) && (t <= 19) then (x && y) ^ (~x && z)
| (20 <= t) && (t <= 39) then x ^ y ^ z
| (40 <= t) && (t <= 59) then (x && y) ^ (x && z) ^ (y && z)
| (60 <= t) && (t <= 80) then x ^ y ^ z
| (60 <= t) && (t <= 79) then x ^ y ^ z
else error "f: t out of range"
Ks : [80][32]