Cryptographic protocol
A cryptographic protocol is an abstract or concrete
Cryptographic protocols are widely used for secure application-level data transport. A cryptographic protocol usually incorporates at least some of these aspects:
- Key agreementor 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,
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
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.
Formal verification
Cryptographic protocols can sometimes be
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[4]
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.[5][6]
- Casper[10]
- CryptoVerif
- Cryptographic Protocol Shapes Analyzer (CPSA)[11]
- Knowledge In Security protocolS (KISS)[12]
- Maude-NRL Protocol Analyzer (Maude-NPA)[13]
- ProVerif
- Scyther[14]
- Tamarin Prover[15]
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
- ^ "Cryptographic Protocol Overview" (PDF). 2015-10-23. Archived from the original (PDF) on 2017-08-29. Retrieved 2015-10-23.
- S2CID 235174220.
- ^ Berry Schoenmakers. "Lecture Notes Cryptographic Protocols" (PDF).
- ^ Fábrega, F. Javier Thayer, Jonathan C. Herzog, and Joshua D. Guttman., Strand Spaces: Why is a Security Protocol Correct?
{{citation}}
: CS1 maint: multiple names: authors list (link) - ^ "Automated Validation of Internet Security Protocols and Applications (AVISPA)". Archived from the original on 22 September 2016. Retrieved 14 February 2024.
- doi:10.1007/978-3-642-28756-5_19. Retrieved 14 February 2024.)
{{cite book}}
: CS1 maint: numeric names: authors list (link - ^ "Constraint Logic-based Attack Searcher (Cl-AtSe)". Archived from the original on 2017-02-08. Retrieved 2016-10-17.
- ^ Open-Source Fixed-Point Model-Checker (OFMC)
- ^ "SAT-based Model-Checker for Security Protocols and Security-sensitive Application (SATMC)". Archived from the original on 2015-10-03. Retrieved 2016-10-17.
- ^ Casper: A Compiler for the Analysis of Security Protocols
- ^ cpsa: Symbolic cryptographic protocol analyzer
- ^ "Knowledge In Security protocolS (KISS)". Archived from the original on 2016-10-10. Retrieved 2016-10-07.
- ^ Maude-NRL Protocol Analyzer (Maude-NPA)
- ^ Scyther
- ^ Tamarin Prover
Further reading
- Ermoshina, Ksenia; Musiani, Francesca; Halpin, Harry (September 2016). "End-to-End Encrypted Messaging Protocols: An Overview" (PDF). In Bagnoli, Franco; et al. (eds.). Internet Science. INSCI 2016. Florence, Italy: Springer. pp. 244–254. ISBN 978-3-319-45982-0.