wolf-lc1 / cryptoverif Goto Github PK
View Code? Open in Web Editor NEWThis project forked from mgrabovsky/cryptoverif
Python implementations for CryptoVerif 1.23 (outdated)
License: Other
This project forked from mgrabovsky/cryptoverif
Python implementations for CryptoVerif 1.23 (outdated)
License: Other
Cryptographic protocol verifier, copyright ENS, CNRS, INRIA, by Bruno Blanchet and David Cadé, 2005-2016 ENS: Ecole Normale Supérieure, 45 rue d'Ulm, 75005 Paris, France CNRS: Centre Nationale de la Recherche Scientifique INRIA: Institut National de Recherche en Informatique et Automatique Domaine de Voluceau - Rocquencourt - B.P. 105 - 78153 Le Chesnay This package contains source files, documentation, and examples of a cryptographic protocol verifier. The material contained in this package is under the CeCILL-B license. (The CeCILL-B license is a BSD-style license. See the file LICENSE for more information.) This software can be used to prove secrecy and authentication properties of cryptographic protocols, in the computational model. (If you want a verifier for the Dolev-Yao model, please download ProVerif.) INSTALL To run this software, you need Objective Caml version 3.00 or higher. Objective Caml can be downloaded from http://caml.inria.fr * under Unix or cygwin Uncompress the archive using tar: gunzip cryptoverif1.23.tar.gz tar -xf cryptoverif1.23.tar or if you have GNU tar: tar -xzf cryptoverif1.23.tar.gz This will create a directory named cryptoverif1.23 in the current directory. Go into this directory, and build the programs: cd cryptoverif1.23 ./build * under Windows NT, 2000, or XP (without cygwin) The recommended way is to use the precompiled binaries for Windows, available as a separate distribution. In order to run implementations of protocols generated by CryptoVerif, you need to have the Caml cryptographic library "cryptokit" installed. This library is available at http://forge.ocamlcore.org/projects/cryptokit/ You need to either - arrange so that the installed cryptokit library is in subdirectory "implementation/cryptokit" of the CryptoVerif distribution (possibly via a symbolic link) - or install the cryptokit library in the "cryptokit" subdirectory of the Caml standard library - or modify the variable CRYPTOKIT in the scripts implementation/npsk/build.sh implementation/wlsk/build_wlsk.sh implementation/ssh/build.sh so that the cryptokit library is included. USAGE This software contains one executable program, cryptoverif. It takes as input a description of a cryptographic protocol, and checks whether it can leak some secrets. The subdirectory examples contains examples of cryptographic protocols. To run CryptoVerif on example X, execute ./cryptoverif examples/X e.g. ./cryptoverif examples/otway-rees3Stream Note: CryptoVerif must be run in the directory that contains the files "default.cvl" and "default.ocvl" (which is the cryptoverif1.23 directory). CryptoVerif accesses these files which contain definitions of cryptographic primitives. COPYRIGHT This software is distributed under CeCILL-B license. The CeCILL-B license is a BSD-style license. See the file LICENSE for more information. BUG REPORTS Bugs and comments should be reported by e-mail to [email protected] ACKNOWLEDGMENTS I warmly thank David Pointcheval for his advice and explanations of the computational proofs of protocols. This project would not have been possible without him. This project was partly supported by ARA SSIA Formacrypt and is partly supported by the ANR project ProSe (decision ANR-2010-VERS-004-01).
A declarative, efficient, and flexible JavaScript library for building user interfaces.
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
An Open Source Machine Learning Framework for Everyone
The Web framework for perfectionists with deadlines.
A PHP framework for web artisans
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
Some thing interesting about web. New door for the world.
A server is a program made to process requests and deliver data to clients.
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
Some thing interesting about visualization, use data art
Some thing interesting about game, make everyone happy.
We are working to build community through open source technology. NB: members must have two-factor auth.
Open source projects and samples from Microsoft.
Google ❤️ Open Source for everyone.
Alibaba Open Source for everyone
Data-Driven Documents codes.
China tencent open source team.