0 | -- BearSSL's "adding holes" algorithm for XOR multiplication
  1 | -- Based on BearSSL ghash_ctmul64.c
  2 |
  3 | module Crypto.Hash.GHash
  4 |
  5 | import Utils.Bytes
  6 | import Data.Bits
  7 | import Data.List
  8 | import Data.Vect
  9 | import Data.DPair
 10 | import Data.Fin
 11 | import Data.Fin.Extra
 12 | import Data.Nat
 13 | import Data.Nat.Order.Properties
 14 | import Utils.Misc
 15 | import Crypto.Hash
 16 |
 17 | HValues : Type
 18 | HValues = (Bits64, Bits64, Bits64, Bits64, Bits64, Bits64)
 19 |
 20 | -- Carryless multiplication with "holes"
 21 | bmul : Bits64 -> Bits64 -> Bits64
 22 | bmul x y =
 23 |   let x0 = x .&. 0x1111111111111111
 24 |       x1 = x .&. 0x2222222222222222
 25 |       x2 = x .&. 0x4444444444444444
 26 |       x3 = x .&. 0x8888888888888888
 27 |       y0 = y .&. 0x1111111111111111
 28 |       y1 = y .&. 0x2222222222222222
 29 |       y2 = y .&. 0x4444444444444444
 30 |       y3 = y .&. 0x8888888888888888
 31 |       z0 = (x0 * y0) `xor` (x1 * y3) `xor` (x2 * y2) `xor` (x3 * y1)
 32 |       z1 = (x0 * y1) `xor` (x1 * y0) `xor` (x2 * y3) `xor` (x3 * y2)
 33 |       z2 = (x0 * y2) `xor` (x1 * y1) `xor` (x2 * y0) `xor` (x3 * y3)
 34 |       z3 = (x0 * y3) `xor` (x1 * y2) `xor` (x2 * y1) `xor` (x3 * y0)
 35 |   in (z0 .&. 0x1111111111111111) .|.
 36 |      (z1 .&. 0x2222222222222222) .|.
 37 |      (z2 .&. 0x4444444444444444) .|.
 38 |      (z3 .&. 0x8888888888888888)
 39 |
 40 | rms : Bits64 -> Index {a=Bits64} -> Bits64 -> Bits64
 41 | rms m s x = (shiftL (x .&. m) s) .|. ((shiftR x s) .&. m)
 42 |
 43 | rev64 : Bits64 -> Bits64
 44 | rev64 x =
 45 |   let x' =
 46 |       (rms 0x0000FFFF0000FFFF 16) $
 47 |       (rms 0x00FF00FF00FF00FF 8 ) $
 48 |       (rms 0x0F0F0F0F0F0F0F0F 4 ) $
 49 |       (rms 0x3333333333333333 2 ) $
 50 |       (rms 0x5555555555555555 1 ) x
 51 |   in (shiftL x' 32) .|. (shiftR x' 32)
 52 |
 53 | gmult_core : Bits64 -> Bits64 -> HValues -> (Bits64, Bits64)
 54 | gmult_core y1 y0 (h0, h0r, h1, h1r, h2, h2r) =
 55 |   let y1r = rev64 y1
 56 |       y0r = rev64 y0
 57 |       y2 = xor y0 y1
 58 |       y2r = xor y0r y1r
 59 |       -- Karatsuba decomposition
 60 |       -- Here we decompose the 128 bit multiplication into
 61 |       -- 3 64-bits multiplication
 62 |       -- The h-suffixed variables are just multiplication for
 63 |       -- reversed bits, which is necessary because we want the
 64 |       -- high bits
 65 |       z0 = bmul y0 h0
 66 |       z1 = bmul y1 h1
 67 |       z2 = bmul y2 h2
 68 |       z0h = bmul y0r h0r
 69 |       z1h = bmul y1r h1r
 70 |       z2h = bmul y2r h2r
 71 |       z2  = xor (xor z0 z1) z2
 72 |       z2h = xor (xor z0h z1h) z2h
 73 |       z0h = shiftR (rev64 z0h) 1
 74 |       z1h = shiftR (rev64 z1h) 1
 75 |       z2h = shiftR (rev64 z2h) 1
 76 |       -- Since the operation is done in big-endian, but GHASH spec
 77 |       -- needs small endian, we flip the bits
 78 |       v0 = z0
 79 |       v1 = xor z0h z2
 80 |       v2 = xor z1 z2h
 81 |       v3 = z1h
 82 |       v3 = (shiftL v3 1) .|. (shiftR v2 63)
 83 |       v2 = (shiftL v2 1) .|. (shiftR v1 63)
 84 |       v1 = (shiftL v1 1) .|. (shiftR v0 63)
 85 |       v0 = (shiftL v0 1)
 86 |       -- Modular reduction to GF[128]
 87 |       v2 = v2 `xor` v0              `xor` (shiftR v0 1)  `xor` (shiftR v0 2) `xor` (shiftR v0 7)
 88 |       v1 = v1 `xor` (shiftL v0 63) `xor` (shiftL v0 62) `xor` (shiftL v0 57)
 89 |       v3 = v3 `xor` v1             `xor` (shiftR v1 1)  `xor` (shiftR v1 2) `xor` (shiftR v1 7)
 90 |       v2 = v2 `xor` (shiftL v1 63) `xor` (shiftL v1 62) `xor` (shiftL v1 57)
 91 |   in (v3, v2)
 92 |
 93 | gcm_mult : HValues -> Vect 16 Bits8 -> Vect 16 Bits8
 94 | gcm_mult h y =
 95 |   let y1 = from_be $ take 8 y
 96 |       y0 = from_be $ drop 8 y
 97 |       (y1', y0') = gmult_core y1 y0 h
 98 |   in to_be {n=8} y1' ++ to_be y0'
 99 |
100 | mk_h_values : Vect 16 Bits8 -> HValues
101 | mk_h_values h =
102 |   let h1  = from_be $ take 8 h
103 |       h0  = from_be $ drop 8 h
104 |       h0r = rev64 h0
105 |       h1r = rev64 h1
106 |       h2  = xor h0 h1
107 |       h2r = xor h0r h1r
108 |   in (h0, h0r, h1, h1r, h2, h2r)
109 |
110 | export
111 | data GHash : Type where
112 |   MkGHash : List Bits8 -> HValues -> Vect 16 Bits8 -> GHash
113 |
114 | hash_until_done : GHash -> GHash
115 | hash_until_done ghash@(MkGHash buffer hval state) =
116 |   case splitAtExact 16 buffer of
117 |     Just (a, b) => hash_until_done $ MkGHash b hval (gcm_mult hval (zipWith xor a state))
118 |     Nothing => ghash
119 |
120 | export
121 | Digest GHash where
122 |   digest_nbyte = 16
123 |   update message (MkGHash buffer hval state) =
124 |     hash_until_done (MkGHash (buffer <+> message) hval state)
125 |   finalize (MkGHash buffer hval state) =
126 |     let (MkGHash _ _ state) = hash_until_done (MkGHash (pad_zero 16 buffer) hval state)
127 |     in state
128 |
129 | export
130 | MAC (Vect 16 Bits8) GHash where
131 |   initialize_mac key = MkGHash [] (mk_h_values key) (replicate _ 0)
132 |