Publicacoes - INESC TEC

Publicações

Publicações por José Bacelar Almeida

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 Episode IV: 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 Trans. Cryptogr. Hardw. Embed. Syst.

Abstract
In this paper we present the first formally verified implementations of Kyber and, to the best of our knowledge, the first such implementations of any post-quantum cryptosystem. We give a (readable) formal specification of Kyber in the EasyCrypt proof assistant, which is syntactically very close to the pseudocode description of the scheme as given in the most recent version of the NIST submission. We present high-assurance open-source implementations of Kyber written in the Jasmin language, along with machine-checked proofs that they are functionally correct with respect to the EasyCrypt specification. We describe a number of improvements to the EasyCrypt and Jasmin frameworks that were needed for this implementation and verification effort, and we present detailed benchmarks of our implementations, showing that our code achieves performance close to existing hand-optimized implementations in C and assembly.

FecharLer 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

2019

Machine-Checked Proofs for Cryptographic Standards

Autores
Almeida, JB; Ruet, CB; Barbosa, M; Barthe, G; Dupressoir, F; Grégoire, B; Laporte, V; Oliveira, T; Stoughton, A; Strub, PY;

Publicação
IACR Cryptol. ePrint Arch.

Abstract