| This dissertation present the research, joint work with Dr. Rakesh Verma, that develops formal methods to check cryptographic protocols. The topics in this general area include complexities of checking security goals such as secrecy and authentication, algorithms to detect attacks to protocols, proofs of safety and correctness of protocols, and prudential protocol design approaches. The research of this dissertation solves several problems of fundamental importance, and the main contributions are organized into several chapters. First, we prove the undecidability of checking secrecy and authentication while considering an insider attacker and realistic protocols that are communication sequences. By this work we solve two open problems posed by Froschle. Second, we prove the undecidability of an open problem on the complexity of checking secrecy of cryptographic protocols posed by Durgin, Lincoln, and Mitchell. Third, we define the security goal of freshness and we analyze the complexities of checking freshness in different settings. Fourth, we improve the proof by Rusinowitch and Turuani showing that checking secrecy with a bounded number of sessions is in Non-deterministic Polynomial time (NP). Especially, we discuss a non-trivial error of the proof and we present a solution to fix the error. The modeling and proving techniques can be applied to other research topics in this area. |
