タマリン・プルーバー
暗号プロトコルの形式検証用ソフトウェア
タマリン・プルーバー
原著者デイヴィッド・ベイスン、キャス・クレマーズ、ヤニック・ドライアー、サイモン・マイヤー、ラルフ・サッセ、ベネディクト・シュミット
開発者Cas Cremers、Jannik Dreier、Ralf Sasse
初回リリース2012年4月24日 （2012年4月24日）
安定版リリース
1.4.1 / 2019年1月18日 ( 2019-01-18 )
リポジトリgithub.com/tamarin-prover/tamarin-prover
言語：Haskell
オペレーティングシステムLinux、macOS
利用可能な言語英語
タイプ自動推論
ライセンスGNU GPL v3
ウェブサイトtamarin-prover.github.io

Tamarin Proverは、暗号プロトコルの形式検証を行うコンピュータソフトウェアプログラムです。[1]トランスポート層セキュリティ1.3、[2] ISO/IEC 9798、[3] DNP3セキュア認証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]

参照

参考文献

  1. ^ ブランシェット、ブルーノ (2014). 「記号モデルにおけるセキュリティプロトコルの自動検証：検証ツール ProVerif」.セキュリティ分析・設計の基礎 VII . コンピュータサイエンス講義ノート. 第8604巻. pp.  54– 87. doi :10.1007/978-3-319-10082-1​​_3. ISBN 978-3-319-10081-4。
  2. ^ Cremers, Cas; Horvat, Marko; Scott, Sam; van der Merwe, Thyla (2016). 「TLS 1.3の自動分析と検証：0-RTT、再開、遅延認証」 . IEEE Symposium on Security and Privacy, 2016, San Jose, CA, USA, 2016年5月22日～26日. IEEE S&P 2016. pp.  470– 485. doi :10.1109/SP.2016.35. ISBN 978-1-5090-0824-7。
  3. ^ 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.
  4. ^ Cremers, Cas ; Dehnel-Wild, Martin ; Milner, Kevin (2017). 「グリッドにおけるセキュアな認証：DNP3: SAv5 の形式的分析」（PDF） .コンピュータセキュリティ - ESORICS 2017 - 第22回ヨーロッパコンピュータセキュリティ研究シンポジウム、オスロ、ノルウェー、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。
  5. ^ Donenfeld, Jason A.; Milne, Kevin (2018), WireGuardプロトコルの形式検証(PDF) 、 2023年5月28日時点のオリジナルからアーカイブ(PDF) 、 2023年11月23日取得; Donenfeld, Jason A., 形式検証、2023年11月13日にオリジナルからアーカイブ、 2023年11月23日取得
  6. ^ 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.
  7. ^ Schmidt, Benedikt (2012).鍵交換プロトコルと物理プロトコルの形式分析（博士論文）. ETH Zurich. doi :10.3929/ethz-a-009898924. hdl :20.500.11850/72713.
  8. ^ マイヤー、サイモン (2012).自動セキュリティプロトコル検証の推進(博士論文). ETH チューリッヒ. doi :10.3929/ethz-a-009790675. hdl :20.500.11850/66840.
  9. ^ Basin, David; Linker, Felix; Sasse, Ralf, iMessage PQ3 メッセージングプロトコルの形式分析(PDF) 、 2024年2月28日時点のオリジナルよりアーカイブ(PDF) 、 2024年3月6日取得
  10. ^ ab P. Remlein、M. Rogacki、U. Stachowiak、「Tamarin ソフトウェア – プロトコル検証セキュリティのためのツール」、2020 Baltic URSI Symposium (URSI)、ワルシャワ、ポーランド、2020 年、pp. 118-123、doi: 10.23919/URSI48707.2020.9254078。
  11. ^ コリン・ボイド、アニッシュ・マチュリア、ダグラス・ステビラ共著。「認証と鍵確立のためのプロトコル」第2版、シュプリンガー、2019年、48ページ
  12. ^ 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年。
  • Tamarin Prover公式ウェブサイト
  • David Wong氏がTamarin Proverの紹介ビデオを作成しました
「https://en.wikipedia.org/w/index.php?title=Tamarin_Prover&oldid=1310371230」から取得