概率关系霍尔逻辑中一种直接的惰性采样证明技术
密码学与安全
2023-11-30 v1 形式语言与自动机理论
计算机科学中的逻辑
摘要
使用随机值的程序可以提前做出所有选择（急切地）或按需采样（惰性地）。在形式化证明中，我们关注两个惰性程序间的不可区分性，这是随机预言机模型（ROM）中的常见要求。虽然重排采样指令常能解决此问题，但当采样分散于多个过程时便会变得复杂。由Bellare与Rogaway于2004年提出的传统方法将程序转换为急切采样，但需假设有限内存、多项式界以及人工重采样函数。我们在概率关系霍尔逻辑（pRHL）中引入一种新方法，直接证明不可区分性，免去了转换及上述假设。我们还在EasyCrypt定理证明器中实现了该方法，表明其可作为传统方法的便捷替代。
引用
@article{arxiv.2311.16844,
title = {A Direct Lazy Sampling Proof Technique in Probabilistic Relational Hoare Logic},
author = {Roberto Metere and Changyu Dong},
journal= {arXiv preprint arXiv:2311.16844},
year = {2023}
}
备注
12 pages, 13 figures, 1 table