在基于Horn理论的方法中将含XOR的协议分析归约到不含XOR的情形
密码学与安全
2008-08-06 v1
摘要
在基于Horn理论的密码协议分析方法中，密码协议和(Dolev-Yao)入侵者通过Horn理论建模，安全性分析归结为求解Horn理论的推导问题。该方法以及基于该方法的工具(包括ProVerif)在关于无界会话数的密码协议自动分析中非常成功。然而，处理诸如异或(XOR)等运算符的代数性质一直存在问题。特别是，ProVerif无法处理XOR。在本文中，我们展示了如何将含XOR的Horn理论的推导问题归约到不含XOR的情形。我们的归约适用于一类表达力丰富的Horn理论。一大类使用XOR运算符的入侵者能力和协议可以通过这些理论建模。我们的归约允许我们使用诸如ProVerif等无法处理XOR但在不含XOR情形下非常高效的工具进行协议分析。我们实现了我们的归约，并与ProVerif结合，将其应用于几个使用XOR运算符的协议的自动分析。在一个案例中，我们发现了一个新的攻击。
引用
@article{arxiv.0808.0634,
title = {Reducing Protocol Analysis with XOR to the XOR-free Case in the Horn Theory Based Approach},
author = {Ralf Kuesters and Tomasz Truderung},
journal= {arXiv preprint arXiv:0808.0634},
year = {2008}
}