The Tamarin prover リポジトリ

この README では、セキュリティプロトコル検証のための Tamarin prover のリポジトリの構成について説明します。対象読者は、Tamarin prover に関心のあるユーザーと将来の開発者です。Tamarin prover のインストールと使用方法については、マニュアルの第2章を参照してください: https://tamarin-prover.github.io/manual/master/book/002_installation.html

開発とコントリビューション

Tamarin prover のソースコードに対する変更の開発、テスト、リリースの方法については、コントリビューション手順を参照してください。

バージョン番号ポリシー

私たちは4つの要素からなるバージョン番号を使用しています。

最初の要素はメジャーバージョン番号です。コードベースの完全な書き換えを示します。
2番目の要素はマイナーバージョン番号です。奇数番号のマイナーバージョンは、早期導入者向けの開発リリースを表すために使用します。偶数番号のマイナーバージョンは、公開リリースを表すために使用し、これらも公開されます。
3番目の要素はバグ修正リリースを示します。
4番目の要素はドキュメントとメタデータの変更を示します。

私たちは、あるバージョンの Tamarin prover の外部インターフェースが、メジャーバージョン番号とマイナーバージョン番号が一致するすべてのバージョンの外部インターフェースと後方互換であることを保証します。

Tamarin prover のすべてのリリースは以下で告知します: http://tamarin-prover.github.io

マニュアル

マニュアルは PDF または HTML として https://tamarin-prover.github.io/manual/index.html で入手できます。

実験的な改良グラフ出力

複雑なプロトコルで作成される可能性のある非常に大きなグラフに役立つかもしれない、実験的な改良グラフ出力を使用できます。この機能を有効にするには、改良グラフに関する手順をお読みください。

Spthy コードエディタ

このプロジェクトには、etc ディレクトリ内の spthy 構文ハイライトとサポートが含まれています。これには Sublime Text、VIM、Notepad++ のサポートが含まれます。

外部ツール

外部ツールは、tree-sitter/ ディレクトリ内の Tree-sitter 文法を使用できます。

プロトコルモデルの例

すべてのプロトコルモデルの例は次のディレクトリにあります

./examples/

私たちが安定しているとみなすすべてのモデルは、Tamarin prover のすべてのインストールに含まれています。インストールされるプロトコルの一覧については tamarin-prover.cabal を参照してください。モデルを整理するために、次のサブディレクトリを使用しています。

accountability/ "Verifying Accountability for Unbounded Sets of Participants" 論文で
                提示された accountability 実装を使用したケーススタディ
csf12/          CSF'12 論文の AKE ケーススタディ。
classic/        [SPORE](http://www.lsv.ens-cachan.fr/Software/spore/table.html)
                にあるような古典的なセキュリティプロトコル
loops/          ループ不変条件と非単調状態を持つプロトコルをテストするための実験
related_work/   ループまたは非単調状態を持つプロトコルに関する関連研究の例
experiments/    その他すべての実験
ake/            双線形ペアリングに基づく ID ベースおよび三者間グループ KE プロトコルを
                含む、より多くの AKE の例
features/       特定の機能を実証する（小さな）モデル
ccs15/	        CCS'15 論文の観測等価性ケーススタディ
csf-18/         CSF'18 論文の XOR ケーススタディ

サブディレクトリをさらに追加して、ここに説明を記述してもかまいません。

一般に、モデルを含むファイルには説明的な名前を使用するようにしています。また、すべての発見事項をプロトコルモデル内のコメントとして文書化しています。さらに、コンテキストをより明確にするために、すべてのファイルで次のヘッダーを使用しています。

/*
   Protocol:    Example
   Modeler:     Simon Meier, Benedikt Schmidt
   Date:        January 2012

   Status:      working

   Description of protocol.

*/

tamarin-prover

人気