LogoopenSUSE Build Service > Projects
Sign Up | Log In

ProVerif: Cryptographic protocol verifier

ProVerif is an automatic cryptographic protocol verifier, in the formal model (so called Dolev-Yao model). This protocol verifier is based on a representation of the protocol by Horn clauses. Its main features are:

It can handle many different cryptographic primitives, including shared- and public-key cryptography (encryption and signatures), hash functions, and Diffie-Hellman key agreements, specified both as rewrite rules or as equations.

It can handle an unbounded number of sessions of the protocol (even in parallel) and an unbounded message space. This result has been obtained thanks to some well-chosen approximations. This means that the verifier can give false attacks, but if it claims that the protocol satisfies some property, then the property is actually satisfied. With Andreas Podelski, we have shown that the considered resolution algorithm terminates on a large class of protocols (the so-called "tagged" protocols, FoSSaCS'03 and TCS). With Xavier Allamigeon, we have implemented attack reconstruction: when the tool cannot prove a property, it tries to reconstruct an attack, that is, an execution trace of the protocol that falsifies the desired property (CSFW'05).

Source Files

Filename Size Changed Actions
_service 75 Bytes Download File
proverif.changes 1.06 KB Download File
proverif.spec 1.72 KB Download File
proverif1.93.tar.gz 528 KB Download File
proverifdoc1.93.tar.gz 782 KB Download File

Comments for home:ptrommler:formal (0)

Login required, please login or signup in order to comment