CryptoVampire is an automated, computationally sound protocol verifier. It turns a protocol specification into an smt file to be proven by some other FOL theorem prover.
It can run standalone (see Usage) or through squirrel (see Squirrel).
CryptoVampire is a plain rust project, so it can be installed via cargo.
$ cargo install --git https://github.com/SecPriv/CryptoVampireYou can use the same command to update.
This repository is a nix flake, therefore:
# get a shell with cryptovampire
$ nix shell github:SecPriv/CryptoVampire
# run cryptovampire
$ nix run github:SecPriv/CryptoVampire -- <args>Then, as with all rust projects, you can compile or run it using cargo:
# compile
cargo build --release
# run
cargo run --release -- <args>NB: Windows and squirrel users:
For this project, cargo will write to /tmp/ccsa/build/dir, thus the executable will be built in /tmp/ccsa/build/dir/release/cryptovampire (resp. /tmp/ccsa/build/dir/debug/cryptovampire) when the --release flag was given (resp. was not given) to cargo. You can override the location of the build directory using the --target-dir <dir> flag to cargo.
NB: release vs debug
Compiling with debug makes the program very eager to crash instead of trying to recover. Especially when reading vampire's output this can lead to crashes that are recovered from in --release mode.
This project is set up to work with nix as well.
nix develop brings you into a shell with all the tools available (cargo, vampire, z3, cvc5, ...). Note that we couldn't get the modified version of vampire to compile using nix; therefore, to use it, you will have to build it yourself from vampire's repository.
Works as expected.
Usability is known to be somewhat poor at the moment.
To use cryptovampire effectively, you will need SMT solvers like (in order of preference) vampire, z3, cvc5, or any other smtlib 2.6 compliant first-order theorem prover.
cryptovampire can run on its own with vampire, z3 and it can learn some information about the runs done with vampire (see auto).
To get the specifics of the command line interface, run:
$ cryptovampire --helpBy default, cryptovampire runs in auto mode with all the solvers it can find in the path, taking a file from the standard input and outputting to the standard output. It may write temporary files wherever the operating system tells it to.
Use the auto command to run in auto mode; run cryptovampire auto --help for more information and see the section auto.
To export to an smt file (or possibly many smt files), use the to-file command. See the to-file section and run cryptovampire to-file --help for more information.
To get the specifics of the command line interface, run:
$ cryptovampire auto --helpIn this mode, cryptovampire attempts to prove everything without user intervention by calling the solvers on its own with (somewhat) optimized files.
--timeout: sets the timeout for all the solvers (default 1s)--num-of-retry:cryptovampirecan learn how to apply the cryptography from runs performed byvampire. This parameter sets how many times it tries (default5).--lemmas: with this flag,cryptovampirewill attempt to prove thelemmaformula of the input file and subsequently use it for the final proof. If any of the lemmas fail,cryptovampirefails. When this option is not activated,cryptovampirestill uses the lemmas as hints to apply cryptographic axioms.
NB:
cryptovampirefails if a solver terminates for an unexplainable reason (e.g., a syntax error). This can cause problems when using older versions of the solver that do not yet support some of their own extensions to thesmtformat. This is notably the case with older versions ofvampire.
To get the specifics of the command line interface, run:
$ cryptovampire to-file --helpRenders one (or many when activating the lemmas) smt file. Without the -o flag, it outputs to the standard output, letting the user pipe the result into the solver of their choice.
NB:
- To get a fully
smtlib-compliant file, use the--cvc5option. Otherwise, the tool will aim for files readable by the latest releasedvampireandz3. Other options make the tool aim for specific versions ofvampire.
NB: mostly broken currently. (squirrel considers a cryptovampire success as a failure)
It is possible to run cryptovampire from the squirrel proof assistant. It will then use the auto mode with default parameters.
To use it, you need to compile squirrel using the cryptovampire branch (available here) and have the cryptovampire executable either available on your PATH or pointed to by the environment variable CRYPTOVAMPIRE_EXECUTABLE.
You will then get access to the cryptovampire tactic. You can also add the optional parameters nt and t to control --num-of-retry and --timeout, respectively.
NB:
- The solvers need to be available in the path.
- It can only work on local goals.
- Like the
smttactic, it doesn't look in the environment for lemmas already proven or admitted axioms. You will need to use theusetactic to explicitly make them available tocryptovampire. - The macros
execandframeare not supported (yet). Theattfunction isn't either. cryptovampirecasts everything to eitherindexormessage, therefore weirder uses of those sorts will lead to failures.- It does support biprocesses and will try to check both sides of the biprocess.
- Unlike
smt, it can use cryptography. - It doesn't support higher-order functions; it will fail if it encounters any.
- for testing purposes, setting
SQUIRREL_CRYPTOVAMPIRE_FORCE_QUANTUMto anything declares the tactic as quantum sound.
Please report any error that isn't "ran out of tries".
You can see example files in the tests directory (all those ending in .ptcl). In particular the files in test/nix, are tested by the CI/CD, so they should ™️ be fully working.
Infix functions don't really exist (yet); therefore, the parser uses parentheses to fake them (e.g., you need to use (a = b) instead of just a = b).
The tool will try to point out any mistakes while reporting where they come from as best as it can.
NB:
- Parsing relies on
pest(for better or worse). You can find the grammar in grammar.pest.