···

       
1
       
1
       
+
       
opam-version: "2.0"

     

       
2
       
2
       
+
       
synopsis: "CryptoVerif: Cryptographic protocol verifier in the computational model"

     

       
3
       
3
       
+
       
description: """

     

       
4
       
4
       
+
       
CryptoVerif is an automatic protocol prover sound in the computational model. It can prove

     

       
5
       
5
       
+
       


     

       
6
       
6
       
+
       
  - secrecy;

     

       
7
       
7
       
+
       
  - correspondences, which include in particular authentication;

     

       
8
       
8
       
+
       
  - indistinguishability between two games.

     

       
9
       
9
       
+
       


     

       
10
       
10
       
+
       
It provides a generic mechanism for specifying the security assumptions on cryptographic primitives, which can handle in particular symmetric encryption, message authentication codes, public-key encryption, signatures, hash functions.

     

       
11
       
11
       
+
       


     

       
12
       
12
       
+
       
The generated proofs are proofs by sequences of games, as used by cryptographers. These proofs are valid for a number of sessions polynomial in the security parameter, in the presence of an active adversary. CryptoVerif can also evaluate the probability of success of an attack against the protocol as a function of the probability of breaking each cryptographic primitive and of the number of sessions (exact security).

     

       
13
       
13
       
+
       


     

       
14
       
14
       
+
       
This software is under development; please use it at your own risk. Comments and bug reports welcome. 

     

       
15
       
15
       
+
       
"""

     

       
16
       
16
       
+
       
maintainer: "Bruno Blanchet <Bruno.Blanchet@inria.fr>"

     

       
17
       
17
       
+
       
authors: "Bruno Blanchet <Bruno.Blanchet@inria.fr> and David Cadé <David.Cade@normalesup.org>"

     

       
18
       
18
       
+
       
license: "CECILL-B"

     

       
19
       
19
       
+
       
homepage: "https://cryptoverif.inria.fr"

     

       
20
       
20
       
+
       
dev-repo: "git+https://gitlab.inria.fr/bblanche/CryptoVerif.git"

     

       
21
       
21
       
+
       
bug-reports: "Bruno.Blanchet@inria.fr"

     

       
22
       
22
       
+
       
depends: [ "ocaml" { >= "4.03" } "ocamlfind" { post } "cryptokit" { post } "conf-m4" { post } ]

     

       
23
       
23
       
+
       
build: [

     

       
24
       
24
       
+
       
       [ "./build" "byte" { !ocaml:native } ] 

     

       
25
       
25
       
+
       
]

     

       
26
       
26
       
+
       
install: [ "./build" "install" "%{prefix}%" ]

     

       
27
       
27
       
+
       
url {

     

       
28
       
28
       
+
       
  src: "https://cryptoverif.inria.fr/cryptoverif2.06.tar.gz"

     

       
29
       
29
       
+
       
  checksum: "md5=44c641a07abb652e6299c7ac71a8945c"

     

       
30
       
30
       
+
       
}