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の根

• statusAsOf : Timestamp

  状態を確認した時刻。取得時刻ではない。署名対象。

• issuer : ValidDID

  発行者および状態系列。署名対象。

• statusSeries : String
• validUntil : Timestamp

  有効期限

• version : MerkleVersion

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

• issuerSignature : Signature

  Issuerの署名

instance instReprMerkleRevocationList : Repr MerkleRevocationList

Equations

• instReprMerkleRevocationList = { reprPrec := reprMerkleRevocationList✝ }

def MerkleRevocationList.verifySignature (mrl : MerkleRevocationList) (issuerPublicKey : PublicKey) (verifySignedSnapshot : MerkleRevocationList → PublicKey → Bool) : Bool

実暗号の署名検証器を明示的に渡す。署名対象はissuer/statusSeries/root/ version/statusAsOf/validUntil。以前の常にtrueを返すスタブを廃止。

Equations

• mrl.verifySignature issuerPublicKey verifySignedSnapshot = verifySignedSnapshot mrl issuerPublicKey

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が改ざん不可。

• context : PresentationContext
• revocationEnabled : Bool

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

• merkleRoot : Option MerkleRoot

  Merkle Root（証明に使う状態時点。現在の最新とは限らない）

• merkleRootVersion : Option MerkleVersion

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

• statusIssuer : Option ValidDID

  元資格の参照と同じ発行者/状態系列。証明に束縛される。

• statusSeries : Option String
• 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生成失敗
• 対象Rootで包含証明が不正 → このRootへの証明生成失敗（過去Rootは別）

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

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

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

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

Equations

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

inductive CurrentRevocationStatus : Type

• unknown : CurrentRevocationStatus
• confirmedRevoked : CurrentRevocationStatus

instance instReprCurrentRevocationStatus : Repr CurrentRevocationStatus

Equations

• instReprCurrentRevocationStatus = { reprPrec := reprCurrentRevocationStatus✝ }

instance instDecidableEqCurrentRevocationStatus : DecidableEq CurrentRevocationStatus

Equations

• instDecidableEqCurrentRevocationStatus x✝ y✝ = if h : x✝.toCtorIdx = y✝.toCtorIdx then isTrue ⋯ else isFalse ⋯

structure RevocationObservation : Type

• proofValid : Bool
• statusAtSnapshotActive : Bool
• statusAsOf : Option Timestamp
• snapshotAgeSeconds : Option ℕ
• snapshotExpired : Option Bool
• currentStatus : CurrentRevocationStatus
• newerAuthenticatedSnapshotKnown : Bool
• provenance : Option (ValidDID × String × MerkleRoot × MerkleVersion)

instance instReprRevocationObservation : Repr RevocationObservation

Equations

• instReprRevocationObservation = { reprPrec := reprRevocationObservation✝ }

def verifyMerkleRootAtVerifier (snapshot : MerkleRevocationList) (issuerPublicKey : PublicKey) (verifySignedSnapshot : MerkleRevocationList → PublicKey → Bool) : Bool

署名検証は時刻による受理判断を含めない。

Equations

• verifyMerkleRootAtVerifier snapshot issuerPublicKey verifySignedSnapshot = snapshot.verifySignature issuerPublicKey verifySignedSnapshot

def snapshotAge (snapshot : MerkleRevocationList) (now : Option Timestamp) : Option ℕ

不明な時計と未来の時刻はunknown。許容時計ずれは実装プロファイルで定義。

Equations

• snapshotAge snapshot now = now.bind fun (t : Timestamp) => if snapshot.statusAsOf.unixTime ≤ t.unixTime then some (t.unixTime - snapshot.statusAsOf.unixTime) else none

def verifyZKPWithRevocation (zkp : UnknownZKP) (publicInputs : ZKPPublicInputWithRevocation) (expectedContext : PresentationContext) (used latest : Option MerkleRevocationList) (issuerPublicKey : PublicKey) (verifySignedSnapshot : MerkleRevocationList → PublicKey → Bool) (verifyProof : UnknownZKP → ZKPPublicInputWithRevocation → Bool) (now : Option Timestamp) (checkStatus knownRevoked : Bool) : RevocationObservation

個別失効確認は認証済みの別証拠から得る。包含証明の欠如からは推論しない。 verifyProofは渡された公開入力との束縛を検証する実装契約。 checkStatus=falseは災害時の失効未確認プロファイルであり、元資格の revocationEnabledを書き換えない。元署名/属性/主体束縛は常に検証する。

Equations

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

def acceptByRevocationPolicy (observation : RevocationObservation) (policy : RevocationObservation → Bool) : Bool

業務上の例外受理を含むポリシー。観測結果を改変せず別値として記録する。

Equations

• acceptByRevocationPolicy observation policy = (observation.proofValid && policy observation)

def retainNewerSnapshot (known candidate : MerkleRevocationList) : MerkleRevocationList

認証済み最新状態を古い提示で上書きしない。別系列は別に保存する。 呼出側は両snapshotの署名を検証済みであること。

Equations

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

theorem older_snapshot_does_not_replace (known candidate : MerkleRevocationList) (h : candidate.version ≤ known.version) : retainNewerSnapshot known candidate = known

theorem unknown_clock_has_unknown_age (snapshot : MerkleRevocationList) : snapshotAge snapshot none = none

theorem invalid_proof_cannot_be_accepted (observation : RevocationObservation) (policy : RevocationObservation → Bool) (h : observation.proofValid = false) : acceptByRevocationPolicy observation policy = false

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として構築された包含証明は、常に検証に失敗する。 対象Rootへの不正な証明の拒否のみを保証。現在の失効は推論しない。

theorem invalid_membership_cannot_generate_zkp (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: 対象Rootで不正な包含証明を拒否

この定理の前提はmerkleProof.verify = false。失効前Rootへの正しい証明は対象外。

証明の流れ:

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

def revocation_security_guarantees : String

定理の対象は入力整合性と状態報告。実暗号、時計の信頼性、最新情報の 到達性は別途検証する。過去Rootへの正しい証明は現在有効を意味しない。

Equations

• revocation_security_guarantees = "Snapshot-bound checks; authenticated freshness; unknown offline status; verifier policy."

theorem confirmed_revocation_survives_old_evidence (zkp : UnknownZKP) (pub : ZKPPublicInputWithRevocation) (expectedContext : PresentationContext) (used latest : Option MerkleRevocationList) (key : PublicKey) (signatureCheck : MerkleRevocationList → PublicKey → Bool) (proofCheck : UnknownZKP → ZKPPublicInputWithRevocation → Bool) (now : Option Timestamp) (checkStatus : Bool) : (verifyZKPWithRevocation zkp pub expectedContext used latest key signatureCheck proofCheck now checkStatus true).currentStatus = CurrentRevocationStatus.confirmedRevoked