Tamarin Prover is a
computer software
Software consists of computer programs that instruct the Execution (computing), execution of a computer. Software also includes design documents and specifications.
The history of software is closely tied to the development of digital comput ...
program for
formal verification
In the context of hardware and software systems, formal verification is the act of proving or disproving the correctness of a system with respect to a certain formal specification or property, using formal methods of mathematics.
Formal ver ...
of
cryptographic protocol
A cryptographic protocol is an abstract or concrete Communications protocol, protocol that performs a information security, security-related function and applies cryptographic methods, often as sequences of cryptographic primitives. A protocol desc ...
s. It has been used to verify
Transport Layer Security
Transport Layer Security (TLS) is a cryptographic protocol designed to provide communications security over a computer network, such as the Internet. The protocol is widely used in applications such as email, instant messaging, and voice over ...
1.3,
ISO/IEC 9798,
Secure Authentication v5,
,
[; ] and the PQ3 Messaging Protocol of
Apple
An apple is a round, edible fruit produced by an apple tree (''Malus'' spp.). Fruit trees of the orchard or domestic apple (''Malus domestica''), the most widely grown in the genus, are agriculture, cultivated worldwide. The tree originated ...
iMessage
iMessage is an instant messaging service developed by Apple Inc. and launched in 2011. iMessage functions exclusively on Apple platforms – including iOS, iPadOS, macOS, watchOS, and visionOS – as part of Apple ecosystem, Apple's approach t ...
.
Tamarin is an open source tool, written in
Haskell
Haskell () is a general-purpose, statically typed, purely functional programming language with type inference and lazy evaluation. Designed for teaching, research, and industrial applications, Haskell pioneered several programming language ...
,
built as a successor to an older verification tool called Scyther.
[ Colin Boyd, Anish Mathuria, Douglas Stebila. "Protocols for Authentication and Key Establishment", Second Edition Springer, 2019. pg 48] Tamarin has automatic proof features, but can also be self-guided.
In Tamarin ''lemmas'' that representing security properties are defined.
[Celi, Sofía, Jonathan Hoyland, Douglas Stebila, and Thom Wiggers. "A tale of two models: Formal verification of KEMTLS via Tamarin." In European Symposium on Research in Computer Security, pp. 63-83. Cham: Springer Nature Switzerland, 2022.] After changes are made to a protocol, Tamarin can verify if the security properties are maintained.
The results of a Tamarin execution will either be a proof that the security property holds within the protocol, an example protocol run where the security property does not hold, or Tamarin could potentially
fail to halt.
[P. Remlein, M. Rogacki and U. Stachowiak, "Tamarin software – the tool for protocols verification security," 2020 Baltic URSI Symposium (URSI), Warsaw, Poland, 2020, pp. 118-123, doi: 10.23919/URSI48707.2020.9254078.]
See also
*
Dolev–Yao model
The Dolev–Yao model, named after its authors Danny Dolev and Andrew Yao, is a formal model used to prove properties of interactive cryptographic protocols.
The network
The network is represented by a set of abstract machines that can excha ...
*
Hybrid argument
References
{{reflist
External links
Tamarin Prover official website* David Wong create
an introductory video on the Tamarin Prover
Cryptographic software
Free software programmed in Haskell
Software using the GNU General Public License
Automated reasoning