Modeling and Verifying Security Protocols with the Applied Pi Calculus and ProVerif (bibtex)
by Bruno Blanchet
Abstract:
ProVerif is an automatic symbolic protocol verifier. It supports a wide range of cryptographic primitives, defined by rewrite rules or by equations. It can prove various security properties: secrecy, authentication, and process equivalences, for an unbounded message space and an unbounded number of sessions. It takes as input a description of the protocol to verify in a dialect of the applied pi calculus, an extension of the pi calculus with cryptography. It automatically translates this protocol description into Horn clauses and determines whether the desired security properties hold by resolution on these clauses. This survey presents an overview of the research on ProVerif.
Reference:
Modeling and Verifying Security Protocols with the Applied Pi Calculus and ProVerif (Bruno Blanchet), In Foundations and Trends in Privacy and Security, volume 1, 2016.
Bibtex Entry:
@Article{BlanchetFnTPS16,
  author = 	 {Bruno Blanchet},
  title = 	 {Modeling and Verifying Security Protocols with the Applied Pi Calculus and {P}ro{V}erif},
  journal = 	 {Foundations and Trends in Privacy and Security},
  year = 	 {2016},
  volume = 	 {1},
  number = 	 {1--2},
  pages = 	 {1--135},
  month = 	 oct,
  abstract = {ProVerif is an automatic symbolic protocol verifier.  It supports a
  wide range of cryptographic primitives, defined by rewrite rules or
  by equations. It can prove various security properties: secrecy,
  authentication, and process equivalences,
  for an unbounded message space and an unbounded number of sessions.
  It takes as input a description of the protocol to verify in a
  dialect of the applied pi calculus, an extension of the pi calculus
  with cryptography.  It automatically translates this protocol description
  into Horn clauses and determines whether
  the desired security properties hold by resolution on these clauses.
  This survey presents an overview of the research on 
  ProVerif.},
  url = {http://dx.doi.org/10.1561/3300000004}
}
Powered by bibtexbrowser