简介 Tamarin power 是一种功能强大的工具，用于对安全协议进行符号建模和分析。它以安全协议模型为输入，指定了以不同角色（如协议启动者、响应者和受信任的密钥服务器）运行协议的代理所采取的行动，敌手的指定以及协议期望属性的指定。然后，Tamarin 可用于自动构建一个证明，即即使协议角色的任意多个实例并行交错，加上敌手的行动，协议也能满足其指定的属性。在本手册中，我们将概述这一工具及其使