Merge pull request #24637 from bruno-blanchet/add-pkg-proverif.2.05

added ProVerif version 2.05

packages/proverif/proverif.2.05/opam

@@ -0,0 +1,42 @@
+opam-version: "2.0"
+synopsis: "ProVerif: Cryptographic protocol verifier in the symbolic model"
+description: """
+ProVerif is an automatic cryptographic protocol verifier, in the symbolic 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.
+
+ProVerif can prove the following properties:
+
+- secrecy (the adversary cannot obtain the secret)
+- authentication and more generally correspondence
+- strong secrecy (the adversary does not see the difference when the value of the secret changes)
+- equivalences between processes that differ only by terms
+
+A survey of ProVerif with references to other papers is available at
+
+Bruno Blanchet. Modeling and Verifying Security Protocols with the Applied Pi Calculus and ProVerif. Foundations and Trends in Privacy and Security, 1(1-2):1-135, October 2016. http://dx.doi.org/10.1561/3300000004
+"""
+maintainer:
+  "Bruno Blanchet <[email protected]>, Vincent Cheval <[email protected]>"
+authors:
+  "Bruno Blanchet <[email protected]>, Vincent Cheval <[email protected]>, Marc Sylvestre"
+homepage: "http://proverif.inria.fr/"
+dev-repo: "git+https://gitlab.inria.fr/bblanche/proverif.git"
+bug-reports: "[email protected]"
+license: "GPL-2.0-or-later"
+
+depends: ["ocaml" { >= "4.03" }
+	  "ocamlfind" {build}
+	  "lablgtk"
+	  "proverifdoc" { = version & post & with-doc} ]
+build: [
+       [ "./build" "byte" { !ocaml:native } ] 
+]
+install: [ "./build" "install" "%{prefix}%" ]
+
+url {
+  src: "https://proverif.inria.fr/proverif2.05.tar.gz"
+  checksum: "md5=7f44869213c887f6e0febc3f890ca064"
+}

packages/proverifdoc/proverifdoc.2.05/opam

@@ -0,0 +1,17 @@
+opam-version: "2.0"
+synopsis: "Documentation for ProVerif, a cryptographic protocol verifier in the symbolic model"
+maintainer:
+  "Bruno Blanchet <[email protected]>, Vincent Cheval <[email protected]>"
+authors:
+  "Bruno Blanchet <[email protected]>, Vincent Cheval <[email protected]>, Ben Smyth <[email protected]>, Marc Sylvestre"
+homepage: "http://proverif.inria.fr/"
+dev-repo: "git+https://gitlab.inria.fr/bblanche/proverif.git"
+bug-reports: "[email protected]"
+license: "Public domain"
+
+install: [  "./installdoc" "%{prefix}%" ]
+
+url {
+  src: "https://proverif.inria.fr/proverifdoc2.05.tar.gz"
+  checksum: "md5=23687ffb2765ce947c114a8fad5e1097"
+}