协议模型的概率注解
密码学与安全
2023-11-03 v1 计算机科学中的逻辑
摘要
我们描述了如何运用带局部性的概率 Hoare 逻辑来对安全性进行推理。作为概念验证，我们分析了 Vernam 与 El-Gamal 密码系统，证明了它们所满足的安全性质并反驳了它们不满足的性质。我们还考虑了一个 Muddy Children 谜题的变体，其中考虑了孩子们的信任与噪声。
引用
@article{arxiv.2108.03901,
title = {Probabilistic annotations for protocol models},
author = {Dusko Pavlovic},
journal= {arXiv preprint arXiv:2108.03901},
year = {2023}
}
备注
17 pages