-
Notifications
You must be signed in to change notification settings - Fork 0
/
MLS.Crypto.Builtins.fsti
105 lines (82 loc) · 4.83 KB
/
MLS.Crypto.Builtins.fsti
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
module MLS.Crypto.Builtins
open Comparse
open MLS.Result
(*** Typeclass definition ***)
type available_ciphersuite =
| AC_mls_128_dhkemx25519_aes128gcm_sha256_ed25519
| AC_mls_128_dhkemx25519_chacha20poly1305_sha256_ed25519
class crypto_bytes (bytes:Type0) = {
[@@@FStar.Tactics.Typeclasses.tcinstance]
base: bytes_like bytes;
bytes_hasEq: squash (hasEq bytes);
ciphersuite: available_ciphersuite;
hash_length: nat;
hash_length_bound: squash (1 <= hash_length /\ hash_length < 256);
hash_max_input_length: nat;
hash_hash: buf:bytes{length buf < hash_max_input_length} -> lbytes bytes hash_length;
kdf_length: nat;
kdf_extract: key:bytes -> data:bytes -> result (lbytes bytes kdf_length);
kdf_expand: prk:bytes -> info:bytes -> len:nat -> result (lbytes bytes len);
hpke_public_key_length: nat;
hpke_public_key_length_bound: squash (hpke_public_key_length < pow2 16);
hpke_private_key_length: nat;
hpke_private_key_length_bound: squash(hpke_private_key_length <= kdf_length);
hpke_kem_output_length: nat;
hpke_gen_keypair: ikm:bytes{length ikm >= hpke_private_key_length} -> result (lbytes bytes hpke_private_key_length & lbytes bytes hpke_public_key_length);
hpke_encrypt: pkR:lbytes bytes hpke_public_key_length -> info:bytes -> ad:bytes -> plaintext:bytes -> entropy:lbytes bytes hpke_private_key_length -> result (lbytes bytes hpke_kem_output_length & bytes);
hpke_decrypt: enc:lbytes bytes hpke_kem_output_length -> skR:lbytes bytes hpke_private_key_length -> info:bytes -> ad:bytes -> ciphertext:bytes -> result bytes;
sign_public_key_length: nat;
sign_private_key_length: nat;
sign_nonce_length: nat;
sign_signature_length: nat;
sign_signature_length_bound: squash (sign_signature_length < 256);
sign_gen_keypair: entropy:lbytes bytes sign_private_key_length -> lbytes bytes sign_public_key_length & lbytes bytes sign_private_key_length;
sign_max_input_length: nat;
sign_sign: lbytes bytes sign_private_key_length -> buf:bytes{length buf < sign_max_input_length} -> entropy:lbytes bytes sign_nonce_length -> lbytes bytes sign_signature_length;
sign_verify: lbytes bytes sign_public_key_length -> buf:bytes{length buf < sign_max_input_length} -> lbytes bytes sign_signature_length -> bool;
aead_nonce_length: nat;
aead_nonce_length_bound: squash (4 <= aead_nonce_length);
aead_key_length: nat;
aead_encrypt: lbytes bytes aead_key_length -> lbytes bytes aead_nonce_length -> ad:bytes -> plaintext:bytes -> result bytes;
aead_decrypt: lbytes bytes aead_key_length -> lbytes bytes aead_nonce_length -> ad:bytes -> ciphertext:bytes -> result bytes;
hmac_length: nat;
hmac_length_bound: squash (hmac_length < 256);
hmac_hmac: key:bytes -> data:bytes -> result (lbytes bytes hmac_length);
string_to_bytes: s:string{b2t (normalize_term (string_is_ascii s))} -> lbytes bytes (String.strlen s);
unsafe_split: b:bytes -> i:nat{i <= length b} -> bytes & bytes;
xor: #n:nat -> lbytes bytes n -> lbytes bytes n -> lbytes bytes n;
}
(*** Utility types ***)
//type hash_type (bytes:Type0) {|crypto_bytes bytes|} = lbytes bytes (hash_length #bytes)
type hpke_public_key (bytes:Type0) {|crypto_bytes bytes|} = lbytes bytes (hpke_public_key_length #bytes)
type hpke_private_key (bytes:Type0) {|crypto_bytes bytes|} = lbytes bytes (hpke_private_key_length #bytes)
type hpke_kem_output (bytes:Type0) {|crypto_bytes bytes|} = lbytes bytes (hpke_kem_output_length #bytes)
type sign_public_key (bytes:Type0) {|crypto_bytes bytes|} = lbytes bytes (sign_public_key_length #bytes)
type sign_private_key (bytes:Type0) {|crypto_bytes bytes|} = lbytes bytes (sign_private_key_length #bytes)
type sign_nonce (bytes:Type0) {|crypto_bytes bytes|} = lbytes bytes (sign_nonce_length #bytes)
type sign_signature (bytes:Type0) {|crypto_bytes bytes|} = lbytes bytes (sign_signature_length #bytes)
type aead_nonce (bytes:Type0) {|crypto_bytes bytes|} = lbytes bytes (aead_nonce_length #bytes)
type aead_key (bytes:Type0) {|crypto_bytes bytes|} = lbytes bytes (aead_key_length #bytes)
(*** Instances ***)
type hacl_star_bytes = Lib.ByteSequence.bytes
val bytes_like_hacl_star_bytes: bytes_like hacl_star_bytes
val mk_concrete_crypto_bytes: available_ciphersuite -> Pure (crypto_bytes hacl_star_bytes)
(requires True) (ensures fun cb -> cb.base == bytes_like_hacl_star_bytes)
(*** Randomness ***)
val randomness:
bytes:Type0 -> {|bytes_like bytes|} ->
list nat ->
Type0
val mk_empty_randomness:
bytes:Type0 -> {|bytes_like bytes|} ->
randomness bytes []
val mk_randomness:
#bytes:Type0 -> {|bytes_like bytes|} ->
#head_size:nat -> #tail_size:list nat ->
(lbytes bytes head_size & randomness bytes tail_size) ->
randomness bytes (head_size::tail_size)
val dest_randomness:
#bytes:Type0 -> {|bytes_like bytes|} ->
#head_size:nat -> #tail_size:list nat ->
randomness bytes (head_size::tail_size) ->
(lbytes bytes head_size & randomness bytes tail_size)