CoqCryptoLine: A Verified Model Checker with Certified Results

We present the verified model checker CoqCryptoLine for cryptographic programs with certified verification results. The CoqCryptoLine verification algorithm consists of two reductions. The algebraic reduction transforms into a root entailment problem; and the bit-vector reduction transforms into an SMT QF_BV problem. We specify and verify both reductions formally using Coq with SSReflect. The CoqCryptoLine tool is built on the OCaml programs extracted from verified reductions. CoqCryptoLine moreover employs certified techniques for solving the algebraic and logic problems. We evaluate CoqCryptoLine on cryptographic programs from industrial security libraries. This artifact is intended to run on TACAS 2023 Artifact Evaluation Virtual Machine for VirtualBox. Instructions of running experiments are available in Readme.txt