|
1 (* Title: Pure/General/sha1.ML |
|
2 Author: Makarius |
|
3 |
|
4 Digesting strings according to SHA-1 (see RFC 3174) -- relatively slow |
|
5 version in pure ML. |
|
6 *) |
|
7 |
|
8 signature SHA1 = |
|
9 sig |
|
10 val digest: string -> string |
|
11 end; |
|
12 |
|
13 structure SHA1: SHA1 = |
|
14 struct |
|
15 |
|
16 (* 32bit words *) |
|
17 |
|
18 infix 4 << >>; |
|
19 infix 3 andb; |
|
20 infix 2 orb xorb; |
|
21 |
|
22 val op << = Word32.<<; |
|
23 val op >> = Word32.>>; |
|
24 val op andb = Word32.andb; |
|
25 val op orb = Word32.orb; |
|
26 val op xorb = Word32.xorb; |
|
27 val notb = Word32.notb; |
|
28 |
|
29 fun rotate k w = w << k orb w >> (0w32 - k); |
|
30 |
|
31 |
|
32 (* hexadecimal words *) |
|
33 |
|
34 fun hex_digit (text, w: Word32.word) = |
|
35 let |
|
36 val d = Word32.toInt (w andb 0wxf); |
|
37 val dig = if d < 10 then chr (ord "0" + d) else chr (ord "a" + d - 10); |
|
38 in (dig ^ text, w >> 0w4) end; |
|
39 |
|
40 fun hex_word w = #1 (funpow 8 hex_digit ("", w)); |
|
41 |
|
42 |
|
43 (* padding *) |
|
44 |
|
45 fun pack_bytes 0 n = "" |
|
46 | pack_bytes k n = pack_bytes (k - 1) (n div 256) ^ chr (n mod 256); |
|
47 |
|
48 fun padded_text str = |
|
49 let |
|
50 val len = size str; |
|
51 val padding = chr 128 ^ replicate_string (~ (len + 9) mod 64) (chr 0) ^ pack_bytes 8 (len * 8); |
|
52 fun byte i = Char.ord (String.sub (if i < len then (str, i) else (padding, (i - len)))); |
|
53 fun word i = |
|
54 Word32.fromInt (byte (4 * i)) << 0w24 orb |
|
55 Word32.fromInt (byte (4 * i + 1)) << 0w16 orb |
|
56 Word32.fromInt (byte (4 * i + 2)) << 0w8 orb |
|
57 Word32.fromInt (byte (4 * i + 3)); |
|
58 in ((len + size padding) div 4, word) end; |
|
59 |
|
60 |
|
61 (* digest *) |
|
62 |
|
63 fun digest_word (i, w, {a, b, c, d, e}) = |
|
64 let |
|
65 val {f, k} = |
|
66 if i < 20 then |
|
67 {f = (b andb c) orb (notb b andb d), |
|
68 k = 0wx5A827999} |
|
69 else if i < 40 then |
|
70 {f = b xorb c xorb d, |
|
71 k = 0wx6ED9EBA1} |
|
72 else if i < 60 then |
|
73 {f = (b andb c) orb (b andb d) orb (c andb d), |
|
74 k = 0wx8F1BBCDC} |
|
75 else |
|
76 {f = b xorb c xorb d, |
|
77 k = 0wxCA62C1D6}; |
|
78 val op + = Word32.+; |
|
79 in |
|
80 {a = rotate 0w5 a + f + e + w + k, |
|
81 b = a, |
|
82 c = rotate 0w30 b, |
|
83 d = c, |
|
84 e = d} |
|
85 end; |
|
86 |
|
87 fun digest str = |
|
88 let |
|
89 val (text_len, text) = padded_text str; |
|
90 |
|
91 (*hash result -- 5 words*) |
|
92 val hash_array : Word32.word Array.array = |
|
93 Array.fromList [0wx67452301, 0wxEFCDAB89, 0wx98BADCFE, 0wx10325476, 0wxC3D2E1F0]; |
|
94 fun hash i = Array.sub (hash_array, i); |
|
95 fun add_hash x i = Array.update (hash_array, i, hash i + x); |
|
96 |
|
97 (*current chunk -- 80 words*) |
|
98 val chunk_array = Array.array (80, 0w0: Word32.word); |
|
99 fun chunk i = Array.sub (chunk_array, i); |
|
100 fun init_chunk pos = |
|
101 Array.modifyi (fn (i, _) => |
|
102 if i < 16 then text (pos + i) |
|
103 else rotate 0w1 (chunk (i - 3) xorb chunk (i - 8) xorb chunk (i - 14) xorb chunk (i - 16))) |
|
104 chunk_array; |
|
105 |
|
106 fun digest_chunks pos = |
|
107 if pos < text_len then |
|
108 let |
|
109 val _ = init_chunk pos; |
|
110 val {a, b, c, d, e} = Array.foldli digest_word |
|
111 {a = hash 0, |
|
112 b = hash 1, |
|
113 c = hash 2, |
|
114 d = hash 3, |
|
115 e = hash 4} |
|
116 chunk_array; |
|
117 val _ = add_hash a 0; |
|
118 val _ = add_hash b 1; |
|
119 val _ = add_hash c 2; |
|
120 val _ = add_hash d 3; |
|
121 val _ = add_hash e 4; |
|
122 in digest_chunks (pos + 16) end |
|
123 else (); |
|
124 val _ = digest_chunks 0; |
|
125 |
|
126 val hex = hex_word o hash; |
|
127 in hex 0 ^ hex 1 ^ hex 2 ^ hex 3 ^ hex 4 end; |
|
128 |
|
129 end; |