用于按需扩充安全分析的同态与极小性
密码学与安全
2018-04-20 v1
摘要
密码协议被用于不同的环境中，但现有的协议分析方法仅关注协议本身，而对环境假设不敏感。LPA 是一个在上下文中分析协议的工具。LPA 使用两个相互协作的程序：CPSA（一个著名的协议分析系统）和 Razor（一个基于 SMT 技术的模型寻找器）。我们的分析遵循按需扩充（enrich-by-need）范式，其中生成并检查协议执行的模型。生成哪些模型的选择十分重要，我们论证并评估了 LPA 构建极小模型的策略。“极小性”可相对于两种预序之一来定义，即同态预序与嵌入预序（即单射同态的预序）；我们讨论了各自的优缺点。我们的主要技术贡献是构建同态极小模型的算法，以及为某一理论的模型生成支持集（set-of-support）的算法，在每种情况下均通过对 SMT 求解器的交互脚本实现。
引用
@article{arxiv.1804.07158,
title = {Homomorphisms and Minimality for Enrich-by-Need Security Analysis},
author = {Daniel J. Dougherty and Joshua D. Guttman and John D. Ramsdell},
journal= {arXiv preprint arXiv:1804.07158},
year = {2018}
}