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
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273

//! The *tls* module provides concrete implementations for the functions used in the term.
//!
//! The module offers a variety of
//! [`DynamicFunction`](puffin::algebra::dynamic_function::DynamicFunction)s which can be used in
//! the fuzzing.

use fn_impl::*;
use puffin::algebra::error::FnError;
use puffin::define_signature;
use puffin::error::Error;

mod key_exchange;
mod key_schedule;

pub mod rustls;
pub mod seeds;
pub mod violation;
pub mod vulnerabilities;

/// This modules contains all the concrete implementations of function symbols.
#[path = "."]
pub mod fn_impl {
    pub mod fn_cert;
    pub mod fn_constants;
    pub mod fn_extensions;
    pub mod fn_fields;
    pub mod fn_messages;
    pub mod fn_transcript;
    pub mod fn_utils;

    pub use fn_cert::*;
    pub use fn_constants::*;
    pub use fn_extensions::*;
    pub use fn_fields::*;
    pub use fn_messages::*;
    pub use fn_transcript::*;
    pub use fn_utils::*;
}

impl From<rustls::error::Error> for Error {
    fn from(error: rustls::error::Error) -> Self {
        Error::Stream(error.to_string())
    }
}

/// Function symbol which can be used for debugging
#[allow(dead_code)]
fn fn_debug(
    message: &crate::tls::rustls::msgs::message::Message,
) -> Result<crate::tls::rustls::msgs::message::Message, FnError> {
    dbg!(message);
    Ok(message.clone())
}

#[macro_export]
macro_rules! nyi_fn {
    ($(#[$attr:meta])*) => {};
}

define_signature!(
    TLS_SIGNATURE,
    // constants
    fn_true
    fn_false
    fn_seq_0
    fn_seq_1
    fn_seq_2
    fn_seq_3
    fn_seq_4
    fn_seq_5
    fn_seq_6
    fn_seq_7
    fn_seq_8
    fn_seq_9
    fn_seq_10
    fn_seq_11
    fn_seq_12
    fn_seq_13
    fn_seq_14
    fn_seq_15
    fn_seq_16
    fn_large_length
    fn_empty_bytes_vec
    fn_large_bytes_vec
    // messages
    fn_alert_close_notify
    fn_application_data
    fn_certificate
    fn_certificate13
    fn_certificate_request
    fn_certificate_request13
    fn_certificate_status
    fn_certificate_verify
    fn_change_cipher_spec
    fn_client_hello
    fn_client_key_exchange
    fn_empty_handshake_message
    fn_encrypted_extensions
    fn_finished
    fn_heartbeat
    fn_heartbeat_fake_length
    fn_hello_request
    fn_hello_retry_request
    fn_key_update
    fn_key_update_not_requested
    fn_message_hash
    fn_new_session_ticket
    fn_new_session_ticket13
    fn_opaque_message
    fn_server_hello
    fn_server_hello_done
    fn_server_key_exchange
    // extensions
    fn_client_extensions_new
    fn_client_extensions_append
    fn_server_extensions_new
    fn_server_extensions_append
    fn_hello_retry_extensions_new
    fn_hello_retry_extensions_append
    fn_cert_req_extensions_new
    fn_cert_req_extensions_append
    fn_cert_extensions_new
    fn_cert_extensions_append
    fn_new_session_ticket_extensions_new
    fn_new_session_ticket_extensions_append
    fn_server_name_extension
    fn_server_name_server_extension
    fn_status_request_extension
    fn_status_request_server_extension
    fn_status_request_certificate_extension
    fn_support_group_extension
    fn_ec_point_formats_extension
    fn_ec_point_formats_server_extension
    fn_signature_algorithm_extension
    fn_signature_algorithm_cert_req_extension
    fn_empty_vec_of_vec
    fn_append_vec
    fn_al_protocol_negotiation
    fn_al_protocol_server_negotiation
    fn_signed_certificate_timestamp_extension
    fn_signed_certificate_timestamp_server_extension
    fn_signed_certificate_timestamp_certificate_extension
    fn_extended_master_secret_extension
    fn_extended_master_secret_server_extension
    fn_session_ticket_request_extension
    fn_session_ticket_offer_extension
    fn_session_ticket_server_extension
    fn_new_preshared_key_identity
    fn_empty_preshared_keys_identity_vec
    fn_append_preshared_keys_identity
    fn_preshared_keys_extension_empty_binder
    fn_preshared_keys_server_extension
    fn_early_data_extension
    fn_early_data_new_session_ticket_extension
    fn_early_data_server_extension
    fn_supported_versions12_extension
    fn_supported_versions13_extension
    fn_supported_versions12_hello_retry_extension
    fn_supported_versions13_hello_retry_extension
    fn_supported_versions12_server_extension
    fn_supported_versions13_server_extension
    fn_cookie_extension
    fn_cookie_hello_retry_extension
    fn_psk_exchange_mode_dhe_ke_extension
    fn_psk_exchange_mode_ke_extension
    fn_certificate_authorities_extension
    fn_signature_algorithm_cert_extension
    fn_key_share_deterministic_extension
    fn_key_share_extension
    fn_key_share_deterministic_server_extension
    fn_key_share_server_extension
    fn_key_share_hello_retry_extension
    fn_transport_parameters_extension
    fn_transport_parameters_server_extension
    fn_renegotiation_info_extension
    fn_renegotiation_info_server_extension
    fn_transport_parameters_draft_extension
    fn_transport_parameters_draft_server_extension
    fn_unknown_client_extension
    fn_unknown_server_extension
    fn_unknown_hello_retry_extension
    fn_unknown_cert_request_extension
    fn_unknown_new_session_ticket_extension
    fn_unknown_certificate_extension
    // fields
    fn_protocol_version13
    fn_protocol_version12
    fn_new_session_id
    fn_empty_session_id
    fn_new_random
    fn_compressions
    fn_compression
    fn_no_key_share
    fn_get_server_key_share
    fn_get_client_key_share
    fn_get_any_client_curve
    fn_verify_data
    fn_verify_data_server
    fn_sign_transcript
    fn_new_cipher_suites
    fn_append_cipher_suite
    fn_cipher_suite12
    fn_cipher_suite13_aes_128_gcm_sha256
    fn_cipher_suite13_aes_256_gcm_sha384
    fn_cipher_suite13_aes_128_ccm_sha256
    fn_weak_export_cipher_suite
    fn_secure_rsa_cipher_suite12
    // utils
    fn_new_flight
    fn_append_flight
    fn_new_opaque_flight
    fn_append_opaque_flight
    fn_new_transcript
    fn_append_transcript
    fn_decrypt_handshake_flight
    fn_decrypt_multiple_handshake_messages
    fn_decrypt_application_flight
    fn_find_server_certificate
    fn_find_server_certificate_request
    fn_find_server_ticket
    fn_find_server_certificate_verify
    fn_find_encrypted_extensions
    fn_find_server_finished
    fn_no_psk
    fn_psk
    fn_decrypt_application
    fn_encrypt_handshake
    fn_encrypt_application
    fn_derive_psk
    fn_derive_binder
    fn_fill_binder
    fn_get_ticket
    fn_get_ticket_age_add
    fn_get_ticket_nonce
    fn_new_transcript12
    fn_decode_ecdh_pubkey
    fn_encode_ec_pubkey12
    fn_new_pubkey12
    fn_encrypt12
    fn_new_certificate
    fn_new_certificates
    fn_append_certificate
    fn_new_certificate_entries
    fn_append_certificate_entry
    fn_named_group_secp384r1
    fn_named_group_x25519
    fn_u64_to_u32
    // transcript functions
    fn_server_hello_transcript
    fn_client_finished_transcript
    fn_server_finished_transcript
    fn_certificate_transcript
    // certificate functions
    fn_bob_cert
    fn_bob_key
    fn_alice_cert
    fn_alice_key
    fn_eve_cert
    fn_random_ec_cert
    fn_certificate_entry
    fn_empty_certificate_chain
    fn_chain_append_certificate_entry
    fn_get_context
    fn_eve_pkcs1_signature
    fn_rsa_sign_client
    fn_rsa_sign_server
    fn_ecdsa_sign_client
    fn_ecdsa_sign_server
    fn_rsa_pss_signature_algorithm
    fn_rsa_pkcs1_signature_algorithm
    fn_invalid_signature_algorithm
    fn_ecdsa_signature_algorithm
);