Tamarin’s Document
on Blogs
官方文档链接
Introduction
工具作用：对安全协议进行自动的符号建模和分析，检查协议是否存在安全属性的违反
工具输入：一个建模好的安全协议模型，攻击者描述，协议所需属性的规范
其中攻击者描述和协议属性规范描述均由Tamarin制定的规则（role）表示。
工具输出：协议
有两种结构证明的模式：
- 全自动模式：结合deduction和equational resoning
- 交互模式：人工引导
Jump to: Navigation