def Holder.storeCredential (wallet : Wallet) (vc : ValidVC) (holderDID : ValidDID) (_h_subject : vc.subjectDID = holderDID) (_h_has_did : wallet.hasDID holderDID) : Wallet

WalletにVCを保存

設計変更: Holder構造体は単なるラッパーなので、操作はWalletレベルで行います。 不変条件 wallet_valid はHolder構築時に一度だけ保証されます。

この関数は単にcredentialsリストにVCを追加するだけで、 identitiesは変更しません。したがって、Wallet.isValidは保持されます。

Equations

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

def Holder.getCredential (wallet : Wallet) (predicate : ValidVC → Bool) : Option ValidVC

Walletから特定のVCを取得

Equations

• Holder.getCredential wallet predicate = List.find? predicate wallet.credentials

structure Holder.ZKPMaterial : Type

ZKP生成の材料をまとめた構造体

すべての可能な材料の組み合わせに対して 適切なZKPが既に存在しているという理想化モデル。

• precomputedProofs : List PrecomputedZKP
• credential : UnknownVC
• statement : PublicInput
• secretKey : SecretKey

def Holder.zkpMaterialToWitness (material : ZKPMaterial) : Witness

ZKPMaterialから証人（Witness）を抽出

暗号学的証明システムでは、証人は秘密情報（秘密鍵）です。 ZKPMaterialの秘密部分を証人として扱います。

Equations

• Holder.zkpMaterialToWitness material = { data := material.secretKey.bytes }

def Holder.zkpMaterialToPublicInput (material : ZKPMaterial) : PublicInput

ZKPMaterialから公開入力（PublicInput）を抽出

公開入力は、証明したいステートメントとナンスを含みます。

Equations

• Holder.zkpMaterialToPublicInput material = material.statement

def Holder.zkpRelation : Relation

ZKP検証の関係式（Relation）

この関係式は、証人（秘密鍵）と公開入力（ステートメント）の関係を定義します。

暗号学的意味：

• 証人が秘密鍵であることを検証
• VCの内容が公開入力と一致することを検証
• ナンスがリプレイ攻撃を防ぐことを検証

実装は抽象化されており、実際のSTARKs検証ロジックに委譲されます。

Equations

• Holder.zkpRelation _publicInput _witness = true

noncomputable def Holder.proofToZKP (proof : Proof) (material : ZKPMaterial) : UnknownZKP

ProofからZeroKnowledgeProofを構築

amtZKP.proverが生成したProofを、AMATELUSのZeroKnowledgeProof型に変換します。 生成されたProofは暗号学的に有効であるため、valid ZKPとして構築されます。

Equations

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

noncomputable def Holder.universalZKPOracle (material : ZKPMaterial) : UnknownZKP

無限のZKP辞書（暗号学的証明器による実装）

この関数は、すべての可能な材料に対してZKPを返します。 理想化モデル（ランダムオラクル）から暗号学的証明器（amtZKP）への移行。

変更点:

• amtZKP.proverを使用してProofを生成
• 生成されたProofはamtZKP.completenessにより有効であることが保証される

暗号学的安全性:

• SecurityAssumptions.amtZKP（STARKs）に依存
• 量子安全性: 128ビット（Grover適用後）
• NIST最小要件: 128ビット
• 結論: ポスト量子暗号時代でも安全

Equations

• Holder.universalZKPOracle material = Holder.proofToZKP (amtZKP.prover (Holder.zkpMaterialToWitness material) (Holder.zkpMaterialToPublicInput material) Holder.zkpRelation) material

theorem Holder.universalZKPOracle_isValid (material : ZKPMaterial) (relation : Relation) : (universalZKPOracle material).isValid relation

定理: オラクルが返すZKPは常に有効である

証明の構造:

1. universalZKPOracleはamtZKP.proverを使ってProofを生成
2. amtZKP.completenessにより、Proofは検証に成功する
3. proofToZKPはProofをvalid ZKPとして構築
4. ZeroKnowledgeProof.valid_zkp_passesにより、valid ZKPは検証に成功

暗号学的仮定への依存:

• amtZKPの性質（completeness）から導出される定理
• SecurityAssumptions.amtZKP_soundness_quantum_secureに依存
• SecurityAssumptions.amtZKP_zeroKnowledge_quantum_secureに依存

noncomputable def Holder.combinePrecomputedProofWithCredential (precomputedProofs : List PrecomputedZKP) (credential : UnknownVC) (statement : PublicInput) (secretKey : SecretKey) : UnknownZKP

ナンスと事前計算されたProofを結合する関数（辞書からの取り出し）

辞書からのルックアップ操作として定義。 これにより、形式的な意味が明確になる。

Equations

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

noncomputable def Holder.presentCredentialAsZKP (wallet : Wallet) (vc : UnknownVC) (holderIdentity : Identity) (statement : PublicInput) (_h_has_identity : holderIdentity ∈ wallet.identities) : UnknownZKP

WalletのIdentityを使ってZKPを生成

Walletは複数のIdentityを持つことができるため、 どのIdentityを使ってZKPを生成するかを明示的に指定します。

Equations

• Holder.presentCredentialAsZKP wallet vc holderIdentity statement _h_has_identity = Holder.combinePrecomputedProofWithCredential wallet.precomputedProofs vc statement holderIdentity.secretKey

def w3cStandardVCContext : W3C.Context

VCのコンテキストを生成（W3C標準）

Equations

• w3cStandardVCContext = { value := "https://www.w3.org/2018/credentials/v1" }

def amtStandardVCType : W3C.CredentialType

VCのタイプを生成（AMTの標準的なVC）

Equations

• amtStandardVCType = { value := "AMTStandardCredential" }

noncomputable def issueCredential (issuerDID : ValidDID) (issuerSecretKey : SecretKey) (subjectDID : ValidDID) (claims : Claims) : UnknownVC

VCを発行する関数

AMATELUSの設計:

• IssuerはDIDComm（またはZKP）で接続確立済み
• IssuerはHolderのValidDIDを既に取得・検証済み
• IssuerとSubjectのDIDは両方ともValidDIDである必要がある

DIDCommフロー:

1. HolderがDIDDocumentを提示
2. Issuerがチャレンジ・レスポンスで秘密鍵所有権を検証
3. 検証成功 → Issuerは ValidDID を取得

実装:

1. Claimsに署名を生成（amtSignature.sign）
2. ValidVCとして構築
3. UnknownVC.validとして返す

W3C VC仕様との関係:

• 「権限」や「認可」のチェックは一切なし
• Verifierが信頼ポリシーに基づいて受け入れ判断を行う

Equations

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

theorem issued_credential_is_cryptographically_valid (issuerDID subjectDID : ValidDID) (issuerSecretKey : SecretKey) (claims : Claims) : let vc := issueCredential issuerDID issuerSecretKey subjectDID claims; vc.isValid

定理: ValidDIDで発行されたVCは暗号学的に有効である

証明の構造:

1. issueCredentialはValidDIDを受け取る
2. amtSignature.signを使って署名を生成
3. amtSignature.completenessにより、署名は検証に成功
4. ValidVCとして構築されるため、UnknownVC.isValidが成立

AMATELUSの設計:

• IssuerはDIDComm（またはZKP）でValidDIDを取得済み
• 発行されるVCは常に暗号学的に有効

重要な注意:

• この定理は「暗号学的に有効」であることのみを保証します
• 「信頼できる」かどうかはVerifierの信頼ポリシーによって決まります

def Verifier.findTrustAnchorForTrustee (dict : TrustAnchorDict) (trusteeDID : UnknownDID) : Option ValidDID

TrustAnchorDictからDIDを受託者として持つ信頼対象DIDを探す

戻り値:

• Option ValidDID: 信頼対象DIDは型レベルで検証済みのValidDIDとして管理されるため、 ValidDIDを直接返すことで型安全性が向上する

Equations

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

def Verifier.checkTrustChainRecursive (dict : TrustAnchorDict) (trustedRoots : List UnknownDID) (issuerDID : UnknownDID) (depth : ℕ) : Prop

信頼チェーンを再帰的に検証する関数（定理化）

この関数は、TrustAnchorDictを使って信頼チェーンを辿ります。

検証ロジック：

1. 検証したいDIDが信頼対象リストに含まれていれば、信頼できる
2. 深さが0になったら、信頼できない（チェーンが長すぎる）
3. そうでなければ、TrustAnchorDictから、このDIDを受託者として持つ信頼対象DIDを探す
4. その信頼対象DIDが信頼できるか再帰的にチェック（深さを1減らす）

Equations

• One or more equations did not get rendered due to their size.
• Verifier.checkTrustChainRecursive dict trustedRoots issuerDID 0 = (issuerDID ∈ trustedRoots)

def Verifier.verifyTrustChain (dict : TrustAnchorDict) (vc : UnknownVC) : Prop

信頼チェーンの検証

設計思想:

• AMATELUSはN階層委任をサポート
• maxChainDepthはInitialMaxDepthを初期値として使用
• 実際の制限は各delegationのmaxDepthで決まる
• 信頼対象DIDのリストはWallet.trustedAnchorsから取得

Equations

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

def Verifier.verifyCredential (verifier : Verifier) (vc : UnknownVC) : Prop

VerifierがVCを検証

Equations

• verifier.verifyCredential vc = (vc.isValid ∧ ∃ (wallet : Wallet), wallet ∈ verifier.wallets ∧ Verifier.verifyTrustChain wallet.trustedAnchors vc)

theorem wallet_store_preserves_validity (wallet : Wallet) (vc : ValidVC) (holderDID : ValidDID) (h_subject : vc.subjectDID = holderDID) (h_has_did : wallet.hasDID holderDID) : wallet.isValid → let wallet' := Holder.storeCredential wallet vc holderDID h_subject h_has_did; wallet'.isValid

Wallet操作: VC保存後の一貫性

証明の構造:

1. storeCredentialはcredentialsリストのみを変更
2. identitiesは変更されない
3. したがって、Wallet.isValidは自明に保持される（定義から）

重要な設計原則 - AMATELUSの責任範囲: この定理は「Wallet操作が型の不変条件を保つ」という純粋に数学的な主張です。

自己責任の範囲:

• Wallet実装にバグがあれば影響を受ける（自己責任）
• しかし、それは「このWalletを選んだ利用者の責任」

他者からの独立性（AMATELUSが保証）:

• 他人のWalletバグが自分に影響しない（暗号学的健全性）
• Verifierは暗号的検証のみに依存
• Basic.lean:1457 verifier_cryptographic_soundnessで形式化済み

theorem verifier_accepts_valid_credential (verifier : Verifier) (vc : UnknownVC) : vc.isValid → (∃ (wallet : Wallet), wallet ∈ verifier.wallets ∧ Verifier.verifyTrustChain wallet.trustedAnchors vc) → verifier.verifyCredential vc

Verifier操作: 有効なVCかつ信頼できるissuerの検証は成功する

証明の構造:

1. UnknownVC.isValid vc が成立（暗号学的に有効）
2. いずれかのWalletでverifyTrustChainが成立する（Verifierが信頼）
3. verifyCredentialが成立する

注: この定理は自明に成立する（verifyCredentialの定義そのもの）