Jazzline: Composable CryptoLine Functional Correctness Proofs for Jasmin Programs

José Bacelar Almeida; Manuel Barbosa; Gilles Barthe; Lionel Blatter; Gustavo Delerue; João Diogo Duarte; Benjamin Gregoire; Tiago Oliveira; Miguel Quaresma; Pierre-Yves Strub; Ming-Hsien Tsai; Bow-Yaw Wang; Bo-Yin Yang

Paper 2026/2815

Jazzline: Composable CryptoLine Functional Correctness Proofs for Jasmin Programs

José Bacelar Almeida

, University of Minho, INESC TEC

Manuel Barbosa

, University of Porto, INESC TEC, Max Planck Institute for Security and Privacy

Gilles Barthe

, Max Planck Institute for Security and Privacy, IMDEA Software

Lionel Blatter

, Max Planck Institute for Security and Privacy

Gustavo Delerue

, University of Porto, PQShield

João Diogo Duarte

, University of Porto, INESC TEC

Benjamin Gregoire

, Inria Sophia-Antipolis

Tiago Oliveira

, Sandbox AQ

Miguel Quaresma

, Max Planck Institute for Security and Privacy

Pierre-Yves Strub

, PQShield

Ming-Hsien Tsai

, National Taiwan University of Science and Technology

Bow-Yaw Wang

, Academia Sinica

Bo-Yin Yang

, Academia Sinica

Abstract

Jasmin is a programming language for high-speed and high-assurance cryptography. Correctness proofs of Jasmin programs are typically carried out deductively in EasyCrypt. This allows generality, modularity and composable reasoning, but does not scale well for low-level architecture-specific routines. CryptoLine offers a semi-automatic approach to formally verify algebraically-rich low-level cryptographic routines. CryptoLine proofs are self-contained: they are not integrated into higher-level formal verification developments. This paper shows how to soundly use CryptoLine to discharge subgoals in functional correctness proofs for complex Jasmin programs. We extend Jasmin with annotations and provide an automatic translation into a CryptoLine model, where most complex transformations are certified. We also formalize and implement the automatic extraction of the semantics of a CryptoLine proof

Note: Author version of a paper published at ACM CCS 2025 (https://doi.org/10.1145/3719027.3744814). Artifact available at https://doi.org/10.5281/zenodo.16604163.

Metadata

Available format(s): PDF
Category: Implementation
Publication info: Published elsewhere. ACM CCS 2025
DOI: 10.1145/3719027.3744814
Keywords: Formal Verification EasyCrypt Jasmin CryptoLine X-Wing Hybrid KEM
Contact author(s): jb @ di uminho pt
mbb @ fc up pt
gilles barthe @ mpi-sp org
lionel blatter @ mpi-sp org
gustavo delerue @ pqshield com
joao @ diogoduarte pt
benjamin gregoire @ inria fr
tiago oliveira @ sandboxquantum com
miguel quaresma @ mpi-sp org
pierre-yves strub @ pqshield com
mhtsai @ cs ntust edu tw
bywang @ iis sinica edu tw
byyang @ iis sinica edu tw
History: 2026-11-10: approved; 2026-11-07: received; See all versions
Short URL: https://ia.cr/2026/2815
License: CC BY

BibTeX

@misc{cryptoeprint:2026/2815,
      author = {José Bacelar Almeida and Manuel Barbosa and Gilles Barthe and Lionel Blatter and Gustavo Delerue and João Diogo Duarte and Benjamin Gregoire and Tiago Oliveira and Miguel Quaresma and Pierre-Yves Strub and Ming-Hsien Tsai and Bow-Yaw Wang and Bo-Yin Yang},
      title = {Jazzline: Composable {CryptoLine} Functional Correctness Proofs for Jasmin Programs},
      howpublished = {Cryptology {ePrint} Archive, Paper 2026/2815},
      year = {2026},
      doi = {10.1145/3719027.3744814},
      url = {https://eprint.iacr.org/2026/2815}
}