論文の概要: Towards automated formal security analysis of SAML V2.0 Web Browser SSO standard - the POST/Artifact use case

• arxiv url: http://arxiv.org/abs/2403.11859v1
• Date: Mon, 18 Mar 2024 15:11:29 GMT
• ステータス: 翻訳完了
• システム内更新日: 2024-03-20 20:00:12.471898
• Title: Towards automated formal security analysis of SAML V2.0 Web Browser SSO standard - the POST/Artifact use case
• Title（参考訳）: SAML V2.0 Web Browser SSO 標準の自動セキュリティ解析に向けて - POST/Artifact のユースケース
• Authors: Zvonimir Hartl, Ante Đerek,
• Abstract要約: シングルサインオン(SSO)プロトコルは、複数のオンラインサービスに対する統一ログインによるユーザ認証を合理化し、ユーザビリティとセキュリティを改善している。 最も一般的なものの一つ。 SSOプロトコルフレームワーク - Security Assertion Markup Language V2.0 (SAML) Web。 シングルサインオン(SSO)プロトコルは、複数のオンラインサービスに対する統一ログインによるユーザ認証を合理化し、改善する。 ユーザビリティとセキュリティ
• 参考スコア（独自算出の注目度）: 0.0
• License: http://creativecommons.org/licenses/by-nc-nd/4.0/
• Abstract: Single Sign-On (SSO) protocols streamline user authentication with a unified login for multiple online services, improving usability and security. One of the most common SSO protocol frameworks - the Security Assertion Markup Language V2.0 (SAML) Web SSO Profile - has been in use for more than two decades, primarily in government, education and enterprise environments. Despite its mission-critical nature, only certain deployments and configurations of the Web SSO Profile have been formally analyzed. This paper attempts to bridge this gap by performing a comprehensive formal security analysis of the SAML V2.0 SP-initiated SSO with POST/Artifact Bindings use case. Rather than focusing on a specific deployment and configuration, we closely follow the specification with the goal of capturing many different deployments allowed by the standard. Modeling and analysis is performed using Tamarin prover - state-of-the-art tool for automated verification of security protocols in the symbolic model of cryptography. Technically, we build a meta-model of the use case that we instantiate to eight different protocol variants. Using the Tamarin prover, we formally verify a number of critical security properties for those protocol variants, while identifying certain drawbacks and potential vulnerabilities.
• Abstract（参考訳）: シングルサインオン(SSO)プロトコルは、複数のオンラインサービスに対する統一ログインによるユーザ認証を合理化し、ユーザビリティとセキュリティを改善している。 最も一般的なSSOプロトコルフレームワークの1つであるSecurity Assertion Markup Language V2.0 (SAML) Web SSO Profileは、主に政府、教育、エンタープライズ環境で20年以上使われてきた。 ミッションクリティカルな性質にもかかわらず、Web SSO Profileの特定の配置と構成のみが公式に分析されている。 本稿では,POST/Artifact Bindingsのユースケースを用いて,SAML V2.0 SP-initiated SSOの総合的なセキュリティ解析を行うことにより,このギャップを埋めようとしている。 特定のデプロイメントや構成に集中するのではなく、標準で許可された多くの異なるデプロイメントをキャプチャすることを目標として、仕様をしっかりとフォローしています。 モデリングと解析は,暗号化のシンボリックモデルにおけるセキュリティプロトコルの自動検証のための最先端ツールであるTamarin proverを用いて行われる。 技術的には、ユースケースのメタモデルを構築し、8つの異なるプロトコルの変種にインスタンス化します。 Tamarinの証明器を使って、これらのプロトコルの変種に対して、いくつかの重要なセキュリティ特性を正式に検証し、特定の欠点と潜在的な脆弱性を特定します。

関連論文リスト

• A Trajectory-Based Safety Audit of Clawdbot (OpenClaw) [77.1549110891026]
  6つのリスク次元にわたるClawdbotの軌道中心評価について述べる。 我々は、完全なインタラクショントラジェクトリ(メッセージ、アクション、ツールコール引数/アウトプット)をログし、自動化されたトラジェクトリ判断とヒューマンレビューの両方を使用して安全性を評価する。
  論文  参考訳（メタデータ） (2026-02-16T00:33:02Z)
• Multi-Agent Taint Specification Extraction for Vulnerability Detection [49.27772068704498]
  コンテナ分析を使用した静的アプリケーションセキュリティテスト(SAST)ツールは、高品質な脆弱性検出結果を提供するものとして広く見なされている。 本稿では,Large Language Models (LLM) のセマンティック理解と従来の静的プログラム解析を戦略的に組み合わせたマルチエージェントシステムであるSemTaintを提案する。 私たちは、SemTaintを最先端のSASTツールであるCodeQLと統合し、これまでCodeQLで検出できなかった162の脆弱性の106を検出して、その効果を実証しています。
  論文  参考訳（メタデータ） (2026-01-15T21:31:51Z)
• ReasAlign: Reasoning Enhanced Safety Alignment against Prompt Injection Attack [52.17935054046577]
  本稿では、間接的インジェクション攻撃に対する安全性アライメントを改善するためのモデルレベルのソリューションであるReasAlignを提案する。 ReasAlignには、ユーザクエリの分析、競合する命令の検出、ユーザの意図したタスクの継続性を維持するための構造化された推論ステップが組み込まれている。
  論文  参考訳（メタデータ） (2026-01-15T08:23:38Z)
• Automated Side-Channel Analysis of Cryptographic Protocol Implementations [9.38081874899831]
  WhatsAppの最初の形式モデルを実装から抽出する。 コンパイル後セキュリティに対する既知のクローンアタックを特定します。 本稿では,暗号プロトコルの実装をサイドチャネル攻撃に対するレジリエンスとして解析する手法を提案する。
  論文  参考訳（メタデータ） (2025-11-14T15:13:49Z)
• BrowserArena: Evaluating LLM Agents on Real-World Web Navigation Tasks [51.803138848305814]
  我々はBrowserArenaを紹介した。BrowserArenaは、ユーザから送信されたタスクを収集するオープンソースのエージェント評価プラットフォームである。 Captcha解決、ポップアップバナー削除、URLへのダイレクトナビゲーションの3つの一貫した障害モードを特定します。 本研究は,Webエージェントの多様性と脆性の両方を明らかにする。
  論文  参考訳（メタデータ） (2025-10-02T15:22:21Z)
• Formal Verification of Physical Layer Security Protocols for Next-Generation Communication Networks (extended version) [1.5997757408973357]
  音響アニメーションを生成するIsabelle形式を用いたNeedham-Schroederプロトコルをモデル化する。 以上の結果から,すべてのシナリオにおいて信頼性が保たれていることが示唆された。 我々は、透かしとジャミングを統合したPLSベースのDiffie-Hellmanプロトコルを提案している。
  論文  参考訳（メタデータ） (2025-08-26T20:59:16Z)
• Understanding the Identity-Transformation Approach in OIDC-Compatible Privacy-Preserving SSO Services [7.080530070342893]
  OpenID Connect(OIDC)により、市販のブラウザを持つユーザは、別の信頼できるWebシステムに設定されたユーザ名と認証(IdP)によって、Redependent Party(RP)と呼ばれる複数のWebサイトにログインすることができる。
  論文  参考訳（メタデータ） (2025-06-02T05:11:01Z)
• Benchmarking Unified Face Attack Detection via Hierarchical Prompt Tuning [58.16354555208417]
  PADとFFDはそれぞれ物理メディアベースのプレゼンテーションアタックとデジタル編集ベースのDeepFakeから顔データを保護するために提案されている。 これら2つのカテゴリの攻撃を同時に処理する統一顔攻撃検出モデルがないことは、主に2つの要因に起因する。 本稿では,異なる意味空間から複数の分類基準を適応的に探索する,視覚言語モデルに基づく階層型プロンプトチューニングフレームワークを提案する。
  論文  参考訳（メタデータ） (2025-05-19T16:35:45Z)
• One For All: Formally Verifying Protocols which use Aggregate Signatures (extended version) [6.604074204101799]
  BLSアグリゲートシグネチャは、DfinityやCloudflareなどによってデプロイされた一般的なアグリゲートシグネチャである。 BLSアグリゲートシグネチャは、プロトコル開発者が慎重に扱わなければならないニュアンスな要件で、正しく使用するのは難しい。 本研究では,タマリンやProVerifなどの形式検証ツールをこれらのシグネチャを用いたプロトコルに適用可能なアグリゲートシグネチャの最初のモデルの設計を行う。
  論文  参考訳（メタデータ） (2025-05-15T14:01:30Z)
• CANTXSec: A Deterministic Intrusion Detection and Prevention System for CAN Bus Monitoring ECU Activations [53.036288487863786]
  物理ECUアクティベーションに基づく最初の決定論的侵入検知・防止システムであるCANTXSecを提案する。 CANバスの古典的な攻撃を検知・防止し、文献では調査されていない高度な攻撃を検知する。 物理テストベッド上での解法の有効性を実証し,攻撃の両クラスにおいて100%検出精度を達成し,100%のFIAを防止した。
  論文  参考訳（メタデータ） (2025-05-14T13:37:07Z)
• DoomArena: A framework for Testing AI Agents Against Evolving Security Threats [84.94654617852322]
  本稿では,AIエージェントのセキュリティ評価フレームワークであるDoomArenaを紹介する。 プラグインフレームワークであり、現実的なエージェントフレームワークと簡単に統合できる。 モジュールであり、エージェントがデプロイされる環境の詳細から攻撃の開発を分離する。
  論文  参考訳（メタデータ） (2025-04-18T20:36:10Z)
• OmniParser V2: Structured-Points-of-Thought for Unified Visual Text Parsing and Its Generality to Multimodal Large Language Models [58.45517851437422]
  VsTP(Visually-situated text parsing)は、自動化された文書理解の需要が高まり、最近顕著な進歩を遂げている。 既存のソリューションは、タスク固有のアーキテクチャと個々のタスクの目的に依存していることが多い。 本稿では,テキストスポッティング,キー情報抽出,テーブル認識,レイアウト解析など,VsTPの典型的なタスクを統一する汎用モデルであるOmni V2を紹介する。
  論文  参考訳（メタデータ） (2025-02-22T09:32:01Z)
• CryptoFormalEval: Integrating LLMs and Formal Verification for Automated Cryptographic Protocol Vulnerability Detection [41.94295877935867]
  我々は,新たな暗号プロトコルの脆弱性を自律的に識別する大規模言語モデルの能力を評価するためのベンチマークを導入する。 私たちは、新しい、欠陥のある通信プロトコルのデータセットを作成し、AIエージェントが発見した脆弱性を自動的に検証する方法を設計しました。
  論文  参考訳（メタデータ） (2024-11-20T14:16:55Z)
• Misbinding Raw Public Keys to Identities in TLS [1.821556502071398]
  本稿では,Raw Public Key (RPK) 認証におけるTLSの安全性について検討する。 このモードはX.509証明書やPre-Shared Keys (PSK)ほど広く研究されていない。 本研究では,適応型 pi calculus と ProVerif 検証ツールを用いた TLS RPK の形式モデルを構築し,RPK モードが識別ミスバインディング攻撃の影響を受けやすいことを示した。
  論文  参考訳（メタデータ） (2024-11-14T19:28:09Z)
• SecCodePLT: A Unified Platform for Evaluating the Security of Code GenAI [47.11178028457252]
  我々はGenAIのリスクをコードする統合的かつ包括的な評価プラットフォームSecCodePLTを開発した。 安全でないコードには、専門家と自動生成を組み合わせたデータ生成のための新しい方法論を導入する。 サイバー攻撃支援のために、我々はモデルに実際の攻撃を引き起こすよう促すサンプルと、我々の環境における動的な指標を構築した。
  論文  参考訳（メタデータ） (2024-10-14T21:17:22Z)
• Excavating Vulnerabilities Lurking in Multi-Factor Authentication Protocols: A Systematic Security Analysis [2.729532849571912]
  単一要素認証(SFA)プロトコルは、しばしばサイドチャネルや他の攻撃技術によってバイパスされる。 この問題を軽減するため,近年,MFAプロトコルが広く採用されている。
  論文  参考訳（メタデータ） (2024-07-29T23:37:38Z)
• SAM-CP: Marrying SAM with Composable Prompts for Versatile Segmentation [88.80792308991867]
  Segment Anything Model (SAM)は、イメージピクセルをパッチにグループ化する機能を示しているが、セグメンテーションにそれを適用することは依然として大きな課題に直面している。 本稿では,SAM-CPを提案する。SAM-CPはSAM以外の2種類の構成可能なプロンプトを確立し,多目的セグメンテーションのために構成する単純な手法である。 実験により、SAM-CPはオープンドメインとクローズドドメインの両方においてセマンティック、例、およびパノプティックセグメンテーションを達成することが示された。
  論文  参考訳（メタデータ） (2024-07-23T17:47:25Z)
• EmInspector: Combating Backdoor Attacks in Federated Self-Supervised Learning Through Embedding Inspection [53.25863925815954]
  フェデレートされた自己教師付き学習(FSSL)は、クライアントの膨大な量の未ラベルデータの利用を可能にする、有望なパラダイムとして登場した。 FSSLはアドバンテージを提供するが、バックドア攻撃に対する感受性は調査されていない。 ローカルモデルの埋め込み空間を検査し,悪意のあるクライアントを検知する埋め込み検査器(EmInspector)を提案する。
  論文  参考訳（メタデータ） (2024-05-21T06:14:49Z)
• Protocols to Code: Formal Verification of a Next-Generation Internet Router [9.971817718196997]
  SCIONルータは、敵の環境でセキュアなパケット転送のための暗号化プロトコルを実行する。 プロトコルのネットワーク全体のセキュリティ特性と,その実装の低レベル特性の両方を検証する。 本稿では,本研究のアプローチを説明し,主な成果を要約し,検証可能なシステムの設計と実装に関する教訓を抽出する。
  論文  参考訳（メタデータ） (2024-05-09T19:57:59Z)
• A Survey and Comparative Analysis of Security Properties of CAN Authentication Protocols [92.81385447582882]
  コントロールエリアネットワーク(CAN)バスは車内通信を本質的に安全でないものにしている。 本稿では,CANバスにおける15の認証プロトコルをレビューし,比較する。 実装の容易性に寄与する本質的な運用基準に基づくプロトコルの評価を行う。
  論文  参考訳（メタデータ） (2024-01-19T14:52:04Z)
• A Novel Approach To User Agent String Parsing For Vulnerability Analysis Using Mutli-Headed Attention [3.3029515721630855]
  マルチヘッド・アテンション・ベース・トランスを用いたUAS解析手法を提案する。 提案手法は,異なるフォーマットの様々なUASを解析する上で,高い性能を示す。 解析されたUASを用いて、公開ITネットワークやリージョンの大部分の脆弱性スコアを推定するフレームワークについても論じる。
  論文  参考訳（メタデータ） (2023-06-06T14:49:25Z)
• FedSOV: Federated Model Secure Ownership Verification with Unforgeable Signature [60.99054146321459]
  フェデレートラーニングにより、複数のパーティがプライベートデータを公開せずにグローバルモデルを学ぶことができる。 本稿では,FedSOVという暗号署名に基づくフェデレート学習モデルのオーナシップ検証手法を提案する。
  論文  参考訳（メタデータ） (2023-05-10T12:10:02Z)
• Secure access system using signature verification over tablet PC [62.21072852729544]
  我々は,シグネチャ検証を用いたWebベースのセキュアアクセスのための,高度に汎用的でスケーラブルなプロトタイプについて述べる。 提案アーキテクチャは,様々な種類のセンサや大規模データベースで動作するように容易に拡張することができる。
  論文  参考訳（メタデータ） (2023-01-11T11:05:47Z)

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

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