論文の概要: 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: タイムセキュリティプロトコルの検証
- Authors: Agnieszka M. Zbrzezny,
- 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} デモも公開されている。
関連論文リスト
- 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)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。