Abstract:



Unbounded Verification, Falsification, and Characterization 
of Security Protocols by Pattern Refinement


Cas J.F. Cremers



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 eitherunbounded correctness, falsification, 
or bounded correctness. (2)Efficient generation of a finite 
representation of an infinite set oftraces in terms of patterns, 
also known as a complete characterization.(3) State-of-the-art 
performance, which has made new types of protocolanalysis 
feasible, such as multi-protocol analysis.