Anonymity, information, and machine-assisted proof
Anonymity, information, and machine-assisted proof
复制标题
匿名、信息和机器辅助证明
DOI：
--
复制
发表时间：
2010
期刊：
影响因子：
--
通讯作者：
A. R. Coble
中科院分区：
文献类型：
--
作者：
A. R. Coble
本报告展示了一种使用机械化定理证明器证明通信系统匿名性保障的技术。该方法基于香农信息论，可用于分析概率程序。用于匿名性的信息论度量提供了定量结果，即使在部分匿名的情况下也是如此。本文中的许多进展普遍适用于信息泄露，而不仅仅适用于隐私属性。通过在机械化定理证明器中开发框架，所有证明在给定模型方面都保证在逻辑和数学上是一致的。此外，系统的规范可以参数化，系统的理想属性可以根据这些参数进行量化；因此，可以一般性地证明系统的属性，而不是特定实例的属性。为了开发本文所述的分析框架，信息、概率和测度的基础理论必须在定理证明器中形式化；这些形式化过程将详细解释。这项基础性工作具有普遍意义，并不局限于此处所说明的应用。所采用的细致、外延的方法确保了数学一致性得以维持。一系列示例说明了形式化信息论如何用于分析和证明在定理证明器中建模的程序的信息泄露。这些示例考虑了多种不同的威胁模型，并展示了如何在所提出的框架中对它们进行描述。最后，所开发的工具用于证明 Dining Cryptographers（DC）协议的匿名性，从而展示了该框架的使用及其在证明隐私属性方面的适用性；DC协议是分析匿名系统新方法的一个标准基准。这项工作包含了针对不限数量的密码学家的DC协议匿名性的首个机器辅助证明。
This report demonstrates a technique for proving the anonymity guarantees of communication systems, using a mechanised theorem-prover. The approach is based on Shannon’s theory of information and can be used to analyse probabilistic programs. The information-theoretic metrics that are used for anonymity provide quantitative results, even in the case of partial anonymity. Many of the developments in this text are applicable to information leakage in general, rather than solely to privacy properties. By developing the framework within a mechanised theorem-prover, all proofs are guaranteed to be logically and mathematically consistent with respect to a given model. Moreover, the specification of a system can be parameterised and desirable properties of the system can quantify over those parameters; as a result, properties can be proved about the system in general, rather than specific instances. In order to develop the analysis framework described in this text, the underlying theories of information, probability, and measure had to be formalised in the theorem-prover; those formalisation are explained in detail. That foundational work is of general interest and not limited to the applications illustrated here. The meticulous, extensional approach that has been taken ensures that mathematical consistency is maintained. A series of examples illustrate how formalised information theory can be used to analyse and prove the information leakage of programs modelled in the theorem-prover. Those examples consider a number of different threat models and show how they can be characterised in the framework proposed. Finally, the tools developed are used to prove the anonymity of the dining cryptographers (DC) protocol, thereby demonstrating the use of the framework and its applicability to proving privacy properties; the DC protocol is a standard benchmark for new methods of analysing anonymity systems. This work includes the first machine-assisted proof of anonymity of the DC protocol for an unbounded number of cryptographers.
影响因子：
1.2
作者：
Clark, David;Hunt, Sebastian;Malacaria, Pasquale
通讯作者：
Malacaria, Pasquale