structure Identity : Type

1つのDIDアイデンティティを表す構造体

Walletは複数のアイデンティティを保持でき、ユーザーは任意にいくつでもDIDを発行できる。 各アイデンティティは、DID、DIDドキュメント、秘密鍵の組として表現される。

設計思想:

• Walletは「自分が所有・管理する検証済みデータ」を格納する
• したがって、IdentityはValidDIDとValidDIDDocumentを使用する
• 外部から受け取ったDIDはUnknownDIDとして受け取り、検証後にValidDIDに変換してからWalletに保存する

• did : ValidDID
• didDocument : ValidDIDDocument
• secretKey : SecretKey

instance instReprIdentity : Repr Identity

Equations

• instReprIdentity = { reprPrec := reprIdentity✝ }

structure PrecomputedZKP : Type

事前計算されたZKP

• partialProof : Proof
• publicStatement : PublicInput

structure TrustAnchorInfo : Type

信頼対象DID情報

このWalletが信頼するDIDに関連する情報を保持する。

• didDocument: 信頼対象のValidDIDDocument
• trustees: このDIDから権限を委譲された受託者のDIDリスト

重要な設計思想: 「トラストアンカー」は固定的な役割ではなく、各Walletの所有者が自由に選択する 信頼対象のDID。家族、友人、職場の同僚、地域コミュニティ、企業、政府など、 誰でも他人から信頼対象として選ばれる可能性がある。

• didDocument : ValidDIDDocument
• trustees : List UnknownDID

def TrustAnchorInfo.isValid (anchorDID : ValidDID) (info : TrustAnchorInfo) : Prop

信頼対象DID情報が正規かどうかを検証

信頼対象のValidDIDとValidDIDDocumentが一致することを確認する。

設計思想:

• TrustAnchorDictがValidDIDをキーとして使用するため、型レベルでDIDの正規性が保証される
• この関数は、ValidDIDがinfo.didDocumentから正しく生成されたかを検証する

Equations

• TrustAnchorInfo.isValid anchorDID info = (anchorDID = UnknownDID.fromValidDocument info.didDocument)

theorem TrustAnchorInfo.valid_info_passes_did_verification (anchorDID : ValidDID) (info : TrustAnchorInfo) : isValid anchorDID info → (UnknownDID.valid anchorDID).isValid info.didDocument

Theorem: 正規の信頼対象DID情報はDID検証に成功する

@[reducible, inline]

abbrev TrustAnchorDict : Type

信頼対象DID辞書の型

辞書: { 信頼対象のValidDID ↦ TrustAnchorInfo }

連想リストとして実装され、ValidDIDをキーとしてTrustAnchorInfoを取得できる。

重要な設計思想:

• 各個人が自分のWalletで、誰を信頼するか（trustedAnchorsに登録するか）を自由に決定
• 「トラストアンカー」は絶対的な役割ではなく、このWalletにとって信頼されているDIDという相対的な関係
• 家族、友人、職場の同僚、地域コミュニティ、企業、政府など、誰でも信頼対象として選ばれうる
• ValidDIDを使用することで、型レベルで検証済みであることを保証
• TrustAnchorInfoにValidDIDDocumentが含まれるため、整合性が保証される

Equations

• TrustAnchorDict = List (ValidDID × TrustAnchorInfo)

def TrustAnchorDict.lookup (dict : TrustAnchorDict) (anchorDID : ValidDID) : Option TrustAnchorInfo

辞書からトラストアンカー情報を検索

Equations

• dict.lookup anchorDID = List.lookup anchorDID dict

def TrustAnchorDict.insert (dict : TrustAnchorDict) (anchorDID : ValidDID) (info : TrustAnchorInfo) : TrustAnchorDict

辞書にトラストアンカー情報を追加

Equations

• dict.insert anchorDID info = (anchorDID, info) :: List.filter (fun (x : ValidDID × TrustAnchorInfo) => match x with | (did, snd) => decide (did ≠ anchorDID)) dict

def TrustAnchorDict.addTrustee (dict : TrustAnchorDict) (anchorDID : ValidDID) (trusteeDID : UnknownDID) : TrustAnchorDict

辞書から受託者を追加

指定されたトラストアンカーの受託者リストに新しい受託者を追加する。

Equations

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

def TrustAnchorDict.allValid (dict : TrustAnchorDict) : Prop

辞書内のすべてのエントリーが正規かどうかを検証

Equations

• dict.allValid = ∀ (anchorDID : ValidDID) (info : TrustAnchorInfo), (anchorDID, info) ∈ dict → TrustAnchorInfo.isValid anchorDID info

structure Wallet : Type

Walletはユーザーの秘密情報を安全に保管する

ユーザーは任意にいくつでもDIDを発行でき、Walletは複数のアイデンティティを保持する。 各アイデンティティは独立したDID、DIDドキュメント、秘密鍵の組として管理される。

設計思想:

• Walletは「自分が所有・管理する検証済みデータ」を格納する
• したがって、credentialsはValidVCのみを格納する
• 外部から受け取ったVCはUnknownVCとして受け取り、検証後にValidVCに変換してからWalletに保存する

• identities : List Identity
• credentials : List ValidVC
• precomputedProofs : List PrecomputedZKP
• trustedAnchors : TrustAnchorDict
• localTime : Timestamp

def Wallet.containsDID (wallet : Wallet) (did : ValidDID) : Bool

WalletにDIDが含まれているかを確認する

Equations

• wallet.containsDID did = wallet.identities.any fun (identity : Identity) => identity.did == did

def Wallet.getIdentity (wallet : Wallet) (did : ValidDID) : Option Identity

WalletからDIDに対応するIdentityを取得する

Equations

• wallet.getIdentity did = List.find? (fun (identity : Identity) => identity.did == did) wallet.identities

def Wallet.hasDID (wallet : Wallet) (did : ValidDID) : Prop

WalletにDIDが含まれていることを表す命題

Equations

• wallet.hasDID did = ∃ (identity : Identity), identity ∈ wallet.identities ∧ identity.did = did

def Wallet.isValidIdentity (identity : Identity) : Prop

Identityが正規かどうかを検証する述語

正規のIdentityは以下の条件を満たす：

1. identity.did = fromValidDocument identity.didDocument

この検証により、悪意のあるHolderが不正な(did, didDocument)ペアを Walletに挿入することを防ぐ。

設計思想:

• IdentityはValidDIDとValidDIDDocumentを使用するため、型レベルで検証済み
• この述語は、ValidDIDがValidDIDDocumentから正しく生成されたかを確認

Equations

• Wallet.isValidIdentity identity = (identity.did = UnknownDID.fromValidDocument identity.didDocument)

def Wallet.isValid (wallet : Wallet) : Prop

Walletが正規かどうかを検証する述語

正規のWalletは、すべてのIdentityが正規であることを保証する。 これにより、wallet_identity_consistency が定理として証明可能になる。

Equations

• wallet.isValid = ∀ (identity : Identity), identity ∈ wallet.identities → Wallet.isValidIdentity identity

theorem Wallet.valid_wallet_has_valid_identities (w : Wallet) (identity : Identity) : w.isValid → identity ∈ w.identities → isValidIdentity identity

Theorem: 正規のWalletに含まれるIdentityは常に正規である

theorem Wallet.valid_wallet_identity_consistency (w : Wallet) (identity : Identity) : w.isValid → identity ∈ w.identities → identity.did = UnknownDID.fromValidDocument identity.didDocument

Theorem: 正規のWalletに含まれるIdentityはDID一貫性を満たす

def Wallet.validateDID (wallet : Wallet) (w3cDID : W3C.DID) : Option ValidDID

WalletからW3C.DIDを検証してValidDIDを取得

新設計で使用: ValidVC.getDelegatorやValidVC.getAuthorizedClaimIDsなどの新しい署名で使用する。

検証方法: Wallet.identitiesまたはWallet.trustedAnchorsから該当するDIDを検索し、 一致するものがあればValidDIDを返す。

パラメータ:

• wallet: 検証に使用するWallet
• w3cDID: 検証するW3C.DID

戻り値:

• Some validDID: Wallet内に該当するValidDIDが見つかった場合
• None: 見つからなかった場合

Equations

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

theorem list_length_pos_of_forall_mem {α : Type u_1} (l : List α) (P : α → Prop) : (∀ (x : α), x ∈ l → P x) → l ≠ [] → l.length > 0

リストが空でないことを長さから証明

structure VerifierAuthMessage : Type

検証者認証メッセージ

偽警官対策: Holderが検証者の正当性を確認するためのメッセージ。 検証者は以下の情報を含むメッセージをHolderに送信する：

1. expectedTrustAnchor: Holderが信頼しているはずのDID
2. verifierDID: 検証者自身のDID
3. verifierCredentials: expectedTrustAnchorから発行された検証者VCのリスト
4. nonce2: リプレイ攻撃防止用のナンス
5. authProof: 検証者がverifierDIDの所有者であることを証明するZKP

Holderは以下を検証する：

• expectedTrustAnchorがHolderのWallet.trustedAnchorsに含まれる
• verifierCredentialsに含まれるVerifierVCがexpectedTrustAnchorから発行されている
• VerifierVCのsubjectがverifierDIDと一致する
• authProofが有効である

これにより、Holderは偽警官（不正な検証者）にZKPを送信することを防ぐことができる。

• expectedTrustAnchor : UnknownDID
• verifierDID : UnknownDID
• verifierCredentials : List UnknownVC
• authProof : UnknownZKP

def VerifierAuthMessage.validateVerifierAuth (msg : VerifierAuthMessage) (holderWallet : Wallet) : Prop

検証者認証メッセージを検証する関数

Holderの視点で、検証者認証メッセージが正当かどうかを検証する。

検証項目:

1. expectedTrustAnchorがHolderのWallet.trustedAnchorsに存在する
2. verifierCredentialsに少なくとも1つのVerifierVCが含まれる
3. すべてのVerifierVCが有効である（UnknownVC.isValid）
4. すべてのVerifierVCのissuerがexpectedTrustAnchorと一致する
5. すべてのVerifierVCのsubjectがverifierDIDと一致する
6. authProofが有効である（ZeroKnowledgeProof.isValid）

Equations

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

theorem VerifierAuthMessage.authentic_verifier_passes (msg : VerifierAuthMessage) (holderWallet : Wallet) (validDID : ValidDID) : msg.expectedTrustAnchor = UnknownDID.valid validDID → (holderWallet.trustedAnchors.lookup validDID).isSome = true → msg.verifierCredentials ≠ [] → (∀ (vc : UnknownVC), vc ∈ msg.verifierCredentials → vc.isValid ∧ vc.getIssuer = msg.expectedTrustAnchor ∧ vc.getSubject = msg.verifierDID) → (∃ (relation : Relation), msg.authProof.isValid relation) → msg.validateVerifierAuth holderWallet

Theorem: 正規の検証者は検証に成功する

Holderが信頼するDIDから正当に発行されたVerifierVCを持ち、 有効なZKPを提示する検証者は、Holderの検証を通過する。

theorem VerifierAuthMessage.fake_verifier_fails (msg : VerifierAuthMessage) (holderWallet : Wallet) : ((match msg.expectedTrustAnchor with | UnknownDID.valid validDID => (holderWallet.trustedAnchors.lookup validDID).isNone = true | UnknownDID.invalid a => True) ∨ (∃ (vc : UnknownVC), vc ∈ msg.verifierCredentials ∧ (¬vc.isValid ∨ vc.getIssuer ≠ msg.expectedTrustAnchor ∨ vc.getSubject ≠ msg.verifierDID)) ∨ ∀ (relation : Relation), ¬msg.authProof.isValid relation) → ¬msg.validateVerifierAuth holderWallet

Theorem: 偽警官（不正な検証者）は検証に失敗する

以下のいずれかの条件を満たす不正な検証者は、Holderの検証を通過しない：

1. Holderが信頼していないDIDを提示する
2. 無効なVerifierVCを提示する
3. 他のDIDから発行されたVerifierVCを提示する
4. 他のDIDのVerifierVCを提示する（なりすまし）
5. 無効なZKPを提示する

structure Holder : Type

Holder: VCを保持し、必要に応じて提示する主体

DID/VCモデルにおける基本設計:

• DID/VCの世界では、全員が基本的にHolderである
• 役割（Issuer、Verifier等）は状況に応じて変わるものであり、固定的ではない
• 一般人でも家族や友達同士でVCを発行できる未来を想定

Wallet保持:

• すべての主体は1つ以上のWalletを保持する
• Wallet内にidentities（DID）、credentials（VC）、trustedAnchorsが含まれる

設計思想（自己責任）:

• Walletの正規性（Wallet.isValid）は不変条件として要求しない
• すべてのWalletアプリにはバグが存在しうる（現実的な仮定）
• バグのあるWalletを使うかどうかは利用者の自己責任
• Verifierは暗号的検証のみに依存し、Wallet実装を信頼しない
• バグのあるWalletが生成したZKP/VCは暗号的検証で弾かれる

• wallets : List Wallet
• wallets_nonempty : self.wallets ≠ []

@[reducible, inline]

abbrev Issuer : Type

Issuer: VCを発行するHolder

DID/VCモデルにおける役割:

• Issuerは固定的な役割ではなく、VC発行時の状況依存の役割
• 任意のHolderがVC発行者になることができる
• 型としてはHolderと同一（エイリアス）

発行と受け入れの関係:

• 誰でもVCを発行できる（W3C VC仕様に準拠）
• 受け取る側が、発行者を信頼するか（Wallet.trustedAnchorsに登録）を決定
• 直接信頼: 発行者が受け取る側のWallet.trustedAnchorsに登録されている
• 委譲信頼: 発行者がauthorizedClaimIDsを持つVC（委譲証明）を提示し、 その委譲元が受け取る側のWallet.trustedAnchorsに登録されている

Equations

• Issuer = Holder

@[reducible, inline]

abbrev Verifier : Type

Verifier: VCを検証するHolder

DID/VCモデルにおける役割:

• Verifierは固定的な役割ではなく、VC検証時の状況依存の役割
• 任意のHolderがVC検証者になることができる
• 型としてはHolderと同一（エイリアス）

偽警官対策:

• 検証者もWalletを持ち、信頼されるDIDから発行されたVerifierVCを保持できる
• 検証時には、Holderに対してこれらのVerifierVCを提示し、自身が正当な検証者であることを証明できる

信頼ポリシー:

• どのDIDを信頼するかは、各HolderがWallet.trustedAnchorsで自由に管理
• 各Holderが独自の信頼ポリシーを持つ（家族、友人、職場、政府など）

Equations

• Verifier = Holder

theorem valid_did_pair_passes (did : ValidDID) (doc : ValidDIDDocument) : did = UnknownDID.fromValidDocument doc → (UnknownDID.valid did).isValid doc

Theorem: ValidDIDとValidDIDDocumentのペアは検証に成功する

型レベルで正規と証明されたValidDIDとValidDIDDocumentのペアは、 UnknownDID.isValidの検証に成功する。

設計思想: この定理は型システムの健全性を示すもので、Wallet実装とは独立。 ValidDIDはUnknownDID.fromValidDocumentから生成されたものであり、 定義から自明に検証に成功する。

theorem verifier_cryptographic_soundness (_verifier : Verifier) (zkp : UnknownZKP) (relation : Relation) : zkp.isValid relation → zkp.verify relation = true

Theorem: Verifierの暗号的健全性（Cryptographic Soundness）

Verifierは暗号的に検証可能な情報のみを信頼し、 Wallet実装の詳細には依存しない。

設計思想の形式化:

• Verifierは以下のみを検証する:
  1. ZKPの暗号的検証（ZeroKnowledgeProof.verify）
  2. VCの署名検証（UnknownVC.isValid）
  3. トラストアンカーチェーンの検証
• Wallet内部の実装、秘密鍵の管理方法、ZKP生成アルゴリズムは検証しない
• したがって、Walletバグは検証結果に影響しない（バグがあれば検証失敗）

証明の要点: ZKPが有効であることは、ZeroKnowledgeProof.isValidの定義により、 ZeroKnowledgeProof.verifyがtrueを返すことと同値である。 この検証は暗号的検証のみに基づき、Wallet実装に依存しない。

theorem protocol_soundness : (∀ (_verifier : Verifier) (zkp : UnknownZKP) (relation : Relation), zkp.isValid relation → zkp.verify relation = true) ∧ (∀ (did : UnknownDID) (doc : ValidDIDDocument), did.isInvalidPair doc → ¬did.isValid doc) ∧ ∀ (vc : ValidVC), (UnknownVC.valid vc).isValid

Theorem: プロトコルの暗号的健全性（Protocol Cryptographic Soundness）

AMATELUSプロトコルは暗号的検証のみに依存し、Wallet実装には依存しない。

現実的な設計思想:

• すべてのアプリにバグがあるのが現実
• しかし、暗号的に不正なデータ（無効な署名、改ざんされたデータ）は検証失敗
• Wallet実装のバグは、暗号的検証で弾かれるため他者に影響しない
• 悪意ある他者とは暗号理論の範囲でのみ信頼が成立

保証される性質:

1. Verifierは暗号的検証のみに依存（ZKP検証、署名検証、トラストチェーン検証）
2. 不正な暗号的ペア（DID ↔ DIDDocument の不一致）は検証失敗
3. Wallet実装の詳細（バグの有無）は検証結果に影響しない

影響範囲の局所化:

• Walletのバグは利用者自身にのみ影響（自己責任）
• バグのあるWalletが生成した不正なデータは、Verifierの暗号的検証で弾かれる
• したがって、他者に影響を与えることはない