An efficient cryptographic protocol verifier based on prolog rules

By Bruno Blanchet. Proceedings. 14th IEEE Computer Security Foundations Workshop, 2001., 2001

1,234 citations recorded by the source corpus.

Subfields: Artificial Intelligence, Computer Networks and Communications, Information Systems

View Paper: https://www.semanticscholar.org/paper/905226530f531fb45fb38e17e99817b7f10f4d3a

How researchers see this paper

The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.

In Artificial Intelligence

In Computer Networks and Communications

In Information Systems

Citations in the corpus

Scyther : semantics and verification of security protocols (2006, methodology): “Nevertheless, the Spi calculus has been successfully used in the area of web services [27] in combination with the ProVerif tool [29], which has led to the development of the TulaFale security tool for Web Services [28].”
Automated verification of selected equivalences for security protocols (2005, methodology): “We also use ProVerif for checking certain equivalences that express authenticity properties in an example from the literature [6].”
A Certifying Compiler for Zero-Knowledge Proofs of Knowledge Based on Sigma-Protocols (2010, neutral): “In [36,37], approaches for extracting models from protocol implementations written in F#, and automatically verifying these models by compilation to symbolic models (resp. computational models) in ProVerif [38] (resp.”
Automated Security Protocol Analysis With the AVISPA Tool (2006, methodology): “tore [48], who have formalized a translation procedure from protocol descriptions in HLPSL to descriptions in the applied pi calculus, which allowed them to apply the ProVerif tool [1,2,21,22] to some of our HLPSL protocol specifications.”
Verifying privacy-type properties of electronic voting protocols (2009, methodology): “The ap pli d i calculus has a family of proof techniques which we can use, and it is partly supported by the ProVerif tool [9].”
Verified Reference Implementations of WS-Security Protocols (2006, methodology): “For instance, the ProVerif [9,8] theorem prover takes a protocol model written in a variant of the pi calculus [23,2] plus target authentication and secrecy goals, and attempts to prove that the model satisfies these goals.”
Moat: Verifying Confidentiality of Enclave Programs (2015, methodology): “Although we do not focus on protocol attacks in this paper, we brieﬂy describe how one can compose protocol-level analysis (performed by a veriﬁer such as ProVerif [11]) with Moat to achieve end-to-end conﬁdentiality guarantees against infrastructure, application, and protocol attacks.”
The TAMARIN Prover for the Symbolic Analysis of Security Protocols (2013, methodology): “The ProVerif tool [2] has been extended to partially handle DH with inverses [8], bilinear pairings [12], and mutable global state [1].”
The AVISPA Tool for the Automated Validation of Internet Security Protocols and Applications (2005, background): “[1, 4, 6, 7, 13, 14], which can analyze small and medium-scale protocols such as those in the Clark/Jacob library [10].”
The Scyther Tool: Verification, Falsification, and Analysis of Security Protocols (2008, methodology): “Even though no abstraction techniques are used by Scyther, it offered a level of performance similar to the abstraction-based ProVerif tool [1].”