maTLS: How to Make TLS Middlebox-aware?

Network Distributed System Security '19

Tamarin Overview

We verify the security of the maTLS protocol with the help of Tamarin

Tamarin

An image will be inserted

▸ Tamarin is built upon a multiset rewriting model

     Tamarin is based on a state-transition model defined by a state that consists of a multiset of factsand a rule that changes one state to another state. A particular fact can trigger several rules so one fact can make several branch. A list of transitions are called trace. The properties to be proved on trace are called lemmas that are in the form of the first-order logic formulae. If a formula is violated, Tamarin generates a graph showing a trace that leads to the contradicting state.

▸ Tamarin assumes the Dolev-Yao adversary

     In the Tamarin execution model, all the messages are sent to the network adversary. This captures the passive adversary who can read all the messages in the network.

▸ Our impentation can be found in the public repository

     The full Tamarin implementation can be found at https://github.com/middlebox-aware-tls/matls-tamarin.git.

Lemmas

Our seven goals are described in the first order logic to be proved in Tamarin

Server Authentication

▸ Desciption

     When a client believes she has finished an maTLS handshake, the corresponding server also believes he has established a session with the client, sharing the same accountability key data.

▸ Formulae

     For a client (C), a server (S), and nonces (nonces), when the handshake in the client's perspective is completed at the time tc, there exists a time ts (before tc) that the server finished the handshake with the client sharing the same nonces, leading to the accountability key.
An image will be inserted

Middlebox Authentication

An image will be inserted

▸ Description

     When the client confirms a middlebox as part of the handshake, the client shares accountability key data with them.

▸ Formulae

     For a client (C), a middlebox (MB), and nonces (nonces), when the handshake in the client's perspective is completed at the time tc, there exists a time tmb (before tc) that the middlebox finished the handshake with the client sharing the same nonces, leading to the accountability key.

Segment Secrecy

▸ Description

     When the maTLS session is established, a client correctly verifies the security parameters used in each segment.

▸ Formulae

     For a client (C), a middlebox (MB), a server (S), nonces (nonces), and security parameters (params), when a client performs security parameter verificationwith params at tc and finishes the handshake at tcomplete, there exist entities that sent the corresponding security parameters to the client at tmb (before tc).
An image will be inserted

Individual Secrecy

An image will be inserted

▸ Description

     At the end of an maTLS handshake, each segment has established distinct TLS keys.

▸ Formulae

     For a client (c), a server (S), and nonces (nonces), when a client finishes a handshake, a keyA established between a1 and a2 and a keyB established between b1 and b2 is different. Otherwise, a1 and b1, a2 and b2 are identical, respectively.

Data Source Authentication

▸ Description

     When a client receives a message from the server during the maTLS record phase, the hash value from the server is a faithful digest of the original message.

▸ Formulae

     For a client (C), a server (S), nonces (nonces), a request (req), and a response (resp), when a client receives a message and believes it is from a server at time trecv, there exists a time tresp that the server sends a response to the client.
(Note that a server can be interchangeable with a middlebox in this formulae since there can be a middlebox such as a web cache that generates a message. Here, we just use a server for brevity.)
An image will be inserted

Modification Accountability

An image will be inserted

▸ Description

     When a client receives a message during the maTLS record phase, the client believes that a middlebox has changed the message if and only if that middlebox did make a change.

▸ Formulae

     For a client (C), a server (S), nonces (nonces), and a request (req), when a client receives a response to a request at the time trecv, there exists the time tmb that a middlebox modifies the message from before to after and the time tc that a client checks the modification. Note that tmb should be earlier than tc and tc should be earlier than or equal to trecv.

Path Integrity

▸ Description

     The client knows the order of the intermediate middleboxes in an maTLS session. Messages will always travel in this order.

▸ Formulae

     For agents (a1, a2, a3) and nonces (nonces), when the path is established in the order that a1 is followed by a2 at ta and a2 is followed by a3 at tb, if a2 forwards the message to a3 at tf, there exists the time tp before tf when a1 forwards the message to a2.
An image will be inserted