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.