Cryptographic protocol
A security protocol (cryptographic protocol or encryption 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.

Cryptographic protocols are widely used for secure application-level data transport. A cryptographic protocol usually incorporates at least some of these aspects:

 Key agreement or establishment
 Entity authentication
 Symmetric encryption and message authentication   material construction
 Secured application-level data transport
 Non-repudiation methods
 Secret sharing methods
 Secure multi-party computation

For example, Transport Layer Security (TLS) is a cryptographic protocol that is used to secure web (HTTPS) connections. It has an entity authentication mechanism, based on the X.509 system; a key setup phase, where a symmetric encryption key is formed by employing public-key cryptography; and an application-level data transport function. These three aspects have important interconnections. Standard TLS does not have non-repudiation support.

There are other types of cryptographic protocols as well, and even the term itself has various readings; Cryptographic application protocols often use one or more underlying key agreement methods, which are also sometimes themselves referred to as "cryptographic protocols". For instance, TLS employs what is known as the Diffie–Hellman key exchange, which although it is only a part of TLS per se, Diffie–Hellman may be seen as a complete cryptographic protocol in itself for other applications.

Advanced cryptographic protocols 
A wide variety of cryptographic protocols go beyond the traditional goals of data confidentiality, integrity, and authentication to also secure a variety of other desired characteristics of computer-mediated collaboration. Blind signatures can be used for digital cash and digital credentials to prove that a person holds an attribute or right without revealing that person's identity or the identities of parties that person transacted with.  Secure digital timestamping can be used to prove that data (even if confidential) existed at a certain time.  Secure multiparty computation can be used to compute answers (such as determining the highest bid in an auction) based on confidential data (such as private bids), so that when the protocol is complete the participants know only their own input and the answer. End-to-end auditable voting systems provide sets of desirable privacy and auditability properties for conducting e-voting.  Undeniable signatures include interactive protocols that allow the signer to prove a forgery and limit who can verify the signature.  Deniable encryption augments standard encryption by making it impossible for an attacker to mathematically prove the existence of a plain text message. Digital mixes create hard-to-trace communications.

Formal verification 
Cryptographic protocols can sometimes be verified formally on an abstract level. When it is done, there is a necessity to formalize the environment in which the protocol operates in order to identify threats. This is frequently done through the Dolev-Yao model.

Logics, concepts and calculi used for formal reasoning of security protocols:

 Burrows–Abadi–Needham logic (BAN logic)
 Dolev–Yao model
 π-calculus
 Protocol composition logic (PCL)
 Strand space

Research projects and tools used for formal verification of security protocols:

 Automated Validation of Internet Security Protocols and Applications (AVISPA) and follow-up project AVANTSSAR
 Constraint Logic-based Attack Searcher (CL-AtSe)
 Open-Source Fixed-Point Model-Checker (OFMC)
 SAT-based Model-Checker (SATMC)
 Casper
 CryptoVerif
 Cryptographic Protocol Shapes Analyzer (CPSA)
 Knowledge In Security protocolS (KISS)
 Maude-NRL Protocol Analyzer (Maude-NPA)
 ProVerif
 Scyther
 Tamarin Prover

Notion of abstract protocol 

To formally verify a protocol it is often abstracted and modelled using Alice & Bob notation. A simple example is the following:

This states that Alice  intends a message for Bob  consisting of a message  encrypted under shared key .

Examples 
 Internet Key Exchange
 IPsec
 Kerberos
 Off-the-Record Messaging
 Point to Point Protocol
 Secure Shell (SSH)
 Signal Protocol
 Transport Layer Security
 ZRTP

See also 

 List of cryptosystems
 Secure channel
 Security Protocols Open Repository
 Comparison of cryptography libraries

References

Further reading