0 | module Network.TLS.AEAD
  1 |
  2 | import Data.Stream
  3 | import Data.Bits
  4 | import Data.Vect
  5 | import Data.List
  6 | import Utils.Misc
  7 | import Utils.Bytes
  8 | import Crypto.AES.Big
  9 | import Crypto.AES.Common
 10 | import Crypto.Hash
 11 | import Crypto.Hash.GHash
 12 | import Crypto.Hash.Poly1305
 13 | import Crypto.ChaCha
 14 |
 15 | public export
 16 | interface AEAD (0 a : Type) where
 17 |   ||| IV generated during key exchange
 18 |   fixed_iv_length : Nat
 19 |   enc_key_length : Nat
 20 |   mac_length : Nat
 21 |   mac_key_length : Nat
 22 |   ||| Part of IV that is sent along with the ciphertext, should always be 0 in TLS 1.3
 23 |   record_iv_length : Nat
 24 |
 25 |   encrypt : Vect enc_key_length Bits8 -> Vect fixed_iv_length Bits8 -> Vect mac_key_length Bits8 -> Nat ->
 26 |             (plaintext : List Bits8) -> (aad : List Bits8) -> (Vect record_iv_length Bits8, List Bits8, Vect mac_length Bits8)
 27 |   decrypt : Vect enc_key_length Bits8 -> Vect fixed_iv_length Bits8 -> Vect record_iv_length Bits8 -> Vect mac_key_length Bits8 -> Nat ->
 28 |             (ciphertext : List Bits8) -> (plaintext_to_aad : List Bits8 -> List Bits8) -> (mac_tag : List Bits8) -> (List Bits8, Bool)
 29 |
 30 | aes_pad_iv_block : {iv : Nat} -> Vect iv Bits8 -> Stream (Vect (iv+4) Bits8)
 31 | aes_pad_iv_block iv = map ((iv ++) . to_be . (cast {to=Bits32})) $ drop 2 nats
 32 |
 33 | aes_keystream : (mode : Mode) -> Vect ((get_n_k mode) * 4) Bits8 -> Vect 12 Bits8 -> Stream Bits8
 34 | aes_keystream mode key iv =
 35 |   stream_concat $ map (toList . encrypt_block mode key) (aes_pad_iv_block iv)
 36 |
 37 | aes_gcm_create_aad : (mode : Mode) -> Vect ((get_n_k mode) * 4) Bits8 -> Vect 12 Bits8 -> List Bits8 -> List Bits8 -> Vect 16 Bits8
 38 | aes_gcm_create_aad mode key iv aad ciphertext =
 39 |   let a = toList $ to_be {n=8} $ cast {to=Bits64} $ 8 * (length aad)
 40 |       c = toList $ to_be {n=8} $ cast {to=Bits64} $ 8 * (length ciphertext)
 41 |       input = pad_zero 16 aad <+> pad_zero 16 ciphertext <+> a <+> c
 42 |       h = encrypt_block mode key (replicate _ 0)
 43 |       output = mac GHash h input
 44 |       j0 = encrypt_block mode key (iv ++ (to_be $ the Bits32 1))
 45 |   in zipWith xor j0 output
 46 |
 47 | public export
 48 | data TLS13_AES_128_GCM : Type where
 49 |
 50 | public export
 51 | AEAD TLS13_AES_128_GCM where
 52 |   fixed_iv_length = 12
 53 |   enc_key_length = 16
 54 |   mac_length = 16
 55 |   mac_key_length = 0
 56 |   record_iv_length = 0
 57 |
 58 |   encrypt key iv mac_key seq_no plaintext aad =
 59 |     let iv' = zipWith xor iv $ integer_to_be _ $ natToInteger seq_no
 60 |         ciphertext = zipWith xor plaintext (toList $ Stream.take (length plaintext) $ aes_keystream AES128 key iv')
 61 |         mac_tag = aes_gcm_create_aad AES128 key iv' aad ciphertext
 62 |     in ([], ciphertext, mac_tag)
 63 |
 64 |   decrypt key iv [] mac_key seq_no ciphertext aadf mac_tag' =
 65 |     let iv' = zipWith xor iv $ integer_to_be _ $ natToInteger seq_no
 66 |         plaintext = zipWith xor ciphertext (toList $ Stream.take (length ciphertext) $ aes_keystream AES128 key iv')
 67 |         mac_tag = aes_gcm_create_aad AES128 key iv' (aadf plaintext) ciphertext
 68 |     in (plaintext, s_eq' (toList mac_tag) mac_tag')
 69 |
 70 | public export
 71 | data TLS12_AES_128_GCM : Type where
 72 |
 73 | public export
 74 | AEAD TLS12_AES_128_GCM where
 75 |   fixed_iv_length = 4
 76 |   enc_key_length = 16
 77 |   mac_length = 16
 78 |   mac_key_length = 0
 79 |   record_iv_length = 8
 80 |
 81 |   encrypt key iv mac_key seq_no plaintext aad =
 82 |     let explicit_iv = to_be {n=8} $ cast {to=Bits64} seq_no
 83 |         iv' = iv ++ explicit_iv
 84 |         ciphertext = zipWith xor plaintext (toList $ Stream.take (length plaintext) $ aes_keystream AES128 key iv')
 85 |         mac_tag = aes_gcm_create_aad AES128 key iv' aad ciphertext
 86 |     in (explicit_iv, ciphertext, mac_tag)
 87 |
 88 |   decrypt key iv explicit_iv mac_key seq_no ciphertext aadf mac_tag' =
 89 |     let iv' = iv ++ explicit_iv
 90 |         plaintext = zipWith xor ciphertext (toList $ Stream.take (length ciphertext) $ aes_keystream AES128 key iv')
 91 |         mac_tag = aes_gcm_create_aad AES128 key iv' (aadf plaintext) ciphertext
 92 |     in (plaintext, s_eq' (toList mac_tag) mac_tag')
 93 |
 94 | public export
 95 | data TLS13_AES_256_GCM : Type where
 96 |
 97 | public export
 98 | AEAD TLS13_AES_256_GCM where
 99 |   fixed_iv_length = 12
100 |   enc_key_length = 32
101 |   mac_length = 16
102 |   mac_key_length = 0
103 |   record_iv_length = 0
104 |
105 |   encrypt key iv mac_key seq_no plaintext aad =
106 |     let iv' = zipWith xor iv $ integer_to_be _ $ natToInteger seq_no
107 |         ciphertext = zipWith xor plaintext (toList $ Stream.take (length plaintext) $ aes_keystream AES256 key iv')
108 |         mac_tag = aes_gcm_create_aad AES256 key iv' aad ciphertext
109 |     in ([], ciphertext, mac_tag)
110 |
111 |   decrypt key iv [] mac_key seq_no ciphertext aadf mac_tag' =
112 |     let iv' = zipWith xor iv $ integer_to_be _ $ natToInteger seq_no
113 |         plaintext = zipWith xor ciphertext (toList $ Stream.take (length ciphertext) $ aes_keystream AES256 key iv')
114 |         mac_tag = aes_gcm_create_aad AES256 key iv' (aadf plaintext) ciphertext
115 |     in (plaintext, s_eq' (toList mac_tag) mac_tag')
116 |
117 | public export
118 | data TLS12_AES_256_GCM : Type where
119 |
120 | public export
121 | AEAD TLS12_AES_256_GCM where
122 |   fixed_iv_length = 4
123 |   enc_key_length = 32
124 |   mac_length = 16
125 |   mac_key_length = 0
126 |   record_iv_length = 8
127 |
128 |   encrypt key iv mac_key seq_no plaintext aad =
129 |     let explicit_iv = to_be {n=8} $ cast {to=Bits64} seq_no
130 |         iv' = iv ++ explicit_iv
131 |         ciphertext = zipWith xor plaintext (toList $ Stream.take (length plaintext) $ aes_keystream AES256 key iv')
132 |         mac_tag = aes_gcm_create_aad AES256 key iv' aad ciphertext
133 |     in (explicit_iv, ciphertext, mac_tag)
134 |
135 |   decrypt key iv explicit_iv mac_key seq_no ciphertext aadf mac_tag' =
136 |     let iv' = iv ++ explicit_iv
137 |         plaintext = zipWith xor ciphertext (toList $ Stream.take (length ciphertext) $ aes_keystream AES256 key iv')
138 |         mac_tag = aes_gcm_create_aad AES256 key iv' (aadf plaintext) ciphertext
139 |     in (plaintext, s_eq' (toList mac_tag) mac_tag')
140 |
141 | chacha_create_aad : Vect 64 Bits8 -> List Bits8 -> List Bits8 -> Vect 16 Bits8
142 | chacha_create_aad polykey aad ciphertext =
143 |   let key = take 32 polykey
144 |       length_aad = toList $ to_le {n=8} $ cast {to=Bits64} $ length aad
145 |       length_ciphertext = toList $ to_le {n=8} $ cast {to=Bits64} $ length ciphertext
146 |       input = pad_zero 16 aad ++ pad_zero 16 ciphertext ++ length_aad ++ length_ciphertext
147 |   in mac Poly1305 key input
148 |
149 | public export
150 | data TLS1213_ChaCha20_Poly1305 : Type where
151 |
152 | public export
153 | AEAD TLS1213_ChaCha20_Poly1305 where
154 |   fixed_iv_length = 12
155 |   enc_key_length = 32
156 |   mac_length = 16
157 |   mac_key_length = 0
158 |   record_iv_length = 0
159 |
160 |   encrypt key iv [] seq_no plaintext aad =
161 |     let k' = from_le {n=4} <$> group 8 4 key
162 |         iv' = zipWith xor iv $ integer_to_be _ $ natToInteger seq_no
163 |         i' = from_le {n=4} <$> group 3 4 iv'
164 |         (polykey :: keystream) = map (\c => chacha_rfc8439_block 10 (cast c) k' i') nats
165 |         ciphertext = zipWith xor plaintext (toList $ Stream.take (length plaintext) $ stream_concat keystream)
166 |         auth_tag = chacha_create_aad polykey aad ciphertext
167 |     in ([], ciphertext, auth_tag)
168 |
169 |   decrypt key iv [] [] seq_no ciphertext aadf mac_tag' =
170 |     let k' = from_le {n=4} <$> group 8 4 key
171 |         iv' = zipWith xor iv $ integer_to_be _ $ natToInteger seq_no
172 |         i' = from_le {n=4} <$> group 3 4 iv'
173 |         (polykey :: keystream) = map (\c => chacha_rfc8439_block 10 (cast c) k' i') nats
174 |         plaintext = zipWith xor ciphertext (toList $ Stream.take (length ciphertext) $ stream_concat keystream)
175 |         auth_tag = chacha_create_aad polykey (aadf plaintext) ciphertext
176 |     in (plaintext, toList auth_tag `s_eq'` mac_tag')
177 |