328 citations · 355 across the 4 of their papers we have counts for
4 papers
The Security Protocol Verifier ProVerif and its Horn Clause Resolution Algorithm
Bruno Blanchet
ProVerif is a widely used security protocol verifier. Internally, ProVerif uses an abstract representation of the protocol by Horn clauses and a resolution algorithm on these claus…
The Applied Pi Calculus: Mobile Values, New Names, and Secure Communication
Martín Abadi, Bruno Blanchet, Cédric Fournet
We study the interaction of the programming construct "new", which generates statically scoped names, with communication via messages on channels. This interaction is crucial in se…
Automatic Verification of Correspondences for Security Protocols
Bruno Blanchet
We present a new technique for verifying correspondences in security protocols. In particular, correspondences can be used to formalize authentication. Our technique is fully autom…
A Static Analyzer for Large Safety-Critical Software
Bruno Blanchet, Patrick Cousot, Radhia Cousot +5
We show that abstract interpretation-based static program analysis can be made efficient and precise enough to formally verify a class of properties for a family of large programs…