论文标题
对分散密钥分布和端到端加密电子邮件的PEP身份验证协议的正式安全分析
A Formal Security Analysis of the pEp Authentication Protocol for Decentralized Key Distribution and End-to-End Encrypted Email
论文作者
论文摘要
要发送加密的电子邮件，用户通常需要创建和交换密钥，以后应通过比较长字符串来手动身份验证。对于普通用户来说，这些任务很麻烦。为了使使用加密电子邮件更容易访问，名为PEP的安全电子邮件应用程序可自动使用密钥管理操作； PEP仍然要求用户执行验证，但是，身份验证过程很简单：用户必须比较熟悉的单词而不是随机字符的字符串，然后应用程序显示了用户通过彩色视觉指示器所达到的信任程度。但是，用户可能无法按预期执行身份验证仪式，PEP的信任评级可能是错误的，也可能是两者兼而有之。要了解PEP的信任评级（以及相应的视觉指标）是否始终如一地分配，我们对PEP的身份验证仪式进行了正式的安全分析。从C中的软件实施中，我们得出了用于公共密钥分布，加密和信任建立的摘要协议的规格；然后，我们将协议对应用PI微积分的变体进行建模，然后正式验证并验证特定的隐私和身份验证属性。我们还讨论可以丰富分析的替代研究方向。
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.
