Title: Verifying cryptographic protocols. Applying the symbolic model to cryptographic APIs for C
Authors: Vanspauwen, Gijs
Jacobs, Bart
Issue Date: Mar-2016
Publisher: Department of Computer Science, KU Leuven
Series Title: CW Reports vol:CW694
Abstract: In this technical report we describe an approach for verifying cryptographic protocol implementations written in C. We statically prove the correctness of these implementations with the general purpose verifier VeriFast. More concretely we prove: memory safety, the absence of explicit and implicit information leaks, and functional correctness which includes protocol integrity. Our invariant-based approach requires an extension of the symbolic model of cryptography in order to work for protocol implementations in C written against an existing cryptographic API.
Publication status: published
KU Leuven publication type: IR
Appears in Collections:Informatics Section

Files in This Item:
File Description Status SizeFormat
CW694.pdfDocument Published 444KbAdobe PDFView/Open


All items in Lirias are protected by copyright, with all rights reserved.