fbpx
Wikipedia

Cryptographic protocol

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.[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 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 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 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 edit

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:

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 edit

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 edit

See also edit

References edit

  1. ^ (PDF). 2015-10-23. Archived from the original (PDF) on 2017-08-29. Retrieved 2015-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)". from the original on 22 September 2016. Retrieved 14 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. Retrieved 14 February 2024.{{cite book}}: CS1 maint: numeric names: authors list (link)
  7. ^ . Archived from the original on 2017-02-08. Retrieved 2016-10-17.
  8. ^ Open-Source Fixed-Point Model-Checker (OFMC)
  9. ^ . 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. ^ . 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 edit

  • 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. doi:10.1007/978-3-319-45982-0_22. ISBN 978-3-319-45982-0.

cryptographic, protocol, cryptographic, protocol, abstract, concrete, protocol, that, performs, security, related, function, applies, cryptographic, methods, often, sequences, cryptographic, primitives, protocol, describes, algorithms, should, used, includes, . 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 1 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 2 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 Contents 1 Advanced cryptographic protocols 2 Formal verification 2 1 Notion of abstract protocol 3 Examples 4 See also 5 References 6 Further readingAdvanced cryptographic protocols editA 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 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 editCryptographic 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 This list is incomplete you can help by adding missing items October 2016 Burrows Abadi Needham logic BAN logic Dolev Yao model p calculus Protocol composition logic PCL Strand space 4 Research projects and tools used for formal verification of security protocols This list is incomplete you can help by adding 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 Notion of abstract protocol edit Main article Security protocol notation To formally verify a protocol it is often abstracted and modelled using Alice amp Bob notation A simple example is the following A B X K A B displaystyle A rightarrow B X K A B nbsp This states that Alice A displaystyle A nbsp intends a message for Bob B displaystyle B nbsp consisting of a message X displaystyle X nbsp encrypted under shared key K A B displaystyle K A B nbsp Examples editInternet Key Exchange IPsec Kerberos Off the Record Messaging Point to Point Protocol Secure Shell SSH Signal Protocol Transport Layer Security ZRTPSee also editList of cryptosystems Secure channel Security Protocols Open Repository Comparison of cryptography librariesReferences edit Cryptographic Protocol Overview PDF 2015 10 23 Archived from the original PDF on 2017 08 29 Retrieved 2015 10 23 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 Berry Schoenmakers Lecture Notes Cryptographic Protocols PDF Fabrega F Javier Thayer Jonathan C Herzog and Joshua D Guttman Strand Spaces Why is a Security Protocol Correct a href Template Citation html title Template Citation citation a 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 Armando A Arsac W Avanesov T Barletta M Calvi A Cappai A Carbone R Chevalier Y 12 more 2012 Flanagan C Konig 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 Retrieved 14 February 2024 a href Template Cite book html title Template Cite book cite book a 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 ProverFurther reading editErmoshina 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 doi 10 1007 978 3 319 45982 0 22 ISBN 978 3 319 45982 0 Retrieved from https en wikipedia org w index php title Cryptographic protocol amp oldid 1214900987, wikipedia, wiki, book, books, library,

article

, read, download, free, free download, mp3, video, mp4, 3gp, jpg, jpeg, gif, png, picture, music, song, movie, book, game, games.