Gentoo Packages

Search

Package Information

Description:

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.

Homepage:

https://bblanche.gitlabpages.inria.fr/proverif/ https://gitlab.inria.fr/bblanche/proverif/

Versions

Metadata

Description

• 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.

Maintainers

• ML (ml@gentoo.org) - Type: project
• Gentoo Mathematics Project (sci-mathematics@gentoo.org) - Type: project

Upstream

• Bugs: https://gitlab.inria.fr/bblanche/proverif/-/issues/

<pkgmetadata>
	<maintainer type="project">
		<email>ml@gentoo.org</email>
		<name>ML</name>
	</maintainer>
	<maintainer type="project">
		<email>sci-mathematics@gentoo.org</email>
		<name>Gentoo Mathematics Project</name>
	</maintainer>
	<longdescription>
    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.
  </longdescription>
	<upstream>
		<bugs-to>https://gitlab.inria.fr/bblanche/proverif/-/issues/</bugs-to>
	</upstream>
</pkgmetadata>

Lint Warnings

• [Warning] Ebuild 9999 uses IUSE flag 'emacs' which is not documented in metadata.xml. Add the flag to metadata.xml <use> section.
• [Warning] Ebuild 2.05 uses IUSE flag 'emacs' which is not documented in metadata.xml. Add the flag to metadata.xml <use> section.
• [Warning] Ebuild 2.04-r1 uses IUSE flag 'emacs' which is not documented in metadata.xml. Add the flag to metadata.xml <use> section.
• [Warning] Missing md5-cache for version 9999. Run 'ebuild <ebuild_file> manifest' or 'egencache' to generate it.
• [Warning] Missing md5-cache for version 2.05. Run 'ebuild <ebuild_file> manifest' or 'egencache' to generate it.
• [Warning] Missing md5-cache for version 2.04-r1. Run 'ebuild <ebuild_file> manifest' or 'egencache' to generate it.

USE Flags

Files

• 50proverif-gentoo.el

Manifest