sci-mathematics / proverif

Cryptographic protocol verifier in the formal model

Official package sites : https://bblanche.gitlabpages.inria.fr/proverif/ · https://gitlab.inria.fr/bblanche/proverif/ ·

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: 1) 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. 2) 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. The considered resolution algorithm terminates on a large class of protocols (the so-called "tagged" protocols). 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.

v9999 :: 0 :: gentoo

Modified
License
GPL-2+
USE flags
emacs ocamlopt

v2.05 :: 0 :: gentoo

Modified
License
GPL-2+
Keywords
~amd64 ~x86
USE flags
emacs ocamlopt

v2.04-r1 :: 0 :: gentoo

Modified
License
GPL-2+
Keywords
~amd64 ~x86
USE flags
emacs ocamlopt

General

emacs
Add support for GNU Emacs
ocamlopt
Enable ocamlopt support (ocaml native code compiler) -- Produces faster programs (Warning: you have to disable/enable it at a global scale)

app-editors / emacs : The extensible, customizable, self-documenting real-time display editor

dev-lang / ocaml : Programming language supporting functional, imperative & object-oriented styles

dev-ml / findlib : OCaml tool to find/use non-standard packages

app-editors / emacs : The extensible, customizable, self-documenting real-time display editor

dev-lang / ocaml : Programming language supporting functional, imperative & object-oriented styles

Repository mirror & CI · gentoo
Merge updates from master
Maciej Barć · gentoo
sci-mathematics/proverif: bump to 2.05
Signed-off-by: Maciej Barć <xgqt@gentoo.org>
Maciej Barć · gentoo
sci-mathematics/proverif: bump to 2.05
Signed-off-by: Maciej Barć <xgqt@gentoo.org>
Repository mirror & CI · gentoo
Merge updates from master
Maciej Barć · gentoo
sci-mathematics/proverif: require ocamlopt
Closes: https://bugs.gentoo.org/916717 Signed-off-by: Maciej Barć <xgqt@gentoo.org>
Repository mirror & CI · gentoo
Merge updates from master
Maciej Barć · gentoo
sci-mathematics/proverif: new package; add 2.04
Signed-off-by: Maciej Barć <xgqt@gentoo.org>