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

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

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

Equations

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

structure ValidDIDDocument : Type

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

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

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

W3C DID仕様への準拠:

• 標準的なW3C.DIDDocumentをそのまま使用
• did:amt仕様に従い、verificationMethodから公開鍵を抽出可能

設計思想:

• DIDDocumentの正規性（所有権検証済み）を型レベルで保証
• Issuerは検証済みのValidDIDDocumentからValidDIDを構築できる
• トラストアンカーのValidDIDDocumentは公的に信頼される

• w3cDoc : W3C.DIDDocument

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: DIDDocumentから計算されたハッシュ値（did:amt仕様のmethod-specific-id）
• purpose: DIDの使用目的（Identity、Communication、TrustAnchor）

did:amt仕様:

• did:amt仕様では、method-specific-idがDIDDocumentのハッシュです
• 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 serializeW3CServiceEndpoint (se : W3C.ServiceEndpoint) : List UInt8

W3C ServiceEndpointをバイト列にシリアライズするヘルパー関数

Equations

• serializeW3CServiceEndpoint se = se.id.toUTF8.data.toList

def serializeW3CServices (services : List W3C.ServiceEndpoint) : List UInt8

W3C UnknownDIDDocumentのserviceフィールド全体をシリアライズ

Equations

• serializeW3CServices services = List.foldl (fun (acc : List UInt8) (se : W3C.ServiceEndpoint) => acc ++ serializeW3CServiceEndpoint se) [] services

def serializeUnknownDIDDocument (doc : ValidDIDDocument) : List UInt8

ValidDIDDocumentをバイト列にシリアライズする関数

シリアライズ形式: id.value ++ verificationMethods ++ services

設計:

• W3C DID仕様に完全準拠
• did:amt仕様に従い、標準フィールドのみを使用
• 決定的: 同じUnknownDIDDocumentは常に同じバイト列を生成
• 単射性: シリアライズ形式により、異なるUnknownDIDDocumentは異なるバイト列を生成（高確率）

Equations

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

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

ValidDIDDocumentからW3C.DIDを抽出する関数

この関数は、所有権検証済みのUnknownDIDDocumentからW3C.DID識別子を抽出します。

AMATELUSでの使用:

• Issuer: チャレンジ検証後、ValidDIDDocumentからW3C.DIDを取得
• トラストアンカー: 公開されたValidDIDDocumentからW3C.DIDを取得
• Verifier: トラストアンカーのValidDIDDocumentからW3C.DIDを取得

did:amt仕様との関係:

• did:amt仕様では、DID生成時にUnknownDIDDocument全体をハッシュ化
• ハッシュはmethod-specific-id部分に含まれる（例: did:amt:0V3R4T7K1Q2P3N4M5...）
• したがって、W3C.DIDのvalueからmethod-specific-idを抽出すればハッシュが得られる

技術仕様:

• 入力: ValidDIDDocument（所有権検証済み）
• 出力: W3C.DID
• 性質: 決定性（同じ入力には同じ出力）

Equations

• ValidDIDDocumentToDID doc = doc.w3cDoc.id

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

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

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

AMATELUSでの使用:

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

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

• 決定性: 同じValidDIDDocumentからは常に同じValidDIDが取得される
• 一意性: did:amt仕様により、method-specific-idがハッシュなので一意性が保証される

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や攻撃者が偽のペアを提示しても 受け入れられないことを保証する。