Cryptographic Verification by Typing for a Sample Protocol Implementation

DOI10.1007/978-3-642-23082-0_3zbMath1344.68072OpenAlexW2169923303MaRDI QIDQ3092172

Andrew D. Gordon, Karthikeyan Bhargavan, 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

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

Uses Software

• VCC
• ASPIER
• F*

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• A calculus for cryptographic protocols: The spi calculus
• Breaking and fixing public-key Kerberos
• Union and Intersection Types for Secure Protocol Implementations
• Roles, stacks, histories: A triple for Hoare
• Keying Hash Functions for Message Authentication
• Analyzing security protocols with secrecy types and logic programs
• A Digital Signature Scheme Secure Against Adaptive Chosen-Message Attacks
• On the security of public key protocols
• Using encryption for authentication in large networks of computers
• Secure distributed programming with value-dependent types
• Modular verification of security protocol code by typing
• Verification, Model Checking, and Abstract Interpretation

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