Computerized systems are present in various aspects of modern society. These systems are used to access and share confidential information. Such sharing is achieved through cryptographic protocols which often employ randomization to introduce unpredictability in their behavior to achieve critical security objectives and make it difficult for the malicious adversaries to infer the underlying execution of the participants. It is imperative to ensure that these protocols meet their security objectives such as confidentiality, privacy, fair exchange, anonymity and availability, as serious flaws have often been discovered in widely used cryptographic protocols. Given the ubiquitous role played by these security protocols and the socio-economic-political consequences that incorrect designs of cryptographic protocols may have, reasoning about their correctness is an important social imperative. This task is challenging because of the presence of malicious adversaries on the Internet as well as the subtle interaction between the concurrent nature of Internet and the various features such as cryptography and randomization used by the protocols. Hence, the development of automated techniques to verify their correctness is needed to manage this complexity, and this is the focus of this project. The presence of randomization introduces subtle challenges in verifying the correctness of security protocols. In particular, when reasoning about adversarial behavior, one must only consider those behaviors in which the scheduling of actions of the adversary is independent of the private random choices of the individual participants. This project aims to develop scalable techniques and tools that faithfully, and automatically verify randomized cryptographic protocols by considering only attacks (by an adversary) that are oblivious of the private data and private coin tosses of protocol participants. There are primarily three research tasks identified in this project. First, theoretical completeness results will be established that will reduce the general security problem for unbounded protocol sessions, session identifiers, and messages to the finite bounded cases. The other two tasks will be devoted to making the finite bounded case more amenable to automation. In the second research task, we will develop automated techniques to verify safety properties of protocols based on new symmetry reduction techniques using SMT solvers. The third research task will develop automated techniques for verifying indistinguishability properties of protocols. We will investigate symmetry reduction techniques using SMT solvers for this task as well.
TWC: Medium: Collaborative: Automated Formal Analysis of Security Protocols with Private Coin Tosses