tamarin-prover/tamarin-prover

# Tamarin prover 仓库 [](https://travis-ci.org/tamarin-prover/tamarin-prover) 本 README 介绍了用于安全协议验证的 Tamarin prover 仓库的组织结构。其目标受众是 Tamarin prover 的感兴趣用户和未来开发者。有关 Tamarin prover 的安装和使用说明，请参阅手册第 2 章： https://tamarin-prover.github.io/manual/master/book/002_installation.html ## 开发与贡献 有关如何开发、测试和发布 Tamarin prover 源代码更改的说明，请参阅[贡献指南](CONTRIBUTING.md)。 ## 版本编号策略 我们使用包含四个组成部分的版本号。 - 第一个组成部分是主版本号。它表示代码库的完全重写。 - 第二个组成部分是次版本号。我们使用奇数次版本号来表示面向早期采用者的开发版本。我们使用偶数次版本号来表示公开发布版本，这些版本也会被发布。 - 第三个组成部分表示错误修复版本。 - 第四个组成部分表示文档和元数据更改。 我们确保 Tamarin prover 某个版本的外部接口与所有主版本号和次版本号相同的版本的外部接口保持向后兼容。 我们在以下网址发布 Tamarin prover 的所有版本： http://tamarin-prover.github.io ## 手册 手册以 PDF 或 HTML 格式提供，网址为 https://tamarin-prover.github.io/manual/index.html ## 实验性改进图输出 您可以使用我们的实验性改进图输出功能，这对于由复杂协议生成的超大图可能有所帮助。要启用此功能，请阅读关于[改进图](/misc/cleandot/README.md)的说明。 ## Spthy 代码编辑器 该项目在 [etc](/etc/) 目录中包含了对 spthy 语法高亮的支持。这包括对 [Sublime Text](/etc/SUBLIME_TEXT.md)、[VIM](/etc/spthy.vim) 和 [Notepad++](/etc/notepad_plus_plus_spthy.xml) 的支持。 ## 外部工具 外部工具可以使用 [tree-sitter/](/tree-sitter/) 目录中的 [Tree-sitter](https://tree-sitter.github.io/tree-sitter/) 语法。 ## 示例协议模型 所有示例协议模型均可在以下目录中找到 ``` ./examples/ ``` 我们认为稳定的所有模型都是每个 Tamarin prover 安装的一部分。请参阅 `tamarin-prover.cabal` 以获取已安装协议的列表。我们使用以下子目录来组织这些模型。 ``` accountability/ case studies using the accountability implementation presented in the "Verifying Accountability for Unbounded Sets of Participants" paper csf12/ the AKE case studies from our CSF'12 paper. classic/ classic security protocols like the ones from [SPORE](http://www.lsv.ens-cachan.fr/Software/spore/table.html) loops/ experiments for testing loop-invariants and protocols with non-monotonic state related_work/ examples from related work on protocols with loops or non-monotonic state experiments/ all other experiments ake/ more AKE examples including ID-based and tripartite group KE protocols based on bilinear pairing features/ (small) models that demonstrate a given feature ccs15/ the observational equivalence case studies from our CCS'15 paper csf-18/ the XOR case studies from the CSF'18 paper ``` 请随意添加更多子目录并在此处进行描述。 通常，我们尝试为包含模型的文件使用描述性名称。我们还将所有发现作为注释记录在协议模型中。此外，我们在所有文件中使用以下标题，以使其上下文更加明确。 ``` /* Protocol: Example Modeler: Simon Meier, Benedikt Schmidt Date: January 2012 Status: working Description of protocol. */ ```

标签：Haskell, Maude, SPROT, Spthy, Tamarin Prover, 协议分析, 图论, 安全协议, 安全模型检测, 定理证明, 密码学, 开源安全工具, 形式化验证, 手动系统调用, 攻击路径分析, 权限提升, 符号分析, 网络安全, 认证协议, 逆向工程平台, 逻辑编程, 防篡改, 隐私保护, 零知识证明