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

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