 | This article has multiple issues. Please help improve it or discuss these issues on the talk page . (Learn how and when to remove these 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.
Public-key cryptography, or asymmetric cryptography, is the field of cryptographic systems that use pairs of related keys. Each key pair consists of a public key and a corresponding private key. Key pairs are generated with cryptographic algorithms based on mathematical problems termed one-way functions. Security of public-key cryptography depends on keeping the private key secret; the public key can be openly distributed without compromising security. There are many kinds of public-key cryptosystems, with different security goals, including digital signature, Diffie-Hellman key exchange, public-key key encapsulation, and public-key encryption.
In cryptography, an initialization vector (IV) or starting variable is an input to a cryptographic primitive being used to provide the initial state. The IV is typically required to be random or pseudorandom, but sometimes an IV only needs to be unpredictable or unique. Randomization is crucial for some encryption schemes to achieve semantic security, a property whereby repeated usage of the scheme under the same key does not allow an attacker to infer relationships between segments of the encrypted message. For block ciphers, the use of an IV is described by the modes of operation.
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 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.
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 of cryptographic protocols. The tool has been developed by Bruno Blanchet and others.
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.
WireGuard is a communication protocol and free and open-source software that implements encrypted virtual private networks (VPNs). It aims to be lighter and better performing than IPsec and OpenVPN, two common tunneling protocols. The WireGuard protocol passes traffic over UDP.
In cryptographic protocol design, cryptographic agility or crypto-agility is the ability to switch between multiple cryptographic primitives.
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 2023, as a tailored modification of TLS.
