CoqCryptoLine: A Verified Model Checker with Certified Results

This is an artifact created for TACAS 2023 submission: CoqCryptoLine: A Verified Model Checker with Certified Results. We present the verified model checker CoqCryptoLine for cryptographic programs with certified verification results. The CoqCryptoLine tool is built on the OCaml programs extracted from verified reductions. We evaluate CoqCryptoLine on cryptographic programs from industrial security libraries. This artifact contains CoqCryptoLine, CryptoLine, walkthrough examples, and benchmarks used to replicate the experimental results (Table 1) in the paper. This artifact is intended to run on TACAS 2023 Artifact Evaluation Virtual Machine for VirtualBox. Instructions of running experiments are available in Readme.txt