From 69d74a4311be33225514d7714416a0a931d15446 Mon Sep 17 00:00:00 2001 From: Bruno Blanchet Date: Tue, 17 Oct 2023 15:11:49 +0200 Subject: [PATCH 1/2] added ProVerif version 2.05 --- packages/proverif/proverif.2.05/opam | 42 ++++++++++++++++++++++ packages/proverifdoc/proverifdoc.2.05/opam | 17 +++++++++ 2 files changed, 59 insertions(+) create mode 100644 packages/proverif/proverif.2.05/opam create mode 100644 packages/proverifdoc/proverifdoc.2.05/opam diff --git a/packages/proverif/proverif.2.05/opam b/packages/proverif/proverif.2.05/opam new file mode 100644 index 00000000000..c099922e860 --- /dev/null +++ b/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 , Vincent Cheval " +authors: + "Bruno Blanchet , Vincent Cheval , Marc Sylvestre" +homepage: "http://proverif.inria.fr/" +dev-repo: "git+https://gitlab.inria.fr/bblanche/proverif.git" +bug-reports: "proverif-dev@inria.fr" +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=04d77912231a75d3000a193876e0e9c8" +} diff --git a/packages/proverifdoc/proverifdoc.2.05/opam b/packages/proverifdoc/proverifdoc.2.05/opam new file mode 100644 index 00000000000..02a53013e9f --- /dev/null +++ b/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 , Vincent Cheval " +authors: + "Bruno Blanchet , Vincent Cheval , Ben Smyth , Marc Sylvestre" +homepage: "http://proverif.inria.fr/" +dev-repo: "git+https://gitlab.inria.fr/bblanche/proverif.git" +bug-reports: "proverif-dev@inria.fr" +license: "Public domain" + +install: [ "./installdoc" "%{prefix}%" ] + +url { + src: "https://proverif.inria.fr/proverifdoc2.05.tar.gz" + checksum: "md5=d4aba1bb794ed6e9631db6ed835a01fe" +} From de1f8e3fdee887f7c2daf890cef8bfbbc25f4574 Mon Sep 17 00:00:00 2001 From: Bruno Blanchet Date: Tue, 17 Oct 2023 15:56:31 +0200 Subject: [PATCH 2/2] added ProVerif version 2.05 --- packages/proverif/proverif.2.05/opam | 2 +- packages/proverifdoc/proverifdoc.2.05/opam | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/packages/proverif/proverif.2.05/opam b/packages/proverif/proverif.2.05/opam index c099922e860..9a94c52c3f6 100644 --- a/packages/proverif/proverif.2.05/opam +++ b/packages/proverif/proverif.2.05/opam @@ -38,5 +38,5 @@ install: [ "./build" "install" "%{prefix}%" ] url { src: "https://proverif.inria.fr/proverif2.05.tar.gz" - checksum: "md5=04d77912231a75d3000a193876e0e9c8" + checksum: "md5=7f44869213c887f6e0febc3f890ca064" } diff --git a/packages/proverifdoc/proverifdoc.2.05/opam b/packages/proverifdoc/proverifdoc.2.05/opam index 02a53013e9f..363b34e66eb 100644 --- a/packages/proverifdoc/proverifdoc.2.05/opam +++ b/packages/proverifdoc/proverifdoc.2.05/opam @@ -13,5 +13,5 @@ install: [ "./installdoc" "%{prefix}%" ] url { src: "https://proverif.inria.fr/proverifdoc2.05.tar.gz" - checksum: "md5=d4aba1bb794ed6e9631db6ed835a01fe" + checksum: "md5=23687ffb2765ce947c114a8fad5e1097" }