Data | Título | Autor(es) | Tipo | Acesso |
2020 | Certified compilation for cryptography: Extended x86 instructions and constant-time verification | Almeida, José Bacelar; Barbosa, Manuel; Barthe, Gilles, et al. | Artigo em ata de conferência | Acesso aberto |
2013 | Certified computer-aided cryptography: efficient provably secure machine code from high-level implementations | Almeida, José Bacelar; Barbosa, Manuel; Barthe, Gilles Jacques Denis, et al. | Artigo em ata de conferência | Acesso aberto |
1999 | Constructor subtyping | Barthe, Gilles Jacques Denis; Frade, M. J. | Artigo em ata de conferência | Acesso aberto |
Jun-1999 | Constructor subtyping: extended version | Frade, M. J.; Barthe, Gilles Jacques Denis | Relatório | Acesso aberto |
30-Out-2017 | A fast and verified software stack for secure function evaluation | Almeida, José Bacelar; Barbosa, Manuel; Barthe, Gilles Jacques Denis, et al. | Artigo em ata de conferência | Acesso aberto |
2012 | Full proof cryptography: verifiable compilation of efficient zero-knowledge protocols | Almeida, José Bacelar; Barbosa, Manuel; Bangerter, Endre, et al. | Artigo em ata de conferência | Acesso aberto |
2018 | hnforcing ideal-world leakage bounds in real-world secret sharing MPC frameworks | Almeida, José Bacelar; Barbosa, Manuel; Barthe, Gilles, et al. | Artigo em ata de conferência | Acesso aberto |
2019 | A machine-checked proof of security for AWS key management service | Almeida, José Bacelar; Barbosa, Manuel; Barthe, Gilles, et al. | Artigo em ata de conferência | Acesso aberto |
2019 | Machine-checked proofs for cryptographic standards indifferentiability of SPONGE and secure high-assurance implementations of SHA-3 | Almeida, José Bacelar; Baritel-Ruet, Cecile; Barbosa, Manuel, et al. | Artigo em ata de conferência | Acesso aberto |
2020 | The last mile: High-Assurance and High-Speed cryptographic implementations | Almeida, José Bacelar; Barbosa, Manuel; Barthe, Gilles, et al. | Artigo em ata de conferência | Acesso aberto |
2004 | Type-based termination of recursive definitions | Barthe, Gilles Jacques Denis; Frade, M. J.; Giménez, E., et al. | Artigo | Acesso aberto |
Jul-2016 | Verifiable side-channel security of cryptographic implementations: constant-time MEE-CBC | Almeida, José Bacelar; Barbosa, Manuel; Barthe, Gilles Jacques Denis, et al. | Artigo em ata de conferência | Acesso aberto |
10-Ago-2016 | Verifying constant-time implementations | Almeida, José Bacelar; Barbosa, Manuel; Barthe, Gilles Jacques Denis, et al. | Artigo em ata de conferência | Acesso aberto |