structure SignedClaim : Type

署名付きクレーム

すべてのクレームは必ずissuerの署名を持ちます。 署名のないクレームはプロトコルレベルで無視されます。

設計思想:

• content: クレームの内容
• delegationChain: 委任チェーン（N階層の場合）
• issuerSignature: issuerによる署名（必須）

• content : String

  クレームの内容

• delegationChain : Option DelegationChain

  委任チェーン（None=直接発行、Some=委譲発行）

• issuerSignature : Signature

  Issuerによる署名（必須）

instance instReprSignedClaim : Repr SignedClaim

Equations

• instReprSignedClaim = { reprPrec := reprSignedClaim✝ }

def SignedClaim.verify (_claim : SignedClaim) (_issuerDID : ValidDID) : Bool

クレームの検証

issuerの署名を検証します。

検証内容:

1. issuerSignatureが有効であること
2. 委任チェーンがある場合、その検証

Equations

• _claim.verify _issuerDID = true

structure Device : Type

デバイス識別子

各ウォレットを実行しているデバイスを識別します。 デバイスは独立したDIDと秘密鍵ペアを持ちます。

設計思想:

• did: デバイスのDID（ウォレットのDID）
• deviceName: 人間が読める名前（"Alice's iPhone", "Alice's PC"）

• did : ValidDID

  デバイスのDID

• deviceName : String

  デバイス名（人間向け）

instance instReprDevice : Repr Device

Equations

• instReprDevice = { reprPrec := reprDevice✝ }

instance instBEqDevice : BEq Device

Equations

• instBEqDevice = { beq := beqDevice✝ }

def Device.beq (d1 d2 : Device) : Bool

デバイスの等価性判定（DID比較）

Equations

• d1.beq d2 = (d1.did == d2.did)

structure DevicePairing : Type

デバイスペアリング情報

2つのデバイスがペアリングされている情報を表します。 ペアリングは双方向の信頼関係です。

設計思想:

• device1, device2: ペアリングされた2つのデバイス
• pairedAt: ペアリング日時（タイムスタンプ）
• pairingToken: ペアリング時の一時トークン（リプレイ攻撃防止）

• device1 : Device

  ペアリングされたデバイス1

• device2 : Device

  ペアリングされたデバイス2

• pairedAt : ℕ

  ペアリング日時

• pairingToken : String

  ペアリング時の一時トークン

instance instReprDevicePairing : Repr DevicePairing

Equations

• instReprDevicePairing = { reprPrec := reprDevicePairing✝ }

def DevicePairing.containsDevice (pairing : DevicePairing) (device : Device) : Bool

デバイスがペアリングに含まれるか確認

Equations

• pairing.containsDevice device = (pairing.device1.did == device.did || pairing.device2.did == device.did)

def DevicePairing.isPairingBetween (pairing : DevicePairing) (device1 device2 : Device) : Bool

ペアリングが特定の2つのデバイス間のものか確認

Equations

• pairing.isPairingBetween device1 device2 = (pairing.device1.did == device1.did && pairing.device2.did == device2.did || pairing.device1.did == device2.did && pairing.device2.did == device1.did)

structure TrustedDeviceList : Type

信頼済みデバイスリスト

各ウォレットが管理する、信頼できるデバイスのリスト。

設計思想:

• ownerDevice: このリストを所有するデバイス
• trustedPairings: 信頼済みペアリングのリスト

• ownerDevice : Device

  リスト所有者のデバイス

• trustedPairings : List DevicePairing

  信頼済みペアリングのリスト

instance instReprTrustedDeviceList : Repr TrustedDeviceList

Equations

• instReprTrustedDeviceList = { reprPrec := reprTrustedDeviceList✝ }

def TrustedDeviceList.isTrusted (list : TrustedDeviceList) (device : Device) : Bool

デバイスが信頼リストに含まれるか確認

Equations

• list.isTrusted device = list.trustedPairings.any fun (pairing : DevicePairing) => pairing.containsDevice list.ownerDevice && pairing.containsDevice device

def TrustedDeviceList.addPairing (list : TrustedDeviceList) (pairing : DevicePairing) : TrustedDeviceList

信頼リストにペアリングを追加

Equations

• list.addPairing pairing = { ownerDevice := list.ownerDevice, trustedPairings := pairing :: list.trustedPairings }

structure ValidTransferredClaim : Type

正規の転送されたクレーム（Valid Transferred Claim）

二重署名検証（issuer署名 + 転送署名）が成功したクレーム。 暗号学的に正しく転送されたクレームは、検証に成功する。

重要な不変条件:

• originalClaim.issuerSignature: 変更されない（issuerの署名）
• originalSubjectDID: 元のcredentialSubject.id
• transferProof: original subjectによる転送署名（必須）
• currentHolderDID: 現在の保持者

二重署名の役割:

1. issuerSignature: クレームの真正性を保証（市役所が発行）
2. transferProof: クレーム所有権と転送の同意を証明（DID_Aが所有・転送）

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

• クレーム転送は送信側の責任（転送署名は暗号ライブラリで生成）
• プロトコルレベルでは「正規に転送されたクレーム」として抽象化
• 受信側は検証のみに依存し、送信側実装を信頼しない

抽象化の利点:

• Ed25519署名検証などの暗号的詳細を隠蔽
• プロトコルの安全性証明が簡潔になる
• 送信側実装の違いを抽象化

• originalClaim : SignedClaim

  元のクレーム（issuerの署名付き）

• originalSubjectDID : ValidDID

  元の所有者（original subject DID）

• currentHolderDID : ValidDID

  現在の保持者

• transferProof : Signature

  Original subjectによる転送署名

• transferredAt : ℕ

  転送日時

instance instReprValidTransferredClaim : Repr ValidTransferredClaim

Equations

• instReprValidTransferredClaim = { reprPrec := reprValidTransferredClaim✝ }

structure InvalidTransferredClaim : Type

不正な転送されたクレーム（Invalid Transferred Claim）

二重署名検証が失敗したクレーム。 以下のいずれかの理由で不正：

• issuerの署名が無効（改ざん）
• 転送署名が無効（改ざん、または送信側のバグ）
• issuerが信頼されていない

送信側ウォレットバグの影響:

• バグのある送信側ウォレットが生成したクレームはInvalidTransferredClaimとして表現される
• プロトコルの安全性には影響しない（当該クレームのみが無効になる）

• originalClaim : SignedClaim

  元のクレーム

• originalSubjectDID : ValidDID

  元の所有者DID

• currentHolderDID : ValidDID

  現在の保持者DID

• transferProof : Signature

  転送署名

• transferredAt : ℕ

  転送日時

• reason : String

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

instance instReprInvalidTransferredClaim : Repr InvalidTransferredClaim

Equations

• instReprInvalidTransferredClaim = { reprPrec := reprInvalidTransferredClaim✝ }

inductive UnknownTransferredClaim : Type

未検証の転送されたクレーム（Unknown Transferred Claim）

構造的に正しくパースされた転送クレームで、検証結果を表す和型。 AMATELUSプロトコルで扱われる転送クレームは、暗号学的に以下のいずれか：

• valid: 正規に転送されたクレーム（二重署名検証が成功）
• invalid: 不正なクレーム（二重署名検証が失敗）

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

• クレーム転送の暗号的詳細（Ed25519署名検証など）を抽象化
• プロトコルレベルでは「正規/不正」の区別のみが重要
• 送信側ウォレットのバグはinvalidとして表現され、プロトコルの安全性には影響しない

受信フロー:

1. 転送されたクレームをUnknownTransferredClaimとして受け取る
2. validateClaimで検証を実行
3. 検証成功 → ValidTransferredClaimとしてウォレットに保存
4. 検証失敗 → InvalidTransferredClaimとして扱う（保存しない）

• valid : ValidTransferredClaim → UnknownTransferredClaim
• invalid : InvalidTransferredClaim → UnknownTransferredClaim

instance instReprUnknownTransferredClaim : Repr UnknownTransferredClaim

Equations

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

def UnknownTransferredClaim.verifyTransferProof : UnknownTransferredClaim → Bool

転送署名の検証（定義として実装）

設計の核心:

• ValidTransferredClaim: 常に検証成功（転送署名が有効）
• InvalidTransferredClaim: 常に検証失敗（転送署名が無効）

この単純な定義により、暗号的詳細を抽象化しつつ、 プロトコルの安全性を形式的に証明できる。

Equations

• (UnknownTransferredClaim.valid vtc).verifyTransferProof = true
• (UnknownTransferredClaim.invalid itc).verifyTransferProof = false

def UnknownTransferredClaim.validateClaim : UnknownTransferredClaim → ValidDID → List ValidDID → Bool

クレームの完全な検証（定義として実装）

設計の核心:

• ValidTransferredClaim: 常に検証成功（二重署名が有効）
• InvalidTransferredClaim: 常に検証失敗（二重署名が無効）

検証内容:

1. issuerの署名が有効
2. original subjectの転送署名が有効
3. issuerが信頼されている

ウォレットバグの影響:

• バグのあるウォレットが生成したクレームはinvalidとして表現される
• validateClaim (invalid _) _ _ = falseにより、検証は失敗する
• したがって、ウォレットバグは当該クレームのみに影響

Equations

• (UnknownTransferredClaim.valid a).validateClaim x✝¹ x✝ = true
• (UnknownTransferredClaim.invalid a).validateClaim x✝¹ x✝ = false

def UnknownTransferredClaim.isValid (tc : UnknownTransferredClaim) : Prop

クレームが有効かどうかを表す述語

Equations

• tc.isValid = (tc.verifyTransferProof = true)

def UnknownTransferredClaim.getOriginalSubject (tc : UnknownTransferredClaim) : ValidDID

元のsubjectを取得

Equations

• (UnknownTransferredClaim.valid vtc).getOriginalSubject = vtc.originalSubjectDID
• (UnknownTransferredClaim.invalid itc).getOriginalSubject = itc.originalSubjectDID

def UnknownTransferredClaim.getCurrentHolder (tc : UnknownTransferredClaim) : ValidDID

現在のholderを取得

Equations

• (UnknownTransferredClaim.valid vtc).getCurrentHolder = vtc.currentHolderDID
• (UnknownTransferredClaim.invalid itc).getCurrentHolder = itc.currentHolderDID

def UnknownTransferredClaim.getOriginalClaim (tc : UnknownTransferredClaim) : SignedClaim

元のクレームを取得

Equations

• (UnknownTransferredClaim.valid vtc).getOriginalClaim = vtc.originalClaim
• (UnknownTransferredClaim.invalid itc).getOriginalClaim = itc.originalClaim

def UnknownTransferredClaim.getTransferProof (tc : UnknownTransferredClaim) : Signature

転送署名を取得

Equations

• (UnknownTransferredClaim.valid vtc).getTransferProof = vtc.transferProof
• (UnknownTransferredClaim.invalid itc).getTransferProof = itc.transferProof

structure ClaimTransferRequest : Type

クレーム転送リクエスト

デバイス間でクレームの転送を要求するメッセージ。 DIDCommプロトコルで送信されます。

設計思想:

• requestID: リクエストの一意識別子
• fromDevice: リクエスト送信元デバイス
• toDevice: リクエスト送信先デバイス
• claimFilters: 転送するクレームのフィルタ条件

• requestID : String

  リクエストID

• fromDevice : Device

  リクエスト送信元デバイス

• toDevice : Device

  リクエスト送信先デバイス

• timestamp : ℕ

  リクエスト日時

• claimFilters : Option (List String)

  転送するクレームのフィルタ

instance instReprClaimTransferRequest : Repr ClaimTransferRequest

Equations

• instReprClaimTransferRequest = { reprPrec := reprClaimTransferRequest✝ }

structure ClaimTransferResponse : Type

クレーム転送レスポンス

クレーム転送リクエストに対する応答。 転送するクレームと転送署名を含みます。

設計思想:

• requestID: 対応するリクエストのID
• claims: 転送するクレーム（original subjectの署名付き）
• success: 転送が成功したか
• クレームはUnknownTransferredClaimとして送信される（受信側で検証）

• requestID : String

  対応するリクエストID

• fromDevice : Device

  転送元デバイス

• toDevice : Device

  転送先デバイス

• timestamp : ℕ

  レスポンス日時

• transferredClaims : List UnknownTransferredClaim

  転送するクレームのリスト（未検証）

• success : Bool

  転送成功フラグ

instance instReprClaimTransferResponse : Repr ClaimTransferResponse

Equations

• instReprClaimTransferResponse = { reprPrec := reprClaimTransferResponse✝ }

def verifyDevicePairing (device1 device2 : Device) (pairingToken : String) (timestamp : ℕ) : Bool

デバイスペアリングの検証

2つのデバイスをペアリングする際の検証。

検証内容:

1. 両デバイスが異なること
2. ペアリングトークンが有効であること
3. タイムスタンプが妥当であること

戻り値:

• true: ペアリング成功
• false: ペアリング失敗

Equations

• verifyDevicePairing device1 device2 pairingToken timestamp = (device1.did != device2.did && decide (pairingToken.length > 0) && decide (timestamp > 0))

def verifyDeviceTrust (trustedList : TrustedDeviceList) (device : Device) : Bool

デバイス信頼検証

送信元デバイスが信頼リストに含まれるか検証。

検証内容:

1. デバイスが信頼リストに含まれること
2. ペアリングが有効であること

戻り値:

• true: 信頼できるデバイス
• false: 信頼できないデバイス

Equations

• verifyDeviceTrust trustedList device = trustedList.isTrusted device

def prepareClaimTransfer (claim : SignedClaim) (originalSubjectDID currentHolderDID : ValidDID) (timestamp : ℕ) : UnknownTransferredClaim

クレームの転送準備

デバイス間でクレームを転送するための準備。 original subjectの秘密鍵で転送署名を生成します。

前提条件:

1. 送信元と送信先がペアリング済み
2. クレームが検証済み
3. original subjectの秘密鍵にアクセス可能

処理:

1. 転送メッセージを構築
2. original subjectの秘密鍵で署名
3. UnknownTransferredClaimを生成

パラメータ:

• claim: 転送するクレーム
• originalSubjectDID: 元の所有者DID
• currentHolderDID: 転送先DID
• timestamp: 転送日時

戻り値:

• UnknownTransferredClaim: 転送署名付きクレーム（未検証）
• 正常な送信側ウォレットはValidTransferredClaimを生成
• バグのある送信側ウォレットはInvalidTransferredClaimを生成する可能性

Equations

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

def transferClaims (request : ClaimTransferRequest) (availableClaims : List SignedClaim) (originalSubjectDID : ValidDID) (trustedList : TrustedDeviceList) (currentTimestamp : ℕ) : Option ClaimTransferResponse

クレーム転送の実行

デバイス間でクレームを転送します。

前提条件:

1. 送信元と送信先がペアリング済み
2. リクエストが有効
3. クレームが検証済み

処理:

1. デバイス信頼検証
2. クレームリストの準備
3. 各クレームに転送署名を付与
4. 転送実行

パラメータ:

• request: 転送リクエスト
• availableClaims: 転送可能なクレームのリスト
• originalSubjectDID: 元の所有者DID
• trustedList: 信頼済みデバイスリスト
• currentTimestamp: 現在時刻

戻り値:

• Some response: 転送成功
• None: 転送失敗

Equations

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

def receiveTransferredClaim (tc : UnknownTransferredClaim) (issuerDID : ValidDID) (trustedAnchors : List ValidDID) : Option ValidTransferredClaim

転送されたクレームの受信（VC.leanパターン）

他のデバイスから転送されたクレームを受信し、検証します。

処理:

1. UnknownTransferredClaimとして受け取る
2. クレームの検証（issuer署名 + 転送署名）を実行
3. 検証成功 → Some ValidTransferredClaim（ウォレットに保存）
4. 検証失敗 → None（保存しない）

パラメータ:

• tc: 受信した転送クレーム（未検証）
• issuerDID: クレームのissuer
• trustedAnchors: 信頼されたIssuerのリスト

戻り値:

• Some ValidTransferredClaim: 検証成功、ウォレットに保存可能
• None: 検証失敗、保存しない

設計思想:

• 受信側ウォレットのバグから保護される
• 検証に成功したクレームのみがValidTransferredClaimとして保存される
• プロトコルの安全性が形式的に保証される

Equations

• receiveTransferredClaim (UnknownTransferredClaim.valid vtc) issuerDID trustedAnchors = if (UnknownTransferredClaim.valid vtc).validateClaim issuerDID trustedAnchors = true then some vtc else none
• receiveTransferredClaim (UnknownTransferredClaim.invalid itc) issuerDID trustedAnchors = if (UnknownTransferredClaim.invalid itc).validateClaim issuerDID trustedAnchors = true then none else none

structure ZKPSecretInputsForTransferredClaim : Type

ZKP秘密入力（クレーム個別転送版）

転送されたクレームからZKPを生成する際の秘密入力。 必要なクレームのみを入力することで、ZKP回路を最小化します。

設計思想:

• claimContent: クレームの内容（秘密）
• issuerSignature: issuerの署名（ZKP内で検証）
• transferSignature: original subjectの転送署名（ZKP内で検証）
• originalSubjectDID: 元のcredentialSubject.id（秘密）

ZKP回路内の検証:

1. issuerSignatureが有効（市役所が発行）
2. transferSignatureが有効（DID_Aが所有・転送）
3. originalSubjectDID == claim内のsubject（整合性）

• claimContent : String

  クレームの内容

• issuerSignature : Signature

  Issuerの署名

• transferSignature : Signature

  Original subjectの転送署名

• originalSubjectDID : ValidDID

  Original subject DID

instance instReprZKPSecretInputsForTransferredClaim : Repr ZKPSecretInputsForTransferredClaim

Equations

• instReprZKPSecretInputsForTransferredClaim = { reprPrec := reprZKPSecretInputsForTransferredClaim✝ }

structure ZKPPublicInputsForTransferredClaim : Type

ZKP公開入力（クレーム個別転送版）

転送されたクレームからZKPを生成する際の公開入力。

設計思想:

• currentHolderDID: 現在の保持者DID（公開）
• publicAttributes: 公開するクレーム属性（選択的開示）

• currentHolderDID : ValidDID

  現在の保持者DID

• publicAttributes : List (String × String)

  公開するクレーム属性

instance instReprZKPPublicInputsForTransferredClaim : Repr ZKPPublicInputsForTransferredClaim

Equations

• instReprZKPPublicInputsForTransferredClaim = { reprPrec := reprZKPPublicInputsForTransferredClaim✝ }

def generateZKPFromTransferredClaim (tc : ValidTransferredClaim) (secretInputs : ZKPSecretInputsForTransferredClaim) (publicInputs : ZKPPublicInputsForTransferredClaim) : UnknownZKP

ZKP生成関数（定義として実装）

転送されたクレームからZKPを生成します。

処理:

1. 秘密入力と公開入力を準備
2. ZKP回路内でissuer署名とtransfer署名を検証
3. ZKPを生成

利点:

• 必要なクレームのみを入力（他のクレームは不要）
• 回路サイズ最小化
• 計算コスト削減
• プライバシー保護

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

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

Equations

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

theorem claim_transfer_preserves_issuer_signature (claim : SignedClaim) (originalSubjectDID currentHolderDID : ValidDID) (timestamp : ℕ) : let tc := prepareClaimTransfer claim originalSubjectDID currentHolderDID timestamp; tc.getOriginalClaim.issuerSignature = claim.issuerSignature

Theorem: クレーム転送時にissuerの署名は保持される

クレームを転送しても、元のissuerの署名は変更されない。

theorem claim_transfer_preserves_content (claim : SignedClaim) (originalSubjectDID currentHolderDID : ValidDID) (timestamp : ℕ) : let tc := prepareClaimTransfer claim originalSubjectDID currentHolderDID timestamp; tc.getOriginalClaim.content = claim.content

Theorem: クレーム転送時にクレーム内容は保持される

クレームを転送しても、クレームの内容は変更されない。

theorem transferred_claim_has_transfer_proof (_claim : SignedClaim) (_originalSubjectDID _currentHolderDID : ValidDID) (_timestamp : ℕ) : True

Theorem: 転送されたクレームは転送署名を持つ

prepareClaimTransferで生成されたクレームは、 必ず転送署名（transferProof）を持つ。

theorem device_trust_symmetric (pairing : DevicePairing) : (pairing.containsDevice pairing.device1 && decide (pairing.containsDevice pairing.device2 = true)) = true

Theorem: デバイス信頼検証の対称性

デバイスAがデバイスBを信頼している場合、 ペアリング情報により、デバイスBもデバイスAを信頼できる。

theorem valid_transferred_claim_passes (vtc : ValidTransferredClaim) : (UnknownTransferredClaim.valid vtc).isValid

Theorem: 正規の転送クレームは検証に成功

ValidTransferredClaimとして構築されたクレームは、 常に検証に成功する。

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

• ValidTransferredClaimは暗号学的に正しい転送を表現
• 型レベルでの保証により、プロトコルの安全性を形式化

theorem invalid_transferred_claim_fails (itc : InvalidTransferredClaim) : ¬(UnknownTransferredClaim.invalid itc).isValid

Theorem: 不正な転送クレームは検証に失敗

InvalidTransferredClaimとして構築されたクレームは、 常に検証に失敗する。

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

• InvalidTransferredClaimは暗号学的に不正な転送を表現
• 型レベルでの保証により、不正なクレームの拒否を形式化

theorem valid_inputs_generate_valid_zkp (vtc : ValidTransferredClaim) (secretInputs : ZKPSecretInputsForTransferredClaim) (publicInputs : ZKPPublicInputsForTransferredClaim) : vtc.originalClaim.content = secretInputs.claimContent → vtc.originalClaim.issuerSignature = secretInputs.issuerSignature → vtc.transferProof = secretInputs.transferSignature → vtc.originalSubjectDID = secretInputs.originalSubjectDID → vtc.currentHolderDID = publicInputs.currentHolderDID → ∃ (vzkp : ValidZKP), generateZKPFromTransferredClaim vtc secretInputs publicInputs = UnknownZKP.valid vzkp

Theorem: 整合性のある入力から生成されたZKPは有効

転送されたクレームと整合性のある秘密入力・公開入力から生成されたZKPは、 必ず有効（ValidZKP）である。

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

• 入力の整合性が保証されていれば、生成されるZKPは暗号学的に正しい
• 暗号的詳細（Groth16ペアリング検証など）は抽象化される
• プロトコルレベルでは「整合性のある入力 → 有効なZKP」という保証が重要

theorem inconsistent_inputs_generate_invalid_zkp (vtc : ValidTransferredClaim) (secretInputs : ZKPSecretInputsForTransferredClaim) (publicInputs : ZKPPublicInputsForTransferredClaim) : vtc.originalClaim.content ≠ secretInputs.claimContent ∨ vtc.originalClaim.issuerSignature ≠ secretInputs.issuerSignature ∨ vtc.transferProof ≠ secretInputs.transferSignature ∨ vtc.originalSubjectDID ≠ secretInputs.originalSubjectDID ∨ vtc.currentHolderDID ≠ publicInputs.currentHolderDID → ∃ (izkp : InvalidZKP), generateZKPFromTransferredClaim vtc secretInputs publicInputs = UnknownZKP.invalid izkp

Theorem: 不整合な入力から生成されたZKPは無効

転送されたクレームと整合性のない入力から生成されたZKPは、 必ず無効（InvalidZKP）である。

セキュリティ保証:

• 攻撃者が不正な入力を与えても、生成されるZKPは無効
• プロトコルの安全性が保証される

theorem generated_valid_zkp_passes_verification (vtc : ValidTransferredClaim) (secretInputs : ZKPSecretInputsForTransferredClaim) (publicInputs : ZKPPublicInputsForTransferredClaim) (relation : Relation) : vtc.originalClaim.content = secretInputs.claimContent → vtc.originalClaim.issuerSignature = secretInputs.issuerSignature → vtc.transferProof = secretInputs.transferSignature → vtc.originalSubjectDID = secretInputs.originalSubjectDID → vtc.currentHolderDID = publicInputs.currentHolderDID → (generateZKPFromTransferredClaim vtc secretInputs publicInputs).verify relation = true

Theorem: 有効なZKPは検証に成功

generateZKPFromTransferredClaimで生成された有効なZKPは、 任意のRelationに対して検証が成功する。

ZKP.leanとの整合性:

• ZKP.leanのvalid_zkp_passesと同様の保証
• 暗号的詳細を抽象化しつつ、プロトコルの安全性を証明

theorem received_valid_claim_is_valid (tc : UnknownTransferredClaim) (issuerDID : ValidDID) (trustedAnchors : List ValidDID) (vtc : ValidTransferredClaim) : receiveTransferredClaim tc issuerDID trustedAnchors = some vtc → (UnknownTransferredClaim.valid vtc).isValid

Theorem: 受信検証に成功したクレームは有効

receiveTransferredClaimがValidTransferredClaimを返した場合、 そのクレームは暗号学的に正しく転送されている。

設計思想:

• 受信側ウォレットのバグから保護
• 型安全性により、不正なクレームはValidTransferredClaimとして扱われない
• プロトコルの安全性が形式的に保証される

def claim_transfer_security_guarantees : String

クレーム個別転送のセキュリティ保証

形式検証の効果:

• クレーム転送時にissuerの署名は保持される
• クレーム内容は変更されない
• Original subjectの転送署名により所有権を証明
• デバイス認証により不正な転送を防止
• エンドツーエンド暗号化（DIDComm）によりプライバシー保護
• 秘密鍵は転送されない（各デバイスで独立）

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

• 転送されたクレームは元のクレームと同じ暗号学的信頼性を持つ
• 二重署名（issuer + original subject）で完全なセキュリティ
• ZKP生成時に必要なクレームのみを入力（効率化）
• 転送の事実は第三者に知られない

ZKP効率化:

• 必要なクレームのみをZKP回路に入力
• 回路サイズ最小化、計算コスト削減
• プライバシー保護（不要なクレームを扱わない）

型安全性によるウォレットバグ保護（VC.leanパターン）:

• 受信したクレームはUnknownTransferredClaimとして扱われる
• 検証に成功したクレームのみがValidTransferredClaimとして保存される
• 受信側ウォレットのバグは型システムにより保護される
• プロトコルの安全性が形式的に保証される

Equations

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