Cryptographic protocol analysis on real C code

DOI10.1007/978-3-540-30579-8_24MaRDI QIDQ5711502zbMATH OpenOpenAlexFDO

Authors Jean Goubault-Larrecq, Fabrice Parrennes

Publication date 6 December 2005

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/b105073

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Cryptography (94A60)

Recommendations

• A static analysis of cryptographic processes: the denotational approach
• scientific article; zbMATH DE number 2163007
• Three systems for cryptographic protocol analysis
• Rule-based static analysis of network protocol implementations
• Security analysis model of behavior based on cryptographic protocols implement at source code level

Cited in

(13)

• Extending H₁-clauses with disequalities
• Safe abstractions of data encodings in formal security protocol models
• Gaining trust by tracing security protocols
• Rule-based static analysis of network protocol implementations
• Crossing the syntactic barrier: hom-disequalities for \({\mathcal H}_1\)-clauses
• Normalization of linear Horn clauses
• Cryptographic Verification by Typing for a Sample Protocol Implementation
• Static evidences for attack reconstruction
• Paths, tree homomorphisms and disequalities for H₁-clauses
• Integrated and automated abstract interpretation, verification and testing of C/C++ modules
• An intrinsic encoding of a subset of C and its application to TLS network packet processing
• Security analysis model of behavior based on cryptographic protocols implement at source code level
• Automatic verification of security protocols in the symbolic model: the verifier ProVerif

Describes a project that uses

Uses Software

• SPASS
• OpenSSL

This page was built for publication: Cryptographic protocol analysis on real C code

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5711502)