Newer
Older
\xkcdchapter[0.27]{Validation}{protocol}{Finally Bob arrives, but everyone's already left}
\lettrine{I}{n} this chapter we will try to understand what requirements (Section \ref{Requirements}) we managed to respect, and which ones we missed. But before doing this we will spend some time to make sure that what we have done is actually safe.
This step will ensure us that the protocol is actually safe to use, and the interaction between the various features of the protocols will not leak the user tokens, or that it will let an attacker impersonate a legitimate user.
\subsection{Formal verification failures}\index{Failed verification!TLS}
TLS has been verified multiple times \cite{Proverif_TLS,TLS_1,TLS_2,TLS_3,TLS_4}, especially in the last couple of years, and the result has always been a positive evaluation.
Although researchers made a lot of work, and their analysis were correct, recently a new attack came out, and it was called \textbf{3Shake} \cite{3Shake} due to its focus being the TLS handshake.
The researchers' work was correct and every formal verification passed, but probably due to the high complexity of the problem, they focused only on the core of TLS, its handshake, and did not consider other extensions. TLS however has been extended multiple times from the original specification, and multiple parts remain optional and were thus not included in the verification.
That turned out to be a big mistake since combining the handshake, connection resumption and rekeying extensions led to a possible hijack of any user connection.
The problems that let the attack go unnoticed were:
\begin{itemize}
\item \textbf{Complexity}: only main parts of the protocol were verified, but a lot of extensions focused on what basically were new key-agreement algorithms, and were not verified as they were optional.
\item \textbf{Lax RFC}: Due to implementation-defined parts, the specification let programmers define a session id as something generated from easy-to-guess or cleartext data, thus making the session id not unique anymore.
The result is that all the verifications were correct, yet myopic, but even by modeling the whole specification this bug might have been left unnoticed as it comes from lax specifications.
Due to this, when an RFC or formal description of the Fenrir protocol is created, the advice is to leave no field undescribed or implementation-defined.
To avoid making mistakes in the formal verification, the obvious choice is to use existing tools designed exactly to analyze protocols and their security properties. We are talking about \textbf{Proverif} \cite{Proverif}, that uses a variant of pi-calculus to check that one or more properties hold on a given specification.
Handling the complete specification of the protocol will be too complex for proverif, so we will model a high-level view of the handshakes and authentication. Authorization will not be modelled, as it can be though as integrated in authentication, and in general we will handle only cleartext communication.
As further checks, we will see how the handshakes behave after the private key is leaked, so that we can check the perfect forward secrecy property of the protocol, or the reaction to a rogue authentication server.
We want to check the resiliency of the handshake and grant their usage even in the future, when an handshake or an algorithm will be broken. For this, our model must include an explicitly broken algorithm, and the model must pass the verification when one of the two parties refuses to use the algorithm. This scenario must be considered to avoid ``downgrade attacks'', which have been exploited multiple times even in TLS (see CRIME.BREACH). These are attacks were a third party forces one or both parties to use older versions of the protocol, through timeouts or message modifications.
The security model that we will use is therefore:
\begin{itemize}
\item The attacker is the network. It can read, modify, inject, replay, block any content.
\item There already exist protocols and versions that are broken yet supported by at least one party.
\item symmetric or asymmetric cryptographic security is assumed to be safe.
\item public key algorithms must support signing and key exchange.
\item Master keys can be lost after the handshake and perfect forward secrecy holds \footnote{this will not be applied to the directory-synchronized handshake, as it is purposely built without such resilience in mind.}
All Fenrir handshakes are based on asymmetric encryption keys that can sign data and generate keys when paired with an other public key. This has been included in the design since some public key algorithms are not meant to be able to encrypt data, only sign it. Encryption is not common in asymmetric encryption, and it has some caveats in RSA, too, where if you blindly encrypt user provided data you can end up leaking the private key. To avoid such problems, Fenrir will only use signing mode and secret key generation on asymmetric algorithms.
For completeness, all three handshakes must be present concurrently in our model, so that interactions between them can be considered, even if this might mean more work for proverif.
Compared to TLS, Fenrir's rekeying is handled in-band and is a simple signed-key exchange that leads to a secret key generation. The problem with this in TLS was that a different, non-unique session id was generated from user-defined data, and that the rekeying was in cleartext. Fenrir's connection id is unique and tied to an encryption key, so there is no need for a second session-id, while the rekeying happens in-band, encrypted, so it is at least as secure as the connection.
For brevity of this chapter, the specifics of the Proverif model is attached in appendix \ref{Appendix}.
The proverif model consists of two files/proofs. The first is used to check if out rekeying and direct authentication \ref{Rogue proof}\index{Proof!Direct Authentication}\index{Direct Authentication!Proof} work like we have designed it in the case of a rogue (or compromised) authentication server. The second instead checks whether the handshakes \ref{Fenrir proof}, their interaction and the perfect forward secrecy are safe and can protect what they are supposed to protect.
The need for multiple models instead of a single, bigger one arises from the complexity of the verification of multiple properties.
This means however that the models need to test incompatible scenarios, so that we do not remake errors like forgetting to test session resumption and rekeying \cite{3Shake}.
There are also some other limitations imposed by proverif, like the inability to use the full XOR instruction. We thus include a simpler version of the xor instruction (commutativity, associativity are not considered). The implementation resembles the symmetric encryption one, and it would not be a good model if the objects being xored had any structure. However they actually are both random keys, so there is no way to distinguish any content. If this assumption is broken, a rogue authentication server might be able to recover the session keys shared between the client and service.
A limitation found in proverif was the lack of optimization. In the if-else branches, if the condition is based on a nonce which is used to model an enumeration, proverif will still try to work with all possible enumerations in the else branch, thus increasing complexity. This is quickly resolved by a second ``if'' in the ``else'' branch that captures only the else condition. The other lack of optimization is the handle of the ``phases", since increasing the number of phases will greatly increase the time spent on the proof, even if those phases are empty.
Since computation requires a lot of time, the handshake model will include two independent tests, in order to get results in a short time (but both can be run at the same time if time is of no concern). The two tests are independent, as one is aimed at testing the Perfect Forward Secrecy of the protocol, while the second one is aimed at the interaction of the different handshakes when working with the same key. This is necessary as the directory-synchronized handshake does not use a master key to implement PFS, so we can't leak its key and expect the secrets to remain such. Since we can not leak the key, we need to check again the interactions of the handshake with the same (non-leaked) key, to be sure that there is no interference.
\section{Requirements validation}
We defined our protocol, and proved it correct, but what requirement have we met, and what could not we meet?
\subsection{Transport requirements}
We managed to meet all transport requirements: we have \textbf{reliable} and \textbf{unreliable} delivery, in \textbf{unordered} or \textbf{ordered} fashion, and the user can get the data as a \textbf{bytestream} or as \textbf{datagrams}. The combination of unordered, unreliable, bytestream will not be supported, as the protocol fragments the data as it sees fit, meaning that the user would not be able to reconstruct the data. Unordered, unreliable datagram is supported, as the usecase is similar to UDP, except that a datagram can span multiple packets.
Thanks to the RaptorQ algorithm, we support both hard and soft unreliability.
Stream \textbf{multiplexing} is the very first thing we find in our protocol, and \textbf{multihoming} and \textbf{mobility} are supported, with the only caveat that the client must be able to prove that it owns the IP address used as source.
\textbf{Efficiency} is higher than TCP+TLS, as the header is quite short. We could have saved some bytes in the packet format, but that might have made parsing more difficult or at least will have misaligned the data, which might slightly increase parsing time on embedded CPUs.
\subsection{Security requirements}
Our protocol grant \textbf{secrecy} and \textbf{authenticity} of the transmitted data, and our \textbf{authentication} includes multiple levels of \textbf{authorizations}.
The \textbf{federated identity} is the core of our protocol, which introduces a trusted third party (the authentication server). Complete trust on the third party however is not required, as multiple shared secrets grants us unprecedented \textbf{robustness} against attacks at the infrastructure of our protocol. \textbf{Advanced authentication} features like multiple tokens, token scoping through the \textit{authentication lattice} and the decoupling of the application and service from their security grants us safety and increase the possible authentication scenarios, increasing the developers' possibilities while simplifying the application development.
As long as the implementation is able to deactivate the \textit{directory synchronized} and the \textit{stateful} handshakes, attacks like DoSes will be quickly mitigated, while amplification attacks have been avoided by design.
\subsection{Non functional requirements}
Contrary to the previous protocols, we do not limit ourselves to a single data delivery mechanism (e.g: reliable \& ordered), leaving the developer with full access to the combination of requirements of its application, be it multistream or unordered delivery. The only transport limitation so far is the lack of multicast support, which requires more analysis. The \textbf{flexibility} requirement is therefore almost completely satisfied.
Security-wise, the developers can now access multiple levels of authorizations, and do not need to require a local account for a service, without managing any security-related function.
\textbf{Interoperability} was the core design of our protocol, and the \textit{federated identity} combined with our \textit{token} usage is designed to grant this requirement. The only downside is a slightly longer connection setup time since not relying on clock synchronization forces us to use more round-trips to check the freshness of the tokens.
Finally, the whole protocol can be implemented in \textbf{user space}. This will let us update and increment the functionality of Fenrir without waiting for kernels to catch up, and lessen impact of security bugs (no privilege escalations). In the future, when the UDP tunnelling will not be required anymore, the Kernel side of the protocol will be a mere forward table, since the kernel only need to send a packet to the correct application in userspace after checking the only cleartext field, the connection id. The special case of connection id 0 (new connection) can still be handled with a second forward table associating a certain public key id with an application.