Reference : A Formal Security Analysis of the pEp Authentication Protocol for Decentralized Key D...
Scientific congresses, symposiums and conference proceedings : Paper published in a book
Engineering, computing & technology : Computer science
Security, Reliability and Trust
http://hdl.handle.net/10993/40580
A Formal Security Analysis of the pEp Authentication Protocol for Decentralized Key Distribution and End-to-End Encrypted Email
English
Vazquez Sandoval, Itzel mailto [University of Luxembourg > Interdisciplinary Centre for Security, Reliability and Trust (SNT) > >]
Lenzini, Gabriele mailto [University of Luxembourg > Interdisciplinary Centre for Security, Reliability and Trust (SNT) > >]
2019
Emerging Technologies for Authorization and Authentication
Springer
Yes
International
2nd International Workshop on Emerging Technologies for Authorization and Authentication - ESORICS International Workshops
27-09-2019
Luxembourg
Luxembourg
[en] formal verification ; authentication protocols ; software security analysis ; privacy-by-default ; secure email ; end-to-end encryption
[en] To send encrypted emails, users typically need to create and exchange keys which later should be manually authenticated, for instance, by comparing long strings of characters. These tasks are cumbersome for the average user. To make more accessible the use of encrypted email, a secure email application named pEp automates the key management operations; pEp still requires the users to carry out the verification, however, the authentication process is simple: users have to compare familiar words instead of strings of random characters, then the application shows the users what level of trust they have achieved via colored visual indicators. Yet, users may not execute the authentication ceremony as intended, pEp's trust rating may be wrongly assigned, or both. To learn whether pEp's trust ratings (and the corresponding visual indicators) are assigned consistently, we present a formal security analysis of pEp's authentication ceremony. From the software implementation in C, we derive the specifications of an abstract protocol for public key distribution, encryption and trust establishment; then, we model the protocol in a variant of the applied pi calculus and later formally verify and validate specific privacy and authentication properties. We also discuss alternative research directions that could enrich the analysis.
http://hdl.handle.net/10993/40580

File(s) associated to this reference

Fulltext file(s):

FileCommentaryVersionSizeAccess
Open access
14.pdfAuthor postprint710.09 kBView/Open

Bookmark and Share SFX Query

All documents in ORBilu are protected by a user license.