0 | module Crypto.Hash.SHA1
 1 |
 2 | import Crypto.Hash.Interfaces
 3 | import Data.Bits
 4 | import Data.DPair
 5 | import Data.Fin
 6 | import Data.Fin.Extra
 7 | import Data.List
 8 | import Data.Nat
 9 | import Data.Nat.Factor
10 | import Data.Vect
11 | import Utils.Misc
12 | import Utils.Bytes
13 | import Data.Stream
14 | import Crypto.Hash.MerkleDamgard
15 |
16 | export
17 | data Sha1 : Type where
18 |   MkSha1 : MerkleDamgard 5 64 Bits32 -> Sha1
19 |
20 | sha1_init_hash_values : Vect 5 Bits32
21 | sha1_init_hash_values =
22 |   [ 0x67452301, 0xEFCDAB89, 0x98BADCFE, 0x10325476, 0xC3D2E1F0 ]
23 |
24 | sha1_extend_message : Vect 16 Bits32 -> Stream Bits32
25 | sha1_extend_message xs = prepend (toList xs) $ go xs
26 |   where
27 |   go : Vect 16 Bits32 -> Stream Bits32
28 |   go xs =
29 |     let
30 |       [wi_16, wi_14, wi_8, wi_3] = the (Vect 4 _) $ map (flip index xs) [0, 2, 8, 13]
31 |       w = rotl 1 (wi_16 `xor` wi_14 `xor` wi_8 `xor` wi_3)
32 |     in
33 |       w :: go (tail xs `snoc` w)
34 |
35 | sha1_compress : (block : Vect 64 Bits8) -> (h : Vect 5 Bits32) -> Vect 5 Bits32
36 | sha1_compress block hash_values = zipWith (+) hash_values $ go Z (sha1_extend_message $ map (from_be {a = Bits32} {n = 4}) $ group 16 4 block) hash_values
37 |   where
38 |   loop : Bits32 -> Bits32 -> Bits32 -> Bits32 -> Bits32 -> Bits32 -> Bits32 -> Bits32 -> Vect 5 Bits32
39 |   loop f k wi a b c d e =
40 |     let temp = (rotl 5 a) + f + e + k + wi
41 |         e = d
42 |         d = c
43 |         c = rotl 30 b
44 |         b = a
45 |         a = temp
46 |     in [a, b, c, d, e]
47 |   go :  Nat -> Stream Bits32 -> Vect 5 Bits32 -> Vect 5 Bits32
48 |   go n (wi :: ws) abc@[a, b, c, d, e] =
49 |     case n `div` 20 of
50 |       0 => go (S n) ws $ loop ((b .&. c) .|. ((complement b) .&. d))  0x5A827999 wi a b c d e
51 |       1 => go (S n) ws $ loop (b `xor` c `xor` d)                     0x6ED9EBA1 wi a b c d e
52 |       2 => go (S n) ws $ loop ((b .&. c) .|. (b .&. d) .|. (c .&. d)) 0x8F1BBCDC wi a b c d e
53 |       3 => go (S n) ws $ loop (b `xor` c `xor` d)                     0xCA62C1D6 wi a b c d e
54 |       _ => abc
55 |
56 | sha1_update : List Bits8 -> Sha1 -> Sha1
57 | sha1_update input (MkSha1 s) =
58 |   let
59 |     Fraction _ 64 nblocks residue_nbyte prf = divMod (s.buffer_nbyte + length input) 64
60 |     (blocks, residue) = splitAt (mult nblocks 64) (replace_vect (sym prf) (s.buffer ++ fromList input))
61 |   in
62 |     MkSha1 $ {buffer := residue, buffer_nbyte := _, buffer_nbyte_constraint := elemSmallerThanBound residue_nbyte }
63 |       ( foldl (\s_, block_ => {hash_values $= sha1_compress block_, npassed_blocks $= S} s_) s (group nblocks 64 blocks) )
64 |
65 | sha1_finalize : Sha1 -> Vect 20 Bits8
66 | sha1_finalize (MkSha1 s) =
67 |   concat $ map (to_be {n = 4}) $
68 |     case pad_theorem {block_nbyte = 64} {residue_max_nbyte = 55} {length_nbyte = 8} (LTESucc LTEZero) Refl s.buffer_nbyte_constraint s.buffer (integer_to_be _ $ 8 * (cast s.npassed_blocks * 64 + cast s.buffer_nbyte)) of
69 |       Left block => sha1_compress block s.hash_values
70 |       Right blocks => let (x1, x2) = splitAt 64 blocks in sha1_compress x2 $ sha1_compress x1 s.hash_values
71 |
72 | export
73 | Digest Sha1 where
74 |   digest_nbyte = 20
75 |   update = sha1_update
76 |   finalize = sha1_finalize
77 |
78 | export
79 | Hash Sha1 where
80 |   block_nbyte = 64
81 |   initialize = MkSha1 $ mk_merkle_damgard sha1_init_hash_values
82 |