author | wenzelm |
Sat, 08 Oct 2016 11:21:29 +0200 | |
changeset 64100 | 9b1573213ebe |
parent 62819 | d3ff367a16a0 |
child 64275 | ac2abc987cf9 |
permissions | -rw-r--r-- |
35628 | 1 |
(* Title: Pure/General/sha1.ML |
2 |
Author: Makarius |
|
62666 | 3 |
Author: Sascha Boehme, TU Muenchen |
35628 | 4 |
|
62666 | 5 |
Digesting strings according to SHA-1 (see RFC 3174). |
35628 | 6 |
*) |
7 |
||
8 |
signature SHA1 = |
|
9 |
sig |
|
41954 | 10 |
eqtype digest |
11 |
val rep: digest -> string |
|
57638
ed58e740a699
less authentic SHA1.digest: trust Scala side on blobs and avoid re-calculation via Foreign Language Interface, which might be a cause of problems;
wenzelm
parents:
41954
diff
changeset
|
12 |
val fake: string -> digest |
62702 | 13 |
val digest: string -> digest |
62666 | 14 |
val test_samples: unit -> unit |
35628 | 15 |
end; |
16 |
||
17 |
structure SHA1: SHA1 = |
|
18 |
struct |
|
19 |
||
62666 | 20 |
(** internal implementation in ML -- relatively slow **) |
21 |
||
22 |
local |
|
23 |
||
35628 | 24 |
(* 32bit words *) |
25 |
||
26 |
infix 4 << >>; |
|
27 |
infix 3 andb; |
|
28 |
infix 2 orb xorb; |
|
29 |
||
30 |
val op << = Word32.<<; |
|
31 |
val op >> = Word32.>>; |
|
32 |
val op andb = Word32.andb; |
|
33 |
val op orb = Word32.orb; |
|
34 |
val op xorb = Word32.xorb; |
|
35 |
val notb = Word32.notb; |
|
36 |
||
37 |
fun rotate k w = w << k orb w >> (0w32 - k); |
|
38 |
||
39 |
||
40 |
(* hexadecimal words *) |
|
41 |
||
42 |
fun hex_digit (text, w: Word32.word) = |
|
43 |
let |
|
44 |
val d = Word32.toInt (w andb 0wxf); |
|
45 |
val dig = if d < 10 then chr (ord "0" + d) else chr (ord "a" + d - 10); |
|
46 |
in (dig ^ text, w >> 0w4) end; |
|
47 |
||
48 |
fun hex_word w = #1 (funpow 8 hex_digit ("", w)); |
|
49 |
||
50 |
||
51 |
(* padding *) |
|
52 |
||
62666 | 53 |
fun pack_bytes 0 _ = "" |
35628 | 54 |
| pack_bytes k n = pack_bytes (k - 1) (n div 256) ^ chr (n mod 256); |
55 |
||
56 |
fun padded_text str = |
|
57 |
let |
|
58 |
val len = size str; |
|
59 |
val padding = chr 128 ^ replicate_string (~ (len + 9) mod 64) (chr 0) ^ pack_bytes 8 (len * 8); |
|
60 |
fun byte i = Char.ord (String.sub (if i < len then (str, i) else (padding, (i - len)))); |
|
61 |
fun word i = |
|
62 |
Word32.fromInt (byte (4 * i)) << 0w24 orb |
|
63 |
Word32.fromInt (byte (4 * i + 1)) << 0w16 orb |
|
64 |
Word32.fromInt (byte (4 * i + 2)) << 0w8 orb |
|
65 |
Word32.fromInt (byte (4 * i + 3)); |
|
66 |
in ((len + size padding) div 4, word) end; |
|
67 |
||
68 |
||
62666 | 69 |
(* digest_string_internal *) |
35628 | 70 |
|
71 |
fun digest_word (i, w, {a, b, c, d, e}) = |
|
72 |
let |
|
73 |
val {f, k} = |
|
74 |
if i < 20 then |
|
75 |
{f = (b andb c) orb (notb b andb d), |
|
76 |
k = 0wx5A827999} |
|
77 |
else if i < 40 then |
|
78 |
{f = b xorb c xorb d, |
|
79 |
k = 0wx6ED9EBA1} |
|
80 |
else if i < 60 then |
|
81 |
{f = (b andb c) orb (b andb d) orb (c andb d), |
|
82 |
k = 0wx8F1BBCDC} |
|
83 |
else |
|
84 |
{f = b xorb c xorb d, |
|
85 |
k = 0wxCA62C1D6}; |
|
86 |
val op + = Word32.+; |
|
87 |
in |
|
88 |
{a = rotate 0w5 a + f + e + w + k, |
|
89 |
b = a, |
|
90 |
c = rotate 0w30 b, |
|
91 |
d = c, |
|
92 |
e = d} |
|
93 |
end; |
|
94 |
||
62666 | 95 |
in |
96 |
||
97 |
fun digest_string_internal str = |
|
35628 | 98 |
let |
99 |
val (text_len, text) = padded_text str; |
|
100 |
||
101 |
(*hash result -- 5 words*) |
|
102 |
val hash_array : Word32.word Array.array = |
|
103 |
Array.fromList [0wx67452301, 0wxEFCDAB89, 0wx98BADCFE, 0wx10325476, 0wxC3D2E1F0]; |
|
104 |
fun hash i = Array.sub (hash_array, i); |
|
105 |
fun add_hash x i = Array.update (hash_array, i, hash i + x); |
|
106 |
||
107 |
(*current chunk -- 80 words*) |
|
108 |
val chunk_array = Array.array (80, 0w0: Word32.word); |
|
109 |
fun chunk i = Array.sub (chunk_array, i); |
|
110 |
fun init_chunk pos = |
|
111 |
Array.modifyi (fn (i, _) => |
|
112 |
if i < 16 then text (pos + i) |
|
113 |
else rotate 0w1 (chunk (i - 3) xorb chunk (i - 8) xorb chunk (i - 14) xorb chunk (i - 16))) |
|
114 |
chunk_array; |
|
115 |
||
116 |
fun digest_chunks pos = |
|
117 |
if pos < text_len then |
|
118 |
let |
|
119 |
val _ = init_chunk pos; |
|
120 |
val {a, b, c, d, e} = Array.foldli digest_word |
|
121 |
{a = hash 0, |
|
122 |
b = hash 1, |
|
123 |
c = hash 2, |
|
124 |
d = hash 3, |
|
125 |
e = hash 4} |
|
126 |
chunk_array; |
|
127 |
val _ = add_hash a 0; |
|
128 |
val _ = add_hash b 1; |
|
129 |
val _ = add_hash c 2; |
|
130 |
val _ = add_hash d 3; |
|
131 |
val _ = add_hash e 4; |
|
132 |
in digest_chunks (pos + 16) end |
|
133 |
else (); |
|
134 |
val _ = digest_chunks 0; |
|
135 |
||
136 |
val hex = hex_word o hash; |
|
137 |
in hex 0 ^ hex 1 ^ hex 2 ^ hex 3 ^ hex 4 end; |
|
138 |
||
62666 | 139 |
end; |
41954 | 140 |
|
62666 | 141 |
|
142 |
(** external implementation in C **) |
|
143 |
||
144 |
local |
|
145 |
||
146 |
(* digesting *) |
|
147 |
||
148 |
fun hex_digit i = if i < 10 then chr (ord "0" + i) else chr (ord "a" + i - 10); |
|
149 |
||
150 |
fun hex_string arr i = |
|
151 |
let val c = CInterface.fromCchar (CInterface.offset i CInterface.Cchar arr) |
|
152 |
in (op ^) (apply2 hex_digit (Integer.div_mod (Char.ord c) 16)) end |
|
153 |
||
154 |
val lib_path = |
|
155 |
("$ML_HOME/" ^ (if ML_System.platform_is_windows then "sha1.dll" else "libsha1.so")) |
|
156 |
|> Path.explode; |
|
157 |
||
158 |
val STRING_INPUT_BYTES = |
|
159 |
CInterface.mkConversion undefined (CInterface.toCbytes o Byte.stringToBytes) |
|
160 |
(CInterface.Cpointer CInterface.Cchar); |
|
161 |
||
162 |
in |
|
163 |
||
164 |
fun digest_string_external str = |
|
165 |
let |
|
166 |
val digest = CInterface.alloc 20 CInterface.Cchar; |
|
167 |
val _ = |
|
168 |
CInterface.call3 |
|
169 |
(CInterface.get_sym (File.platform_path lib_path) "sha1_buffer") |
|
170 |
(STRING_INPUT_BYTES, CInterface.LONG, CInterface.POINTER) |
|
171 |
CInterface.POINTER (str, size str, CInterface.address digest); |
|
172 |
in fold (suffix o hex_string digest) (0 upto 19) "" end; |
|
173 |
||
174 |
end; |
|
175 |
||
176 |
||
177 |
||
178 |
(** type digest **) |
|
41954 | 179 |
|
180 |
datatype digest = Digest of string; |
|
181 |
||
182 |
fun rep (Digest s) = s; |
|
57638
ed58e740a699
less authentic SHA1.digest: trust Scala side on blobs and avoid re-calculation via Foreign Language Interface, which might be a cause of problems;
wenzelm
parents:
41954
diff
changeset
|
183 |
val fake = Digest; |
ed58e740a699
less authentic SHA1.digest: trust Scala side on blobs and avoid re-calculation via Foreign Language Interface, which might be a cause of problems;
wenzelm
parents:
41954
diff
changeset
|
184 |
|
62819
d3ff367a16a0
careful export of type-dependent functions, without losing their special status;
wenzelm
parents:
62702
diff
changeset
|
185 |
val _ = ML_system_pp (fn _ => fn _ => Pretty.to_polyml o Pretty.str o quote o rep); |
62663 | 186 |
|
62666 | 187 |
fun digest_string str = digest_string_external str |
188 |
handle CInterface.Foreign msg => |
|
189 |
(warning (msg ^ "\nUsing slow ML implementation of SHA1.digest"); digest_string_internal str); |
|
190 |
||
191 |
val digest = Digest o digest_string; |
|
192 |
||
193 |
||
194 |
||
195 |
(** SHA1 samples found in the wild **) |
|
196 |
||
197 |
local |
|
198 |
||
199 |
fun check (msg, key) = |
|
200 |
let val key' = rep (digest msg) in |
|
201 |
if key = key' then () |
|
202 |
else |
|
203 |
raise Fail ("SHA1 library integrity test failed on " ^ quote msg ^ ":\n" ^ |
|
204 |
key ^ " expected, but\n" ^ key' ^ " was found") |
|
205 |
end; |
|
206 |
||
207 |
in |
|
208 |
||
209 |
fun test_samples () = |
|
210 |
List.app check |
|
211 |
[("", "da39a3ee5e6b4b0d3255bfef95601890afd80709"), |
|
212 |
("a", "86f7e437faa5a7fce15d1ddcb9eaeaea377667b8"), |
|
213 |
("abc", "a9993e364706816aba3e25717850c26c9cd0d89d"), |
|
214 |
("abcdefghijklmnopqrstuvwxyz", "32d10c7b8cf96570ca04ce37f2a19d84240d3a89"), |
|
215 |
("The quick brown fox jumps over the lazy dog", "2fd4e1c67a2d28fced849ee1bb76e7391b93eb12"), |
|
216 |
(replicate_string 100 "\000", "ed4a77d1b56a118938788fc53037759b6c501e3d"), |
|
217 |
("a\000b", "4a3dec2d1f8245280855c42db0ee4239f917fdb8"), |
|
218 |
("\000\001", "3f29546453678b855931c174a97d6c0894b8f546")]; |
|
219 |
||
35628 | 220 |
end; |
62666 | 221 |
|
222 |
val _ = test_samples (); |
|
223 |
||
224 |
end; |