Abstract: Models and Methods for the Automated Analysis of Security Protocols Sebastian Mödersheim The automated analysis of security protocols requires efficient methods to address the specific problems that arise in the verification of security protocols, such as the deductions of an intruder. In this thesis, we develop new such methods and improve existing ones. Our proposed methods are built upon symbolic model- checking with constraints to efficiently represent the intruder. We integrate into the constraint-based approach ideas from partial-order reduction to deal with the problem of parallelism, leading to a novel technique called constraint differentiation. Moreover, we use modular rewriting techniques to allow for the consideration of algebraic properties of cryptographic operations.We have implemented these techniques into the tool OFMC (On-The-Fly Model-Checker for security protocols). As we demonstrate by a number of case studies and experiments on complex security protocols, OFMC has improved the state of the art both in terms of performance and in terms of the class of security protocols that can be considered. As part of the AVISPA tool, OFMC is used by dozens of researchers and protocol designers world wide to validate the design of security protocols.Besides the development of methods and tools, this thesis is also concerned with the subtle issues of modeling security protocols. We define a formalism for unambiguously specifying security protocols, their goals, and the intruder model. Moreover, we formally compare our model with other models based on over- approximation and formally describe their relationship. Besides a better understanding of these models, this allows us to prove that safety of a protocol in the over- approximation implies its safety in the standard model.