def extractPublicKey (doc : W3C.DIDDocument) : Option PublicKey

W3C.DIDDocumentから主要な公開鍵を抽出するヘルパー関数

verificationMethodの最初のエントリから公開鍵を取得します。 AMATELUSでは、did:amt仕様に従い、verificationMethodに必ず公開鍵が含まれます。

Equations

• extractPublicKey doc = do let vm ← doc.verificationMethod.head? let encoded ← vm.publicKeyMultibase AMT.decodePublicKey encoded

noncomputable def derivedDIDV0 (pk : PublicKey) : W3C.DID

Formal derivation using the repository's abstract hash model. For actual SHA3-512 execution use AMT.deriveWith with a verified backend.

Equations

• derivedDIDV0 pk = AMT.didFromHash (hashForDID (AMT.templateV0 pk).toUTF8.data.toList)

structure ValidDIDDocument : Type

正規のDIDDocument（所有権検証済み）

以下のいずれかの方法で検証されたDIDDocument：

1. Issuerによるチャレンジ検証: DIDCommでHolderが秘密鍵所有権を証明
2. トラストアンカー: 政府配布のウォレットに登録済み、または公式サイトからダウンロード

W3C DID仕様への準拠:

• W3C.DIDDocumentのVersion 0固定形と導出結果との整合性を保持
• did:amt仕様に従い、verificationMethodから公開鍵を抽出可能

設計思想:

• テンプレートとの整合性を型レベルで保証。秘密鍵所有権の検証は別途必要
• Issuerは検証済みのValidDIDDocumentからValidDIDを構築できる
• トラストアンカーのValidDIDDocumentは公的に信頼される

• w3cDoc : W3C.DIDDocument
• publicKey : PublicKey
• keySize : self.publicKey.bytes.length = 32
• canonical : AMT.matchesV0 self.w3cDoc self.publicKey (derivedDIDV0 self.publicKey) = true

instance instReprValidDIDDocument : Repr ValidDIDDocument

Equations

• instReprValidDIDDocument = { reprPrec := reprValidDIDDocument✝ }

structure InValidDIDDocument : Type

不正なDIDDocument

秘密鍵所有権が未検証、または検証に失敗したDIDDocument。 以下のいずれかの理由で不正：

• チャレンジ検証に失敗
• 改ざんされたDIDDocument
• 信頼できないソースから取得

• w3cDoc : W3C.DIDDocument
• reason : String

instance instReprInValidDIDDocument : Repr InValidDIDDocument

Equations

• instReprInValidDIDDocument = { reprPrec := reprInValidDIDDocument✝ }

inductive UnknownDIDDocument : Type

未検証のDIDDocument（和型）

構造的に正しくパースされたDIDDocumentで、所有権検証の結果を表す和型。 Holderから提示されるUnknownDIDDocumentは、以下のいずれか：

• valid: 所有権検証済みのDIDDocument
• invalid: 所有権未検証または検証失敗のDIDDocument

命名の意図:

• 「UnknownDIDDocument」= 構造的にパース成功したが、所有権検証の状態は未確定または既知
• W3C.DIDDocument（検証前）とは異なり、検証結果を含む

AMATELUSでの使用:

• HolderはUnknownDIDDocument（和型）をIssuerに提示
• Issuerはチャレンジで検証し、成功ならValidDIDDocumentを獲得
• ValidDIDDocumentからValidDIDを構築可能

• valid : ValidDIDDocument → UnknownDIDDocument
• invalid : InValidDIDDocument → UnknownDIDDocument

instance instBEqUnknownDIDDocument : BEq UnknownDIDDocument

UnknownDIDDocumentのBeqインスタンス（W3C DID識別子で比較）

Equations

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

instance instReprUnknownDIDDocument : Repr UnknownDIDDocument

UnknownDIDDocumentのReprインスタンス

Equations

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

def UnknownDIDDocument.getW3CDoc : UnknownDIDDocument → W3C.DIDDocument

UnknownDIDDocumentからW3C.DIDDocumentを取得

Equations

• (UnknownDIDDocument.valid v).getW3CDoc = v.w3cDoc
• (UnknownDIDDocument.invalid i).getW3CDoc = i.w3cDoc

def UnknownDIDDocument.isValid : UnknownDIDDocument → Prop

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

Equations

• (UnknownDIDDocument.valid v).isValid = True
• (UnknownDIDDocument.invalid i).isValid = False

def extractMethodSpecificId (did : W3C.DID) : String

W3C.DIDからmethod-specific-idを抽出するヘルパー関数

did:amt仕様では、method-specific-idがハッシュそのものです。 例: "did:amt:0V3R4T7K1Q2P3N4M5..." → "0V3R4T7K1Q2P3N4M5..."

Equations

• extractMethodSpecificId did = match W3C.parseDID did.value with | none => "" | some (fst, id) => id

inductive DIDPurpose : Type

DIDの種類（目的）

Identity DID:

• 身分証明用の永続的なDID
• 運転免許証、パスポート、資格情報など身分を示すVCの主体
• 長期間保持され、複数のサービスで参照される可能性がある

Communication DID:

• 通信毎に生成される一時的なDID
• サービス毎に異なる通信相手との通信に使用
• VCが発行されない場合は破棄
• VCが発行される場合は、Walletで通信相手DIDと紐づけて保存
• 複数サービス間での名寄せ回避: ZKP不学性により、複数のサービスから 異なる通信用DIDを観測しても、背後にある同じIdentity DIDを推測困難
• サービス内ログイン: 保存された同じ通信用DIDで認証継続（名寄せ不要）

Trust Anchor DID:

• 政府や公式機関による固定的なDID
• VC発行者として使用（自治体、銀行等）
• トラストアンカーとして公式サイトから配布
• 永続的かつ公開的に信頼される

• Identity : DIDPurpose
• Communication : DIDPurpose
• TrustAnchor : DIDPurpose

instance instReprDIDPurpose : Repr DIDPurpose

Equations

• instReprDIDPurpose = { reprPrec := reprDIDPurpose✝ }

instance instDecidableEqDIDPurpose : DecidableEq DIDPurpose

Equations

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

structure ValidDID : Type

正規のDID（検証済み）

Wallet内に対応するIdentityがあり、秘密鍵を保持しているDID。

フィールド:

• w3cDID: W3C DID仕様に準拠したDID識別子
• hash: DIDを含まない固定テンプレートから計算されたハッシュ値
• purpose: DIDの使用目的（Identity、Communication、TrustAnchor）

did:amt仕様:

• method-specific-idは生成用テンプレートのハッシュをCrockford Base32で符号化した値
• hashフィールドはこのハッシュ値を保持します
• w3cDIDのmethod-specific-id部分とhashの符号化結果は一致する必要があります

設計思想:

• Identity DID: 永続的、複数のサービスで使用可能
• Communication DID: 一時的、VC発行なしなら破棄
• Trust Anchor DID: 公開的、Issuer/Verifierが使用

• w3cDID : W3C.DID
• hash : Hash
• purpose : DIDPurpose

instance instReprValidDID : Repr ValidDID

Equations

• instReprValidDID = { reprPrec := reprValidDID✝ }

instance instDecidableEqValidDID : DecidableEq ValidDID

Equations

• instDecidableEqValidDID = decEqValidDID✝

structure InvalidDID : Type

不正なDID

Wallet内にIdentityがない、または盗難されたDID。

フィールド:

• w3cDID: W3C DID仕様に準拠したDID識別子
• reason: 不正と判断された理由

• w3cDID : W3C.DID
• reason : String

instance instReprInvalidDID : Repr InvalidDID

Equations

• instReprInvalidDID = { reprPrec := reprInvalidDID✝ }

instance instDecidableEqInvalidDID : DecidableEq InvalidDID

Equations

• instDecidableEqInvalidDID = decEqInvalidDID✝

inductive UnknownDID : Type

UnknownDID (Unknown Decentralized Identifier)

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

• valid: 正規のDID（Wallet内に対応するIdentityがある）
• invalid: 不正なDID（Wallet内にIdentityがない、または盗難DID）

設計の利点:

• DIDの正規性をプロトコルレベルで明確に区別
• Walletバグや悪意の攻撃を型レベルで表現
• ZKP/VC/DIDPairと完全に統一された設計
• ValidDIDにはハッシュ値を保持（did:amt仕様に準拠）

AMATELUSのDIDComm（VC発行フロー）:

• HolderがIssuerにDIDを送信してVC発行を依頼
• IssuerはDIDを受け取り、VCに埋め込む（issuer/subjectフィールド）
• Walletバグで間違ったDIDを送るとinvalidになる
• 悪意のあるHolderが他人のDIDを使うとinvalidになる
• いずれの場合も、VCは発行されるが、そのVCを使うことができない （Holderが秘密鍵を持っていないため、ZKPを生成できない）

ZKP/VC/DIDPairとの設計の一貫性:

• ZeroKnowledgeProof、VerifiableCredential、DIDPairと同じパターン（Valid/Invalid + 和型）
• 統一された形式検証アプローチ

• valid : ValidDID → UnknownDID
• invalid : InvalidDID → UnknownDID

instance instBEqUnknownDID : BEq UnknownDID

DIDのBeqインスタンス

Equations

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

instance instReprUnknownDID : Repr UnknownDID

DIDのReprインスタンス

Equations

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

instance instDecidableEqUnknownDID : DecidableEq UnknownDID

DIDのDecidableEqインスタンス

Equations

• instDecidableEqUnknownDID (UnknownDID.valid v1) (UnknownDID.valid v2) = if h : v1 = v2 then isTrue ⋯ else isFalse ⋯
• instDecidableEqUnknownDID (UnknownDID.invalid i1) (UnknownDID.invalid i2) = if h : i1 = i2 then isTrue ⋯ else isFalse ⋯
• instDecidableEqUnknownDID (UnknownDID.valid a_2) (UnknownDID.invalid a_3) = isFalse ⋯
• instDecidableEqUnknownDID (UnknownDID.invalid a_2) (UnknownDID.valid a_3) = isFalse ⋯

def serializeUnknownDIDDocument (doc : ValidDIDDocument) : List UInt8

Hash only the fixed pre-DID template, never the completed document.

Equations

• serializeUnknownDIDDocument doc = (AMT.templateV0 doc.publicKey).toUTF8.data.toList

noncomputable def ValidDIDDocumentToDID (doc : ValidDIDDocument) : W3C.DID

Reconstruct the DID from the public key instead of trusting a supplied id.

Equations

• ValidDIDDocumentToDID doc = derivedDIDV0 doc.publicKey

noncomputable def validateAMTDocument (version : ℕ) (doc : W3C.DIDDocument) : Option ValidDIDDocument

The formal-model boundary rejects unsupported versions and altered final fields. This does not establish key ownership or execute real SHA3-512.

Equations

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

theorem valid_document_id_is_derived (doc : ValidDIDDocument) : doc.w3cDoc.id = derivedDIDV0 doc.publicKey

The stored document id is necessarily the locally derived id.

theorem same_key_same_preimage (a b : ValidDIDDocument) (h : a.publicKey = b.publicKey) : serializeUnknownDIDDocument a = serializeUnknownDIDDocument b

Changing a completed document cannot change the preimage if its key is unchanged.

noncomputable def UnknownDID.fromValidDocument (doc : ValidDIDDocument) : ValidDID

ValidDIDDocumentからValidDIDを生成（デフォルト: Identity）

ValidDIDDocumentをシリアライズしてハッシュを計算し、ValidDIDを構築します。 この関数は、既存のコードとの互換性を保つため、デフォルトでIdentityを選択します。

AMATELUSでの使用:

• Issuer: チャレンジ検証後にValidDIDを取得（通常はIdentity）
• Verifier: トラストアンカーの公開UnknownDIDDocumentからValidDIDを取得

この定義により、以下が保証される：

• 決定性: 同じValidDIDDocumentからは常に同じValidDIDが取得される
• DID文字列はテンプレートのハッシュから導出する。衝突耐性は暗号バックエンドの責務。

Equations

• UnknownDID.fromValidDocument doc = { w3cDID := ValidDIDDocumentToDID doc, hash := hashForDID (serializeUnknownDIDDocument doc), purpose := DIDPurpose.Identity }

noncomputable def UnknownDID.fromValidDocumentWithPurpose (doc : ValidDIDDocument) (purpose : DIDPurpose) : ValidDID

ValidDIDDocumentからValidDIDを生成（目的指定版）

パラメータ:

• doc: ValidDIDDocument
• purpose: DIDの使用目的（Identity、Communication、TrustAnchor）

AMATELUSでの使用:

• Holder: 通信毎に通信用DIDを生成（Communication）
• Issuer/Verifier: 特定の目的でDID生成時

Equations

• UnknownDID.fromValidDocumentWithPurpose doc purpose = { w3cDID := ValidDIDDocumentToDID doc, hash := hashForDID (serializeUnknownDIDDocument doc), purpose := purpose }

noncomputable def UnknownDID.fromDocument (doc : UnknownDIDDocument) : UnknownDID

UnknownDIDDocumentからDID（和型）を生成する（デフォルト: Identity）

変換:

• ValidDIDDocument → ValidDID（w3cDIDとhashを含む、purposeはIdentityに固定）
• InValidDIDDocument → InvalidDID（w3cDIDとreasonを含む）

この関数により、UnknownDIDDocumentの正規性がDIDの正規性に反映されます。 既存のコードとの互換性を保つため、デフォルトでIdentityを選択します。

Equations

• UnknownDID.fromDocument (UnknownDIDDocument.valid v) = UnknownDID.valid (UnknownDID.fromValidDocument v)
• UnknownDID.fromDocument (UnknownDIDDocument.invalid i) = UnknownDID.invalid { w3cDID := i.w3cDoc.id, reason := "Invalid UnknownDIDDocument: " ++ i.reason }

noncomputable def UnknownDID.fromDocumentWithPurpose (doc : UnknownDIDDocument) (purpose : DIDPurpose) : UnknownDID

UnknownDIDDocumentからDID（和型）を生成する（目的指定版）

パラメータ:

• doc: UnknownDIDDocument
• purpose: DIDの使用目的（Identity、Communication、TrustAnchor）

変換:

• ValidDIDDocument → ValidDID（w3cDIDとhashとpurposeを含む）
• InValidDIDDocument → InvalidDID（w3cDIDとreasonを含む）

この関数により、UnknownDIDDocumentの正規性がDIDの正規性に反映されます。

Equations

• UnknownDID.fromDocumentWithPurpose (UnknownDIDDocument.valid v) purpose = UnknownDID.valid (UnknownDID.fromValidDocumentWithPurpose v purpose)
• UnknownDID.fromDocumentWithPurpose (UnknownDIDDocument.invalid i) purpose = UnknownDID.invalid { w3cDID := i.w3cDoc.id, reason := "Invalid UnknownDIDDocument: " ++ i.reason }

def UnknownDID.getMethodSpecificId : UnknownDID → String

DIDからmethod-specific-id（ハッシュ）を取得

did:amt仕様では、method-specific-idがハッシュそのものです。

Equations

• (UnknownDID.valid v).getMethodSpecificId = extractMethodSpecificId v.w3cDID
• (UnknownDID.invalid i).getMethodSpecificId = extractMethodSpecificId i.w3cDID

def UnknownDID.toValidDID (did : UnknownDID) : Option ValidDID

UnknownDIDからValidDIDへの変換

valid: Some ValidDIDを返す invalid: noneを返す

設計思想: invalidなDIDで発行されたVCは、InvalidVCとして扱われるべきです。 この関数により、DIDの正規性がVCの正規性に正しく反映されます。

Equations

• (UnknownDID.valid v).toValidDID = some v
• (UnknownDID.invalid i).toValidDID = none

def UnknownDID.isValid (did : UnknownDID) (doc : ValidDIDDocument) : Prop

DIDがValidDIDDocumentから正しく生成されたかを検証（デフォルト: Identity）

パラメータ:

• did: 検証対象のDID
• doc: ValidDIDDocument

検証:

• did が valid で、fromValidDocument doc と等しい場合のみ成功
• invalid なDIDは常に失敗

既存のコードとの互換性を保つため、デフォルトでIdentityを選択します。

Equations

• (UnknownDID.valid v).isValid doc = (v = UnknownDID.fromValidDocument doc)
• (UnknownDID.invalid i).isValid doc = False

def UnknownDID.isValidWithPurpose (did : UnknownDID) (doc : ValidDIDDocument) (purpose : DIDPurpose) : Prop

DIDがValidDIDDocumentから正しく生成されたかを検証（目的指定版）

パラメータ:

• did: 検証対象のDID
• doc: ValidDIDDocument
• purpose: 期待されるDIDの使用目的

検証:

• did が valid で、fromValidDocumentWithPurpose doc purpose と等しい場合のみ成功
• invalid なDIDは常に失敗

Equations

• (UnknownDID.valid v).isValidWithPurpose doc purpose = (v = UnknownDID.fromValidDocumentWithPurpose doc purpose)
• (UnknownDID.invalid i).isValidWithPurpose doc purpose = False

def UnknownDID.isCanonicalPair (did : UnknownDID) (doc : ValidDIDDocument) : Prop

正規のDID-DIDドキュメントのペア（デフォルト: Identity）

HolderがVerifierに提示するペアは、この述語を満たす必要がある。 正規のペアは、DIDがValidDIDDocumentから正しく生成されたものである。 既存のコードとの互換性を保つため、デフォルトでIdentityを選択します。

Equations

• did.isCanonicalPair doc = did.isValid doc

def UnknownDID.isInvalidPair (did : UnknownDID) (doc : ValidDIDDocument) : Prop

不正なDID-DIDドキュメントのペア（デフォルト: Identity）

以下のいずれかの場合、ペアは不正である：

1. DIDとValidDIDDocumentが一致しない
2. InValidDIDDocumentから生成されたDID

Equations

• did.isInvalidPair doc = ¬did.isValid doc

def UnknownDID.isCanonicalPairWithPurpose (did : UnknownDID) (doc : ValidDIDDocument) (purpose : DIDPurpose) : Prop

正規のDID-DIDドキュメントのペア（目的指定版）

HolderがVerifierに提示するペアは、この述語を満たす必要がある。 正規のペアは、DIDがValidDIDDocumentから正しく生成されたものであり、 purposeが一致しているものである。

Equations

• did.isCanonicalPairWithPurpose doc purpose = did.isValidWithPurpose doc purpose

def UnknownDID.isInvalidPairWithPurpose (did : UnknownDID) (doc : ValidDIDDocument) (purpose : DIDPurpose) : Prop

不正なDID-DIDドキュメントのペア（目的指定版）

以下のいずれかの場合、ペアは不正である：

1. DIDとValidDIDDocumentが一致しない
2. InValidDIDDocumentから生成されたDID
3. purposeが期待値と異なる

Equations

• did.isInvalidPairWithPurpose doc purpose = ¬did.isValidWithPurpose doc purpose

theorem UnknownDID.invalid_pair_fails_validation (did : UnknownDID) (doc : ValidDIDDocument) : did.isInvalidPair doc → ¬did.isValid doc

Theorem: 不正なペアは検証に失敗する

HolderがVerifierに不正な(did, doc)ペアを提示した場合、 isValid did doc = Falseとなり、検証は失敗する。

theorem UnknownDID.validation_ensures_canonical (did : UnknownDID) (doc : ValidDIDDocument) : did.isValid doc → did.isCanonicalPair doc

Theorem: 検証成功は正規性を保証する

isValid did doc = Trueならば、(did, doc)は正規のペアである。 これは定義から自明だが、明示的に定理として示す。

theorem UnknownDID.verifier_rejects_invalid_pair (did : UnknownDID) (doc : ValidDIDDocument) : ¬did.isValid doc → ∃ (verificationFailed : Bool), verificationFailed = true

Theorem: Verifierは不正なペアを受け入れない（健全性）

Verifierが(did, doc)ペアを受け取った時、 isValid did doc = Falseならば、検証は失敗する。

これは、不正なHolderや攻撃者が偽のペアを提示しても 受け入れられないことを保証する。