Formal security analysis of authentication in an asynchronous communication model

Abstract: Formal analysis of security protocols is becoming increasingly relevant. In formal analysis, a model is created of a protocol or system, and propositions about the security of the model are written. A program is then used to verify that the propositions hold, or find examples of where they do not. This report uses formal methods to analyse the authentication aspect of a protocol that allows private individuals, enterprises, and systems to securely and asynchronously share sensitive data. Unpublished, early drafts of the protocol were studied and algorithms described in it were verified with the help of the formal verification tool Tamarin Prover. The analysis revealed two replay attacks. Improvements to the protocol were suggested based on this analysis. In later versions of the protocol, the improvements have been implemented by the protocol developers.