A Formal Security Analysis of the pEp Authentication Protocol for Decentralized Key Distribution and End-to-End Encrypted Email

TL;DR

This paper provides a formal security analysis of the pEp email encryption protocol, verifying its trust establishment process and highlighting potential issues in user authentication and trust ratings.

Contribution

It introduces a formal model of pEp's authentication protocol and verifies its privacy and authentication properties using formal methods.

Findings

pEp's trust ratings can be inconsistently assigned

The formal model reveals potential vulnerabilities in user verification

Verification confirms certain privacy and authentication guarantees

Abstract

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.