Cryptographic Verification by Typing for a Sample Protocol Implementation

DOI10.1007/978-3-642-23082-0_3MaRDI QIDQ3092172zbMATH OpenOpenAlexFDO

Authors Karthikeyan Bhargavan, Andrew D. Gordon, Cédric Fournet

Publication date 16 September 2011

Published in Foundations of Security Analysis and Design VI (Search for Journal in Brave)

Full work available at URL https://hal.inria.fr/hal-01295013/file/cryptographic_verification_fosad10.pdf

Mathematics Subject Classification ID

Data encryption (aspects in computer science) (68P25) Cryptography (94A60)

Recommendations

• Type-Based Automated Verification of Authenticity in Cryptographic Protocols
• Modular verification of security protocol code by typing
• Type-based automated verification of authenticity in asymmetric cryptographic protocols
• The practice of cryptographic protocol verification
• scientific article; zbMATH DE number 1927556
• scientific article; zbMATH DE number 1614701
• scientific article; zbMATH DE number 7297874
• Logic for verifying public-key cryptographic protocols

Cites work

• A calculus for cryptographic protocols: The spi calculus
• A Digital Signature Scheme Secure Against Adaptive Chosen-Message Attacks
• Analyzing security protocols with secrecy types and logic programs
• Breaking and fixing public-key Kerberos
• scientific article; zbMATH DE number 1583788 (Why is no real title available?)
• scientific article; zbMATH DE number 1296290 (Why is no real title available?)
• scientific article; zbMATH DE number 1302834 (Why is no real title available?)
• scientific article; zbMATH DE number 2086729 (Why is no real title available?)
• Keying hash functions for message authentication
• Modular verification of security protocol code by typing
• On the security of public key protocols
• Roles, stacks, histories: a triple for Hoare
• Secure distributed programming with value-dependent types
• Union and Intersection Types for Secure Protocol Implementations
• Using encryption for authentication in large networks of computers
• Verification, Model Checking, and Abstract Interpretation

Cited in

(9)

• Equivalence properties by typing in cryptographic branching protocols
• Type-based automated verification of authenticity in asymmetric cryptographic protocols
• Type-Based Automated Verification of Authenticity in Cryptographic Protocols
• scientific article; zbMATH DE number 1927556 (Why is no real title available?)
• Secure distributed programming with value-dependent types
• Modular verification of security protocol code by typing
• Logical foundations of secure resource management in protocol implementations
• Secure distributed programming with value-dependent types
• Verified interoperable implementations of security protocols

Describes a project that uses

Uses Software

• VCC
• ASPIER
• F*

This page was built for publication: Cryptographic Verification by Typing for a Sample Protocol Implementation

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