Name
Title | ||
|---|---|---|
Verifying Cryptographic Software Correctness with Respect to Reference Implementations |
Abstract | ||
|---|---|---|
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. |
Year | DOI | Venue |
|---|---|---|
2009 | 10.1007/978-3-642-04570-7_5 | FMICS |
Keywords | Field | DocType |
program equivalence,interactive proof construction process,reference implementations,verification infrastructure,cryptographic software development,interactive proof technique,fundamental notion,verifying cryptographic software correctness,verification condition,verification process,natural invariant,difficult result,software development | Programming language,Cryptography,Computer science,Automated theorem proving,Implementation,Theoretical computer science,Reference implementation,Stream cipher,Software development,Software verification,Proof assistant | Conference |
Volume | ISSN | Citations |
5825 | 0302-9743 | 5 |
PageRank | References | Authors |
0.46 | 11 | 4 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| José Bacelar Almeida | 1 | 102 | 8.34 |
| Manuel Barbosa | 2 | 337 | 24.91 |
| Jorge Sousa Pinto | 3 | 160 | 23.19 |
| Bárbara Vieira | 4 | 32 | 2.87 |