| Reference : A multifaceted formal analysis of end-to-end encrypted email protocols and cryptograp... |
| Dissertations and theses : Doctoral thesis | |||
| Engineering, computing & technology : Computer science | |||
| Security, Reliability and Trust | |||
| http://hdl.handle.net/10993/44819 | |||
| A multifaceted formal analysis of end-to-end encrypted email protocols and cryptographic authentication enhancements | |
| English | |
Vazquez Sandoval, Itzel  [University of Luxembourg > Interdisciplinary Centre for Security, Reliability and Trust (SNT) > IRiSC >] | |
| 3-Nov-2020 | |
| University of Luxembourg, Esch-sur-Alzette, Luxemburgo | |
| Docteur en Informatique | |
| Lenzini, Gabriele | |
| Ryan, Peter Y A | |
| Viganò, Luca | |
| Lafourcade, Pascal | |
| Martinelli, Fabio | |
| [en] secure email ; end-to-end encryption ; formal verification ; cryptographic protocols ; symbolic models ; private email ; authentication ; reverse engineering ; socio-technical formal analysis | |
| [en] Largely owing to cryptography, modern messaging tools (e.g., Signal) have reached a considerable degree of sophistication, balancing advanced security features with high usability. This has not been the case for email, which however, remains the most pervasive and interoperable form of digital communication. As sensitive information (e.g., identification documents, bank statements, or the message in the email itself) is frequently exchanged by this means, protecting the privacy of email communications is a justified concern which has been emphasized in the last years.
A great deal of effort has gone into the development of tools and techniques for providing email communications with privacy and security, requirements that were not originally considered. Yet, drawbacks across several dimensions hinder the development of a global solution that would strengthen security while maintaining the standard features that we expect from email clients. In this thesis, we present improvements to security in email communications. Relying on formal methods and cryptography, we design and assess security protocols and analysis techniques, and propose enhancements to implemented approaches for end-to-end secure email communication. In the first part, we propose a methodical process relying on code reverse engineering, which we use to abstract the specifications of two end-to-end security protocols from a secure email solution (called pEp); then, we apply symbolic verification techniques to analyze such protocols with respect to privacy and authentication properties. We also introduce a novel formal framework that enables a system's security analysis aimed at detecting flaws caused by possible discrepancies between the user's and the system's assessment of security. Security protocols, along with user perceptions and interaction traces, are modeled as transition systems; socio-technical security properties are defined as formulas in computation tree logic (CTL), which can then be verified by model checking. Finally, we propose a protocol that aims at securing a password-based authentication system designed to detect the leakage of a password database, from a code-corruption attack. In the second part, the insights gained by the analysis in Part I allow us to propose both, theoretical and practical solutions for improving security and usability aspects, primarily of email communication, but from which secure messaging solutions can benefit too. The first enhancement concerns the use of password-authenticated key exchange (PAKE) protocols for entity authentication in peer-to-peer decentralized settings, as a replacement for out-of-band channels; this brings provable security to the so far empirical process, and enables the implementation of further security and usability properties (e.g., forward secrecy, secure secret retrieval). A second idea refers to the protection of weak passwords at rest and in transit, for which we propose a scheme based on the use of a one-time-password; furthermore, we consider potential approaches for improving this scheme. The hereby presented research was conducted as part of an industrial partnership between SnT/University of Luxembourg and pEp Security S.A. | |
| Interdisciplinary Centre for Security, Reliability and Trust (SnT) | |
| pEp Security S.A. | |
| Researchers ; Professionals ; Students | |
| http://hdl.handle.net/10993/44819 |
| File(s) associated to this reference | ||||||||||||||
|
Fulltext file(s):
| ||||||||||||||
All documents in ORBilu are protected by a user license.
