Visible to the public Verifying cryptographic protocols by Tamarin Prover

TitleVerifying cryptographic protocols by Tamarin Prover
Publication TypeConference Paper
Year of Publication2020
AuthorsVinarskii, Evgenii, Demakov, Alexey, Kamkin, Alexander, Yevtushenko, Nina
Conference Name2020 Ivannikov Memorial Workshop (IVMEM)
KeywordsComplexity theory, composability, compositionality, Computational modeling, cryptographic protocols, cryptography, formal specifications, Planing, policy-based governance, privacy, protocol verification, pubcrawl, security, Session key secrecy, Tamarin prover, Verification of cryptographic protocols
AbstractCryptographic protocols are utilized for establishing a secure session between "honest" agents which communicate strictly according to the protocol rules as well as for ensuring the authenticated and confidential transmission of messages. The specification of a cryptographic protocol is usually presented as a set of requirements for the sequences of transmitted messages including the format of such messages. Note that protocol can describe several execution scenarios. All these requirements lead to a huge formal specification for a real cryptographic protocol and therefore, it is difficult to verify the security of the whole cryptographic protocol at once. In this paper, to overcome this problem, we suggest verifying the protocol security for its fragments. Namely, we verify the security properties for a special set of so-called traces of the cryptographic protocol. Intuitively, a trace of the cryptographic protocol is a sequence of computations, value checks, and transmissions on the sides of "honest" agents permitted by the protocol. In order to choose such set of traces, we introduce an Adversary model and the notion of a similarity relation for traces. We then verify the security properties of selected traces with Tamarin Prover. Experimental results for the EAP and Noise protocols clearly show that this approach can be promising for automatic verification of large protocols.
Citation Keyvinarskii_verifying_2020