Skip to main content
main-content

Tipp

Weitere Kapitel dieses Buchs durch Wischen aufrufen

2020 | OriginalPaper | Buchkapitel

A Formal Security Analysis of the \(p\equiv p\) Authentication Protocol for Decentralized Key Distribution and End-to-End Encrypted Email

verfasst von: Itzel Vazquez Sandoval, Gabriele Lenzini

Erschienen in: Emerging Technologies for Authorization and Authentication

Verlag: Springer International Publishing

share
TEILEN

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 \(p\equiv p\) automates the key management operations; \(p\equiv p\) 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, \(p\equiv p\) ’s trust rating may be wrongly assigned, or both. To learn whether \(p\equiv p\) ’s trust ratings (and the corresponding visual indicators) are assigned consistently, we present a formal security analysis of \(p\equiv p\) ’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.
Literatur
4.
Zurück zum Zitat Abadi, M., Fournet, C.: Mobile values, new names, and secure communication. In: Acm Sigplan Notices, vol. 36, pp. 104–115. ACM (2001) Abadi, M., Fournet, C.: Mobile values, new names, and secure communication. In: Acm Sigplan Notices, vol. 36, pp. 104–115. ACM (2001)
6.
Zurück zum Zitat Basin, D., Cremers, C., Meier, S.: Provably repairing the ISO/IEC 9798 standard for entity authentication. J. Comput. Secur. 21(6), 817–846 (2013) MATHCrossRef Basin, D., Cremers, C., Meier, S.: Provably repairing the ISO/IEC 9798 standard for entity authentication. J. Comput. Secur. 21(6), 817–846 (2013) MATHCrossRef
7.
Zurück zum Zitat Basin, D., Dreier, J., Hirschi, L., Radomirovic, S., Sasse, R., Stettler, V.: A formal analysis of 5G authentication. In: Proceedings of the 2018 ACM SIGSAC Conference on Computer and Communications Security, pp. 1383–1396. ACM (2018) Basin, D., Dreier, J., Hirschi, L., Radomirovic, S., Sasse, R., Stettler, V.: A formal analysis of 5G authentication. In: Proceedings of the 2018 ACM SIGSAC Conference on Computer and Communications Security, pp. 1383–1396. ACM (2018)
8.
Zurück zum Zitat Basin, D., Radomirovic, S., Schmid, L.: Modeling human errors in security protocols. In: 2016 IEEE 29th Computer Security Foundations Symposium (CSF), pp. 325–340. IEEE (2016) Basin, D., Radomirovic, S., Schmid, L.: Modeling human errors in security protocols. In: 2016 IEEE 29th Computer Security Foundations Symposium (CSF), pp. 325–340. IEEE (2016)
9.
Zurück zum Zitat Blanchet, B.: An efficient cryptographic protocol verifier based on prolog rules. In: 14th IEEE Computer Security Foundations Workshop, pp. 82–96. IEEE (2001) Blanchet, B.: An efficient cryptographic protocol verifier based on prolog rules. In: 14th IEEE Computer Security Foundations Workshop, pp. 82–96. IEEE (2001)
12.
Zurück zum Zitat Cohn-Gordon, K., Cremers, C., Dowling, B., Garratt, L., Stebila, D.: A formal security analysis of the signal messaging protocol. In: 2017 IEEE European Symposium on Security and Privacy (EuroS&P), pp. 451–466. IEEE (2017) Cohn-Gordon, K., Cremers, C., Dowling, B., Garratt, L., Stebila, D.: A formal security analysis of the signal messaging protocol. In: 2017 IEEE European Symposium on Security and Privacy (EuroS&P), pp. 451–466. IEEE (2017)
14.
Zurück zum Zitat Dechand, S., Schürmann, D., Busse, K., Acar, Y., Fahl, S., Smith, M.: An empirical study of textual key-fingerprint representations. In: 25th \(\{\)USENIX \(\}\) Security Symposium ( \(\{\)USENIX \(\}\) Security 16), pp. 193–208 (2016) Dechand, S., Schürmann, D., Busse, K., Acar, Y., Fahl, S., Smith, M.: An empirical study of textual key-fingerprint representations. In: 25th \(\{\)USENIX \(\}\) Security Symposium ( \(\{\)USENIX \(\}\) Security 16), pp. 193–208 (2016)
15.
Zurück zum Zitat Dolev, D., Yao, A.C.: On the security of public key protocols. In: Proceedings of the 22nd Annual Symposium on Foundations of Computer Science, SFCS 1981, pp. 350–357. IEEE Computer Society, Washington, DC (1981) Dolev, D., Yao, A.C.: On the security of public key protocols. In: Proceedings of the 22nd Annual Symposium on Foundations of Computer Science, SFCS 1981, pp. 350–357. IEEE Computer Society, Washington, DC (1981)
16.
Zurück zum Zitat Dreier, J., Hirschi, L., Radomirovic, S., Sasse, R.: Automated unbounded verification of stateful cryptographic protocols with exclusive OR. In: 2018 IEEE 31st Computer Security Foundations Symposium (CSF), pp. 359–373. IEEE (2018) Dreier, J., Hirschi, L., Radomirovic, S., Sasse, R.: Automated unbounded verification of stateful cryptographic protocols with exclusive OR. In: 2018 IEEE 31st Computer Security Foundations Symposium (CSF), pp. 359–373. IEEE (2018)
20.
Zurück zum Zitat Lowe, G.: A hierarchy of authentication specifications. In: Proceedings 10th Computer Security Foundations Workshop, pp. 31–43. IEEE (1997) Lowe, G.: A hierarchy of authentication specifications. In: Proceedings 10th Computer Security Foundations Workshop, pp. 31–43. IEEE (1997)
21.
Zurück zum Zitat Mauw, S., Cremers, C.: Operational Semantics and Verification of Security Protocols. Springer, Heidelberg (2012) MATH Mauw, S., Cremers, C.: Operational Semantics and Verification of Security Protocols. Springer, Heidelberg (2012) MATH
24.
Zurück zum Zitat The Radicati Group: Email Statistics Report, 2018–2022. Technical report (2018) The Radicati Group: Email Statistics Report, 2018–2022. Technical report (2018)
25.
Zurück zum Zitat Unger, N., et al.: SoK: secure messaging. In: 2015 IEEE Symposium on Security and Privacy, pp. 232–249. IEEE (2015) Unger, N., et al.: SoK: secure messaging. In: 2015 IEEE Symposium on Security and Privacy, pp. 232–249. IEEE (2015)
26.
Zurück zum Zitat Vazquez-Sandoval, I., Lenzini, G.: Experience report: how to extract security protocols’ specifications from C libraries. In: IEEE 42nd Annual COMPSAC 2018, Tokyo, Japan, Vol. 2, pp. 719–724 (2018) Vazquez-Sandoval, I., Lenzini, G.: Experience report: how to extract security protocols’ specifications from C libraries. In: IEEE 42nd Annual COMPSAC 2018, Tokyo, Japan, Vol. 2, pp. 719–724 (2018)
27.
Zurück zum Zitat Whitten, A., Tygar, J.D.: Why Johnny can’t encrypt: a usability evaluation of PGP 5.0. In: USENIX Security Symposium, vol. 348 (1999) Whitten, A., Tygar, J.D.: Why Johnny can’t encrypt: a usability evaluation of PGP 5.0. In: USENIX Security Symposium, vol. 348 (1999)
28.
Zurück zum Zitat Zimmermann, P.R.: The Official PGP User’s Guide. MIT Press, Cambridge (1995) Zimmermann, P.R.: The Official PGP User’s Guide. MIT Press, Cambridge (1995)
Metadaten
Titel
A Formal Security Analysis of the Authentication Protocol for Decentralized Key Distribution and End-to-End Encrypted Email
verfasst von
Itzel Vazquez Sandoval
Gabriele Lenzini
Copyright-Jahr
2020
DOI
https://doi.org/10.1007/978-3-030-39749-4_11

Premium Partner