Our Methodology
Protocol analysis can be done at several levels, and using various tools. We choose in particular to use the following methodologies.
Provable Security
The security-by-design paradigm aims to provide schemes that are secure against generic attacks, as opposed to protocols that resist attacks known up to that point. This paradigm allows experts to prove cryptographic schemes secure before they are deployed in real-world applications.
The greatest strength of provable security is its ability to guarantee security against arbitrary attacks within a generic adversarial category. This includes both existing and future attacks.
However, one of the main limitations of provable security is that a security proof is only as accurate as the model in which it is given. There is a clear tradeoff between the accuracy of the model and the complexity of the proof; to make proofs possible, many details of the system and the adversary�s interactions are abstracted away. Consequently, protocols that are proved secure may still have flaws, as was the case of TLS 1.2.
The existence of these attacks does not contradict the security proof; they simply fall outside the security model. On the other hand, an overly-strong security model usually leads to either impossibility proofs (i.e. a proof tht the desired security notion is unattainable) or to a lack of a proof � which may mean the protocol is insecure, or it may mean that no proof can be formalized.
Provable security remains to date one of the strongest tools permitting sound protocol design for real-world applications. We use this approach too, mitigating some of its deficiencies by using either automated verification or cryptanalysis (see below).
Automated Proofs
A promising solution to the shortcomings of provable security is to use the automated verification of cryptographic systems. Although many such frameworks exist for the symbolic model of cryptography, comparatively little work has been done to develop machine-checked frameworks to reason directly in the computational model commonly used by cryptographers.
Throughout the last decades several tools for automated verification have been designed, e.g., Proverif, Tamarin, Sapiq+, etc. Each tool has its own approach to verifying cryptographic protocols, and they leverage the significant computational power of a computer to run much larger-scales analyses than could be done by hand. Such tools can be used to find flaws in cryptographic designs, but also to prove them secure. An aspect we take into account is the large-scale analysis of both users and data. Depending on the protocols we will design throughout this project, the most appropriate automated-verification tool will be deployed towards obtaining a formal proof of their security. We will also use such tools to find any existing flaws in current designs, or identifying weak spots in the complex 5G infrastructure.
Finally, note that, while a formal security proof can provide reasonable confidence in the deployment of specific cryptographic primitives and protocols, such proofs only confirm the soundness of the protocol design, and not also the implementations. In this project, we will build high-assurance implementations of cryptographic constructions and protocols in a safe subset of the Rust programming language and using tools like F* to formally verify their correctness and security. Our goal will be, on the one hand, to provide high-assurance implementations of the protocols we propose, for the use of the entire cryptographic community, and on the other hand, to provide auditing and testing tools for implementations in order to reveal potential flaws.
Cryptanalysis
Security proofs -- whether automated or computational -- can provide generic and formal guarnatees regarding the properties of cryptographic primitives and protocols. However, two of their main limitations are: the inability to take into account all the details of real-world attacks; and the necessity of basing the proof on some assumptions regarding the security of underlying primitives. Indeed, some primitives, such as hash functions and block- and stream-ciphers, can only be provided with limited security proofs. Consequently the security both of those primitives themselves and all cryptographic countermeasures using them rely on an assumption, rather than a proof of their security. The validity of such assumptions cannot currently be proved; instead we validate such assumptions by subjecting these primitives to extensive cryptanalysis. In other words, one tries to find ways to attack such cryptographic algorithms by exploiting their underlying structure.
We want to study the security of real-world privacy-preserving protocols, such as OTR, Olvid, WireGuard, etc. and, by understanding the security and privacy guarantees that they provide, improve them.