TWC: Medium: Collaborative: Automated Formal Analysis of Security Protocols with Private Coin Tosses

计算机化系统存在于现代社会的各个方面。这些系统用于访问和共享机密信息。这种共享是通过加密协议实现的，加密协议通常采用随机化来引入其行为的不可预测性，以实现关键的安全目标，并使恶意对手难以推断参与者的底层执行。必须确保这些协议满足其安全目标，例如机密性，隐私性，公平交换，匿名性和可用性，因为在广泛使用的密码协议中经常发现严重的缺陷。考虑到这些安全协议所扮演的无处不在的角色，以及不正确的密码协议设计可能带来的社会经济政治后果，对它们的正确性进行推理是一个重要的社会需求。这项任务是具有挑战性的，因为在互联网上的恶意对手的存在，以及互联网的并发性质和各种功能，如加密和随机化的协议之间的微妙的相互作用。因此，需要开发自动化技术来验证其正确性，以管理这种复杂性，这是本项目的重点。随机化的存在给验证安全协议的正确性带来了微妙的挑战。特别是，当推理对抗行为时，我们必须只考虑那些对手的行动计划与个体参与者的私人随机选择无关的行为。 该项目旨在开发可扩展的技术和工具，通过只考虑攻击（对手）来忠实地自动验证随机加密协议，这些攻击不知道协议参与者的私人数据和私人硬币投掷。 本项目主要有三个研究任务。首先，将建立理论上的完整性结果，这将减少无界协议会话，会话标识符和消息的有限有界情况下的一般安全问题。另外两个任务将致力于使有限有界的情况下更适合自动化。在第二个研究任务中，我们将开发自动化技术来验证协议的安全属性的基础上，新的对称性减少技术，使用SMT求解器。第三个研究任务是开发自动化技术来验证协议的不可扩展性。我们也将研究使用SMT求解器的对称性约简技术。

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.