論文の概要: Understanding the Usability of Cryptographic Verification Tools

• arxiv url: http://arxiv.org/abs/2609.16323v1
• Date: Mon, 14 Sep 2026 20:40:52 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-09-16 14:56:08.238451
• Title: Understanding the Usability of Cryptographic Verification Tools
• Title（参考訳）: 暗号検証ツールの有用性の理解
• Abstract要約: 本稿では,多摩林,ProVerif,および関連するプロトコル検証者の経験者を対象とした探索的人間中心研究について述べる。 調査対象は,タマリン,ProVerif,関連ツールを用いたハンズオン経験のある研究者,大学院生,実践者であった。
• 参考スコア（独自算出の注目度）: 1.5604334108839177
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Cryptographic protocol verification tools are widely used to analyze the security of complex protocols, yet how users interact with these tools remains comparatively understudied. We present an exploratory human-centered study of experienced users of Tamarin, ProVerif, and related protocol verifiers. Our survey included researchers, graduate students, and practitioners with hands-on experience using Tamarin, ProVerif, or related tools. The findings reveal usability barriers across the verification workflow, including difficulties debugging non-termination and performance issues, and the lack of systematic methods for validating formal models against real protocols. When proofs fail without concrete attacks, users commonly simplify models, add helper lemmas, and revisit modeling abstractions. Participants also called for actionable diagnostics, clearer explanations of results, visualization, and automation for recurring proof tasks. Our findings suggest that persistent usability challenges arise from the gap between protocol-level reasoning and the verifier's formal model, proof procedures, and diagnostic output. We derive concrete design priorities for improving the accessibility, interpretability, and usability of cryptographic protocol verification tools.
• Abstract（参考訳）: 暗号プロトコル検証ツールは、複雑なプロトコルのセキュリティを分析するために広く使われているが、これらのツールとユーザがどのようにやりとりするかは、まだ十分に研究されていない。 本稿では,多摩林,ProVerif,および関連するプロトコル検証者の経験者を対象とした探索的人間中心研究について述べる。 調査対象は,タマリン,ProVerif,関連ツールを用いたハンズオン経験のある研究者,大学院生,実践者であった。 この結果から、非終端とパフォーマンスの問題のデバッグが困難であることや、実際のプロトコルに対して形式的なモデルを検証するための体系的な方法がないことなど、検証ワークフローにおけるユーザビリティの障壁が明らかになった。 具体的な攻撃なしに証明が失敗すると、ユーザーは一般的にモデルを単純化し、ヘルパーの補題を追加し、モデリングの抽象化を再考する。 参加者はまた、実行可能な診断、結果のより明確な説明、可視化、繰り返し行われる証明タスクの自動化も要求した。 本研究は, プロトコルレベルの推論と検証者の形式モデル, 証明手順, 診断結果とのギャップから, 永続的なユーザビリティの課題が生じることを示唆している。 我々は、暗号プロトコル検証ツールのアクセシビリティ、解釈可能性、使用性を改善するための具体的な設計優先順位を導出する。

関連論文リスト

• AI Slop and Hallucinations in Vulnerability Assessment: A Survey on Reasoning Failures and Trustworthy Mitigation [48.55515767840701]
  AIスロープ(AI slop)は、アーティファクト、幻覚的脆弱性、可視だが正しくないパッチ、セマンティックに再パッケージされたバグレポートである。 本稿では,実証的証拠を調査し,統一メカニズムを特定し,信頼に値するトリアージへの道筋をたどる。
  論文  参考訳（メタデータ） (2026-08-26T11:48:38Z)
• AutoTam: Specifying Secure Protocol Implementations with Tamarin Model Generation [0.0]
  本稿では,プロトコル実装のためのドメイン固有言語を用いて,トレース特性の検証を行う新しい言語ファースト手法を提案する。 検証のためのタマリン証明器を目標とし、検証された普遍的トレース特性が実装に戻すことを証明する。 我々は、署名されたDiffie-HellmanプロトコルとWireGuard VPNプロトコルの正確なモデルの実装と生成にツールを使用します。
  論文  参考訳（メタデータ） (2026-06-18T08:34:17Z)
• IMMACULATE: A Practical LLM Auditing Framework via Verifiable Computation [49.796717294455796]
  経済的なモチベーションのある逸脱を検出するための実践的な監査フレームワークIMMACULATEを提案する。 IMMACULATEは、検証可能な計算を用いて少数のリクエストを選択的に監査し、暗号オーバーヘッドを償却しながら強力な検出保証を達成する。
  論文  参考訳（メタデータ） (2026-02-26T07:21:02Z)
• Demystifying deep search: a holistic evaluation with hint-free multi-hop questions and factorised metrics [89.1999907891494]
  We present WebDetective, a benchmark of hint-free multi-hop questions with a control Wikipedia sandbox。 25の最先端モデルに対する我々の評価は、すべてのアーキテクチャにまたがる体系的な弱点を明らかにしている。 私たちはエージェントワークフローであるEvidenceLoopを開発し、ベンチマークが特定する課題を明示的にターゲットしています。
  論文  参考訳（メタデータ） (2025-10-01T07:59:03Z)
• Scan-do Attitude: Towards Autonomous CT Protocol Management using a Large Language Model Agent [39.72587188702086]
  プロトコル構成要求の解釈と実行を支援するために,LLM(Large Language Model)ベースのエージェントフレームワークが提案されている。 このエージェントは、コンテキスト内学習、命令フォロー、構造化ツールコール機能を組み合わせて、関連するプロトコル要素を特定し、正確な修正を適用する。
  論文  参考訳（メタデータ） (2025-09-24T16:04:11Z)
• Validating Solidity Code Defects using Symbolic and Concrete Execution powered by Large Language Models [0.0]
  本稿では,Slither-based detectors, Large Language Models (LLMs), Kontrol, Forgeを統合した新しい検出パイプラインを提案する。 私たちのアプローチは、欠陥を確実に検出し、証明を生成するように設計されています。
  論文  参考訳（メタデータ） (2025-09-16T12:46:11Z)
• Evaluating Language Model Reasoning about Confidential Information [95.64687778185703]
  言語モデルが文脈的堅牢性を示すか、文脈依存型安全仕様に準拠する能力を示すかを検討する。 我々は,ユーザ要求がいつ承認されたか,言語モデルが正しく判断できるかどうかを測定するベンチマーク(PasswordEval)を開発した。 現在のオープンソースとクローズドソースのモデルでは、一見単純な作業に苦労しています。
  論文  参考訳（メタデータ） (2025-08-27T15:39:46Z)
• Deep Learning Models for Robust Facial Liveness Detection [56.08694048252482]
  本研究では,現代のアンチスプーフィング手法の欠陥に対処する新しい深層学習モデルを用いて,ロバストな解を提案する。 テクスチャ解析と実際の人間の特性に関連する反射特性を革新的に統合することにより、我々のモデルは、顕著な精度でレプリカと真の存在を区別する。
  論文  参考訳（メタデータ） (2025-08-12T17:19:20Z)
• Formal Verification of Permission Voucher [1.4732811715354452]
  Permission Voucher Protocolは、分散環境におけるセキュアで認証されたアクセス制御のために設計されたシステムである。 この分析では、重要なセキュリティ特性を評価するために、象徴的検証のための最先端のツールであるTamarin Proverを使用している。 結果は、メッセージの改ざん、偽装、リプレイなどの一般的な攻撃に対するプロトコルの堅牢性を確認する。
  論文  参考訳（メタデータ） (2024-12-18T14:11:50Z)
• CryptoFormalEval: Integrating LLMs and Formal Verification for Automated Cryptographic Protocol Vulnerability Detection [41.94295877935867]
  我々は,新たな暗号プロトコルの脆弱性を自律的に識別する大規模言語モデルの能力を評価するためのベンチマークを導入する。 私たちは、新しい、欠陥のある通信プロトコルのデータセットを作成し、AIエージェントが発見した脆弱性を自動的に検証する方法を設計しました。
  論文  参考訳（メタデータ） (2024-11-20T14:16:55Z)
• DT-SIM: Property-Based Testing for MPC Security [2.0308771704846245]
  プロパティベースのテストはセキュアプロトコルのセキュリティバグの検出に有効である。 セキュアマルチパーティ計算(MPC)を特に対象とする。 MPCプロトコルのビットレベル実装において,様々な欠陥を検出するテストを作成する。
  論文  参考訳（メタデータ） (2024-03-08T02:02:24Z)
• Unsupervised Continual Anomaly Detection with Contrastively-learned Prompt [80.43623986759691]
  UCADと呼ばれる新しい非教師付き連続異常検出フレームワークを提案する。 このフレームワークは、対照的に学習したプロンプトを通じて、UDAに継続的な学習能力を持たせる。 我々は総合的な実験を行い、教師なし連続異常検出とセグメンテーションのベンチマークを設定した。
  論文  参考訳（メタデータ） (2024-01-02T03:37:11Z)
• Deepfake Detection: A Comprehensive Survey from the Reliability Perspective [20.873480187150804]
  キノコ入りのDeepfake合成材料がインターネット上に流通し、政治家、有名人、そして世界中の個人に深刻な社会的影響を与えている。 現在のDeepfake検出領域では、トランスファービリティ、解釈可能性、堅牢性という、信頼性を重視した3つの研究課題を識別する。
  論文  参考訳（メタデータ） (2022-11-20T06:31:23Z)

関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。

指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。