技術要約：タイムド・オパシティ（Timed Opacity）の明るい側面

1. 問題提起

本論文は、タイムド・オートマトン（Timed Automata: TAs）におけるタイムド・オパシティ（timed opacity）問題を扱う。タイムド・オパシティは、攻撃者が一部のアクションとそのタイムスタンプを観測できるシステムにおいて、指定された「プライベート」な場所に関する情報の漏洩がないことを定式化したものである。核心となるセキュリティ目標は、システムの実行中にプライベートな場所が訪問されたかどうかを、攻撃者が確信を持って推論できないようにすることである。

この問題は、Cassez [Cas09] による先駆的な研究に端を発している。同研究は、一般的なTA、さらには制限されたサブクラスである**イベント記録オートマトン（Event-Recording Automata: ERA）においてさえ、タイムド・オパシティが決定不能（undecidable）**であることを示した。この決定不能性は、タイムスタンプを相関させるために攻撃者に必要なメモリが無制限であること、およびTAの無限の状態空間に起因する。著者らは、システムモデルまたは攻撃者の能力のいずれかを制限することで、決定可能性を取り戻し、この問題の「明るい側面（bright sides）」を特定することを目指している。

本論文では、プライベートな実行によって生成されるトレースの集合（$Tr_{priv}$）と、パブリックな実行による集合（$Tr_{pub}$）の関係に基づき、以下の3つのオパシティのバリアントを定義している：

1. $\exists$-opacity: プライベートな実行とパブリックな実行の両方に共通するトレースが少なくとも一つ存在する（最も弱い形式）。
2. Weak opacity（弱オパシティ）: すべてのプライベートなトレースはパブリックなトレースでもある（$Tr_{priv} \subseteq Tr_{pub}$）。
3. Full opacity（完全オパシティ）: プライベートなトレースの集合とパブリックなトレースの集合が同一である（$Tr_{priv} = Tr_{pub}$）。

2. 手法

著者らは、オートマトン理論的な構成、古典的なTA問題（到達可能性、言語包含）への帰着、および複雑性解析を組み合わせて用いている。

2.1. 相互還元フレームワーク

基礎的な手法論的貢献は、オパシティのバリアントと古典的なTA問題の間の**相互還元性（inter-reducibility）**の確立である：

• Weak vs. Full Opacity: プライベートな実行とパブリックな実行を入れ替える構成によって、これらが相互還元可能であることが証明された（定理 4.5）。これにより、著者らは決定可能性の証明において、通常は弱オパシティに焦点を当てることが可能となった。
• $\exists$-opacity vs. Reachability: 相互還元可能であることが証明された。到達可能性はTAにおいてPSPACE完全であるため、これにより$\exists$-オパシティの複雑性が確立される。
• Weak Opacity vs. Language Inclusion: 相互還元可能であることが証明された。一般的なTAにおいて言語包含は決定不能であるため、これは一般的なケースにおける弱/完全オパシティの決定不能性を説明している。

2.2. サブクラス解析

著者らは、特定のTAのサブクラスについてオパシティを分析している：

• One-action TAs: アルファベットのサイズを削減。
• One-clock TAs: クロックの数を削減（$\epsilon$-遷移の有無を含む）。
• Discrete Time TAs: クロックの値を実数（$\mathbb{R}_{\ge 0}$）ではなく自然数（$\mathbb{N}$）に制限。
• Observable ERAs (oERAs): クロックをリセットするすべてのアクションが観測可能である新しいサブクラス（クロックをリセットする隠れた$\epsilon$-遷移が存在しない）。

2.3. 攻撃者予算の削減

TAの全クラスを扱うために、著者らは攻撃者の「予算」を制限する新しい手法を導入している。彼らは、攻撃者がシステムをいつ観測するかを決定するタイム選択関数（time selection functions）（$\sigma$）を定義している。以下の3つの具体的な設定が分析されている：

1. 最初の $N$ 個の観測: 攻撃者は最初の $N$ 個の観測可能なアクションのみを見る。
2. $N$ 個の静的タイムスタンプ: 攻撃者は $N$ 個の時点を事前に選択し、各時点の後に発生する最初の動作を観測する。
3. $N$ 個の動的タイムスタンプ: 攻撃者は、以前の観測に基づいて次の観測時刻を適応的に選択する。

これらの限定された設定における決定可能性を証明するために、著者らは**「ティック（tick）」構成を導入している。これは、グローバルな「ティック」クロックと補助クロックを用いて、タイムド・ワードの等価類**（整数部分および分数部分の相対的な順序に基づく）を**アンタイムド（untimed）**なトレースへとエンコードする手法である。これにより、限定された観測下でのタイムド言語包含問題を、有限の正規オートマトン（具体的には $N$-bounded 言語）の言語包含問題へと変換する。

3. 主な貢献と結果

3.1. 相互還元性と複雑性

• Weak と Full オパシティの同値性: 弱オパシティを判定することは、完全オパシティを判定することと多項式時間で同値であることを証明した。これにより、サブクラスの分析が簡素化される。
• $\exists$-オパシティの複雑性: 一般的なTAにおいて、この問題はPSPACE完全である。One-clock TAにおいても、$\exists$-オパシティはPSPACE完全であり続けることが証明された（定理 5.1）。これは従来の境界を精緻化するものである。

3.2. サブクラスにおける決定可能性

本論文は、弱/完全オパシティに関する決定可能性の境界を明確に描き出している：

• 決定不能:
  • 単一のアクションを持つTA（$\epsilon$-遷移がない場合でも）（定理 5.2）。
  • 2つ以上のクロックを持つTA（定理 5.7）。
  • $\epsilon$-遷移を伴う単一のクロックを持つTA（定理 5.4）。
• 決定可能:
  • $\epsilon$-遷移を伴わない単一のクロックを持つTA：**非原始再帰的（non-primitive recursive）**な複雑さで決定可能（定理 5.5）。
  • **離散時間（discrete time）**上のTA：EXPSPACE完全な複雑さで決定可能（系 5.14）。
  • Observable ERAs (oERAs)：PSPACE完全な複雑さで決定可能（定理 5.16）。

注：本論文はまた、離散時間TAにおけるタイムド言語包含がEXPSPACE完全であることも確立している。これは、決定可能であることは既知であったが、正確な複雑性が不明であった結果である。

3.3. 限定された攻撃者予算（主要な貢献）

最も重要な貢献は、攻撃者の観測予算が $N$ 回の観測に制限されている場合、全クラスのTAに対してオパシティが決定可能になることを示した点である。

• 設定: この結果は、「最初の $N$ 個のイベント」、「$N$ 個の静的タイムスタンプ」、「$N$ 個の動的タイムスタンプ」のすべての攻撃者モデルにおいて成立する。
• 複雑性: これら3つの設定における決定問題は、すべて Co-NEXPTIME完全 である（定理 6.19, 系 6.20, 定理 6.31, 定理 6.33）。
• メカニズム: 証明は、「ティック」構成を用いて、タイムドの問題を $N$-bounded タイムド言語の包含問題へと還元することに依拠している。これは Co-NEXPTIME 完全であることが示されている。

3.4. 組み合わせによる制限

著者らは、モデルの制限（例：one-clock, discrete time）と攻撃者予算の組み合わせについても分析している。

• $N$ 回の観測を行うone-action TAの場合、問題は依然として Co-NEXPTIME完全 である。
• $N$ 回の観測を行うone-clock TAの場合、問題は PSPACE困難（PSPACE-hard） であり、かつ Co-NEXPTIME に属する（定理 6.35）。
• $N$ 回の観測を行う oERAs の場合、問題は PSPACE完全 である（定理 6.37）。

4. 意義と主張

本論文は、Cassez [09] による負の結果を超えて、タイムド・オパシティの決定可能性のランドスケープを包括的に特徴づけている。

• 境界の明確化: 本研究は、決定不能性を引き起こす最小限の条件（例：one-clock TAにおける $\epsilon$-遷移の存在や、アクションの数）を正確に特定している。
• 実用的な決定可能性: 攻撃者の予算（有限の観測）を制限するという概念を導入することで、攻撃者が無制限のイベントシーケンスを観測できない限り、全クラスのタイムド・オートマトンに対してオパシティが決定可能であることを示している。これは、攻撃者が限られたリソースや監視能力しか持たない現実的なシナリオをモデル化している。
• 複雑性のタイトネス: 論文は、様々な設定に対して正確な複雑性クラス（PSPACE, EXPSPACE, Co-NEXPTIME）を提供しており、オパシティ検証の計算コストに関する理解を深めている。
• 手法論的革新: 「ティック」構成とタイム選択関数の使用は、部分観測下でのタイムド・システムを分析するための新しいツールを提供し、高密度時間（dense-time）セマンティクスと有限状態検証技術の間の架け橋となっている。

著者らは、高度に表現力豊かな設定（無制限の観測を行う一般的なTA）では決定不能性が存続するものの、攻撃者の力を有限の予算に制限することで、完全なTA形式論理に適用可能な、堅牢で決定可能なフレームワークが得られると結論付けている。