論文の概要: BMC4TimeSec: Verification Of Timed Security Protocols
- arxiv url: http://arxiv.org/abs/2602.17590v1
- Date: Thu, 19 Feb 2026 18:12:01 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-02-20 15:21:29.293168
- Title: BMC4TimeSec: Verification Of Timed Security Protocols
- Title(参考訳): BMC4TimeSec: タイムセキュリティプロトコルの検証
- Abstract要約: 我々は、TSP(Timed Security Protocol)を検証するエンドツーエンドツールであるBMC4TimeSecを紹介する。
BMC4TimeSecでは、TSPの実行はTIS/TIIS環境(アクション、インターリーブ、遅延、ライフタイム)を実装し、知識自動はエージェントを実装している。
- 参考スコア(独自算出の注目度): 0.3655021726150367
- License: http://creativecommons.org/licenses/by-nc-nd/4.0/
- Abstract: We present BMC4TimeSec, an end-to-end tool for verifying Timed Security Protocols (TSP) based on SMT-based bounded model checking and multi-agent modelling in the form of Timed Interpreted Systems (TIS) and Timed Interleaved Interpreted Systems (TIIS). In BMC4TimeSec, TSP executions implement the TIS/TIIS environment (join actions, interleaving, delays, lifetimes), and knowledge automata implement the agents (evolution of participant knowledge, including the intruder). The code is publicly available on \href{https://github.com/agazbrzezny/BMC4TimeSec}{GitHub}, as is a \href{https://youtu.be/aNybKz6HwdA}{video} demonstration.
- Abstract(参考訳): 我々は,TIS(Timed Interpreted Systems)とTIIS(Timed Interleaved Interpreted Systems)という形式で,SMTに基づく有界モデルチェックとマルチエージェントモデリングに基づく,TSP(Timed Security Protocol)のエンドツーエンド検証ツールであるBMC4TimeSecを提案する。
BMC4TimeSecでは、TSP実行はTIIS/TIIS環境(アクション、インターリーブ、遅延、ライフタイム)を実装し、知識オートマトンはエージェント(侵入者を含む参加者の知識の進化)を実装している。
コードは \href{https://github.com/agazbrzezny/BMC4TimeSec}{GitHub} で公開されており、また \href{https://youtu.be/aNybKz6HwdA}{video} デモも公開されている。
関連論文リスト
- Speculative Macro Commit for Faster Tool-Using Agents [18.574702996656935]
2層エージェントシステムの実行機構である textbfSpeculative Macro Commit (SMC) を導入する。
SMCは、トレーニングトレースから繰り返し発生するマルチアクションスケルトンをマイニングし、マクロライブラリーに保存する。
AppWorldでは,SAベースラインを7.7%,シーケンシャル実行を44.9%削減する。
論文 参考訳(メタデータ) (2026-09-03T00:31:43Z) - From Attack Simulation to SIEM Rule: Deterministic Detection-as-Code Synthesis with Probe-Level Traceability [51.56484100374058]
セキュリティチームは、自身のシステムに対する攻撃をシミュレートして、監視が真の侵入者を捕まえるかどうかをチェックする。
人間はそのギャップを手でブリッジし、それぞれの発見を読み、対応するシグマルールを書きます。
ロックされたコーパスからプローブが引き出されると,この変換が部分的に自動化されることを示す。
論文 参考訳(メタデータ) (2026-06-03T14:26:25Z) - Speculative Interaction Agents: Building Real-Time Agents with Asynchronous I/O and Speculative Tool Calling [64.40340291543971]
我々は,小さなエッジスケールモデルとのリアルタイムインタラクションを実現するための投機的インタラクションエージェントを提案する。
また、ストリーミング入力と非同期応答を処理するためにモデルを適応させるクロックベースのトレーニング手法を提案する。
このアプローチは、Qwen2.5-3B-InstructとLlama-3.2-3B-Instructモデルを複数のツール呼び出しベンチマークで1.6-2.2$times$ Speedupを提供する。
論文 参考訳(メタデータ) (2026-05-13T11:20:52Z) - Tamper-Proofing with Self-Modifying Code [0.0]
決定論的普遍チューリングマシン上の自己修正符号(SMC)は、同じモデル上の非SMC符号でシミュレートすることができる。
我々は、一度タイミング、順序、自己検査効果が観測可能なものとして扱われると、商品システムにおいて事実上忠実でない非SMC再生が検出可能なコストになると主張している。
Introspective and polymorphic SMC, reliable clock, and timing predicates to bind Runtime checks to execution behavior。
論文 参考訳(メタデータ) (2026-04-14T07:44:17Z) - ForeSea: AI Forensic Search with Multi-modal Queries for Video Surveillance [56.15563109738998]
ForeSeaは3段階のプラグアンドプレイパイプラインを備えたAI法医学検索システムである。
ForeSeaは従来のビデオRAGモデルよりも精度を3.5%向上し、一時IoUは11.0向上した。
論文 参考訳(メタデータ) (2026-03-24T07:15:28Z) - Mixed Choice in Asynchronous Multiparty Session Types [0.47248250311484113]
非同期混合選択(MC)を用いたマルチパーティセッションタイプ(MST)フレームワークを提案する。
本稿では,分散参加者間のプロトコル状態の過渡的不整合を可能にするMCのコアコンストラクトを提案する。
我々は,グローバル型と分散ローカル型プロジェクション間の進捗特性と運用対応を確立することで,システムの正当性を証明した。
論文 参考訳(メタデータ) (2026-02-27T11:21:58Z) - AlcheMinT: Fine-grained Temporal Control for Multi-Reference Consistent Video Generation [58.844504598618094]
本稿では、被験者駆動ビデオ生成のための明示的なタイムスタンプ条件付きフレームワークAlcheMinTを提案する。
提案手法では,時間間隔の符号化を解き放つ新しい位置符号化機構を導入する。
我々は、視覚的アイデンティティとビデオキャプションの結合を強化するために、主観記述型テキストトークンを導入し、世代間あいまいさを緩和する。
論文 参考訳(メタデータ) (2025-12-11T18:59:34Z) - AegisMCP: Online Graph Intrusion Detection for Tool-Augmented LLMs on Edge Devices [5.081228499547384]
本稿では,プロトコルレベルの侵入検知器であるAegisMCPを紹介する。
AegisMCPは、ウィンドウ毎のサブ秒モデル推論とエンドツーエンドの警告を実現する。
論文 参考訳(メタデータ) (2025-10-22T10:50:22Z) - Code2MCP: Transforming Code Repositories into MCP Services [53.234097255779744]
Model Context Protocol (MCP)は、大規模言語モデルがどのようにツールを使用するかの標準を作成することを目的としている。
私たちは、GitHubリポジトリを機能的なMSPサービスに自動的に変換するエージェントベースのフレームワークであるCode2MCPを紹介します。
Code2MCPはバイオインフォマティクス、数学、流体力学などの科学分野におけるオープンソースの計算ライブラリの変換に成功している。
論文 参考訳(メタデータ) (2025-09-07T06:13:25Z) - An Open-source Implementation and Security Analysis of Triad's TEE Trusted Time Protocol [1.1060425537315088]
Intel SGXのようなTrusted Execution Environments (TEE)では、TEEをホストする悪意のあるシステムがTEEの時間の概念を操作できる。
Triadのような以前の作業では、TEEが信頼できるタイムソースを維持するためのプロトコルが提案されていた。
このプロトコルに脆弱性を実証的に示す。
論文 参考訳(メタデータ) (2025-07-28T14:02:59Z) - Leveraging Temporal Contextualization for Video Action Recognition [47.8361303269338]
本稿では,TC-CLIP (Temporally Contextualized CLIP) と呼ばれる映像理解のためのフレームワークを提案する。
ビデオの時間的情報注入機構である時間的コンテキスト化(TC)を導入する。
Video-Prompting (VP)モジュールはコンテキストトークンを処理し、テキストのモダリティで情報的なプロンプトを生成する。
論文 参考訳(メタデータ) (2024-04-15T06:24:56Z) - TF-CLIP: Learning Text-free CLIP for Video-based Person
Re-Identification [60.5843635938469]
ビデオベースのReIDのための一段階のテキストフリーCLIP学習フレームワークTF-CLIPを提案する。
より具体的には、テキスト機能を置き換えるために、アイデンティティ固有のシーケンス機能をCLIPメモリとして抽出する。
提案手法は,MARS,LS-VID,iLIDS-VIDの他の最先端手法よりも優れた結果を示す。
論文 参考訳(メタデータ) (2023-12-15T09:10:05Z) - Timed Actors and Their Formal Verification [0.21756081703275998]
Timed Rebecaは非同期メッセージパッシングによって通信するカプセル化されたコンポーネントで構成されるシステムをモデル化するために使用することができる。
本稿では,FTTS (Floating-Time Transition System) とTTS (Common Timed Transition System) の両方を,これらのモデルのセマンティクスとして用いる方法について説明する。
モデルチェックツールセットは、スケジューリング可能性分析、デッドロックとキューオーバーフローチェック、アサーションベースのTimed Rebecaモデルの検証をサポートする。
論文 参考訳(メタデータ) (2023-09-13T20:50:11Z) - Spatiotemporal Inconsistency Learning for DeepFake Video Detection [51.747219106855624]
本稿では,水平方向と垂直方向の両方で隣接するフレーム間の時間差を利用して,TIMにおける新しい時間的モデリングパラダイムを提案する。
ISMは、SIMからの空間情報とTIMからの時間情報とを同時に利用し、より包括的な時空間表現を確立する。
論文 参考訳(メタデータ) (2021-09-04T13:05:37Z) - SMT-based Safety Verification of Parameterised Multi-Agent Systems [78.04236259129524]
パラメータ化マルチエージェントシステム(MAS)の検証について検討する。
特に、与えられた状態公式として特徴づけられる不要な状態が、所定のMASで到達可能かどうかについて検討する。
論文 参考訳(メタデータ) (2020-08-11T15:24:05Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。