Loading article…
 | |
 | |
| 原作者 | デヴィッド・ベイシン、カス・クレメルス、ヤニク・ドライアー、サイモン・マイヤー、ラルフ・サッセ、ベネディクト・シュミット |
|---|---|
| 開発者 | カス・クレメルス、ヤニク・ドライアー、ラルフ・サッセ |
| 初回リリース | 2012年4月24日 |
| 安定リリース | 1.4.1 / 2019年1月18日 |
| リポジトリ | github.com/tamarin-prover/tamarin-prover |
| 書かれた | ハスケル |
| オペレーティング·システム | Linux、macOS |
| 利用可能 | 英語 |
| タイプ | 自動推論 |
| ライセンス | GNU GPL v3 |
| Webサイト | タマリン-prover.github.io |
Tamarin Proverは、暗号プロトコルの形式検証を行うコンピュータソフトウェアプログラムです。[1] Transport Layer Security 1.3、[2] ISO/IEC 9798、[3] DNP3 Secure Authentication v5、[4] WireGuard、[5] [6] [7] [8] Apple iMessageのPQ3メッセージングプロトコルの検証に使用されています。[9]
TamarinはHaskellで書かれたオープンソースツールで、[10] Scytherと呼ばれる古い検証ツールの後継として構築されました。[11] Tamarinには自動証明機能がありますが、自己ガイドも可能です。[11] Tamarinでは、セキュリティ特性を表す補題が定義されています。 [12]プロトコルに変更が加えられた後、Tamarinはセキュリティ特性が維持されているかどうかを検証できます。[12] Tamarinの実行結果は、プロトコル内でセキュリティ特性が保持されていることの証明、セキュリティ特性が保持されないプロトコル実行の例、またはTamarinが停止に失敗する可能性があります。[12] [10]
参照
参考文献
- ^ Blanchet, B. (2014). シンボリック モデルでのセキュリティ プロトコルの自動検証: 検証ツール ProVerif。In: Aldini, A.、Lopez, J.、Martinelli, F. (eds) Foundations of Security Analysis and Design VII。FOSAD FOSAD 2013 2012. Lecture Notes in Computer Science、vol 8604。Springer、Cham。
- ^ Cremers, Cas; Horvat, Marko; Scott, Sam; van der Merwe, Thyla (2016). 「TLS 1.3 の自動分析と検証: 0-RTT、再開、遅延認証」。IEEEセキュリティとプライバシーに関するシンポジウム、2016、米国カリフォルニア州サンノゼ、2016 年 5 月 22 ～ 26 日。IEEE S&P 2016。pp. 470～485。doi : 10.1109 /SP.2016.35。ISBN 978-1-5090-0824-7。
- ^ Basin, David; Cremers, Cas; Meier, Simon (2013). 「エンティティ認証のための ISO/IEC 9798 標準の証明可能な修復」(PDF) . Journal of Computer Security . 21 (6): 817–846. doi :10.3233/JCS-130472. hdl :20.500.11850/69793.
- ^ Cremers, Cas ; Dehnel-Wild, Martin; Milner, Kevin (2017). 「グリッドにおけるセキュアな認証: DNP3: SAv5 の形式的分析」(PDF) .コンピュータ セキュリティ - ESORICS 2017 - 22nd European Symposium on Research in Computer Security、オスロ、ノルウェー、2017 年 9 月 11 ～ 15 日、議事録、パート I . ESORICS 2017. オスロ、ノルウェー: Springer. pp. 389–407. doi :10.1007/978-3-319-66402-6_23. ISBN 978-3-319-66401-9。
- ^ Donenfeld, Jason A.; Milne, Kevin (2018)、「WireGuard プロトコルの形式的検証」(PDF)、2023 年 5 月 28 日のオリジナルからアーカイブ(PDF) 、 2023 年 11 月 23 日取得; Donenfeld, Jason A., 形式検証、2023-11-13 にオリジナルからアーカイブ、2023-11-23に取得
- ^ Schmidt, Benedikt; Meier, Simon; Cremers, Cas ; Basin, David (2012). 「Diffie-Hellman プロトコルの自動分析と高度なセキュリティ プロパティ」(PDF)。第 25 回 IEEE コンピュータ セキュリティ基盤シンポジウム、CSF 2012、米国マサチューセッツ州ケンブリッジ、2012 年 6 月 25 ～ 27 日。CSF 2012。マサチューセッツ州ケンブリッジ: IEEE コンピュータ ソサエティ。pp. 78 ～ 94。
- ^ Schmidt, Benedikt (2012).鍵交換プロトコルと物理プロトコルの形式分析(博士論文). ETH Zurich. doi :10.3929/ethz-a-009898924. hdl :20.500.11850/72713.
- ^ Meier, Simon (2012).自動セキュリティプロトコル検証の推進(博士論文). ETH Zurich. doi :10.3929/ethz-a-009790675. hdl :20.500.11850/66840.
- ^ Basin, David; Linker, Felix; Sasse, Ralf, iMessage PQ3 メッセージング プロトコルの形式分析(PDF)、2024 年 2 月 28 日のオリジナルからアーカイブ(PDF) 、2024 年 3 月 6 日に取得
- ^ ab P. Remlein、M. Rogacki、U. Stachowiak、「Tamarin ソフトウェア – プロトコル検証セキュリティのためのツール」、2020 Baltic URSI Symposium (URSI)、ワルシャワ、ポーランド、2020 年、pp. 118-123、doi: 10.23919/ URSI48707.2020.9254078。
- ^ コリン・ボイド、アニッシュ・マトゥリア、ダグラス・ステビラ共著 。「認証と鍵確立のためのプロトコル」第 2 版 Springer、2019 年、48 ページ
- ^ abc Celi、Sofía、Jonathan Hoyland、Douglas Stebila、Thom Wiggers。「2つのモデルの物語：TamarinによるKEMTLSの形式検証」。European Symposium on Research in Computer Security、pp. 63-83。Cham：Springer Nature Switzerland、2022年。
外部リンク
- タマリン・プローバー公式サイト
- David Wong が Tamarin Prover の紹介ビデオを作成しました。