面向密码协议设计与验证的数据中心方法
密码学与安全
2019-10-08 v1
摘要
我们提出 MetaCP（Meta Cryptography Protocol，元密码协议）验证工具，这是一种通过图形界面简化安全协议设计的自动化工具。该图形界面可视为非关系型数据库的现代化编辑器，其数据为协议。协议信息以 XML 存储，采用固定格式与语法，旨在包含指定任意类型协议所需的全部信息。该 XML 可视为一种几乎无语义的语言，不同的插件赋予其严格语义，将协议建模为多种后端验证语言。在本文中，我们通过展示 MetaCP 如何借助 Tamarin prover 插件从图形化设计到形式化验证协议，来演示这一新方法的有效性。尽管过去已提出过类似方法，最著名的是 AVISPA 工具，但此前没有任何方法能提供如此低的学习曲线和易用性（即使对非安全专业人员也是如此），同时兼具与最先进验证工具集成的灵活性。
引用
@article{arxiv.1910.02656,
title = {Towards a Data Centric Approach for the Design and Verification of Cryptographic Protocols},
author = {Luca Arnaboldi and Roberto Metere},
journal= {arXiv preprint arXiv:1910.02656},
year = {2019}
}
备注
3 pages, 2 figures, to appear in the Proceedings of ACM CCS 2019 - Poster Session