Unbounded verification, falsification, and characterization of security protocols by pattern refinement

We present a new verification algorithm for security protocols that allows for unbounded verification, falsification, and complete characterization. The algorithm provides a number of novel features, including: (1) Guaranteed termination, after which the result is either unbounded correctness, falsification, or bounded correctness. (2) Efficient generation of a finite representation of an infinite set of traces in terms of patterns, also known as a complete characterization. (3) State-of-the-art performance, which has made new types of protocol analysis feasible, such as multi-protocol analysis. Categories and Subject Descriptors C.2.2 [Computer-communication Networks]: Network Protocols--Protocol verification General Terms Security, Theory, Verification Keywords Security protocol analysis, unbounded verification, falsification, characterization

• Type: Conference
• Year: 2008
• Where: CCS
• Authors: Cas J. F. Cremers
• Keywords: CCS 2008, Complete Characterization, Security Privacy, Security Protocol, Unbounded Verification