L. Bozga, C. Ene and Y. Lakhnech
A symbolic decision procedure for cryptographic protocols with time stamps (2004)
A symbolic decision procedure for cryptographic protocols with time stamps (2004)
TR-2004-2.pdf
TR-2004-2.ps
Keywords: Security, Cryptographic Protocols, Time stamps. Decidability, Verification
Abstract: A central question in the domain of program semantics and program verification is the existence of a complete inference system for assertions of the form $pimodelsvarphi$ meaning that program $pi$ satisfies property $varphi$. A stronger version of this question asks for an effective (decidable) complete inference system. We investigate these questions for cryptographic protocols focusing on authentication and confidentiality properties. While it is not difficult to see that a complete and effective inference system cannot exist when an unbounded number of sessions are considered, we prove that such a system exists for bounded protocols. More, precisely 1.) we provide a complete weakest pre-condition calculus for bounded cryptographic protocols and 2.) we show that assertions needed for completeness of the calculus are expressible in a decidable second order logic on terms.
