Cryptographic protocol

Source: Wikipedia, the free encyclopedia.

A cryptographic protocol is an abstract or concrete

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.[1]

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

For example,

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.

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

Dolev-Yao
model.

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

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]
    • Constraint Logic-based Attack Searcher (CL-AtSe)[7]
    • Open-Source Fixed-Point Model-Checker (OFMC)[8]
    • SAT-based Model-Checker (SATMC)[9]
  • 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

See also

References

  1. ^ "Cryptographic Protocol Overview" (PDF). 2015-10-23. Archived from the original (PDF) on 2017-08-29. Retrieved 2015-10-23.
  2. S2CID 235174220
    .
  3. ^ Berry Schoenmakers. "Lecture Notes Cryptographic Protocols" (PDF).
  4. ^ 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)
  5. ^ "Automated Validation of Internet Security Protocols and Applications (AVISPA)". Archived from the original on 22 September 2016. Retrieved 14 February 2024.
  6. doi:10.1007/978-3-642-28756-5_19. Retrieved 14 February 2024.{{cite book}}: CS1 maint: numeric names: authors list (link
    )
  7. ^ "Constraint Logic-based Attack Searcher (Cl-AtSe)". Archived from the original on 2017-02-08. Retrieved 2016-10-17.
  8. ^ Open-Source Fixed-Point Model-Checker (OFMC)
  9. ^ "SAT-based Model-Checker for Security Protocols and Security-sensitive Application (SATMC)". Archived from the original on 2015-10-03. Retrieved 2016-10-17.
  10. ^ Casper: A Compiler for the Analysis of Security Protocols
  11. ^ cpsa: Symbolic cryptographic protocol analyzer
  12. ^ "Knowledge In Security protocolS (KISS)". Archived from the original on 2016-10-10. Retrieved 2016-10-07.
  13. ^ Maude-NRL Protocol Analyzer (Maude-NPA)
  14. ^ Scyther
  15. ^ Tamarin Prover

Further reading