···11-opam-version: "2.0"
22-maintainer: "dev@ocsigen.org"
33-authors: "dev@ocsigen.org"
44-synopsis: "Client/server Web framework"
55-description: "Eliom is a framework for implementing client/server Web applications. It introduces new concepts to simplify the implementation of common behaviors, and uses advanced static typing features of OCaml to check many properties of the Web application at compile-time. Eliom allows implementing the whole application as a single program that includes both the client and the server code. We use a syntax extension to distinguish between the two sides. The client-side code is compiled to JS using Ocsigen Js_of_ocaml."
66-homepage: "http://ocsigen.org/eliom/"
77-bug-reports: "https://github.com/ocsigen/eliom/issues/"
88-license: "LGPL-2.1-only WITH OCaml-LGPL-linking-exception"
99-dev-repo: "git+https://github.com/ocsigen/eliom.git"
1010-build: [make]
1111-depends: [
1212- "ocaml" {>= "4.06.1" & < "5.1"}
1313- "ocamlfind"
1414- "deriving" {>= "0.6"}
1515- "ppx_deriving"
1616- "ppx_tools" {>= "0.99.3"}
1717- "js_of_ocaml" {>= "3.0" & < "3.3"}
1818- "js_of_ocaml-lwt" {< "3.3"}
1919- "js_of_ocaml-ocamlbuild" {build}
2020- "js_of_ocaml-ppx"
2121- "js_of_ocaml-ppx" {<= "3.0.2"} | "js_of_ocaml-ppx_deriving_json" {< "3.5"}
2222- "js_of_ocaml-tyxml" {< "3.2.0"}
2323- "lwt_log"
2424- "lwt_ppx"
2525- "lwt_camlp4"
2626- "tyxml" {>= "4.0.0" & < "4.3.0"}
2727- "ocsigenserver" {>= "2.10" & < "3.0.0"}
2828- "ipaddr" {>= "2.1"}
2929- "reactiveData" {>= "0.2.1"}
3030- "dbm" | "sqlite3"
3131- "base-bytes"
3232-]
3333-url {
3434- src: "https://github.com/jrochel/eliom/archive/6.4.0.tar.gz"
3535- checksum: [
3636- "md5=8e5694fefb152c9372b9a32a08a826be"
3737- "sha512=0de9d360fc00e36b093d2b22c3d5b5f497302017c8bdc54dc47dd38c0e0fd3fa02384431ff8fbe3e67db9947daf1dbcbf266791e23ea01ee6112bd684befc16c"
3838- ]
3939-}
4040-available: false # source tarball not available
-62
packages/gappa/gappa.1.3.5/opam
···11-opam-version: "2.0"
22-maintainer: "7895506+MSoegtropIMC@users.noreply.github.com"
33-authors: "Guillaume Melquiond"
44-bug-reports: "https://gitlab.inria.fr/gappa/gappa/-/issues"
55-homepage: "https://gitlab.inria.fr/gappa/gappa"
66-dev-repo: "git+https://gitlab.inria.fr/gappa/gappa.git"
77-license: "CeCILL"
88-patches: [
99- "remake.patch"
1010- "0001-Added-configure-for-c-11.patch"
1111-]
1212-build: [
1313- [ "autoreconf" ]
1414- # Note: configure.in seems to reference this file
1515- [ "touch" "stamp-config_h.in" ]
1616- [ "./configure"
1717- # If someone knows how to ask MacPorts for the usual include and lib path, please tell me
1818- "CXXFLAGS=-I/opt/local/include" { os-distribution = "macports" & os = "macos" }
1919- "LDFLAGS=-L/opt/local/lib" { os-distribution = "macports" & os = "macos" }
2020- # Support installing on Apple Silicon with Homebrew
2121- "CXXFLAGS=-I/opt/homebrew/include" { os-distribution = "homebrew" & os = "macos" & arch = "arm64"}
2222- "LDFLAGS=-L/opt/homebrew/lib" { os-distribution = "homebrew" & os = "macos" & arch = "arm64"}
2323- "--build=%{arch}%-pc-cygwin" { os = "win32" & os-distribution = "cygwinports" }
2424- "--host=%{arch}%-w64-mingw32" { os = "win32" & os-distribution = "cygwinports" }
2525- "--target=%{arch}%-w64-mingw32" { os = "win32" & os-distribution = "cygwinports" }
2626- "--prefix=%{prefix}%"
2727- ]
2828- [ "./remake" "--jobs=%{jobs}%" ]
2929-]
3030-install: [ "./remake" "-d" "install" ]
3131-depends: [
3232- "conf-g++" {build}
3333- "conf-autoconf" {build}
3434- "conf-automake" {build}
3535- "conf-gmp"
3636- "conf-mpfr"
3737- "conf-boost"
3838- "conf-bison" {build}
3939- "conf-flex" {build}
4040-]
4141-synopsis: "Tool intended for formally proving properties on numerical programs dealing with floating-point or fixed-point arithmetic"
4242-url {
4343- src: "https://gitlab.inria.fr/gappa/gappa/-/archive/gappa-1.3.5.tar.gz"
4444- checksum: "sha512=29ce59af97e6d60547a193b43538f4812ff74fb01a812cda7109855219457fa7a47f59ea39aff2a5e03fd70181e024a3296b4f48300818a81f62fd2d8629c389"
4545-}
4646-extra-source "remake.patch" {
4747- src:
4848- "https://raw.githubusercontent.com/ocaml/opam-source-archives/main/patches/gappa/remake.patch"
4949- checksum: [
5050- "sha256=365967b9cd294d485302b6c14a072ac06d3238bfeb313eaae07159a8542fc5ff"
5151- "md5=d66b718118ae5bf61c661905f6f0db96"
5252- ]
5353-}
5454-extra-source "0001-Added-configure-for-c-11.patch" {
5555- src:
5656- "https://raw.githubusercontent.com/ocaml/opam-source-archives/main/patches/gappa/0001-Added-configure-for-c-11.patch"
5757- checksum: [
5858- "sha256=5d9ff1e6461834c2d3d6c4cb1f9dd7424a4a681b40cab19a6fbbe0ff8d50284e"
5959- "md5=b6a6dbe9a12feae79eab038864208a3c"
6060- ]
6161-}
6262-available: false # source tarball not available / wrong checksum
···11-opam-version: "2.0"
22-maintainer: "gwenael.delaval@inria.fr"
33-authors: "Gwenaël Delaval"
44-homepage: "http://bzr.inria.fr"
55-build: [
66- ["./configure" "--prefix" prefix]
77- [make]
88-]
99-depends: [
1010- "ocaml" {< "5.0"}
1111- "ocamlfind"
1212- "menhir" {< "20141215"}
1313- "ocamlgraph"
1414- "camlp4"
1515- "ocamlbuild" {build}
1616-]
1717-depopts: ["lablgtk"]
1818-install: [make "install"]
1919-synopsis: "Compiler for the Heptagon/BZR synchronous programming language"
2020-description: """
2121-Heptagon/BZR is a synchronous dataflow language whose syntax and
2222-semantics is inspired from Lustre, with a syntax allowing the
2323-expression of control structures (e.g., switch or mode automata).
2424-Heptagon/BZR is a research compiler, whose aim is to facilitate
2525-experimentation. The current version of the compiler includes the
2626-following features:
2727-- Inclusion of discrete controller synthesis within the compilation
2828-- Expression and compilation of array values with modular memory optimization
2929-See http://bzr.inria.fr for further informations."""
3030-url {
3131- src:
3232- "https://gforge.inria.fr/frs/download.php/33440/heptagon-1.00.06.tar.gz"
3333- checksum: "md5=5ab84717e8b14009660b7f8e91d4e553"
3434-}
3535-available: false # source tarball not available
···11-opam-version: "2.0"
22-maintainer: "gautier.hattenberger@enac.fr"
33-homepage: "https://www.eei.cena.fr/products/ivy"
44-build: make
55-remove: [
66- ["ocamlfind" "remove" "ivy"]
77- ["ocamlfind" "remove" "glibivy"]
88-]
99-depends: ["ocaml" "ocamlfind" "conf-tcl" "conf-glib-2" "conf-libpcre" "base-unsafe-string"]
1010-install: [make "install" "COMPAT_SYMLINK_CREATE=no"]
1111-synopsis: "This OCaml-library interfaces the Ivy software bus C-library"
1212-description: """
1313-Standalone linking and with the glib mainloop are provided.
1414-See https://www.eei.cena.fr/products/ivy for information on the Ivy Software bus and the required ivy-c library."""
1515-flags: light-uninstall
1616-url {
1717- src: "https://www.eei.cena.fr/products/ivy/download/packages/ivy-ocaml_1.2-2.tar.gz"
1818- checksum: [
1919- "sha256=a334f144570d276cfe1f0187b91594f22b7ef24d8356af960321b25844febf4c"
2020- "sha512=51c00f14139db6d11822d5cfbd29d49ba8d41c71280919ee9c4768478d324e7486b4f1b06d7208a63b4c10e9f1617a3927f235db74901538a28dd69e7a99ca4f"
2121- ]
2222-}
2323-available: false # source tarball not available
-34
packages/ivy/ivy.1.3.1/opam
···11-opam-version: "2.0"
22-maintainer: "gautier.hattenberger@enac.fr"
33-homepage: "https://www.eei.cena.fr/products/ivy"
44-build: [
55- [make]
66-]
77-install: [make "install"]
88-remove: [
99- ["ocamlfind" "remove" "ivy"]
1010- ["ocamlfind" "remove" "glibivy"]
1111- ["ocamlfind" "remove" "tkivy"]
1212-]
1313-depends: [
1414- "ocaml"
1515- "ocamlfind" {build}
1616- "conf-tk"
1717- "conf-glib-2"
1818- "conf-libpcre"
1919- "base-unsafe-string"
2020-]
2121-synopsis: "This OCaml-library interfaces the Ivy software bus C-library"
2222-description: """
2323-Standalone linking and with the glib mainloop are provided.
2424-See https://www.eei.cena.fr/products/ivy for information on the Ivy Software bus and the required ivy-c library."""
2525-flags: light-uninstall
2626-url {
2727- src:
2828- "https://www.eei.cena.fr/products/ivy/download/packages/ivy-ocaml_1.3.1.tar.xz"
2929- checksum: [
3030- "sha256=b7b5d179f9ea2ca7cb8d135b75ed2a0236632759303fc307aca098985cffdeb6"
3131- "md5=02ce97a82f5a95b1b256095580b0fa85"
3232- ]
3333-}
3434-available: false # source tarball not available
-35
packages/javalib/javalib.2.3.1/opam
···11-opam-version: "2.0"
22-maintainer: "sawja@inria.fr"
33-homepage: "http://javalib.gforge.inria.fr"
44-authors: " "
55-build: [
66- ["./configure.sh"]
77- [make "ptrees"]
88-]
99-install: [
1010- [make "installptrees"]
1111- [make]
1212- [make "install"]
1313-]
1414-remove: [
1515- ["ocamlfind" "remove" "javalib"]
1616- ["ocamlfind" "remove" "ptrees"]
1717-]
1818-depends: [
1919- "ocaml" {< "5.0"}
2020- "ocamlfind"
2121- "camlzip" {= "1.05"}
2222- "extlib" {>= "1.5.1" & <= "1.6.0"}
2323-]
2424-synopsis:
2525- "Javalib is a library written in OCaml which aims at providing a high level representation of Java .class files."
2626-description: """
2727-Thus it stands for a good starting point for people who want to develop static analyses for
2828-Java byte-code programs, benefiting from the strength of OCaml language."""
2929-flags: light-uninstall
3030-url {
3131- src:
3232- "https://gforge.inria.fr/frs/download.php/file/34920/javalib-2.3.1.tar.bz2"
3333- checksum: "md5=31e33a2c462f8bbda79218f9041f3639"
3434-}
3535-available: false # source tarball not available
-38
packages/javalib/javalib.2.3.2/opam
···11-opam-version: "2.0"
22-maintainer: "sawja@inria.fr"
33-build: [
44- ["./configure.sh"]
55- [make "ptrees"]
66-]
77-#bug-reports: "sawja@inria.fr"
88-install: [
99- [make "installptrees"]
1010- [make]
1111- [make "install"]
1212-]
1313-bug-reports: "https://gforge.inria.fr/tracker/?atid=2815&group_id=686&func=browse"
1414-remove: [
1515- ["ocamlfind" "remove" "javalib"]
1616- ["ocamlfind" "remove" "ptrees"]
1717-]
1818-homepage: "http://sawja.inria.fr"
1919-depends: [
2020- "ocaml" {>= "4.00" & < "5.0"}
2121- "ocamlfind"
2222- "camlzip" {>= "1.05"}
2323- "camlp4"
2424- "extlib-compat" {< "1.7.0"}
2525-]
2626-synopsis:
2727- "Javalib is a library written in OCaml with the aim to provide a high level representation of Java .class files."
2828-description: """
2929-Thus it stands for a good starting point for people who want to develop static analyses for
3030-Java byte-code programs, benefiting from the strength of OCaml language."""
3131-authors: "Javalib development team"
3232-flags: light-uninstall
3333-url {
3434- src:
3535- "https://gforge.inria.fr/frs/download.php/file/36092/javalib-2.3.2.tar.bz2"
3636- checksum: "md5=17ec3fabb1472dd3324ec68fb63b22a6"
3737-}
3838-available: false # source tarball not available
-38
packages/javalib/javalib.2.3.3/opam
···11-opam-version: "2.0"
22-maintainer: "sawja@inria.fr"
33-build: [
44- ["./configure.sh"]
55- [make "ptrees"]
66-]
77-license: "LGPL-2.1-only WITH OCaml-LGPL-linking-exception"
88-install: [
99- [make "installptrees"]
1010- [make]
1111- [make "install"]
1212-]
1313-bug-reports: "https://gforge.inria.fr/tracker/?atid=2815&group_id=686&func=browse"
1414-remove: [
1515- ["ocamlfind" "remove" "javalib"]
1616- ["ocamlfind" "remove" "ptrees"]
1717-]
1818-homepage: "http://sawja.inria.fr"
1919-depends: [
2020- "ocaml" {>= "4.00" & < "4.06.0"}
2121- "ocamlfind"
2222- "camlzip" {>= "1.05"}
2323- "camlp4"
2424- "extlib-compat"
2525-]
2626-synopsis:
2727- "Javalib is a library written in OCaml with the aim to provide a high level representation of Java .class files."
2828-description: """
2929-Thus it stands for a good starting point for people who want to develop static analyses for
3030-Java byte-code programs, benefiting from the strength of OCaml language."""
3131-authors: "Javalib development team"
3232-flags: light-uninstall
3333-url {
3434- src:
3535- "https://gforge.inria.fr/frs/download.php/file/36307/javalib-2.3.3.tar.bz2"
3636- checksum: "md5=a4d4b06e8f4860db34c128e760fa8397"
3737-}
3838-available: false # source tarball not available
-38
packages/javalib/javalib.2.3.4/opam
···11-opam-version: "2.0"
22-maintainer: "sawja@inria.fr"
33-authors: "Javalib development team"
44-homepage: "http://sawja.inria.fr"
55-bug-reports: "https://gforge.inria.fr/tracker/?atid=2815&group_id=686&func=browse"
66-license: "LGPL-2.1-only WITH OCaml-LGPL-linking-exception"
77-build: [
88- ["./configure.sh"]
99- [make "ptrees"]
1010-]
1111-install: [
1212- [make "installptrees"]
1313- [make]
1414- [make "install"]
1515-]
1616-remove: [
1717- ["ocamlfind" "remove" "javalib"]
1818- ["ocamlfind" "remove" "ptrees"]
1919-]
2020-depends: [
2121- "ocaml" {>= "4.02" & < "5.0"}
2222- "ocamlfind"
2323- "camlzip" {>= "1.05"}
2424- "camlp4"
2525- "extlib-compat"
2626-]
2727-synopsis:
2828- "Javalib is a library written in OCaml with the aim to provide a high level representation of Java .class files."
2929-description: """
3030-Thus it stands for a good starting point for people who want to develop static analyses for
3131-Java byte-code programs, benefiting from the strength of OCaml language."""
3232-flags: light-uninstall
3333-url {
3434- src:
3535- "https://gforge.inria.fr/frs/download.php/file/37154/javalib-2.3.4.tar.bz2"
3636- checksum: "md5=4707eda130e41d1d7f0506cc0c77eff1"
3737-}
3838-available: false # source tarball not available
-39
packages/javalib/javalib.2.3.5/opam
···11-opam-version: "2.0"
22-maintainer: "sawja@inria.fr"
33-authors: "Javalib development team"
44-homepage: "http://sawja.inria.fr"
55-bug-reports: "https://gforge.inria.fr/tracker/?atid=2815&group_id=686&func=browse"
66-license: "LGPL-2.1-only WITH OCaml-LGPL-linking-exception"
77-build: [
88- ["./configure.sh"]
99- [make "ptrees"]
1010-]
1111-install: [
1212- [make "installptrees"]
1313- [make]
1414- [make "install"]
1515-]
1616-remove: [
1717- ["ocamlfind" "remove" "javalib"]
1818- ["ocamlfind" "remove" "ptrees"]
1919-]
2020-depends: [
2121- "ocaml" {>= "4.02" & < "5.0"}
2222- "ocamlfind"
2323- "camlzip" {>= "1.05"}
2424- "camlp4"
2525- "extlib"
2626- "camomile" {< "2.0.0"}
2727-]
2828-synopsis:
2929- "Javalib is a library written in OCaml with the aim to provide a high level representation of Java .class files."
3030-description: """
3131-Thus it stands for a good starting point for people who want to develop static analyses for
3232-Java byte-code programs, benefiting from the strength of OCaml language."""
3333-flags: light-uninstall
3434-url {
3535- src:
3636- "https://gforge.inria.fr/frs/download.php/file/37655/javalib-2.3.5.tar.bz2"
3737- checksum: "md5=7111616e58b366ca269baf4867677082"
3838-}
3939-available: false # source tarball not available
···11-opam-version: "2.0"
22-maintainer:
33- "Bruno Blanchet <bruno.blanchet@inria.fr>, Marc Sylvestre <marc.sylvestre@inria.fr>"
44-authors:
55- "Bruno Blanchet <bruno.blanchet@inria.fr>, Vincent Cheval <vincent.cheval@icloud.com>, Ben Smyth <research@bensmyth.com>, Marc Sylvestre <marc.sylvestre@inria.fr>"
66-homepage: "http://proverif.inria.fr/"
77-bug-reports: "bruno.blanchet@inria.fr"
88-license: "GPL-1.0-or-later"
99-build: [
1010- ["./build" "ocb.byte"] {!ocaml:native}
1111- ["./build" "ocb.native"] {ocaml:native}
1212-]
1313-install: [ "./build" "install" "%{prefix}%" ]
1414-1515-remove: [
1616- [ "rm" "-rf"
1717- "%{prefix}%/doc/proverif"
1818- "%{prefix}%/bin/proverif"
1919- "%{prefix}%/bin/proveriftotex"
2020- "%{prefix}%/bin/proverif.exe"
2121- "%{prefix}%/bin/proveriftotex.exe"
2222- ]
2323-]
2424-depends: [
2525- "ocaml" {< "4.06.0"}
2626- "ocamlfind"
2727- "ocamlbuild"
2828-]
2929-depexts: [
3030- [[] ["graphviz"] ]
3131-]
3232-synopsis: "ProVerif: Cryptographic protocol verifier in the symbolic model"
3333-description: """
3434-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:
3535-3636-- 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.
3737-3838-- 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.
3939-4040-This verifier can prove the following properties:
4141-4242-- secrecy (the adversary cannot obtain the secret, CSFW'01)
4343-- authentication and more generally correspondence properties (Journal of Computer Security, 17(4):363-434, 2009)
4444-- strong secrecy (the adversary does not see the difference when the value of the secret changes, IEEE S&P'04)
4545-- equivalences between processes that differ only by terms (Journal of Logic and Algebraic Programming, 75(1):3-51, 2008 with Martín Abadi and Cédric Fournet)"""
4646-flags: light-uninstall
4747-url {
4848- src: "http://proverif.inria.fr/proverif1.97.tar.gz"
4949- checksum: "md5=7cc9cefde0178e75e1e69c2c146b5e3a"
5050-}
5151-available: false # source tarball not available
-55
packages/proverif/proverif.1.97pl1/opam
···11-opam-version: "2.0"
22-maintainer:
33- "Bruno Blanchet <bruno.blanchet@inria.fr>, Marc Sylvestre <marc.sylvestre@inria.fr>"
44-authors:
55- "Bruno Blanchet <bruno.blanchet@inria.fr>, Vincent Cheval <vincent.cheval@icloud.com>, Ben Smyth <research@bensmyth.com>, Marc Sylvestre <marc.sylvestre@inria.fr>"
66-homepage: "http://proverif.inria.fr/"
77-bug-reports: "bruno.blanchet@inria.fr"
88-license: "GPL-1.0-or-later"
99-build: [
1010- ["./build" "ocb.byte"] {!ocaml:native}
1111- ["./build" "ocb.native"] {ocaml:native}
1212-]
1313-install: [ "./build" "install" "%{prefix}%" ]
1414-1515-remove: [
1616- [ "rm" "-rf"
1717- "%{prefix}%/doc/proverif"
1818- "%{prefix}%/bin/proverif"
1919- "%{prefix}%/bin/proveriftotex"
2020- "%{prefix}%/bin/proverif.exe"
2121- "%{prefix}%/bin/proveriftotex.exe"
2222- ]
2323-]
2424-depends: [
2525- "ocaml" {< "4.06.0"}
2626- "ocamlfind"
2727- "ocamlbuild"
2828-]
2929-depexts: [
3030- [[] ["graphviz"] ]
3131-]
3232-synopsis: "ProVerif: Cryptographic protocol verifier in the symbolic model"
3333-description: """
3434-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:
3535-3636-- 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.
3737-3838-- 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.
3939-4040-ProVerif can prove the following properties:
4141-4242-- secrecy (the adversary cannot obtain the secret)
4343-- authentication and more generally correspondence
4444-- strong secrecy (the adversary does not see the difference when the value of the secret changes)
4545-- equivalences between processes that differ only by terms
4646-4747-A survey of ProVerif with references to other papers is available at
4848-4949-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"""
5050-flags: light-uninstall
5151-url {
5252- src: "http://proverif.inria.fr/proverif1.97pl1.tar.gz"
5353- checksum: "md5=d41ad700772545c8a5d618c7889a1500"
5454-}
5555-available: false # source tarball not available
-51
packages/proverif/proverif.1.97pl3/opam
···11-opam-version: "2.0"
22-maintainer:
33- "Bruno Blanchet <bruno.blanchet@inria.fr>, Marc Sylvestre <marc.sylvestre@inria.fr>"
44-authors:
55- "Bruno Blanchet <bruno.blanchet@inria.fr>, Vincent Cheval <vincent.cheval@icloud.com>, Ben Smyth <research@bensmyth.com>, Marc Sylvestre <marc.sylvestre@inria.fr>"
66-homepage: "http://proverif.inria.fr/"
77-bug-reports: "bruno.blanchet@inria.fr"
88-license: "GPL-1.0-or-later"
99-build: [
1010- ["./build" "ocb.byte"] {!ocaml:native}
1111- ["./build" "ocb.native"] {ocaml:native}
1212-]
1313-install: [ "./build" "install" "%{prefix}%" ]
1414-1515-remove: [
1616- [ "rm" "-rf"
1717- "%{prefix}%/doc/proverif"
1818- "%{prefix}%/bin/proverif"
1919- "%{prefix}%/bin/proveriftotex"
2020- "%{prefix}%/bin/proverif.exe"
2121- "%{prefix}%/bin/proveriftotex.exe"
2222- ]
2323-]
2424-depends: ["ocaml" "ocamlfind" "ocamlbuild"]
2525-depexts: [
2626- [[] ["graphviz"] ]
2727-]
2828-synopsis: "ProVerif: Cryptographic protocol verifier in the symbolic model"
2929-description: """
3030-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:
3131-3232-- 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.
3333-3434-- 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.
3535-3636-ProVerif can prove the following properties:
3737-3838-- secrecy (the adversary cannot obtain the secret)
3939-- authentication and more generally correspondence
4040-- strong secrecy (the adversary does not see the difference when the value of the secret changes)
4141-- equivalences between processes that differ only by terms
4242-4343-A survey of ProVerif with references to other papers is available at
4444-4545-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"""
4646-flags: light-uninstall
4747-url {
4848- src: "http://proverif.inria.fr/proverif1.97pl3.tar.gz"
4949- checksum: "md5=947a428f71cc335aeea8d178c1e8e84f"
5050-}
5151-available: false # source tarball not available
-29
packages/sawja/sawja.1.5.1/opam
···11-opam-version: "2.0"
22-maintainer: "sawja@inria.fr"
33-homepage: "http://javalib.gforge.inria.fr"
44-authors: " "
55-build: [
66- ["./configure.sh"]
77- [make]
88-]
99-install: [make "install"]
1010-remove: [
1111- ["ocamlfind" "remove" "sawja"]
1212-]
1313-depends: [
1414- "ocaml" { < "5.0.0" }
1515- "ocamlfind"
1616- "javalib" {= "2.3.1"}
1717-]
1818-synopsis:
1919- "Provide a high level representation of Java bytecode programs and static analysis tools."
2020-description: """
2121-Sawja is a library written in OCaml, relying on Javalib to provide a high level representation of Java bytecode programs. Its name stands for Static Analysis Workshop for JAva. Whereas Javalib is dedicated to isolated classes, Sawja handles bytecode programs with their class hierarchy and control flow algorithms.
2222-Moreover, Sawja provides some stackless intermediate representations of code, called JBir and A3Bir. The transformation algorithm, common to these representations, has been formalized and proved to be semantics-preserving."""
2323-flags: light-uninstall
2424-url {
2525- src:
2626- "https://gforge.inria.fr/frs/download.php/file/34921/sawja-1.5.1.tar.bz2"
2727- checksum: "md5=3a9b750faa7a368ec6aaaa0206fac40b"
2828-}
2929-available: false # source tarball not available
-34
packages/sawja/sawja.1.5.2/opam
···11-opam-version: "2.0"
22-maintainer: "sawja@inria.fr"
33-build: [
44- ["./configure.sh"]
55- [make]
66-]
77-remove: [
88- ["ocamlfind" "remove" "sawja"]
99-]
1010-license: "GPL-3.0-only"
1111-install: [
1212- [make "install"]
1313-]
1414-bug-reports: "https://gforge.inria.fr/tracker/?atid=2815&group_id=686&func=browse"
1515-homepage: "http://sawja.inria.fr"
1616-depends: [
1717- "ocaml" {>= "4.00" & < "4.06.0"}
1818- "ocamlfind" {build}
1919- "conf-perl" {build}
2020- "javalib" {>= "2.3.2" & <= "2.3.5"}
2121-]
2222-synopsis:
2323- "Provide a high level representation of Java bytecode programs and static analysis tools"
2424-description: """
2525-Sawja is a library written in OCaml, relying on Javalib to provide a high level representation of Java bytecode programs. Its name stands for Static Analysis Workshop for JAva. Whereas Javalib is dedicated to isolated classes, Sawja handles bytecode programs with their class hierarchy and control flow algorithms.
2626-Moreover, Sawja provides some stackless intermediate representations of code, called JBir and A3Bir. The transformation algorithm, common to these representations, has been formalized and proved to be semantics-preserving."""
2727-authors: "Sawja development team"
2828-flags: light-uninstall
2929-url {
3030- src:
3131- "https://gforge.inria.fr/frs/download.php/file/36093/sawja-1.5.2.tar.bz2"
3232- checksum: "md5=12afa3651ea39413d2cb0e1775f587c4"
3333-}
3434-available: false # source tarball not available
-34
packages/sawja/sawja.1.5.3/opam
···11-opam-version: "2.0"
22-maintainer: "sawja@inria.fr"
33-build: [
44- ["./configure.sh"]
55- [make]
66-]
77-remove: [
88- ["ocamlfind" "remove" "sawja"]
99-]
1010-bug-reports: "sawja@inria.fr"
1111-install: [
1212- [make "install"]
1313-]
1414-homepage: "http://sawja.inria.fr"
1515-depends: [
1616- "ocaml" {>= "4.02" & < "5.0.0"}
1717- "ocamlfind" {build}
1818- "conf-perl" {build}
1919- "javalib" {>= "2.3.4" & <= "2.3.5"}
2020- "extlib-compat" {>= "1.7.0"}
2121-]
2222-synopsis:
2323- "Provide a high level representation of Java bytecode programs and static analysis tools"
2424-description: """
2525-Sawja is a library written in OCaml, relying on Javalib to provide a high level representation of Java bytecode programs. Its name stands for Static Analysis Workshop for JAva. Whereas Javalib is dedicated to isolated classes, Sawja handles bytecode programs with their class hierarchy and control flow algorithms.
2626-Moreover, Sawja provides some stackless intermediate representations of code, called JBir and A3Bir. The transformation algorithm, common to these representations, has been formalized and proved to be semantics-preserving."""
2727-authors: "Sawja development team"
2828-flags: light-uninstall
2929-url {
3030- src:
3131- "https://gforge.inria.fr/frs/download.php/file/37403/sawja-1.5.3.tar.bz2"
3232- checksum: "md5=25ff421a3f932881234ed5b05b94ac8d"
3333-}
3434-available: false # source tarball not available