Movatterモバイル変換


[0]ホーム

URL:


Jump to content
WikipediaThe Free Encyclopedia
Search

Cryptographic protocol

From Wikipedia, the free encyclopedia
Aspect of cryptography

Acryptographic protocol is an abstract or concreteprotocol that performs asecurity-related function and appliescryptographic methods, often as sequences ofcryptographic 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,Transport Layer Security (TLS) is a cryptographic protocol that is used to secure web (HTTPS) connections.[2] It has an entity authentication mechanism, based on theX.509 system; a key setup phase, where asymmetric 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; Cryptographicapplication protocols often use one or more underlyingkey agreement methods, which are also sometimes themselves referred to as "cryptographic protocols". For instance, TLS employs what is known as theDiffie–Hellman key exchange, which although it is only a part of TLSper se, Diffie–Hellman may be seen as a complete cryptographic protocol in itself for other applications.

Advanced cryptographic protocols

[edit]

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.[3]Blind signatures can be used fordigital cash anddigital 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 conductinge-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

[edit]

Cryptographic protocols can sometimes beverified 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 theDolev-Yao model.

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

This list isincomplete; you can help byadding missing items.(October 2016)

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

This list isincomplete; you can help byadding missing items.(October 2016)
  • 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]
  • Squirrel[16]

Notion of abstract protocol

[edit]
Main article:Security protocol notation

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

AB:{X}KA,B{\displaystyle A\rightarrow B:\{X\}_{K_{A,B}}}

This states thatAliceA{\displaystyle A} intends a message for BobB{\displaystyle B} consisting of a messageX{\displaystyle X} encrypted under shared keyKA,B{\displaystyle K_{A,B}}.

Examples

[edit]

See also

[edit]

References

[edit]
  1. ^"Cryptographic Protocol Overview"(PDF). 2015-10-23. Archived fromthe original(PDF) on 2017-08-29. Retrieved2015-10-23.
  2. ^Chen, Shan; Jero, Samuel; Jagielski, Matthew; Boldyreva, Alexandra; Nita-Rotaru, Cristina (2021-07-01)."Secure Communication Channel Establishment: TLS 1.3 (over TCP Fast Open) versus QUIC".Journal of Cryptology.34 (3): 26.doi:10.1007/s00145-021-09389-w.ISSN 0933-2790.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. Retrieved14 February 2024.
  6. ^Armando, A.; Arsac, W; Avanesov, T.; Barletta, M.; Calvi, A.; Cappai, A.; Carbone, R.; Chevalier, Y.; +12 more (2012). Flanagan, C.; König, B. (eds.).The AVANTSSAR Platform for the Automated Validation of Trust and Security of Service-Oriented Architectures. Vol. 7214. LNTCS. pp. 267–282.doi:10.1007/978-3-642-28756-5_19. Retrieved14 February 2024.{{cite book}}: CS1 maint: numeric names: authors list (link)
  7. ^"Constraint Logic-based Attack Searcher (Cl-AtSe)". Archived fromthe original on 2017-02-08. Retrieved2016-10-17.
  8. ^Open-Source Fixed-Point Model-Checker (OFMC)
  9. ^"SAT-based Model-Checker for Security Protocols and Security-sensitive Application (SATMC)". Archived fromthe original on 2015-10-03. Retrieved2016-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 fromthe original on 2016-10-10. Retrieved2016-10-07.
  13. ^Maude-NRL Protocol Analyzer (Maude-NPA)
  14. ^Scyther
  15. ^Tamarin Prover
  16. ^Squirrel Prover

Further reading

[edit]
General
Mathematics
Retrieved from "https://en.wikipedia.org/w/index.php?title=Cryptographic_protocol&oldid=1315577681"
Category:
Hidden categories:

[8]ページ先頭

©2009-2026 Movatter.jp