structure Timestamp : Type

タイムスタンプを表す型

• unixTime : ℕ

instance instReprTimestamp : Repr Timestamp

Equations

• instReprTimestamp = { reprPrec := reprTimestamp✝ }

instance instDecidableEqTimestamp : DecidableEq Timestamp

Equations

• instDecidableEqTimestamp = decEqTimestamp✝

structure ZKProofCore : Type

Zero-Knowledge Proof の基本構造

すべてのZKPはこの基本構造を含む。

注意: W3Cが標準化しているのは一般的なproof構造であり、 ZKP固有の構造ではありません。この構造はAMATELUSのZKP実装のために定義されています。

参考: W3C VC Data Model 2.0 の Proof 仕様（一般的な証明構造）

• proof : Proof
• publicInput : PublicInput
• proofPurpose : String
• created : Timestamp

structure VerifierAuthZKPCore : Type

Verifier認証用ZKPの基本構造

Verifierが自身の正当性を証明するためのZKP。 "私（verifierDID）は、信頼できるトラストアンカーから 発行されたVerifierVCを保持している"ことを証明。

• core : ZKProofCore
• verifierDID : UnknownDID
• credentialType : String

structure HolderCredentialZKPCore : Type

Holder資格証明用ZKPの基本構造

Holderが特定の属性を証明するためのZKP。 "私は特定の属性を満たすVCを保持している"ことを証明。 例: "私は20歳以上である"、"私は運転免許を持っている"など

ゼロ知識性の保証: HolderのDIDは含まれない。ZKPの本質は「誰が」ではなく「何を」証明するか。 Verifierは属性の正当性のみを検証し、Holderの身元は知らない。

• core : ZKProofCore
• claimedAttributes : String

@[reducible, inline]

abbrev VerifierAuthZKP : Type

VerifierAuthZKPの型エイリアス（MutualAuthenticationで使用）

Equations

• VerifierAuthZKP = VerifierAuthZKPCore

@[reducible, inline]

abbrev HolderCredentialZKP : Type

HolderCredentialZKPの型エイリアス（MutualAuthenticationで使用）

Equations

• HolderCredentialZKP = HolderCredentialZKPCore

structure ValidZKP : Type

正規のゼロ知識証明 (Valid Zero-Knowledge Proof)

暗号学的に正しく生成されたZKP。 任意のRelationに対して暗号的検証が成功する（verifyを通過する）。

設計思想:

• ZKPの生成はWalletの責任（暗号ライブラリの実装詳細）
• プロトコルレベルでは「正規に生成されたZKP」として抽象化
• Verifierは暗号的検証のみに依存し、Wallet実装を信頼しない

抽象化の利点:

• Groth16のペアリング検証などの暗号的詳細を隠蔽
• プロトコルの安全性証明が簡潔になる
• Wallet実装の違いを抽象化（同じプロトコルで多様なWallet実装が可能）

• zkpType : VerifierAuthZKPCore ⊕ HolderCredentialZKPCore

structure InvalidZKP : Type

不正なゼロ知識証明 (Invalid Zero-Knowledge Proof)

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

• Witness（秘密情報）が不正
• 証明データπが改ざんされている
• ランダムネスが不足している（Walletバグ）
• 署名検証に失敗する
• Relationが不一致

Walletバグの影響:

• バグのあるWalletが生成したZKPはInvalidZKPとして表現される
• プロトコルの安全性には影響しない（当該利用者のみが影響を受ける）

• zkpType : VerifierAuthZKPCore ⊕ HolderCredentialZKPCore
• reason : String

inductive UnknownZKP : Type

未検証のゼロ知識証明 (Unknown Zero-Knowledge Proof)

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

• valid: 正規に生成されたZKP（暗号的に正しい）
• invalid: 不正なZKP（暗号的に間違っている、または改ざんされている）

設計の利点:

• ZKP検証の暗号的詳細（Groth16のペアリング計算など）を抽象化
• プロトコルレベルでは「正規/不正」の区別のみが重要
• Wallet実装のバグはinvalidとして表現され、プロトコルの安全性には影響しない

• valid : ValidZKP → UnknownZKP
• invalid : InvalidZKP → UnknownZKP

def UnknownZKP.getCore : UnknownZKP → ZKProofCore

ZKPから基本構造を取得

Equations

• (UnknownZKP.valid vzkp).getCore = match vzkp.zkpType with | Sum.inl verifier => verifier.core | Sum.inr holder => holder.core
• (UnknownZKP.invalid izkp).getCore = match izkp.zkpType with | Sum.inl verifier => verifier.core | Sum.inr holder => holder.core

def UnknownZKP.verify : UnknownZKP → Relation → Bool

ZKP検証関数（定義として実装）

設計の核心:

• 正規のZKP（valid）: 常に検証成功（暗号的に正しい）
• 不正なZKP（invalid）: 常に検証失敗（暗号的に間違っている）

この単純な定義により、暗号的詳細（Groth16ペアリング検証など）を 抽象化しつつ、プロトコルの安全性を形式的に証明できる。

Relationパラメータの意味: 実際の実装では、Relationに応じて異なる検証ロジックが実行されますが、 プロトコルレベルでは「ValidZKPは任意のRelationに対して検証成功」 という抽象化で十分です。

Walletバグの影響:

• バグのあるWalletが生成したZKPはinvalidとして表現される
• verify (invalid _) _ = falseにより、検証は失敗する
• したがって、Walletバグは当該利用者のみに影響

Equations

• (UnknownZKP.valid a).verify x✝ = true
• (UnknownZKP.invalid a).verify x✝ = false

def UnknownZKP.isValid (zkp : UnknownZKP) (relation : Relation) : Prop

ZKPが有効かどうかを表す述語

Equations

• zkp.isValid relation = (zkp.verify relation = true)

theorem UnknownZKP.valid_zkp_passes (vzkp : ValidZKP) (relation : Relation) : (valid vzkp).isValid relation

Theorem: 正規のZKPは常に検証成功

暗号学的に正しく生成されたZKPは、任意のRelationに対して 検証が成功する。これは定義から自明だが、明示的に定理として示す。

theorem UnknownZKP.invalid_zkp_fails (izkp : InvalidZKP) (relation : Relation) : ¬(invalid izkp).isValid relation

Theorem: 不正なZKPは常に検証失敗

暗号学的に不正なZKPは、どのRelationに対しても検証が失敗する。 これにより、Walletバグや改ざんされたZKPが受け入れられないことを保証。

structure DeviceConstraints : Type

デバイスの計算資源制約を表す構造体

• storageAvailable : ℕ
• computationAvailable : ℕ
• timeIdle : ℕ

instance instReprDeviceConstraints : Repr DeviceConstraints

Equations

• instReprDeviceConstraints = { reprPrec := reprDeviceConstraints✝ }

instance instDecidableEqDeviceConstraints : DecidableEq DeviceConstraints

Equations

• instDecidableEqDeviceConstraints = decEqDeviceConstraints✝

structure ZKPRequirements : Type

ZKP生成の資源要件を表す構造体

• storagePrecomp : ℕ
• computationPrecomp : ℕ
• timePrecomp : ℕ
• timeRealtimeNonce : ℕ

instance instReprZKPRequirements : Repr ZKPRequirements

Equations

• instReprZKPRequirements = { reprPrec := reprZKPRequirements✝ }

instance instDecidableEqZKPRequirements : DecidableEq ZKPRequirements

Equations

• instDecidableEqZKPRequirements = decEqZKPRequirements✝