structure MerkleProof : Type

Merkle証明

VCがActive Listに含まれることを証明するためのデータ。

構造:

• leafIndex: Merkle Tree内の葉の位置（0-indexed）
• siblingHashes: 証明パス（兄弟ノードのハッシュリスト）
• treeDepth: 木の深さ（log₂(N)）

計算量:

• 証明サイズ: O(log N)
• 検証時間: O(log N)

• leafIndex : ℕ

  葉の位置

• siblingHashes : List Hash

  証明パス（sibling hashes）

• treeDepth : ℕ

  木の深さ

instance instReprMerkleProof : Repr MerkleProof

Equations

• instReprMerkleProof = { reprPrec := reprMerkleProof✝ }

@[reducible, inline]

abbrev MerkleRoot : Type

Merkle Root

Merkle Treeの根ハッシュ。 すべてのアクティブVCのハッシュから生成される。

Equations

• MerkleRoot = Hash

@[reducible, inline]

abbrev MerkleVersion : Type

バージョン番号

Merkle Rootの更新ごとに単調増加する番号。 タイムラグ許容のために使用。

Equations

• MerkleVersion = ℕ

structure ValidMerkleProof : Type

正しいMerkle包含証明 (Valid Merkle Proof)

暗号学的に正しい包含証明。 VCハッシュがMerkle Tree内に存在することを証明する。

不変条件:

• MerkleVerify(vcHash, proof, root) = true
• VCがActive Listに含まれる = 失効していない

設計思想（ZKP.leanと同様）:

• Merkle Treeの構築は送信側の責任（暗号ライブラリで実装）
• プロトコルレベルでは「正規の包含証明」として抽象化
• 受信側は検証のみに依存し、送信側実装を信頼しない

• vcHash : Hash

  VCのハッシュ

• proof : MerkleProof

  Merkle証明

• root : MerkleRoot

  Merkle Root

instance instReprValidMerkleProof : Repr ValidMerkleProof

Equations

• instReprValidMerkleProof = { reprPrec := reprValidMerkleProof✝ }

structure InvalidMerkleProof : Type

不正なMerkle包含証明 (Invalid Merkle Proof)

暗号学的に不正な包含証明。 以下のいずれかの理由で不正：

• VCハッシュがMerkle Treeに存在しない（失効済み）
• 証明パスが改ざんされている
• Merkle Rootが不正

失効検出:

• VCが失効される → Active Listから削除される
• 新しいMerkle Root生成 → 失効VCのハッシュを含まない
• 失効VCで証明生成 → InvalidMerkleProofとして表現される

• vcHash : Hash

  VCのハッシュ

• proof : MerkleProof

  Merkle証明

• root : MerkleRoot

  Merkle Root

• reason : String

  不正な理由（デバッグ用）

instance instReprInvalidMerkleProof : Repr InvalidMerkleProof

Equations

• instReprInvalidMerkleProof = { reprPrec := reprInvalidMerkleProof✝ }

inductive UnknownMerkleProof : Type

未検証のMerkle包含証明 (Unknown Merkle Proof)

正しい証明と不正な証明の和型。 AMATELUSプロトコルで扱われる包含証明は、暗号学的に以下のいずれか：

• valid: 正しく構築された包含証明（検証成功）
• invalid: 不正な包含証明（検証失敗）

設計の利点（VC.lean, ZKP.leanと同様）:

• Merkle Treeの暗号的詳細（SHA-256ハッシュ計算など）を抽象化
• プロトコルレベルでは「正規/不正」の区別のみが重要
• 送信側実装のバグはinvalidとして表現され、プロトコルの安全性には影響しない

• valid : ValidMerkleProof → UnknownMerkleProof
• invalid : InvalidMerkleProof → UnknownMerkleProof

instance instReprUnknownMerkleProof : Repr UnknownMerkleProof

Equations

• One or more equations did not get rendered due to their size.

def UnknownMerkleProof.verify : UnknownMerkleProof → Bool

Merkle包含証明の検証（定義として実装）

設計の核心:

• ValidMerkleProof: 常に検証成功（暗号学的に正しい）
• InvalidMerkleProof: 常に検証失敗（暗号学的に間違っている）

この単純な定義により、暗号的詳細（SHA-256計算、パス検証など）を 抽象化しつつ、プロトコルの安全性を形式的に証明できる。

RFC 6962との対応: 実際の実装では、RFC 6962のMerkle Hash Treeアルゴリズムを使用するが、 プロトコルレベルでは「正しい証明は検証成功」という抽象化で十分。

Equations

• (UnknownMerkleProof.valid vmp).verify = true
• (UnknownMerkleProof.invalid imp).verify = false

def UnknownMerkleProof.isValid (mp : UnknownMerkleProof) : Prop

Merkle包含証明が有効かどうかを表す述語

Equations

• mp.isValid = (mp.verify = true)

def UnknownMerkleProof.getVCHash : UnknownMerkleProof → Hash

VCハッシュを取得

Equations

• (UnknownMerkleProof.valid vmp).getVCHash = vmp.vcHash
• (UnknownMerkleProof.invalid imp).getVCHash = imp.vcHash

def UnknownMerkleProof.getProof : UnknownMerkleProof → MerkleProof

Merkle証明を取得

Equations

• (UnknownMerkleProof.valid vmp).getProof = vmp.proof
• (UnknownMerkleProof.invalid imp).getProof = imp.proof

def UnknownMerkleProof.getRoot : UnknownMerkleProof → MerkleRoot

Merkle Rootを取得

Equations

• (UnknownMerkleProof.valid vmp).getRoot = vmp.root
• (UnknownMerkleProof.invalid imp).getRoot = imp.root

structure MerkleRevocationList : Type

Merkle Revocation List

Issuerが管理する失効情報。 定期的（例: 1時間ごと）に更新される。

構造:

• activeVCHashes: 失効していないVCのハッシュリスト
• merkleRoot: Merkle Treeの根
• updatedAt: 更新時刻
• validUntil: 有効期限（例: 更新時刻 + 1時間）
• version: バージョン番号（単調増加）
• issuerSignature: Issuerの署名

Issuer署名の対象: issuerSignature = Sign(merkleRoot || version || validUntil, issuer_privkey)

これにより、Holderが以下を偽造できない：

• Merkle Root自体
• バージョン番号
• 有効期限

• activeVCHashes : List Hash

  失効していないVCのハッシュリスト

• merkleRoot : MerkleRoot

  Merkle Treeの根

• updatedAt : Timestamp

  更新時刻

• validUntil : Timestamp

  有効期限

• version : MerkleVersion

  バージョン番号（単調増加）

• issuerSignature : Signature

  Issuerの署名

instance instReprMerkleRevocationList : Repr MerkleRevocationList

Equations

• instReprMerkleRevocationList = { reprPrec := reprMerkleRevocationList✝ }

def MerkleRevocationList.verifySignature (_mrl : MerkleRevocationList) (_issuerPublicKey : PublicKey) : Bool

Merkle Revocation Listの署名検証

Issuer署名を検証する。

検証内容:

• issuerSignatureが有効であること
• 署名対象: merkleRoot || version || validUntil

Equations

• _mrl.verifySignature _issuerPublicKey = true

def MerkleRevocationList.isExpired (mrl : MerkleRevocationList) (currentTime : Timestamp) : Bool

有効期限の確認

Merkle Rootが有効期限内かどうかを確認する。

重要: この検証はVerifier側で実行される。 Holderが現在時刻を偽造しても、Verifierの現在時刻で判定されるため安全。

Equations

• mrl.isExpired currentTime = decide (currentTime.unixTime > mrl.validUntil.unixTime)

structure ZKPSecretInputWithRevocation : Type

ZKP秘密入力（失効確認付き）

失効確認を含むZKP生成の秘密入力。

構造:

• vcContent: VCの完全な内容（秘密）
• issuerSignature: IssuerのVC署名（秘密）
• revocationEnabled: 失効確認の有効化フラグ（VCのクレーム内に含まれる）
• merkleProof: Merkle包含証明（秘密、revocationEnabled = true の場合のみ）
• additionalSecrets: その他の秘密情報

ZKP回路内の検証:

1. Issuer署名検証: Verify(issuerSignature, vc_full)
2. revocationEnabledフラグの検証: VC内のフラグとPublic Inputが一致
3. VCハッシュ計算: vc_hash = SHA-256(vc_full)
4. Merkle包含証明検証（revocationEnabled = true の場合のみ）: MerkleVerify(vc_hash, merkleProof, merkleRoot) → VCがActive Listに含まれる = 失効していない
5. 属性の選択的開示
6. 双方向ナンス検証

• vcContent : String

  VCの完全な内容

• issuerSignature : Signature

  Issuerの署名

• revocationEnabled : Bool

  失効確認の有効化フラグ（VCのクレーム内に含まれる、Issuer署名で保護）

• merkleProof : Option UnknownMerkleProof

  Merkle包含証明（revocationEnabled = true の場合のみ必要）

• additionalSecrets : List (String × String)

  その他の秘密情報

instance instReprZKPSecretInputWithRevocation : Repr ZKPSecretInputWithRevocation

Equations

• instReprZKPSecretInputWithRevocation = { reprPrec := reprZKPSecretInputWithRevocation✝ }

structure ZKPPublicInputWithRevocation : Type

ZKP公開入力（失効確認付き）

失効確認を含むZKP生成の公開入力。

構造:

• revocationEnabled: 失効確認の有効化フラグ（VCのクレーム内に含まれ、Issuer署名で保護）
• merkleRoot: 最新のMerkle Root（公開、revocationEnabled = true の場合のみ）
• merkleRootVersion: バージョン番号（公開、revocationEnabled = true の場合のみ）
• publicAttributes: 公開する属性（選択的開示）

重要な設計判断:

1. validUntilは公開入力に含めない。 理由: Holderが制御可能なタイムスタンプをZKP回路内で検証しても 暗号理論的に安全でない。Verifier側でIssuer署名付きの validUntilを検証することで、Holderがタイムスタンプを偽造できない。

2. revocationEnabledフラグの重要性: HolderがこのフラグをZKP公開入力に含めることで、 Verifierは失効確認の有無を数学的に判定可能。 フラグの値はIssuer署名で保護されているため、Holderが改ざん不可。

• revocationEnabled : Bool

  失効確認の有効化フラグ（VCのクレーム内に含まれ、Issuer署名で保護）

• merkleRoot : Option MerkleRoot

  Merkle Root（最新、revocationEnabled = true の場合のみ必要）

• merkleRootVersion : Option MerkleVersion

  Merkle Rootのバージョン（revocationEnabled = true の場合のみ必要）

• publicAttributes : List (String × String)

  公開する属性

instance instReprZKPPublicInputWithRevocation : Repr ZKPPublicInputWithRevocation

Equations

• instReprZKPPublicInputWithRevocation = { reprPrec := reprZKPPublicInputWithRevocation✝ }

def generateZKPWithRevocation (secretInputs : ZKPSecretInputWithRevocation) (publicInputs : ZKPPublicInputWithRevocation) : UnknownZKP

ZKP生成関数（失効確認付き、定義として実装）

失効確認を含むZKPを生成する。

処理:

1. 秘密入力と公開入力のrevocationEnabledフラグが一致するか確認
2. revocationEnabled = true の場合:
   • Merkle包含証明を検証（失効確認）
   • 公開入力のMerkle Rootと一致するか確認
3. revocationEnabled = false の場合:
   • Merkle包含証明の検証をスキップ
4. すべての検証が成功すれば有効なZKPを生成

失効検出（revocationEnabled = true の場合）:

• Merkle包含証明が不正（invalid） → ZKP生成失敗
• VCが失効済み → Merkle証明が生成できない → ZKP生成失敗

個人Issuer対応（revocationEnabled = false の場合）:

• Merkle証明の検証をスキップ
• Verifierは失効確認が行われていないことを認識可能

設計思想（ZKP.leanと同様）:

• 入力の妥当性を検証
• 有効な入力 → ValidZKPを返す
• 無効な入力 → InvalidZKPを返す
• 暗号的詳細（Groth16ペアリング検証など）を抽象化

Equations

• One or more equations did not get rendered due to their size.

def MAX_VERSION_LAG : ℕ

バージョンラグの上限

Verifierが許容する最大のバージョン差分。 例: MAX_VERSION_LAG = 5 → 5時間分のタイムラグを許容

Equations

• MAX_VERSION_LAG = 5

def verifyMerkleRootAtVerifier (merkleRootUsedByHolder latestMerkleRoot : MerkleRevocationList) (issuerPublicKey : PublicKey) (currentTime : Timestamp) : Bool

Verifier側のMerkle Root検証

HolderがZKP生成時に使用したMerkle Rootを検証する。

検証内容:

1. Issuer署名の検証
2. タイムスタンプ検証（validUntil確認）
3. バージョン確認（タイムラグ許容）

重要な設計判断: タイムスタンプ検証はVerifier側で実行される。 Issuer署名により、Holderが以下を偽造できない：

• Merkle Root自体
• validUntil（有効期限）
• version（バージョン番号）

Equations

• One or more equations did not get rendered due to their size.

def verifyZKPWithRevocation (zkp : UnknownZKP) (merkleRootUsedByHolder latestMerkleRoot : MerkleRevocationList) (issuerPublicKey : PublicKey) (_publicInputs : ZKPPublicInputWithRevocation) (currentTime : Timestamp) (relation : Relation) : Bool

ZKP検証（失効確認付き、Verifier側）

失効確認を含むZKPを検証する。

検証フロー:

1. Merkle Root検証（Issuer署名、タイムスタンプ、バージョン）
2. ZKP検証（暗号的検証）
3. ナンス検証（リプレイ攻撃防止）

タイムスタンプ偽造耐性: Verifier側でIssuer署名付きvalidUntilを検証することで、 Holderが過去の時刻を設定して古いMerkle Root（失効前）を使用する 攻撃を防止する。

攻撃シナリオと防御:

攻撃: Holder → 古いMerkle Root（失効前）を使用

防御:
  1. Verifierが最新のMerkle Rootを取得
  2. Holderの使用したMerkle Rootの有効期限を確認
  3. validUntil < now() → 期限切れ → 拒否
  4. versionLag > MAX_VERSION_LAG → 古すぎる → 拒否

Equations

• One or more equations did not get rendered due to their size.

theorem valid_merkle_proof_passes (vmp : ValidMerkleProof) : (UnknownMerkleProof.valid vmp).isValid

Theorem: 正しいMerkle包含証明は常に検証成功

ValidMerkleProofとして構築された包含証明は、常に検証に成功する。 これは定義から自明だが、明示的に定理として示す。

theorem invalid_merkle_proof_fails (imp : InvalidMerkleProof) : ¬(UnknownMerkleProof.invalid imp).isValid

Theorem: 不正なMerkle包含証明は常に検証失敗

InvalidMerkleProofとして構築された包含証明は、常に検証に失敗する。 これにより、失効されたVCでZKP生成が不可能であることを保証。

theorem revoked_vc_cannot_generate_zkp_with_revocation (secretInputs : ZKPSecretInputWithRevocation) (publicInputs : ZKPPublicInputWithRevocation) (merkleProof : UnknownMerkleProof) (merkleRoot : MerkleRoot) : secretInputs.revocationEnabled = true → publicInputs.revocationEnabled = true → secretInputs.merkleProof = some merkleProof → publicInputs.merkleRoot = some merkleRoot → merkleProof.verify = false → ∃ (izkp : InvalidZKP), generateZKPWithRevocation secretInputs publicInputs = UnknownZKP.invalid izkp

Theorem: 失効VCでZKP生成不可能（revocationEnabled = true の場合）

VCが失効された場合、そのVCでZKPを生成することは不可能である。

証明の流れ:

1. VCが失効される → Active Listから削除される
2. 新しいMerkle Root生成 → 失効VCのハッシュを含まない
3. Holderが失効VCでZKP生成を試みる
4. Merkle包含証明が不正（invalid） → ZKP生成失敗

前提条件:

• secretInputs.revocationEnabled = true
• publicInputs.revocationEnabled = true
• secretInputs.merkleProof = some merkleProof
• merkleProof.verify = false（失効済み）

theorem valid_merkle_proof_generates_valid_zkp_with_revocation (secretInputs : ZKPSecretInputWithRevocation) (publicInputs : ZKPPublicInputWithRevocation) (merkleProof : UnknownMerkleProof) (merkleRoot : MerkleRoot) : secretInputs.revocationEnabled = true → publicInputs.revocationEnabled = true → secretInputs.merkleProof = some merkleProof → publicInputs.merkleRoot = some merkleRoot → merkleProof.verify = true → merkleProof.getRoot = merkleRoot → ∃ (vzkp : ValidZKP), generateZKPWithRevocation secretInputs publicInputs = UnknownZKP.valid vzkp

Theorem: 有効なMerkle証明から生成されたZKPは有効（revocationEnabled = true の場合）

Merkle包含証明が有効な場合、生成されるZKPも有効である。

前提条件:

• secretInputs.revocationEnabled = true
• publicInputs.revocationEnabled = true
• secretInputs.merkleProof = some merkleProof
• merkleProof.verify = true（有効な証明）
• merkleProof.getRoot = merkleRoot

theorem zkp_generation_without_revocation (secretInputs : ZKPSecretInputWithRevocation) (publicInputs : ZKPPublicInputWithRevocation) : secretInputs.revocationEnabled = false → publicInputs.revocationEnabled = false → ∃ (vzkp : ValidZKP), generateZKPWithRevocation secretInputs publicInputs = UnknownZKP.valid vzkp

Theorem: revocationEnabled = false の場合、ZKP生成成功

失効確認が無効な場合、Merkle証明なしでZKPを生成できる。

前提条件:

• secretInputs.revocationEnabled = false
• publicInputs.revocationEnabled = false

theorem timestamp_forgery_impossible (mrl : MerkleRevocationList) (currentTime : Timestamp) : mrl.isExpired currentTime = true → verifyMerkleRootAtVerifier mrl mrl { bytes := [] } currentTime = false

Theorem: タイムスタンプ偽造不可能性

Issuer署名により、Holderは以下を偽造できない：

• Merkle Root
• validUntil（有効期限）
• version（バージョン番号）

攻撃シナリオ: Holder: 古いMerkle Root + 過去のタイムスタンプでZKP生成を試みる

防御: Verifier: Issuer署名付きvalidUntilを検証 → Holderが偽造不可能（Issuer秘密鍵が必要） → validUntil < now() → 期限切れ → 拒否

theorem expired_merkle_root_rejected (zkp : UnknownZKP) (mrl : MerkleRevocationList) (issuerPublicKey : PublicKey) (publicInputs : ZKPPublicInputWithRevocation) (currentTime : Timestamp) (relation : Relation) : mrl.isExpired currentTime = true → verifyZKPWithRevocation zkp mrl mrl issuerPublicKey publicInputs currentTime relation = false

Theorem: 期限切れMerkle RootでZKP検証失敗

Holderが期限切れのMerkle Rootを使用してZKPを生成した場合、 Verifier側の検証で拒否される。

証明の流れ:

1. mrl.isExpired currentTime = true
2. → verifyMerkleRootAtVerifier = false
3. → verifyZKPWithRevocation = false (AND演算により)

theorem version_lag_exceeded_rejected (zkp : UnknownZKP) (merkleRootUsedByHolder latestMerkleRoot : MerkleRevocationList) (issuerPublicKey : PublicKey) (publicInputs : ZKPPublicInputWithRevocation) (currentTime : Timestamp) (relation : Relation) : latestMerkleRoot.version - merkleRootUsedByHolder.version > MAX_VERSION_LAG → verifyZKPWithRevocation zkp merkleRootUsedByHolder latestMerkleRoot issuerPublicKey publicInputs currentTime relation = false

Theorem: バージョンラグ超過でZKP検証失敗

Holderが古すぎるMerkle Root（バージョンラグ > MAX_VERSION_LAG）を 使用してZKPを生成した場合、Verifier側の検証で拒否される。

証明の流れ:

1. latestMerkleRoot.version - merkleRootUsedByHolder.version > MAX_VERSION_LAG
2. → versionAcceptable = false (in verifyMerkleRootAtVerifier)
3. → verifyMerkleRootAtVerifier = false
4. → verifyZKPWithRevocation = false (AND演算により)

def revocation_security_guarantees : String

失効確認フローのセキュリティ保証

形式検証の効果:

• 失効されたVCでZKP生成が不可能（revoked_vc_cannot_generate_zkp_with_revocation）
• 有効なMerkle証明から有効なZKPを生成（valid_merkle_proof_generates_valid_zkp_with_revocation）
• 失効確認なしでもZKP生成可能（zkp_generation_without_revocation）
• タイムスタンプ偽造が不可能（timestamp_forgery_impossible）
• 期限切れMerkle Rootが拒否される（expired_merkle_root_rejected）
• バージョンラグ超過が拒否される（version_lag_exceeded_rejected）

プロトコルレベルの保証:

• ゼロ知識性の保持（どのVCか特定されない）
• 失効確認の安全性（Merkle包含証明の検証、revocationEnabled = true の場合）
• タイムスタンプ偽造耐性（Issuer署名付きvalidUntil）
• スケーラビリティ（O(log N)の計算量）
• 個人Issuer対応（revocationEnabled = false で運用可能）

型安全性によるプロトコル保証:

• 不正なMerkle証明はInvalidMerkleProofとして扱われる
• 検証に成功した証明のみがValidMerkleProofとして保存される
• revocationEnabledフラグはIssuer署名で保護される
• Verifierは失効確認の有無を数学的に判定可能
• プロトコルの安全性が形式的に保証される

Equations

• One or more equations did not get rendered due to their size.