概率与不确定系统中信息泄漏的定量分析
Quantitative Analysis of Information Leakage in Probabilistic and Nondeterministic Systems
摘要：
本论文讨论了形式化方法在安全性，特别是匿名性方面的应用。更具体地说，我们开发的框架，规范的匿名性，并提出算法，其验证。由于在实践中匿名协议总是会泄漏一些信息，我们专注于定量属性，它捕获协议泄漏的信息量。这篇论文的主要贡献是cpCTL，第一个时间逻辑，允许规范和验证的条件概率（这是大多数匿名属性的关键成分）。此外，我们已经考虑了几个突出的信息泄漏的定义，并开发了第一个算法，使我们能够计算（甚至近似）的匿名协议的信息泄漏根据这些定义。我们还研究了分布式匿名协议规范和分析中的一个众所周知的问题，即全信息调度。为了克服这个问题，我们提出了另一种概念的调度和相应的调整几个匿名属性的文献。我们的最后一个主要贡献是一个调试技术，有助于检测安全协议中的缺陷。
英文摘要：
This thesis addresses the foundational aspects of formal methods for applications in security and in particular in anonymity. More concretely, we develop frameworks for the specification of anonymity properties and propose algorithms for their verification. Since in practice anonymity protocols always leak some information, we focus on quantitative properties, which capture the amount of information leaked by a protocol. The main contribution of this thesis is cpCTL, the first temporal logic that allows for the specification and verification of conditional probabilities (which are the key ingredient of most anonymity properties). In addition, we have considered several prominent definitions of information-leakage and developed the first algorithms allowing us to compute (and even approximate) the information leakage of anonymity protocols according to these definitions. We have also studied a well-known problem in the specification and analysis of distributed anonymity protocols, namely full-information scheduling. To overcome this problem, we have proposed an alternative notion of scheduling and adjusted accordingly several anonymity properties from the literature. Our last major contribution is a debugging technique that helps on the detection of flaws in security protocols.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
