A machine-checked proof of security for AWS key management service

We present a machine-checked proof of security for the domain management protocol of Amazon Web Services' KMS (Key Management Service) a critical security service used throughout AWS and by AWS customers. Domain management is at the core of AWS KMS; it governs the top-level keys that anchor the...

ver descrição completa

Detalhes bibliográficos
Autor principal: Almeida, José Bacelar (author)
Outros Autores: Barbosa, Manuel (author), Barthe, Gilles (author), Campagna, Matthew (author), Cohen, Ernie (author), Gregoire, Benjamin (author), Pereira, Vitor (author), Portela, Bernardo (author), Strub, Pierre-Yves (author), Tasiran, Serdar (author)
Formato: conferencePaper
Idioma:eng
Publicado em: 2019
Assuntos:
Provable-Security
Machine-Checked Proof
Key Management
Engenharia e Tecnologia::Engenharia Eletrotécnica, Eletrónica e Informática
Science & Technology
Texto completo:http://hdl.handle.net/1822/66487
País:Portugal
Oai:oai:repositorium.sdum.uminho.pt:1822/66487
Descrição
Resumo:We present a machine-checked proof of security for the domain management protocol of Amazon Web Services' KMS (Key Management Service) a critical security service used throughout AWS and by AWS customers. Domain management is at the core of AWS KMS; it governs the top-level keys that anchor the security of encryption services at AWS. We show that the protocol securely implements an ideal distributed encryption mechanism under standard cryptographic assumptions. The proof is machine-checked in the EasyCrypt proof assistant and is the largest EasyCrypt development to date.

Registos relacionados