 | This article has multiple issues. Please help improve it or discuss these issues on the talk page . (Learn how and when to remove these template messages)
|
| Initial release | 2005 |
|---|---|
| Stable release | 1.21 / September 3, 2015 |
| Written in | OCaml |
| Available in | English |
| License | Mainly the GNU GPL / Windows binary BSD licenses |
| Website | prosecco |
CryptoVerif is a software tool for the automatic reasoning about security protocols written by Bruno Blanchet. [1]
It provides a mechanism for specifying the security assumptions on cryptographic primitives, which can handle in particular
CryptoVerif claims to evaluate the probability of a successful attack against a protocol relative to the probability of breaking each cryptographic primitive, i.e. it can establish concrete security.
Articles related to cryptography include:
In cryptography, a random oracle is an oracle that responds to every unique query with a (truly) random response chosen uniformly from its output domain. If a query is repeated, it responds the same way every time that query is submitted.
In cryptography, an oblivious transfer (OT) protocol is a type of protocol in which a sender transfers one of potentially many pieces of information to a receiver, but remains oblivious as to what piece has been transferred.
A security 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.
Secure multi-party computation is a subfield of cryptography with the goal of creating methods for parties to jointly compute a function over their inputs while keeping those inputs private. Unlike traditional cryptographic tasks, where cryptography assures security and integrity of communication or storage and the adversary is outside the system of participants, the cryptography in this model protects participants' privacy from each other.
CCM mode is a mode of operation for cryptographic block ciphers. It is an authenticated encryption algorithm designed to provide both authentication and confidentiality. CCM mode is only defined for block ciphers with a block length of 128 bits.
In cryptography, a security parameter is a way of measuring of how "hard" it is for an adversary to break a cryptographic scheme. There are two main types of security parameter: computational and statistical, often denoted by and , respectively. Roughly speaking, the computational security parameter is a measure for the input size of the computational problem on which the cryptographic scheme is based, which determines its computational complexity, whereas the statistical security parameter is a measure of the probability with which an adversary can break the scheme.
EAX mode (encrypt-then-authenticate-then-translate) is a mode of operation for cryptographic block ciphers. It is an Authenticated Encryption with Associated Data (AEAD) algorithm designed to simultaneously provide both authentication and privacy of the message with a two-pass scheme, one pass for achieving privacy and one for authenticity for each block.
Cryptographic primitives are well-established, low-level cryptographic algorithms that are frequently used to build cryptographic protocols for computer security systems. These routines include, but are not limited to, one-way hash functions and encryption functions.
In cryptography, key wrap constructions are a class of symmetric encryption algorithms designed to encapsulate (encrypt) cryptographic key material. The Key Wrap algorithms are intended for applications such as protecting keys while in untrusted storage or transmitting keys over untrusted communications networks. The constructions are typically built from standard primitives such as block ciphers and cryptographic hash functions.
Strong secrecy is a term used in formal proof-based cryptography for making propositions about the security of cryptographic protocols. It is a stronger notion of security than syntactic secrecy. Strong secrecy is related with the concept of semantic security or indistinguishability used in the computational proof-based approach. Bruno Blanchet provides the following definition for strong secrecy:
Cryptography, or cryptology, is the practice and study of techniques for secure communication in the presence of adversarial behavior. More generally, cryptography is about constructing and analyzing protocols that prevent third parties or the public from reading private messages. Modern cryptography exists at the intersection of the disciplines of mathematics, computer science, information security, electrical engineering, digital signal processing, physics, and others. Core concepts related to information security are also central to cryptography. Practical applications of cryptography include electronic commerce, chip-based payment cards, digital currencies, computer passwords, and military communications.
There are various implementations of the Advanced Encryption Standard, also known as Rijndael.
ProVerif is a software tool for automated reasoning about the security properties found in cryptographic protocols. The tool has been developed by Bruno Blanchet.
Mordechai M. "Moti" Yung is a cryptographer and computer scientist known for his work on cryptovirology and kleptography.
The Signal Protocol is a non-federated cryptographic protocol that can be used to provide end-to-end encryption for voice calls 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 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.
In cryptography, security level is a measure of the strength that a cryptographic primitive — such as a cipher or hash function — achieves. Security level is usually expressed as a number of "bits of security", where n-bit security means that the attacker would have to perform 2n operations to break it, but other methods have been proposed that more closely model the costs for an attacker. This allows for convenient comparison between algorithms and is useful when combining multiple primitives in a hybrid cryptosystem, so there is no clear weakest link. For example, AES-128 is designed to offer a 128-bit security level, which is considered roughly equivalent to a RSA using 3072-bit key.
WireGuard is a communication protocol and free and open-source software that implements encrypted virtual private networks (VPNs), and was designed with the goals of ease of use, high speed performance, and low attack surface. It aims for better performance and more power than IPsec and OpenVPN, two common tunneling protocols. The WireGuard protocol passes traffic over UDP.
Cryptographic agility is a practice paradigm in designing information security protocols and standards in a way so that they can support multiple cryptographic primitives and algorithms at the same time. Then the systems implementing a particular standard can choose which combination of primitives they want to use. The primary goal of cryptographic agility was to enable rapid adaptations of new cryptographic primitives and algorithms without making disruptive changes to the systems' infrastructure.
Application Layer Transport Security (ALTS) is a Google-developed authentication and transport encryption system used for securing Remote Procedure Call (RPC) within Google machines. Google started its development in 2007, as a tailored modification of TLS.
