Original author(s) | David Basin, Cas Cremers, Jannik Dreier, Simon Meier, Ralf Sasse, Benedikt Schmidt |
---|---|
Developer(s) | Cas Cremers, Jannik Dreier, Ralf Sasse |
Initial release | April 24, 2012 |
Stable release | 1.4.1 / January 18, 2019 |
Repository | github |
Written in | Haskell |
Operating system | Linux, macOS |
Available in | English |
Type | Automated reasoning |
License | GNU GPL v3 |
Website | tamarin-prover |
Tamarin Prover is a computer software program for formal verification of cryptographic protocols. [1] It has been used to verify Transport Layer Security 1.3, [2] ISO/IEC 9798, [3] DNP3 Secure Authentication v5, [4] WireGuard, [5] [6] [7] [8] and the PQ3 Messaging Protocol of Apple iMessage. [9]
Tamarin is an open source tool, written in Haskell, [10] built as a successor to an older verification tool called Scyther. [11] Tamarin has automatic proof features, but can also be self-guided. [11] In Tamarin lemmas that representing security properties are defined. [12] After changes are made to a protocol, Tamarin can verify if the security properties are maintained. [12] 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. [12] [10]
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 digital signature is a mathematical scheme for verifying the authenticity of digital messages or documents. A valid digital signature on a message gives a recipient confidence that the message came from a sender known to the recipient.
In cryptography, a key-agreement protocol is a protocol whereby two parties generate a cryptographic key as a function of information provided by each honest party so that no party can predetermine the resulting value. In particular, all honest participants influence the outcome. A key-agreement protocol is a specialisation of a key-exchange protocol.
Wi-Fi Protected Access (WPA), Wi-Fi Protected Access 2 (WPA2), and Wi-Fi Protected Access 3 (WPA3) are the three security certification programs developed after 2000 by the Wi-Fi Alliance to secure wireless computer networks. The Alliance defined these in response to serious weaknesses researchers had found in the previous system, Wired Equivalent Privacy (WEP).
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 password-authenticated key agreement (PAK) method is an interactive method for two or more parties to establish cryptographic keys based on one or more parties' knowledge of a password.
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, limiting damage. 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.
Virgil Dorin Gligor is a Romanian-American professor of electrical and computer engineering who specializes in the research of network security and applied cryptography.
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 can be used for proving security properties of cryptographic protocols that use symmetric-key and public-key cryptography. PCL is designed around a process calculus with actions for various possible protocol steps.
ProVerif is a software tool for automated reasoning about the security properties of cryptographic protocols. The tool has been developed by Bruno Blanchet and others.
Post-quantum cryptography (PQC), sometimes referred to as quantum-proof, quantum-safe, or quantum-resistant, is the development of cryptographic algorithms that are currently thought to be secure against a cryptanalytic attack by a quantum computer. Most widely-used public-key algorithms rely on the difficulty of one of three mathematical problems: the integer factorization problem, the discrete logarithm problem or the elliptic-curve discrete logarithm problem. All of these problems could be easily solved on a sufficiently powerful quantum computer running Shor's algorithm or even faster and less demanding alternatives.
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 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.
Messaging Layer Security (MLS) is a security layer for end-to-end encrypting messages. It is maintained by the MLS working group of the Internet Engineering Task Force, and is designed to provide an efficient and practical security mechanism for groups as large as 50,000 and for those who access chat systems from multiple devices.
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.
Automotive security refers to the branch of computer security focused on the cyber risks related to the automotive context. The increasingly high number of ECUs in vehicles and, alongside, the implementation of multiple different means of communication from and towards the vehicle in a remote and wireless manner led to the necessity of a branch of cybersecurity dedicated to the threats associated with vehicles. Not to be confused with automotive safety.
In computer science, choreographic programming is a programming paradigm where programs are compositions of interactions among multiple concurrent participants.