cryptol/examples/MD5.cry

// 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