用于标准化有状态协议的形式化支持
密码学与安全
2018-04-17 v1
摘要
许多密码协议被设计为仅使用通过开放网络传递的消息来实现其目标。基于充分理解的基础，存在众多工具用于设计和分析纯粹依赖消息传递的协议。然而，当面对依赖非局部、可变状态来协调多个局部会话的协议时，这些工具遇到了困难。我们改造了这些工具之一，CPSA，以提供用于推理状态的自动化支持。我们使用瑞恩的信封协议作为示例，展示了消息传递推理如何与状态推理集成以产生有趣且强大的结果。
引用
@article{arxiv.1509.07552,
title = {Formal Support for Standardizing Protocols with State},
author = {Joshua D. Guttman and Moses D. Liskov and John D. Ramsdell and Paul D. Rowe},
journal= {arXiv preprint arXiv:1509.07552},
year = {2018}
}