2 papers
cs.PL2025
KEM-IND-CCA-Preserving Compilation of Jasmin's ML-KEM
Santiago Arranz-Olmos, Gilles Barthe, Lionel Blatter +4
High-assurance cryptography provides strong guarantees that source implementations are functionally correct and provably secure. In this paper, we demonstrate that the Jasmin compi…
cs.LO2025
A quantitative probabilistic relational Hoare logic
Martin Avanzini, Gilles Barthe, Davide Davoli +1
We introduce eRHL, a program logic for reasoning about relational expectation properties of pairs of probabilistic programs. eRHL is quantitative, i.e., its pre- and post-condition…