Verificação formal de protocolos criptográficos : o caso dos protocolos em cascata

AUTOR(ES)

Rodrigo Borges Nogueira

DATA DE PUBLICAÇÃO

2008

RESUMO

Ensuring the security of cryptographic protocols is not a simple task. The Dolev-Yao model, proposed in the early 80s, is an important mathematical modeling method of cryptographic protocols, enabling the analysis and verification of the safety of these protocols. But the analytical verification does not guarantee that implementations are not error-prone. Indeed, we have, in the history of protocols, a lot of examples with flaws detected even after a decade of its introduction. Thus, formal method approaches are very useful to ensure the security of protocol implementations. In this work, we use the PVS (Prototype Verification System) to specify and mechanically verify the safety of a protocol class in the Dolev- Yao model: the two-party cascade protocols. By verifying our specification, we have detected a few flaws in the original definitions and we have proposed more general concepts and lemmas.

ASSUNTO(S)

verificação formal ciencia da computacao pvs formal verification pvs cryptographic protocols protocolos criptográficos

Documentos Relacionados

• Formal verification of fair exchange protocols using the strand spaces method
• A APLICAÇÃO DE PROTOCOLOS CRIPTOGRÁFICOS NA GESTÃO DE DOCUMENTOS ELETRÔNICOS DE UMA SECRETARIA ACADÊMICA: ESTUDO DE CASO DA SOCIESC
• Verificação formal de workflows com spin
• Verificação e prototipação de redes intrachip : o estudo de caso Hermes-TB
• Verificação formal de sistemas discretos distribuídos.