Publicacoes - INESC TEC

Publicações

Publicações por José Bacelar Almeida

2009

Verifying Cryptographic Software Correctness with Respect to Reference Implementations

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

Publicação
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.

FecharLer Abstract

2009

Deductive Verification of Cryptographic Software

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

Publicação
First NASA Formal Methods Symposium - NFM 2009, Moffett Field, California, USA, April 6-8, 2009.

Abstract

2023

Formally verifying Kyber Part I: Implementation Correctness

Autores
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;

Publicação
IACR Cryptol. ePrint Arch.

Abstract

2021

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

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

Publicação
IACR Cryptol. ePrint Arch.

Abstract

2021

Towards Formal Verification of Password Generation Algorithms used in Password Managers

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

Publicação
CoRR

Abstract

2021

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

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

Publicação
CoRR

Abstract