Integrating Logics and Process Calculi for Cryptographic Protocol Analysis
Mauricio Papa, Oliver Bremer, John C. Hale, Sujeet Shenoi · 2003
This paper describes a formalism for cryptographic protocol simulation and analysis that integrates logic and process calculus components. Novel features include the comprehensive modeling of encrypted and unencrypted messages, an expressive message passing semantics and sophisticated constructs for modeling principals. Moreover, the seamless integration of inference rules for communication, reduction and information analysis supports formal proofs about the knowledge and behavior of principals, and about the properties of protocols.