项目作者: tamarin-prover

项目描述 :
用于安全协议验证的Tamarin证明器的主要源代码存储库。
高级语言: Haskell
项目地址: git://github.com/tamarin-prover/tamarin-prover.git
创建时间: 2012-02-22T20:03:23Z
项目社区:https://github.com/tamarin-prover/tamarin-prover

开源协议:GNU General Public License v3.0

下载


The Tamarin prover repository

master branch build-status

This README describes the organization of the repository of the Tamarin prover
for security protocol verification. Its intended audience are interested
users and future developers of the Tamarin prover. For installation
and usage instructions of the Tamarin prover see chapter 2 of the manual:
https://tamarin-prover.github.io/manual/master/book/002_installation.html

Developing and contributing

See contributing instructions for instructions on how to develop,
test and release changes to the Tamarin prover source code.

Version Numbering Policy

We use version numbers with four components.

  • The first component is the major version number. It indicates complete
    rewrites of the codebase.
  • The second component is the minor version number. We use odd minor version
    numbers to denote development releases intended for early adopters. We use
    even minor version numbers to denote public releases, which are also
    published.
  • The third component indicates bugfix releases.
  • The fourth component indicates documentation and meta-data changes.

We ensure that the external interface of a version of the Tamarin prover is backwards
compatible with the external interface of all versions that agree on the major
and minor version number.

We announce all releases of the Tamarin prover on:
http://tamarin-prover.github.io

Manual

The manual is available as PDF or HTML at https://tamarin-prover.github.io/manual/index.html

Experimental improved graph output

You can use our experimental improved graph output which may be
helpful for very large graphs that can be created for complicated
protocols. To enable this feature read the instructions about
improved graphs.

Spthy code editors

The project contains support for spthy syntax highlighting and support
in the etc directory. This includes support for Sublime Text, VIM and Notepad++.

External tools

External tools may use the Tree-sitter grammar
in the tree-sitter/ directory.

Example Protocol Models

All example protocol models are found in the directory

  1. ./examples/

All models that we consider stable
are part of every installation of the Tamarin prover. See
tamarin-prover.cabal for the list of installed protocols. We use the
following sub-directories to organize the models.

  1. accountability/ case studies using the accountability implementation presented in
  2. the "Verifying Accountability for Unbounded Sets of Participants" paper
  3. csf12/ the AKE case studies from our CSF'12 paper.
  4. classic/ classic security protocols like the ones from
  5. [SPORE](http://www.lsv.ens-cachan.fr/Software/spore/table.html)
  6. loops/ experiments for testing loop-invariants and protocols with
  7. non-monotonic state
  8. related_work/ examples from related work on protocols with loops or
  9. non-monotonic state
  10. experiments/ all other experiments
  11. ake/ more AKE examples including ID-based and tripartite group KE
  12. protocols based on bilinear pairing
  13. features/ (small) models that demonstrate a given feature
  14. ccs15/ the observational equivalence case studies from our CCS'15 paper
  15. csf-18/ the XOR case studies from the CSF'18 paper

Feel free to add more sub-directories and describe them here.

In general, we try use descriptive names for files containing the models. We
also document all our findings as comments in the protocol model. Moreover,
we use the following header in all files to make their context more explicit.

  1. /*
  2. Protocol: Example
  3. Modeler: Simon Meier, Benedikt Schmidt
  4. Date: January 2012
  5. Status: working
  6. Description of protocol.
  7. */