Implementations of cryptographic protocols, such as OpenSSL for example, contain bugs affecting security, which cannot be detected by just analyzing abstract protocols (e.g., SSL or TLS). We describe how cryptographic protocol verification techniques based on solving clause sets can be applied to detect vulnerabilities of C programs in the Dolev-Yao model, statically. This involves integrating fairly simple pointer analysis techniques with an analysis of which messages an external intruder may collect and forge. This also involves relating concrete run-time data with abstract, logical terms representing messages. To this end, we make use of so-called trust assertions. The output of the analysis is a set of clauses in the decidable class ℋ1, which can then be solved independently. This can be used to establish secrecy properties, and to detect some other bugs. © Springer-Verlag Berlin Heidelberg 2005.
CITATION STYLE
Goubault-Larrecq, J., & Parrennes, F. (2005). Cryptographic protocol analysis on real C code. In Lecture Notes in Computer Science (Vol. 3385, pp. 363–379). Springer Verlag. https://doi.org/10.1007/978-3-540-30579-8_24
Mendeley helps you to discover research relevant for your work.