論文の概要: Formal Verification of Permission Voucher

• arxiv url: http://arxiv.org/abs/2412.16224v1
• Date: Wed, 18 Dec 2024 14:11:50 GMT
• ステータス: 翻訳完了
• システム内更新日: 2024-12-24 15:55:22.535976
• Title: Formal Verification of Permission Voucher
• Title（参考訳）: パーミッションボウチャーの形式的検証
• Authors: Khan Reaz, Gerhard Wunder,
• Abstract要約: Permission Voucher Protocolは、分散環境におけるセキュアで認証されたアクセス制御のために設計されたシステムである。 この分析では、重要なセキュリティ特性を評価するために、象徴的検証のための最先端のツールであるTamarin Proverを使用している。 結果は、メッセージの改ざん、偽装、リプレイなどの一般的な攻撃に対するプロトコルの堅牢性を確認する。
• 参考スコア（独自算出の注目度）: 1.4732811715354452
• License:
• Abstract: Formal verification is a critical process in ensuring the security and correctness of cryptographic protocols, particularly in high-assurance domains. This paper presents a comprehensive formal analysis of the Permission Voucher Protocol, a system designed for secure and authenticated access control in distributed environments. The analysis employs the Tamarin Prover, a state-of-the-art tool for symbolic verification, to evaluate key security properties such as authentication, confidentiality, integrity, mutual authentication, and replay prevention. We model the protocol's components, including trust relationships, secure channels, and adversary capabilities under the Dolev-Yao model. Verification results confirm the protocol's robustness against common attacks such as message tampering, impersonation, and replay. Additionally, dependency graphs and detailed proofs demonstrate the successful enforcement of security properties like voucher authenticity, data confidentiality, and key integrity. The study identifies potential enhancements, such as incorporating timestamp-based validity checks and augmenting mutual authentication mechanisms to address insider threats and key management challenges. This work highlights the advantages and limitations of using the Tamarin Prover for formal security verification and proposes strategies to mitigate scalability and performance constraints in complex systems.
• Abstract（参考訳）: 形式検証は、特に高セキュリティ領域における暗号プロトコルのセキュリティと正当性を保証するための重要なプロセスである。 本稿では,分散環境におけるセキュアかつ認証されたアクセス制御のためのシステムであるPermission Voucher Protocolの包括的形式解析について述べる。 この分析では、認証、機密性、完全性、相互認証、再生防止といった重要なセキュリティ特性を評価するために、象徴的検証のための最先端ツールであるTamarin Proverを使用している。 我々は、信頼関係、セキュアチャネル、およびDolev-Yaoモデルの下での敵機能を含むプロトコルのコンポーネントをモデル化する。 検証結果は、メッセージの改ざん、偽装、リプレイなどの一般的な攻撃に対するプロトコルの堅牢性を確認する。 さらに、依存性グラフと詳細な証明は、ブーチャーの認証、データの機密性、キーの完全性といったセキュリティプロパティの実施が成功していることを示している。 この研究は、タイムスタンプベースの妥当性チェックの導入や、インサイダーの脅威や鍵管理上の課題に対処するための相互認証機構の強化など、潜在的な機能強化を明らかにしている。 本研究は,Tamarin Proverを公式なセキュリティ検証に使用するメリットと限界を強調し,複雑なシステムにおけるスケーラビリティとパフォーマンスの制約を軽減するための戦略を提案する。

関連論文リスト

• Balancing Confidentiality and Transparency for Blockchain-based Process-Aware Information Systems [46.404531555921906]
  機密性と透明性の両立を目的とした,ブロックチェーンベースのPAISアーキテクチャを提案する。 スマートコントラクトは公開インタラクションを制定、強制、保存し、属性ベースの暗号化技術は機密情報へのアクセス許可を指定するために採用されている。
  論文  参考訳（メタデータ） (2024-12-07T20:18:36Z)
• Securing Legacy Communication Networks via Authenticated Cyclic Redundancy Integrity Check [98.34702864029796]
  認証サイクル冗長性チェック(ACRIC)を提案する。 ACRICは、追加のハードウェアを必要とせずに後方互換性を保持し、プロトコルに依存しない。 ACRICは最小送信オーバーヘッド(1ms)で堅牢なセキュリティを提供する。
  論文  参考訳（メタデータ） (2024-11-21T18:26:05Z)
• Excavating Vulnerabilities Lurking in Multi-Factor Authentication Protocols: A Systematic Security Analysis [2.729532849571912]
  単一要素認証(SFA)プロトコルは、しばしばサイドチャネルや他の攻撃技術によってバイパスされる。 この問題を軽減するため,近年,MFAプロトコルが広く採用されている。
  論文  参考訳（メタデータ） (2024-07-29T23:37:38Z)
• Quantum-Secure Certificate-Less Conditional Privacy-Preserving Authentication for VANET [4.8124555241328375]
  既存の格子ベースの認証方式は、マスターシークレットキーの漏洩とキーエスクロー問題の潜在的な問題に対処するには不十分である。 本稿では,システム全体の効率を保ちつつ,欠陥を解消する量子セキュア認証方式を提案する。
  論文  参考訳（メタデータ） (2024-03-20T16:50:36Z)
• Evidence Tampering and Chain of Custody in Layered Attestations [0.0]
  分散システムにおいて、信頼決定は、遠隔検定によって生成される完全性証明に基づいて行われる。 提案手法は, 証拠が検出されることなく, 証拠を改ざんできる「戦略」を改ざんするだけでなく, 証拠を改ざんするための全ての改ざん機会を識別するアルゴリズムを提案する。 当社の取り組みは,プロトコル設計者が可能な限り最小かつ信頼性の高いコンポーネントの集合に機会を阻害する証拠を減らすことを支援することを目的としています。
  論文  参考訳（メタデータ） (2024-01-31T21:54:53Z)
• A Survey and Comparative Analysis of Security Properties of CAN Authentication Protocols [92.81385447582882]
  コントロールエリアネットワーク(CAN)バスは車内通信を本質的に安全でないものにしている。 本稿では,CANバスにおける15の認証プロトコルをレビューし,比較する。 実装の容易性に寄与する本質的な運用基準に基づくプロトコルの評価を行う。
  論文  参考訳（メタデータ） (2024-01-19T14:52:04Z)
• Rely-guarantee Reasoning about Concurrent Memory Management: Correctness, Safety and Security [0.0]
  メモリ管理の誤った仕様と実装は、システムのクラッシュや悪用可能な攻撃につながる可能性がある。 本稿では,実世界のOSにおける並列メモリ管理の最初の正式な仕様と機構的証明について述べる。
  論文  参考訳（メタデータ） (2023-09-17T03:41:10Z)
• FedSOV: Federated Model Secure Ownership Verification with Unforgeable Signature [60.99054146321459]
  フェデレートラーニングにより、複数のパーティがプライベートデータを公開せずにグローバルモデルを学ぶことができる。 本稿では,FedSOVという暗号署名に基づくフェデレート学習モデルのオーナシップ検証手法を提案する。
  論文  参考訳（メタデータ） (2023-05-10T12:10:02Z)
• Quantum Proofs of Deletion for Learning with Errors [91.3755431537592]
  完全同型暗号方式として, 完全同型暗号方式を初めて構築する。 我々の主要な技術要素は、量子証明器が古典的検証器に量子状態の形でのLearning with Errors分布からのサンプルが削除されたことを納得させる対話的プロトコルである。
  論文  参考訳（メタデータ） (2022-03-03T10:07:32Z)
• Joint Differentiable Optimization and Verification for Certified Reinforcement Learning [91.93635157885055]
  安全クリティカル制御システムのためのモデルベース強化学習では,システム特性を正式に認定することが重要である。 本稿では,強化学習と形式検証を共同で行う枠組みを提案する。
  論文  参考訳（メタデータ） (2022-01-28T16:53:56Z)

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

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