0 | module Network.TLS.HKDF
3 | import Crypto.Hash.HMAC
7 | import Data.Stream.Extra
13 | hkdf_extract : (0 algo : Type) -> Hash algo => List Bits8 -> List Bits8 -> Vect (digest_nbyte {algo}) Bits8
14 | hkdf_extract algo salt ikm = mac (HMAC algo) salt ikm
16 | hkdf_expand_stream : (0 algo : Type) -> Hash algo => List Bits8 -> List Bits8 -> Stream Bits8
17 | hkdf_expand_stream algo prk info = stream_concat (snd <$> iterate go (Z, []))
19 | go : (Nat, List Bits8) -> (Nat, List Bits8)
21 | let i' = cast {to=Bits8} (S i)
22 | body = last ++ info ++ [i']
23 | in (S i, toList $
mac (HMAC algo) prk body)
26 | hkdf_expand : (0 algo : Type) -> Hash algo => (l : Nat) -> List Bits8 -> List Bits8 -> Vect l Bits8
27 | hkdf_expand algo l prk info = take l $
hkdf_expand_stream algo prk info
29 | tls13_constant : List Bits8
30 | tls13_constant = string_to_ascii "tls13 "
33 | tls13_hkdf_expand_label : (0 algo : Type) -> Hash algo => (secret : List Bits8) -> (label : List Bits8) -> (context : List Bits8) -> (length : Nat) -> Vect length Bits8
34 | tls13_hkdf_expand_label algo secret label context lth =
35 | let l = to_be {n=2} $
cast {to=Bits16} lth
36 | l' = cast {to=Bits8} $
(6 + length label)
37 | i' = cast {to=Bits8} $
length context
38 | body = ((toList l) <+> [l'] <+> tls13_constant <+> label <+> [i'] <+> context)
39 | in hkdf_expand algo lth secret body
42 | record HandshakeKeys (iv : Nat) (key : Nat) where
43 | constructor MkHandshakeKeys
44 | handshake_secret : List Bits8
45 | client_handshake_key : Vect key Bits8
46 | server_handshake_key : Vect key Bits8
47 | client_handshake_iv : Vect iv Bits8
48 | server_handshake_iv : Vect iv Bits8
49 | client_traffic_secret : List Bits8
50 | server_traffic_secret : List Bits8
53 | record ApplicationKeys (iv : Nat) (key : Nat) where
54 | constructor MkApplicationKeys
55 | client_application_key : Vect key Bits8
56 | server_application_key : Vect key Bits8
57 | client_application_iv : Vect iv Bits8
58 | server_application_iv : Vect iv Bits8
61 | tls13_handshake_derive : (0 algo : Type) -> Hash algo => (iv : Nat) -> (key : Nat) -> List Bits8 -> List Bits8 -> HandshakeKeys iv key
62 | tls13_handshake_derive algo iv key shared_secret hello_hash =
63 | let zeros = List.replicate (digest_nbyte {algo}) (the Bits8 0)
64 | early_secret = toList $
hkdf_extract algo [the Bits8 0] zeros
65 | empty_hash = toList $
hash algo []
66 | derived_secret = tls13_hkdf_expand_label algo early_secret (string_to_ascii "derived") empty_hash $
digest_nbyte {algo}
67 | handshake_secret = toList $
hkdf_extract algo (toList derived_secret) shared_secret
68 | client_handshake_traffic_secret = toList $
69 | tls13_hkdf_expand_label algo handshake_secret (string_to_ascii "c hs traffic") hello_hash $
digest_nbyte {algo}
70 | server_handshake_traffic_secret = toList $
71 | tls13_hkdf_expand_label algo handshake_secret (string_to_ascii "s hs traffic") hello_hash $
digest_nbyte {algo}
72 | client_handshake_key =
73 | tls13_hkdf_expand_label algo client_handshake_traffic_secret (string_to_ascii "key") [] key
74 | client_handshake_iv =
75 | tls13_hkdf_expand_label algo client_handshake_traffic_secret (string_to_ascii "iv") [] iv
76 | server_handshake_key =
77 | tls13_hkdf_expand_label algo server_handshake_traffic_secret (string_to_ascii "key") [] key
78 | server_handshake_iv =
79 | tls13_hkdf_expand_label algo server_handshake_traffic_secret (string_to_ascii "iv") [] iv
82 | client_handshake_key
83 | server_handshake_key
86 | (toList client_handshake_traffic_secret)
87 | (toList server_handshake_traffic_secret)
90 | tls13_application_derive : {iv : Nat} -> {key : Nat} -> (0 algo : Type) -> Hash algo => HandshakeKeys iv key -> List Bits8 -> ApplicationKeys iv key
91 | tls13_application_derive algo (MkHandshakeKeys handshake_secret _ _ _ _ _ _) handshake_hash =
92 | let zeros = List.replicate (digest_nbyte {algo}) (the Bits8 0)
93 | empty_hash = toList $
hash algo []
95 | tls13_hkdf_expand_label algo handshake_secret (string_to_ascii "derived") empty_hash $
digest_nbyte {algo}
96 | master_secret = toList $
hkdf_extract algo (toList derived_secret) zeros
97 | client_application_traffic_secret = toList $
98 | tls13_hkdf_expand_label algo master_secret (string_to_ascii "c ap traffic") handshake_hash $
digest_nbyte {algo}
99 | server_application_traffic_secret = toList $
100 | tls13_hkdf_expand_label algo master_secret (string_to_ascii "s ap traffic") handshake_hash $
digest_nbyte {algo}
101 | client_application_key =
102 | tls13_hkdf_expand_label algo client_application_traffic_secret (string_to_ascii "key") [] key
103 | client_application_iv =
104 | tls13_hkdf_expand_label algo client_application_traffic_secret (string_to_ascii "iv") [] iv
105 | server_application_key =
106 | tls13_hkdf_expand_label algo server_application_traffic_secret (string_to_ascii "key") [] key
107 | server_application_iv =
108 | tls13_hkdf_expand_label algo server_application_traffic_secret (string_to_ascii "iv") [] iv
109 | in MkApplicationKeys client_application_key server_application_key client_application_iv server_application_iv
112 | tls13_verify_data : (0 algo : Type) -> Hash algo => List Bits8 -> List Bits8 -> List Bits8
113 | tls13_verify_data algo traffic_secret records_hash =
114 | let finished_key = toList $
115 | tls13_hkdf_expand_label algo traffic_secret (string_to_ascii "finished") [] $
digest_nbyte {algo}
116 | in toList $
hkdf_extract algo finished_key records_hash
119 | record Application2Keys (iv : Nat) (key : Nat) (mac : Nat) where
120 | constructor MkApplication2Keys
121 | master_secret : Vect 48 Bits8
122 | client_mac_key : Vect mac Bits8
123 | server_mac_key : Vect mac Bits8
124 | client_application_key : Vect key Bits8
125 | server_application_key : Vect key Bits8
126 | client_application_iv : Vect iv Bits8
127 | server_application_iv : Vect iv Bits8
129 | hmac_stream : Hash algo -> List Bits8 -> List Bits8 -> Stream Bits8
130 | hmac_stream hwit secret seed =
132 | $
map (\ax => toList $
mac (HMAC algo) secret $
ax <+> seed)
134 | $
iterate (toList . mac (HMAC algo) secret) seed
137 | tls12_application_derive : Hash algo -> (iv : Nat) -> (key : Nat) -> (mac : Nat) -> List Bits8 -> List Bits8 -> List Bits8 ->
138 | Application2Keys iv key mac
139 | tls12_application_derive hwit iv key mac shared_secret client_random server_random =
140 | let master_secret =
142 | $
hmac_stream hwit shared_secret
143 | $
(string_to_ascii "master secret") <+> client_random <+> server_random
146 | (toList master_secret)
147 | (string_to_ascii "key expansion" <+> server_random <+> client_random)
148 | (client_mac_key, secret_material) = Misc.splitAt mac secret_material
149 | (server_mac_key, secret_material) = Misc.splitAt mac secret_material
150 | (client_application_key, secret_material) = Misc.splitAt key secret_material
151 | (server_application_key, secret_material) = Misc.splitAt key secret_material
152 | (client_application_iv, secret_material) = Misc.splitAt iv secret_material
153 | (server_application_iv, secret_material) = Misc.splitAt iv secret_material
154 | in MkApplication2Keys
158 | client_application_key
159 | server_application_key
160 | client_application_iv
161 | server_application_iv
164 | tls12_client_verify_data : Hash algo -> (n : Nat) -> List Bits8 -> List Bits8 -> Vect n Bits8
165 | tls12_client_verify_data algo n master_secret records_hash =
166 | take _ $
hmac_stream algo master_secret (string_to_ascii "client finished" <+> records_hash)
169 | tls12_server_verify_data : Hash algo -> (n : Nat) -> List Bits8 -> List Bits8 -> Vect n Bits8
170 | tls12_server_verify_data algo n master_secret records_hash =
171 | take _ $
hmac_stream algo master_secret (string_to_ascii "server finished" <+> records_hash)