mirror of
https://github.com/GaloisInc/cryptol.git
synced 2024-09-19 01:49:11 +03:00
272 lines
8.6 KiB
Plaintext
272 lines
8.6 KiB
Plaintext
// Copyright (c) 2001, 2014 Galois, Inc.
|
|
// Distributed under the terms of the BSD3 license (see LICENSE file)
|
|
//
|
|
// MD5 digest algorithm from RFC 1321
|
|
// https://www.ietf.org/rfc/rfc1321.txt
|
|
//
|
|
// Based on a previous Cryptol 1.* implementation
|
|
|
|
// Swap byte order from network to host order (long word)
|
|
ntohl : [32] -> [32]
|
|
ntohl w = join (reverse (groupBy`{8} w))
|
|
|
|
// Swap byte order from host to network order (long word)
|
|
htonl : [32] -> [32]
|
|
htonl w = join (reverse (groupBy`{8} w))
|
|
|
|
// Swap byte order from host to network order (long long word)
|
|
htonll : [64] -> [64]
|
|
htonll w = join (reverse (groupBy`{8} w))
|
|
|
|
// apply a function to every element of a sequence
|
|
map : {n, a, b} (a -> b) -> [n]a -> [n]b
|
|
map f xs = [ f x | x <- xs ]
|
|
|
|
// fold with left associativity
|
|
foldl : {n, a, b} (fin n) => a -> (a -> b -> a) -> [n]b -> a
|
|
foldl seed f xs = res ! 0
|
|
where res = [seed] # [ f a x | a <- res
|
|
| x <- xs
|
|
]
|
|
|
|
// Test driver. Given a sequence of bytes, calculate the MD5 sum.
|
|
test s = md5 (join s)
|
|
|
|
// Reference implementation of MD5 on exactly 16 bytes.
|
|
|
|
md5_ref : [16][8] -> [16][8]
|
|
md5_ref msg = map reverse (groupBy`{8} (md5`{p=319} (join (map reverse msg))))
|
|
|
|
md5_ref' : [128] -> [128]
|
|
md5_ref' msg = join (md5_ref (groupBy`{8} msg))
|
|
|
|
|
|
|
|
// The state of the MD5 algorithm after each 512 bit block
|
|
// consists of 4 32-bit words.
|
|
type MD5State = ([32],[32],[32],[32])
|
|
|
|
// Main MD5 algorithm.
|
|
//
|
|
// First, pad the message to a multiple of 512 bits.
|
|
// Next, initilize the MD5 state using the fixed values from the RFC.
|
|
// Then, process each message block in turn by computing
|
|
// the MD5 rounds using the message block. Add the result
|
|
// of the final round to the current MD5 state.
|
|
// Finally, return the current MD5 state after all blocks are processed,
|
|
// interpreting the 4 32-bit words as a single 128-bit sequence.
|
|
|
|
md5 : {a, b, p} (fin p, 512 * b == 65 + (a + p), 64 >= width a, 511 >= p) =>
|
|
[a] -> [128]
|
|
md5 msg = md5output finalState
|
|
where
|
|
finalState : MD5State
|
|
finalState = foldl initialMD5State processBlock blocks
|
|
|
|
blocks : [b][512]
|
|
blocks = groupBy`{512} (pad `{a,p} msg)
|
|
|
|
add : MD5State -> MD5State -> MD5State
|
|
add (a, b, c, d) (e, f, g, h) = (a + e, b + f, c + g, d + h)
|
|
|
|
processBlock : MD5State -> [512] -> MD5State
|
|
processBlock st blk = add st (computeRounds (decodeBlock blk) st)
|
|
|
|
|
|
// Initial seed for the digest rounds
|
|
//
|
|
// See RFC 1321, section 3.3
|
|
|
|
initialMD5State : MD5State
|
|
initialMD5State = (A, B, C, D)
|
|
where
|
|
f x = ntohl (join x)
|
|
A = f [ 0x01, 0x23, 0x45, 0x67 ]
|
|
B = f [ 0x89, 0xAB, 0xCD, 0xEF ]
|
|
C = f [ 0xFE, 0xDC, 0xBA, 0x98 ]
|
|
D = f [ 0x76, 0x54, 0x32, 0x10 ]
|
|
|
|
|
|
// Each MD5 message block 512 bits long, interpreted as a sequence of 16 32-bit words
|
|
// Each word is given as a sequence of 4 bytes, with LEAST significant byte first
|
|
// Each byte is given as a sequence of 8 bits, with MOST significant bit first
|
|
//
|
|
// The output of the algorithm is a sequence of 4 words, interpreted as above
|
|
//
|
|
// See RFC 1321, section 2
|
|
|
|
decodeBlock : [512] -> [16][32]
|
|
decodeBlock s = map ntohl (groupBy`{32} s)
|
|
|
|
|
|
// Interpret 4 32-bit words as a single 128-bit sequence
|
|
//
|
|
// See RFC 1321 section 3.5
|
|
|
|
md5output : MD5State -> [128]
|
|
md5output (a,b,c,d) = htonl a # htonl b # htonl c # htonl d
|
|
|
|
|
|
|
|
// Given an arbitrary byte sequence whose length can be described
|
|
// by a 64-bit number, pad the message so it is exactly a multiple of 512.
|
|
//
|
|
// This is done by adding a single 1 bit to the end of the message, and
|
|
// then adding enough zero bits to make the whole message 64 bits shorter
|
|
// than a multiple of 512. The size (in bits) of the original message is
|
|
// then appended to complete the padded message.
|
|
//
|
|
// See RFC 1321, sections 3.1 and 3.2
|
|
|
|
pad : {a, p} (fin p, 64 >= width a) => [a] -> [65 + (a + p)]
|
|
pad msg =
|
|
msg # [True] # zero # htonll sz
|
|
where
|
|
sz : [64]
|
|
sz = width msg
|
|
|
|
|
|
|
|
// Given a message block (interpreted as 16 32-bit words) and a current MD5 state
|
|
// (as 4 32-bit words) compute the values of all the rounds of the MD5 algorithm.
|
|
//
|
|
// In the main MD5 function, the final round will be used to compute the next MD5 state.
|
|
//
|
|
// See RFC 1321, section 3.4
|
|
|
|
computeRounds : [16][32] -> MD5State -> MD5State
|
|
computeRounds msg st = rounds (msg,st) @ 64
|
|
|
|
rounds : ([16][32], MD5State) -> [65]MD5State
|
|
rounds (msg, (a0, b0, c0, d0)) =
|
|
[ (a, b, c, d) | a <- as
|
|
| b <- bs
|
|
| c <- cs
|
|
| d <- ds
|
|
]
|
|
where
|
|
bs =
|
|
[b0] #
|
|
[box (i, a, b, c, d, m, t, s) | i <- [0 .. 63]
|
|
| a <- as
|
|
| b <- bs
|
|
| c <- cs
|
|
| d <- ds
|
|
| m <- join [m @@ p | m <- [msg, msg, msg, msg]
|
|
| p <- permutes
|
|
]
|
|
| t <- sineTbl
|
|
| s <- s_constants
|
|
]
|
|
cs = [c0] # bs
|
|
ds = [d0] # cs
|
|
as = [a0] # ds
|
|
|
|
|
|
// 'S' constants from the MD5 algorithm, used to indicated how many
|
|
// bits to rotate in the box function.
|
|
//
|
|
// See RFC 1321, section 3.4, and the appendix on page 10
|
|
|
|
s_constants : [64][6]
|
|
s_constants =
|
|
repeat4 [7, 12, 17, 22] #
|
|
repeat4 [5, 9, 14, 20] #
|
|
repeat4 [4, 11, 16, 23] #
|
|
repeat4 [6, 10, 15, 21]
|
|
where
|
|
repeat4 abcd = abcd # abcd # abcd # abcd
|
|
|
|
|
|
// This table of permutations indicates which word of the message block to
|
|
// use in a given MD5 round. Its structure is most evident via observing
|
|
// the indices of the message block in the order they are used in the MD5
|
|
// reference implementation.
|
|
//
|
|
// See the appendix of RFC 1321, starting on page 13.
|
|
|
|
permutes : [4][16][4]
|
|
permutes =
|
|
[ [ 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15]
|
|
, [ 1, 6, 11, 0, 5, 10, 15, 4, 9, 14, 3, 8, 13, 2, 7, 12]
|
|
, [ 5, 8, 11, 14, 1, 4, 7, 10, 13, 0, 3, 6, 9, 12, 15, 2]
|
|
, [ 0, 7, 14, 5, 12, 3, 10, 1, 8, 15, 6, 13, 4, 11, 2, 9]
|
|
]
|
|
|
|
|
|
// The main "box" operation. The first argument indicates
|
|
// the round number, which is used to select between the box
|
|
// operations, F, G, H, and I.
|
|
//
|
|
// See RFC 1321, section 3.4
|
|
|
|
box : ([6], [32], [32], [32], [32], [32], [32], [6]) -> [32]
|
|
box (i, a, b, c, d, m, t, s) =
|
|
b + (a + boxfunc (i, b, c, d) + m + t <<< s)
|
|
|
|
boxfunc : ([6],[32],[32],[32]) -> [32]
|
|
boxfunc (i, b, c, d) =
|
|
if i < 16 then F (b, c, d) else
|
|
if i < 32 then G (b, c, d) else
|
|
if i < 48 then H (b, c, d) else
|
|
I (b, c, d)
|
|
|
|
F : ([32], [32], [32]) -> [32]
|
|
F (x, y, z) = x && y || (~x) && z
|
|
|
|
G : ([32], [32], [32]) -> [32]
|
|
G (x, y, z) = x && z || y && ~z
|
|
|
|
H : ([32], [32], [32]) -> [32]
|
|
H (x, y, z) = x ^ y ^ z
|
|
|
|
I : ([32], [32], [32]) -> [32]
|
|
I (x, y, z) = y ^ (x || ~z)
|
|
|
|
|
|
// The table of values generated from the sin function, as described
|
|
// in RFC 1321, section 3.4. These values are transcribed from
|
|
// the appendix, starting on page 13.
|
|
|
|
sineTbl : [64][32]
|
|
sineTbl =
|
|
[0xD76AA478, 0xE8C7B756, 0x242070DB, 0xC1BDCEEE, 0xF57C0FAF,
|
|
0x4787C62A, 0xA8304613, 0xFD469501, 0x698098D8, 0x8B44F7AF,
|
|
0xFFFF5BB1, 0x895CD7BE, 0x6B901122, 0xFD987193, 0xA679438E,
|
|
0x49B40821, 0xF61E2562, 0xC040B340, 0x265E5A51, 0xE9B6C7AA,
|
|
0xD62F105D, 0x02441453, 0xD8A1E681, 0xE7D3FBC8, 0x21E1CDE6,
|
|
0xC33707D6, 0xF4D50D87, 0x455A14ED, 0xA9E3E905, 0xFCEFA3F8,
|
|
0x676F02D9, 0x8D2A4C8A, 0xFFFA3942, 0x8771F681, 0x6D9D6122,
|
|
0xFDE5380C, 0xA4BEEA44, 0x4BDECFA9, 0xF6BB4B60, 0xBEBFBC70,
|
|
0x289B7EC6, 0xEAA127FA, 0xD4EF3085, 0x04881D05, 0xD9D4D039,
|
|
0xE6DB99E5, 0x1FA27CF8, 0xC4AC5665, 0xF4292244, 0x432AFF97,
|
|
0xAB9423A7, 0xFC93A039, 0x655B59C3, 0x8F0CCC92, 0xFFEFF47D,
|
|
0x85845DD1, 0x6FA87E4F, 0xFE2CE6E0, 0xA3014314, 0x4E0811A1,
|
|
0xF7537E82, 0xBD3AF235, 0x2AD7D2BB, 0xEB86D391]
|
|
|
|
|
|
// The MD5 test suite from RFC 1321, appendix A.5
|
|
|
|
property r0 = test ""
|
|
== 0xd41d8cd98f00b204e9800998ecf8427e
|
|
|
|
property r1 = test "a"
|
|
== 0x0cc175b9c0f1b6a831c399e269772661
|
|
|
|
property r2 = test "abc"
|
|
== 0x900150983cd24fb0d6963f7d28e17f72
|
|
|
|
property r3 = test "message digest"
|
|
== 0xf96b697d7cb7938d525a2f31aaf161d0
|
|
|
|
property r4 = test "abcdefghijklmnopqrstuvwxyz"
|
|
== 0xc3fcd3d76192e4007dfb496cca67e13b
|
|
|
|
property r5 = test "ABCDEFGHIJKLMNOPQRSTUVWXYZabcdefghijklmnopqrstuvwxyz0123456789"
|
|
== 0xd174ab98d277d9f5a5611c2c9f419d9f
|
|
|
|
property r6 = test "12345678901234567890123456789012345678901234567890123456789012345678901234567890"
|
|
== 0x57edf4a22be3c955ac49da2e2107b67a
|
|
|
|
alltests = r0 /\ r1 /\ r2 /\ r3 /\ r4 /\ r5 /\ r6
|