Crate bertie

Bertie is a minimal, high-assurance implementation of TLS 1.3

It is built upon the following design principles:

1. Purely functional: no mutable data structures or externally visible side-effects.
2. Verification friendly: written in a way that can be translated to verifiable models
3. Succinct and minimal: configured with a single protocol version and cipher suite.

In particular, the protocol code in Bertie is passed through the hax verification toolchain to generate F* code that can be formally verified for correctness and security.

Bertie is a library, which you can add as a dependency in your project. The API for this library is in tls13api. To create a Bertie client, you will need to use the methods for the tls13api::Client type. Similarly, you will use the methods for tls13api::Server to run a Bertie server.

For simple examples of how to use these APIs, look at the source code of tls13client and tls13server.

Re-exports

• pub use tls13api::Client;
• pub use tls13api::Server;

Modules

• server
  TLS 1.3 Server
• stream
  Streaming API
• test_utils
• tls13api
  Public TLS 1.3 API
• tls13cert
  X.509 Certificates
• tls13crypto
• tls13utils

Enums

• AlertDescription
• AlertLevel
• ContentType

Functions

• get_hs_type