问远程认证协议的形式化建模与自动验证
EN

Cryptography用户

提问于 2020-12-07 16:05:10

回答 2查看 90关注 0票数 0

我参与了通信协议的设计，该协议需要在交换任何其他数据之前对通信双方进行相互的远程认证。我们发现了几种用于密码协议符号安全分析的工具，如ProVerif、Tamarin或Verifpal。

然而，我们几乎没有对密码协议进行正式分析的经验。前面提到的工具的手册已经提供了一些例子。有没有其他好的来源可以具体地解释如何以机器检查的方式形式化一个安全的通信协议？考虑到远程认证的重点，是否还有更适合这项任务的其他工具？

发布于 2020-12-08 12:00:48

也许这是一个很好的起点：

“基于TPM 2.0的直接匿名认证计划的正式分析和实施”，出现在ASIACCS 2020上：

它使用Tamarin prover，Tamarin模型文件可供下载。

票数 1

发布于 2021-09-07 12:39:10

Sigma协议可能与“相互远程认证”(您定义它的方式)非常相关。这“理论”可得的背景下，伊莎贝尔证明。

票数 0

页面原文内容由Cryptography提供。腾讯云小微IT领域专用引擎提供翻译支持

原文链接：

https://crypto.stackexchange.com/questions/86748

复制

相似问题

问远程认证协议的形式化建模与自动验证EN