4 段階検証モデル

E2E 検証可能投票の 4 段階検証モデルの設計と各段階の保証を解説します。

段階間の依存関係

概念モデルとしては 4 段階を順に評価しますが、実行場所は段階ごとに異なります（Stage 1 はクライアント、Stage 2-4 はサーバー中心）。実行責務の詳細は 設計と実行フロー を参照してください。

flowchart LR
  subgraph "証拠の生成"
    V["投票時<br/>投票レシート発行"]
    F["集計時<br/>zkVM 実行"]
  end

  subgraph "4 段階検証"
    S1["Stage 1<br/>Cast-as-Intended"]
    S2["Stage 2<br/>Recorded-as-Cast"]
    S3["Stage 3<br/>Counted-as-Recorded"]
    S4["Stage 4<br/>STARK Verification"]
  end

  V --> S1
  V --> S2
  F --> S3
  F --> S4

  S1 ~~~ S2
  S2 ~~~ S3
  S3 ~~~ S4

Stage 1: Cast-as-Intended

目的

投票者が意図した選択肢のコミットメントが、サーバーから返却された投票レシートと一致することを確認します。これにより、サーバーが投票者の選択を差し替える攻撃を検出します。

検証する内容

/verify 画面のクライアントコードがローカルに保持された 3 つの値（選挙 ID、選択肢、乱数）からコミットメントを再計算し、投票レシートのコミットメント値と照合します。

flowchart LR
  subgraph "投票時に確定したデータ"
    EID[選挙 ID]
    CH[選択肢]
    RND[乱数]
  end

  subgraph "再計算"
    HASH["SHA-256<br/>(ドメインタグ || 選挙ID || 選択肢 || 乱数)"]
  end

  subgraph "照合"
    CMP{"一致?"}
    REC[投票レシートの<br/>コミットメント]
  end

  EID --> HASH
  CH --> HASH
  RND --> HASH
  HASH --> CMP
  REC --> CMP

必要な証拠

voteReceipt は cast-time 証跡を store から再構成できた場合にだけ /api/verify から返ります。再構成できない場合の動作は 設計原則 3 を参照してください。

失敗モード

限界

Cast-as-Intended は以下の証拠に依存します:

• クライアント保持のローカル証拠（選挙 ID、選択肢、乱数）
• /api/verify が返す投票レシート（voteReceipt）

いずれかが欠ける場合、この段階は not_run になり最終判定は Verified になりません。

Stage 2: Recorded-as-Cast

目的

投票者のコミットメントが、追記専用の掲示板（CT Merkle ツリー）に正しく記録されていることを確認します。さらに、掲示板が追記専用性を維持していること（過去のエントリが削除・改変されていないこと）を検証します。

検証する内容

この段階には 3 系統の検証があります。UI ステップとの対応関係は ゲーティングロジック を参照してください。

flowchart TB
  subgraph "2a: 包含証明"
    IP["包含証明の検証<br/>自分のコミットメントが<br/>ツリーに存在するか"]
  end

  subgraph "2b: 整合性証明"
    CP["整合性証明の検証<br/>投票時のルートから<br/>最終ルートへの追記専用性"]
  end

  subgraph "2c: 第三者 STH 検証"
    STH["STH 合意の検証<br/>独立したソース間で<br/>ツリー状態が一致するか"]
  end

  IP --> RESULT{"Recorded 系の証拠を総合評価"}
  CP --> RESULT
  STH --> RESULT

2a: 包含証明（Inclusion Proof）

RFC 6962 の PATH 関数に基づく CT スタイルの Merkle 包含証明を検証し、投票者のコミットメントが掲示板のツリーに含まれていることを確認します。検証者はリーフハッシュと監査パスからルートハッシュを再計算し、期待されるルートと照合します。

2b: 整合性証明（Consistency Proof）

投票時点のツリー状態（ルートとサイズ）から、最終的なツリー状態への遷移が追記のみで行われたことを検証します。RFC 6962 の SUBPROOF アルゴリズムに基づく整合性証明により、サーバーが過去のエントリを密かに削除したり順序を変更したりするスプリットビュー攻撃を検出します。

2c: 第三者 STH 検証（オプション）

複数の独立した STH（Signed Tree Head）ソースに問い合わせ、合意が成立しているかを確認します。これにより、サーバーが検証者ごとに異なるツリー状態を提示するスプリットビュー攻撃を検出します。照合条件の詳細は チェック一覧 を参照してください。

必要な証拠

userVote.proof.treeSize は整合性証明における authoritative な oldSize であり、現行実装では voteReceipt.bulletinIndex + 1 との一致も要求します。cast-time 証跡が欠ける場合の fail-closed 動作は 設計原則 3 を参照してください。

失敗モード

Stage 3: Counted-as-Recorded

目的

掲示板に記録された全投票が、zkVM の集計処理に正しく含まれたことを確認します。投票の除外、欠落、重複がないことに加え、公開された claimed tally（表示用集計値）が zkVM の verifiedTally と一致することを検証し、集計結果の完全性と整合性を保証します。

検証する内容

この段階では 10 個の required チェックが全て success であることを要求します。

verificationSteps[].status も最終サマリーも、Counted stage で required 扱いになるチェック群全体から導出されます。journal がない場合は guard により stage 自体が not_run になります。UI ステップとの対応や journal 省略時の詳細は ゲーティングロジック を参照してください。

flowchart TD
  subgraph PUBLIC["public 系 required (6)"]
    P["counted_input_sanity<br/>counted_unique_indices<br/>counted_unique_<br/>commitments<br/>counted_election_<br/>manifest_consistent<br/>counted_close_<br/>statement_consistent<br/>counted_input_<br/>commitment_match"]
  end

  subgraph ZK["zk 系 required (4)"]
    Z["counted_tally_consistent<br/>counted_missing_<br/>indices_zero<br/>counted_expected_<br/>vs_tree_size<br/>counted_my_vote_<br/>included"]
  end

  RESULT{"10 required 全て success?"}
  PASS["Counted: success"]
  FAIL["Verified をブロック"]

  P --> RESULT
  Z --> RESULT
  RESULT -->|Yes| PASS
  RESULT -->|No| FAIL

必要な証拠

公開入力サマリーはサーバー内部表現であり、レスポンスにそのまま含まれません。inputCommitment が束縛するのは public-input.json の部分集合です。Counted stage では journal と slot-based なフィールド（excludedSlots 等）を正とし、missingIndices / invalidIndices / excludedCount は互換用としてのみ扱います。解決順序の詳細は チェック一覧 を参照してください。各チェックの判定ロジックは チェック一覧 を参照してください。

重要な判定: 除外数（excludedSlots / excludedCount）

excludedSlots は fail-closed（安全側に倒す）判定に使う除外数です。excludedCount は互換性のために残る旧名称で、同じ値を指します。

• excludedSlots == 0: 除外なし（正常）
• excludedSlots > 0: 掲示板スロットの未提示または計上失敗（即座に検証失敗）

counted_missing_indices_zero が除外数を解決し、0 でなければ failed になります。解決の優先順序は チェック一覧 を参照してください。除外数が残っている限り、最終判定は「Verified」を表示しません。

失敗モード

Stage 4: STARK Verification

目的

zkVM の実行が正しく行われたことを STARK 証明（レシート）の暗号学的検証により確認します。レシートの検証に成功すれば、ジャーナルの内容（集計結果、除外情報、入力コミットメント等）がゲストプログラムの正しい実行の結果であることが保証されます。

検証する内容

flowchart LR
  subgraph "入力"
    RCP[レシート<br/>Seal + Journal]
    EID[期待 Image ID]
  end

  subgraph "Rust 検証サービス"
    VF["Receipt::verify(imageId)"]
  end

  subgraph "結果"
    OK["success<br/>暗号学的に検証済み"]
    NG["failed<br/>証明が無効"]
    DM["dev_mode<br/>フェイクレシート"]
  end

  RCP --> VF
  EID --> VF
  VF --> OK
  VF --> NG
  VF --> DM

検証の 2 段階

STARK Verification では 2 つのチェックを実行します。

Image ID 照合: 検証サービスの report が利用できる場合、receipt_image_id が期待 Image ID と一致することを確認します。加えてホストが主張する Image ID（imageId）や comparison-only の journal.imageId とも矛盾しないことを検証します（解決順の詳細は チェック一覧 の stark_image_id_match を参照）。Image ID はゲストプログラムから導出される暗号的識別子であり、プログラムの改変やホスト主張値の食い違いを検出します。

レシート検証: RISC Zero の Receipt::verify() を呼び出し、Seal（STARK 証明）がジャーナルと Image ID に対して暗号学的に正当であることを検証します。この検証は計算量が多いため、サーバー側の Rust 検証サービスで実行されます。

必要な証拠

開発モードの検出

RISC0_DEV_MODE=1 で生成されたレシートは InnerReceipt::Fake 型であり、暗号学的な保証を持ちません。検証サービスはこれを dev_mode ステータスとして報告します。チェック評価では、設定に応じて dev_mode は success または not_run に正規化されます（既定では not_run 側）。

失敗モード

UI ステップと最終判定

UI ステップの対応チェック、集約ルール、最終 verdict の決定方法は ゲーティングロジック を参照してください。