Verifying Cryptographic Software Correctness with Respect to Reference Implementations

• Tipo: Artigo em Livro de Atas de Conferência Internacional
• Data: 2009

Autores

Almeida, JB (Autor) Outra; Barbosa, M (Autor) Outra; Pinto, JS (Autor) Outra; Vieira, B (Autor) Outra

Ata de Conferência Internacional

Título: FORMAL METHODS FOR INDUSTRIAL CRITICAL SYSTEMS

Páginas: 37-52

14th International Workshop on Formal Methods for Industrial Critical Systems

Eindhoven, NETHERLANDS, NOV 02-03, 2009

Indexação

ISI Web of Knowledge - 3 Citações

Scopus - 5 Citações

Outras Informações

ID Authenticus: P-003-Q4B

DOI: 10.1007/978-3-642-04570-7_5

Abstract (EN): 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.

Idioma: Inglês

Tipo (Avaliação Docente): Científica

Nº de páginas: 16