Publications

Publications by José Bacelar Almeida

2009

Verifying Cryptographic Software Correctness with Respect to Reference Implementations

Authors
Almeida, JB; Barbosa, M; Pinto, JS; Vieira, B;

Publication
FORMAL METHODS FOR INDUSTRIAL CRITICAL SYSTEMS

Abstract
This paper presents techniques developed to check program equivalences in the context of cryptographic software development, where specifications are typically reference implementations. The techniques allow for the integration of interactive proof techniques (required given the difficulty and generality of the results sought) in a verification infrastructure that is capable of discharging many verification conditions automatically. To this end, the difficult results in the verification process (to be proved interactively) are isolated as a set of lemmas. The fundamental notion of natural invariant is used to link the specification level and the interactive proof construction process.

CloseRead Abstract

2009

Deductive Verification of Cryptographic Software

Authors
Barbosa, M; Almeida, JB; Pinto, JS; Vieira, B;

Publication
First NASA Formal Methods Symposium - NFM 2009, Moffett Field, California, USA, April 6-8, 2009.

Abstract

2023

Formally verifying Kyber Part I: Implementation Correctness

Authors
Almeida, JB; Barbosa, M; Barthe, G; Grégoire, B; Laporte, V; Léchenet, JC; Oliveira, T; Pacheco, H; Quaresma, M; Schwabe, P; Séré, A; Strub, PY;

Publication
IACR Cryptol. ePrint Arch.

Abstract

2021

Machine-checked ZKP for NP-relations: Formally Verified Security Proofs and Implementations of MPC-in-the-Head

Authors
Almeida, JB; Barbosa, M; Correia, ML; Eldefrawy, K; Lengrand, SG; Pacheco, H; Pereira, V;

Publication
IACR Cryptol. ePrint Arch.

Abstract

2021

Towards Formal Verification of Password Generation Algorithms used in Password Managers

Authors
Grilo, M; Ferreira, JF; Almeida, JB;

Publication
CoRR

Abstract

2021

Machine-checked ZKP for NP-relations: Formally Verified Security Proofs and Implementations of MPC-in-the-Head

Authors
Bacelar Almeida, JC; Barbosa, M; Eldefrawy, K; Lengrand, SG; Pacheco, H; Pereira, V;

Publication
CoRR

Abstract