基于迹枚举关系的定量超性质验证
Verification of Quantitative Hyperproperties Using Trace Enumeration Relations
摘要：
许多重要的密码原语提供了概率安全保证，可以指定为定量超性质;这些规范规定了系统中存在一定数量的满足某些约束的痕迹。这种超性质的验证是非常具有挑战性的，因为它们涉及到对无限数量的不同迹线的同时推理。在本文中，我们介绍了一种技术的基础上的概念的迹枚举关系的数量超性质的验证。这些关系使我们能够减少跟踪计数的问题之一的模型计数的公式在一阶逻辑。我们还介绍了一套推理规则的机器检查推理的数量满足解决方案的一阶公式（又名模型计数）。将这两个组件放在一起，可以半自动验证无限状态系统的定量超性质。我们使用我们的方法来证明的机密性的访问模式在路径的大小无界的RAM，一个简单的交互式零知识证明协议的可靠性，以及其他应用程序的定量hyperproperties研究在过去的工作。
英文摘要：
Many important cryptographic primitives offer probabilistic guarantees of security that can be specified as quantitative hyperproperties; these are specifications that stipulate the existence of a certain number of traces in the system satisfying certain constraints. Verification of such hyperproperties is extremely challenging because they involve simultaneous reasoning about an unbounded number of different traces. In this paper, we introduce a technique for verification of quantitative hyperproperties based on the notion of trace enumeration relations. These relations allow us to reduce the problem of trace-counting into one of model-counting of formulas in first-order logic. We also introduce a set of inference rules for machine-checked reasoning about the number of satisfying solutions to first-order formulas (aka model counting). Putting these two components together enables semi-automated verification of quantitative hyperproperties on infinite state systems. We use our methodology to prove confidentiality of access patterns in Path ORAMs of unbounded size, soundness of a simple interactive zero-knowledge proof protocol as well as other applications of quantitative hyperproperties studied in past work.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
