Type-Based Automated Verification of Authenticity in Cryptographic Protocols

Gordon and Jeffrey have proposed a type and effect system for checking authenticity in cryptographic protocols. The type system reduces the protocol verification problem to the type checking problem, but protocols must be manually annotated with non-trivial types and effects. To automate the verification of cryptographic protocols, we modify Gordon and Jeffrey's type system and develop a type inference algorithm. Key modifications for enabling automated type inference are introduction of fractional effects and replacement of typing rules with syntaxdirected ones. We have implemented and tested a prototype protocol verifier based on our type system.

• Type: Conference
• Year: 2009
• Where: ESOP
• Authors: Daisuke Kikuchi, Naoki Kobayashi
• Keywords: Cryptographic Protocols, ESOP 2009, Programming Languages, Type Inference, Type System