Strategy properties for cryptographic protocols

In this thesis we introduce the alternating mu-calculus (AMC) for cryptographic protocols and show in which cases this logic is decidable and in which cases it is not. We also give tight complexity bounds for the decidable classes of this problem. We extend the constraint solving approach developed for reachability properties to strategy properties and show how to utilize existing constraint solvers as a black box to decide strategy properties when a bounded number of sessions is considered and no bound on the message length is imposed. We give an alternative proof of the impossibility result given by Chadha et~al. based on an axiomatic approach. In order to formulate the properties of protocols we extend ATL by what we call move selectors. With move selectors one can talk about different kinds of behaviors (such as honest, dishonest, and optimistic behavior) of participants in a natural way rather than model each kind of possible behavior in an ad hoc fashion