一种足以验证隐私性质的应用 pi 演算互模拟同余
密码学与安全
2018-11-07 v1 计算机科学中的逻辑
摘要
本文首次对应用 pi 演算中作为同余关系的最粗互模拟概念——开放杆互模拟——进行了深入研究。证明了更适合构造互模拟的标记互模拟的开放变体（准开放互模拟）与开放杆互模拟一致。这些互模拟同余被证明可由一种直觉主义模态逻辑刻画，该逻辑可用于例如在某隐私性质被违反时描述对隐私的攻击。开放杆互模拟提供了一种验证密码协议的组合方法，因为所证性质可在任意上下文中复用，包括输入前缀下。此外，开放杆互模拟足够粗，可用于推理密码协议的安全与隐私性质；相比之下，更细的互模拟同余——开放互模拟——无法验证某些隐私性质。
引用
@article{arxiv.1811.02536,
title = {A Bisimilarity Congruence for the Applied pi-Calculus Sufficiently Coarse to Verify Privacy Properties},
author = {Ross Horne},
journal= {arXiv preprint arXiv:1811.02536},
year = {2018}
}