Tamarin Prover

Last updated
Tamarin Prover
Original author(s) David Basin, Cas Cremers, Jannik Dreier, Simon Meier, Ralf Sasse, Benedikt Schmidt
Developer(s) Cas Cremers, Jannik Dreier, Ralf Sasse
Initial releaseApril 24, 2012 (2012-04-24)
Stable release
1.4.1 / January 18, 2019 (2019-01-18)
Repository github.com/tamarin-prover/tamarin-prover
Written in Haskell
Operating system Linux, macOS
Available inEnglish
Type Automated reasoning
License GNU GPL v3
Website tamarin-prover.github.io

Tamarin Prover is a computer software program for formal verification of cryptographic protocols. It has been used to verify Transport Layer Security 1.3, [1] ISO/IEC 9798, [2] DNP3 Secure Authentication v5, [3] and WireGuard. [4] [5] [6] [7]

Related Research Articles

In computing, Internet Protocol Security (IPsec) is a secure network protocol suite that authenticates and encrypts packets of data to provide secure encrypted communication between two computers over an Internet Protocol network. It is used in virtual private networks (VPNs).

A cryptographic protocol is an abstract or concrete protocol that performs a security-related function and applies cryptographic methods, often as sequences of cryptographic primitives. A protocol describes how the algorithms should be used and includes details about data structures and representations, at which point it can be used to implement multiple, interoperable versions of a program.

In cryptography, a zero-knowledge password proof (ZKPP) is a type of zero-knowledge proof that allows one party to prove to another party that it knows a value of a password, without revealing anything other than the fact that it knows the password to the verifier. The term is defined in IEEE P1363.2, in reference to one of the benefits of using a password-authenticated key exchange (PAKE) protocol that is secure against off-line dictionary attacks. A ZKPP prevents any party from verifying guesses for the password without interacting with a party that knows it and, in the optimal case, provides exactly one guess in each interaction.

In cryptography, a password-authenticated key agreement method is an interactive method for two or more parties to establish cryptographic keys based on one or more party's knowledge of a password.

SPEKE is a cryptographic method for password-authenticated key agreement.

In cryptography, forward secrecy (FS), also known as perfect forward secrecy (PFS), is a feature of specific key-agreement protocols that gives assurances that session keys will not be compromised even if long-term secrets used in the session key exchange are compromised. For HTTPS, the long-term secret is typically the private key of the server. Forward secrecy protects past sessions against future compromises of keys or passwords. By generating a unique session key for every session a user initiates, the compromise of a single session key will not affect any data other than that exchanged in the specific session protected by that particular key. This by itself is not sufficient for forward secrecy which additionally requires that a long-term secret compromise does not affect the security of past session keys.

In public-key cryptography, the Station-to-Station (STS) protocol is a cryptographic key agreement scheme. The protocol is based on classic Diffie–Hellman, and provides mutual key and entity authentication. Unlike the classic Diffie–Hellman, which is not secure against a man-in-the-middle attack, this protocol assumes that the parties have signature keys, which are used to sign messages, thereby providing security against man-in-the-middle attacks.

<span class="mw-page-title-main">DNP3</span> Computer network protocol

Distributed Network Protocol 3 (DNP3) is a set of communications protocols used between components in process automation systems. Its main use is in utilities such as electric and water companies. Usage in other industries is not common. It was developed for communications between various types of data acquisition and control equipment. It plays a crucial role in SCADA systems, where it is used by SCADA Master Stations, Remote Terminal Units (RTUs), and Intelligent Electronic Devices (IEDs). It is primarily used for communications between a master station and RTUs or IEDs. ICCP, the Inter-Control Center Communications Protocol, is used for inter-master station communications. Competing standards include the older Modbus protocol and the newer IEC 61850 protocol.

Non-interactive zero-knowledge proofs are cryptographic primitives, where information between a prover and a verifier can be authenticated by the prover, without revealing any of the specific information beyond the validity of the statement itself. This function of encryption makes direct communication between the prover and verifier unnecessary, effectively removing any intermediaries. The core trustless cryptography "proofing" involves a hash function generation of a random number, constrained within mathematical parameters determined by the prover and verifier.

Virgil Dorin Gligor is a Romanian-American professor of electrical and computer engineering who specializes in the research of network security and applied cryptography.

<span class="mw-page-title-main">Crypto-1</span> Stream cipher

Crypto1 is a proprietary encryption algorithm and authentication protocol created by NXP Semiconductors for its MIFARE Classic RFID contactless smart cards launched in 1994. Such cards have been used in many notable systems, including Oyster card, CharlieCard and OV-chipkaart.

Protocol Composition Logic is a formal method that is used for proving security properties of protocols that use symmetric key and Public key cryptography. PCL is designed around a process calculi with actions for possible protocol steps like generating some random number, perform encryption and decryption, send and receive messages and digital signature verification actions.

ProVerif is a software tool for automated reasoning about the security properties found in cryptographic protocols. The tool has been developed by Bruno Blanchet.

<span class="mw-page-title-main">Moti Yung</span> Israeli computer scientist

Mordechai M. "Moti" Yung is a cryptographer and computer scientist known for his work on cryptovirology and kleptography.

Casimier Joseph Franciscus "Cas" Cremers is a computer scientist and a faculty member at the CISPA Helmholtz Center for Information Security in Saarbruecken, Germany.

In cryptography, the Double Ratchet Algorithm is a key management algorithm that was developed by Trevor Perrin and Moxie Marlinspike in 2013. It can be used as part of a cryptographic protocol to provide end-to-end encryption for instant messaging. After an initial key exchange it manages the ongoing renewal and maintenance of short-lived session keys. It combines a cryptographic so-called "ratchet" based on the Diffie–Hellman key exchange (DH) and a ratchet based on a key derivation function (KDF), such as a hash function, and is therefore called a double ratchet.

The Signal Protocol is a non-federated cryptographic protocol that provides end-to-end encryption for voice and instant messaging conversations. The protocol was developed by Open Whisper Systems in 2013 and was first introduced in the open-source TextSecure app, which later became Signal. Several closed-source applications have implemented the protocol, such as WhatsApp, which is said to encrypt the conversations of "more than a billion people worldwide" or Google who provides end-to-end encryption by default to all RCS-based conversations between users of their Google Messages app for one-to-one conversations. Facebook Messenger also say they offer the protocol for optional Secret Conversations, as does Skype for its Private Conversations.

Gavin Lowe is a British academic. He is a professor of computer science and tutorial fellow at St Catherine's College, Oxford, a professor at the University of Oxford, and President of the Senior Common Room of St Catherine's College, Oxford. His research interests include computer security, for which he developed the cryptographic protocol analysis tool Casper, and concurrency.

Adrian Perrig is a Swiss computer science researcher and professor at ETH Zurich, leading the Network Security research group. His research focuses on networking and systems security, and specifically on the design of a secure next-generation internet architecture.

In computer science, choreographic programming is a programming paradigm where programs are compositions of interactions among multiple concurrent participants.

References

  1. Cremers, Cas; Horvat, Marko; Scott, Sam; van der Merwe, Thyla (2016). "Automated Analysis and Verification of TLS 1.3: 0-RTT, Resumption and Delayed Authentication". IEEE Symposium on Security and Privacy, 2016, San Jose, CA, USA, May 22-26, 2016. IEEE S&P 2016. pp. 470–485. doi:10.1109/SP.2016.35. ISBN   978-1-5090-0824-7.
  2. Basin, David; Cremers, Cas; Meier, Simon (2013). "Provably repairing the ISO/IEC 9798 standard for entity authentication" (PDF). Journal of Computer Security. 21 (6): 817–846. doi:10.3233/JCS-130472.
  3. Cremers, Cas; Dehnel-Wild, Martin; Milner, Kevin (2017). "Secure Authentication in the Grid: A Formal Analysis of DNP3: SAv5" (PDF). Computer Security - ESORICS 2017 - 22nd European Symposium on Research in Computer Security, Oslo, Norway, September 11-15, 2017, Proceedings, Part I. ESORICS 2017. Oslo, Norway: Springer. pp. 389–407. doi:10.1007/978-3-319-66402-6_23. ISBN   978-3-319-66401-9.
  4. Donenfeld, Jason A.; Milne, Kevin (2018), Formal Verification of the WireGuard Protocol (PDF), archived (PDF) from the original on 2023-05-28, retrieved 2023-11-23; Donenfeld, Jason A., Formal Verification, archived from the original on 2023-11-13, retrieved 2023-11-23
  5. Schmidt, Benedikt; Meier, Simon; Cremers, Cas; Basin, David (2012). "Automated analysis of Diffie-Hellman protocols and advanced security properties" (PDF). 25th IEEE Computer Security Foundations Symposium, CSF 2012, Cambridge, MA, USA, June 25-27, 2012. CSF 2012. Cambridge, MA: IEEE Computer Society. pp. 78–94.
  6. Schmidt, Benedikt (2012). Formal analysis of key exchange protocols and physical protocols (PhD thesis). doi:10.3929/ethz-a-009898924.
  7. Meier, Simon (2012). Advancing automated security protocol verification (PhD thesis). doi:10.3929/ethz-a-009790675.