CiVerLy helps you analyze primitives from symmetric cryptography.
First, implement the cipher in the format CiVerLy expects. CiVerLy can then automatically apply methods from the academic literature to generate mixed-integer linear programming (MILP) or satisfiability (SAT) models that describe the linear or differential properties of the cipher. Solving these models produces linear or differential trails, which allow you to assess the security of the primitive. Check out the ciphers already implemented in CiVerLy for examples.
CiVerLy is built on SageMath and is intentionally modular. For example, model generation and solving are separable, so they can run on different machines. The modular design also makes it easy to extend CiVerLy (for instance, to integrate additional cryptographic techniques).
This project was developed by cryptosolutions GmbH on behalf of the German Federal Office for Information Security (BSI). As part of the effort to strengthen IT security, CiVerLy has been released as open-source software and made freely available to the scientific community.
See docs/build/ for the reference manual (HTML and PDF).
This project is licensed under the EUROPEAN UNION PUBLIC LICENCE v. 1.2 (EUPL 1.2) with an additional non-endorsement clause; see LICENSE for details.