Editing Cryptographic protocol (section)

== Formal verification ==
Cryptographic protocols can sometimes be [[Formal verification|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:
{{Incomplete list|date=October 2016}}
* [[Burrows–Abadi–Needham logic|Burrows–Abadi–Needham logic (BAN logic)]]
* [[Dolev–Yao model]]
* [[π-calculus]]
* [[Protocol composition logic|Protocol composition logic (PCL)]]
* Strand space<ref>{{citation|title=Strand Spaces: Why is a Security Protocol Correct?|author=Fábrega, F. Javier Thayer, Jonathan C. Herzog, and Joshua D. Guttman.}}</ref>

Research projects and tools used for formal verification of security protocols:
{{Incomplete list|date=October 2016}}
* Automated Validation of Internet Security Protocols and Applications (AVISPA) and follow-up project AVANTSSAR.<ref>{{cite web |url=http://avispa-project.org/ |title=Automated Validation of Internet Security Protocols and Applications (AVISPA) |access-date=14 February 2024 |archive-url=https://web.archive.org/web/20160922202730/http://www.avispa-project.org/ |archive-date=22 September 2016 |url-status=live}}</ref><ref name=TAP_1>{{cite book| title=The AVANTSSAR Platform for the Automated Validation of Trust and Security of Service-Oriented Architectures| author1=Armando, A.| author2=Arsac, W| author3=Avanesov, T.| author4=Barletta, M.| author5=Calvi, A.| author6=Cappai, A.| author7=Carbone, R.| author8=Chevalier, Y.| author9=+12 more|  editor1=Flanagan, C.| editor2=König, B.| url=https://link.springer.com/chapter/10.1007/978-3-642-28756-5_19| publisher=LNTCS| volume=7214| pages=267–282| date=2012| access-date=14 February 2024| doi=10.1007/978-3-642-28756-5_19}}</ref>
** Constraint Logic-based Attack Searcher (CL-AtSe)<ref>{{Cite web |url=https://cassis.loria.fr/wiki/Wiki.jsp?page=Cl-Atse |title=Constraint Logic-based Attack Searcher (Cl-AtSe) |access-date=2016-10-17 |archive-date=2017-02-08 |archive-url=https://web.archive.org/web/20170208141835/https://cassis.loria.fr/wiki/Wiki.jsp?page=Cl-Atse |url-status=dead }}</ref>
** Open-Source Fixed-Point Model-Checker (OFMC)<ref>[http://people.compute.dtu.dk/samo/ Open-Source Fixed-Point Model-Checker (OFMC)]</ref>
** SAT-based Model-Checker (SATMC)<ref>{{Cite web |url=http://www.ai-lab.it/satmc/ |title=SAT-based Model-Checker for Security Protocols and Security-sensitive Application (SATMC) |access-date=2016-10-17 |archive-url=https://web.archive.org/web/20151003010538/http://www.ai-lab.it/satmc/ |archive-date=2015-10-03 |url-status=dead }}</ref>
* Casper<ref>[http://www.cs.ox.ac.uk/people/gavin.lowe/Security/Casper/index.html Casper: A Compiler for the Analysis of Security Protocols]</ref>
* [[CryptoVerif]]
* Cryptographic Protocol Shapes Analyzer (CPSA)<ref>[https://hackage.haskell.org/package/cpsa cpsa: Symbolic cryptographic protocol analyzer]</ref>
* Knowledge In Security protocolS (KISS)<ref>{{Cite web |url=http://www.lsv.ens-cachan.fr/~ciobaca/kiss/ |title=Knowledge In Security protocolS (KISS) |access-date=2016-10-07 |archive-url=https://web.archive.org/web/20161010085620/http://www.lsv.ens-cachan.fr/~ciobaca/kiss/ |archive-date=2016-10-10 |url-status=dead }}</ref>
* Maude-NRL Protocol Analyzer (Maude-NPA)<ref>[http://personales.upv.es/sanesro/Maude-NPA_Protocols/ Maude-NRL Protocol Analyzer (Maude-NPA)]</ref>
* [[ProVerif]]
* Scyther<ref>[https://www.cs.ox.ac.uk/people/cas.cremers/scyther/ Scyther]</ref>
* [[Tamarin Prover]]<ref>[https://tamarin-prover.github.io/ Tamarin Prover]</ref>
* Squirrel<ref>[https://squirrel-prover.github.io/ Squirrel Prover]</ref>

=== Notion of abstract protocol ===
{{main|Security protocol notation}}
To formally verify a protocol it is often abstracted and modelled using [[security protocol notation|Alice & Bob notation]]. A simple example is the following:
:<math>A\rightarrow B:\{X\}_{K_{A,B}}</math>

This states that [[Alice and Bob|Alice]] <math>A</math> intends a message for Bob <math>B</math> consisting of a message <math>X</math> encrypted under shared key <math>K_{A,B}</math>.