0 | module Crypto.Hash.MerkleDamgard
  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 |
 15 | public export
 16 | record MerkleDamgard (internal_state_nbyte : Nat) (0 block_nbyte : Nat) (0 word_type : Type) where
 17 |   constructor MkMerkleDamgard
 18 |   hash_values : Vect internal_state_nbyte word_type
 19 |   buffer_nbyte : Nat
 20 |   buffer_nbyte_constraint : LT buffer_nbyte block_nbyte
 21 |   buffer : Vect buffer_nbyte Bits8
 22 |   npassed_blocks : Nat
 23 |
 24 | export
 25 | mk_merkle_damgard : (init_hash_values : Vect internal_state_nbyte word_type) ->
 26 |                     {auto 0 prf : LTE 1 block_nbyte} ->
 27 |                     MerkleDamgard internal_state_nbyte block_nbyte word_type
 28 | mk_merkle_damgard x {prf = LTESucc prf'} = MkMerkleDamgard x 0 (LTESucc LTEZero) [] 0
 29 |
 30 | public export
 31 | pad_lemma : {residue_nbyte, length_nbyte, residue_max_nbyte, block_nbyte : Nat}
 32 |   -> LTE 1 block_nbyte
 33 |   -> (residue_max_nbyte + 1 + length_nbyte = block_nbyte)
 34 |   -> LTE residue_nbyte residue_max_nbyte
 35 |   -> (plus residue_nbyte (S (plus (minus residue_max_nbyte residue_nbyte) length_nbyte))) = block_nbyte
 36 | pad_lemma remilia flandre sakuya =
 37 |   rewrite sym flandre in
 38 |   rewrite sym $ plusSuccRightSucc residue_nbyte (plus (minus residue_max_nbyte residue_nbyte) length_nbyte) in
 39 |   rewrite plusAssociative residue_nbyte (minus residue_max_nbyte residue_nbyte) length_nbyte in
 40 |   rewrite plusCommutative residue_nbyte (minus residue_max_nbyte residue_nbyte) in
 41 |   rewrite plusMinusLte residue_nbyte residue_max_nbyte sakuya in
 42 |   rewrite plusCommutative residue_max_nbyte 1 in
 43 |     Refl
 44 |
 45 | public export
 46 | pad_over_lemma : {residue_nbyte, length_nbyte, residue_max_nbyte, block_nbyte : Nat}
 47 |   -> (residue_max_nbyte + 1 + length_nbyte = block_nbyte)
 48 |   -> LT residue_nbyte block_nbyte
 49 |   -> plus residue_nbyte (S (plus (plus (minus block_nbyte residue_nbyte) residue_max_nbyte) length_nbyte)) = (plus block_nbyte (plus block_nbyte 0))
 50 | pad_over_lemma flandre cirno =
 51 |   rewrite sym $ plusSuccRightSucc residue_nbyte (plus (plus (minus block_nbyte residue_nbyte) residue_max_nbyte) length_nbyte) in
 52 |   rewrite plusAssociative residue_nbyte (plus (minus block_nbyte residue_nbyte) residue_max_nbyte) length_nbyte in
 53 |   rewrite plusAssociative residue_nbyte (minus block_nbyte residue_nbyte) residue_max_nbyte in
 54 |   rewrite plusCommutative residue_nbyte (minus block_nbyte residue_nbyte) in
 55 |   rewrite plusMinusLte residue_nbyte block_nbyte (lteSuccLeft cirno) in
 56 |   rewrite sym $ plusAssociative block_nbyte residue_max_nbyte length_nbyte in
 57 |   rewrite plusSuccRightSucc block_nbyte (plus residue_max_nbyte length_nbyte) in
 58 |   rewrite plusZeroRightNeutral block_nbyte in
 59 |   rewrite flandre' in
 60 |     Refl
 61 |   where
 62 |   flandre' : S (plus residue_max_nbyte length_nbyte) = block_nbyte
 63 |   flandre' = rewrite sym flandre in rewrite plusCommutative residue_max_nbyte 1 in Refl
 64 |
 65 | public export
 66 | pad_residue : {residue_nbyte, length_nbyte, residue_max_nbyte, block_nbyte : _}
 67 |   -> (0 _ : LTE 1 block_nbyte)
 68 |   -> (0 _ : (residue_max_nbyte + 1 + length_nbyte = block_nbyte))
 69 |   -> (0 _ : LTE residue_nbyte residue_max_nbyte)
 70 |   -> Vect residue_nbyte Bits8
 71 |   -> Vect length_nbyte Bits8
 72 |   -> Vect block_nbyte Bits8
 73 | pad_residue remilia flandre sakuya residue b_length =
 74 |    replace_vect (pad_lemma remilia flandre sakuya) $
 75 |      residue
 76 |      ++ [0b10000000]
 77 |      ++ replicate (minus residue_max_nbyte residue_nbyte) 0
 78 |      ++ b_length
 79 |
 80 | public export
 81 | pad_over_residue : {residue_nbyte, length_nbyte, residue_max_nbyte, block_nbyte : _}
 82 |   -> (0 _ : LTE 1 block_nbyte)
 83 |   -> (0 _ : residue_max_nbyte + 1 + length_nbyte = block_nbyte)
 84 |   -> (0 _ : LT residue_max_nbyte residue_nbyte)
 85 |   -> (0 _ : LT residue_nbyte block_nbyte)
 86 |   -> Vect residue_nbyte Bits8
 87 |   -> Vect length_nbyte Bits8
 88 |   -> Vect (2 * block_nbyte) Bits8
 89 | pad_over_residue remilia flandre rumia cirno residue b_length =
 90 |   replace_vect (pad_over_lemma flandre cirno) $
 91 |     residue
 92 |     ++ [0b10000000]
 93 |     ++ replicate (minus block_nbyte residue_nbyte + residue_max_nbyte) 0
 94 |     ++ b_length
 95 |
 96 | public export
 97 | pad_theorem : {residue_nbyte, length_nbyte, residue_max_nbyte, block_nbyte : _}
 98 |   -> (0 _ : LTE 1 block_nbyte)
 99 |   -> (0 _ : residue_max_nbyte + 1 + length_nbyte = block_nbyte)
100 |   -> (0 _ : LT residue_nbyte block_nbyte)
101 |   -> Vect residue_nbyte Bits8
102 |   -> Vect length_nbyte Bits8
103 |   -> Either (Vect block_nbyte Bits8) (Vect (block_nbyte + block_nbyte) Bits8)
104 | pad_theorem remilia flandre cirno input b_length =
105 |   case isLTE residue_nbyte residue_max_nbyte of
106 |     Yes sakuya => Left $ pad_residue remilia flandre sakuya input b_length
107 |     No rumia => Right $ replace_vect (cong (plus block_nbyte) (plusZeroRightNeutral block_nbyte)) $ pad_over_residue remilia flandre (notLTEImpliesGT rumia) cirno input b_length
108 |