inductive PrivateKeyAccessibility : Type

秘密鍵へのアクセス可能性

状態:

• available: 秘密鍵が手元にある（署名操作が可能）
• unavailable: 秘密鍵が手元にない（紛失、破損など）
• permanently_lost: 全ての鍵コピーが失われたことを別途確認した状態（死亡とは独立）

• available : PrivateKeyAccessibility
• unavailable : PrivateKeyAccessibility
• unknown : PrivateKeyAccessibility
• permanently_lost : PrivateKeyAccessibility

instance instReprPrivateKeyAccessibility : Repr PrivateKeyAccessibility

Equations

• instReprPrivateKeyAccessibility = { reprPrec := reprPrivateKeyAccessibility✝ }

instance instBEqPrivateKeyAccessibility : BEq PrivateKeyAccessibility

Equations

• instBEqPrivateKeyAccessibility = { beq := beqPrivateKeyAccessibility✝ }

inductive AbuseRisk : Type

悪用懸念の有無

状態:

• suspected: 第三者に秘密鍵が渡った可能性がある（盗難、乗っ取りなど）
• no_concern: 悪用の懸念はない（破損、故障など）

• suspected : AbuseRisk
• no_concern : AbuseRisk

instance instReprAbuseRisk : Repr AbuseRisk

Equations

• instReprAbuseRisk = { reprPrec := reprAbuseRisk✝ }

instance instBEqAbuseRisk : BEq AbuseRisk

Equations

• instBEqAbuseRisk = { beq := beqAbuseRisk✝ }

inductive PrivateKeyState : Type

秘密鍵の状態

状態:

• normal: 正常（秘密鍵が利用可能で問題なし）
• leaked: 漏洩（秘密鍵が手元にあるが、第三者に渡った可能性がある）
• lost: 紛失（秘密鍵が手元にない、悪用懸念の有無を区別）
• updating: 更新中（新旧の秘密鍵が両方手元にある）
• deceased: 本人死亡（鍵コピーの利用可能性は不明）
• under_guardianship: 被後見人（本人は秘密鍵にアクセス可能だが法的制限あり）

• normal : PrivateKeyState
• leaked : PrivateKeyState
• lost : AbuseRisk → PrivateKeyState
• updating : PrivateKeyState
• deceased : PrivateKeyState
• under_guardianship : PrivateKeyState

instance instReprPrivateKeyState : Repr PrivateKeyState

Equations

• instReprPrivateKeyState = { reprPrec := reprPrivateKeyState✝ }

def PrivateKeyState.getAccessibility : PrivateKeyState → PrivateKeyAccessibility

秘密鍵状態のアクセス可能性を取得

Equations

• PrivateKeyState.normal.getAccessibility = PrivateKeyAccessibility.available
• PrivateKeyState.leaked.getAccessibility = PrivateKeyAccessibility.available
• (PrivateKeyState.lost a).getAccessibility = PrivateKeyAccessibility.unavailable
• PrivateKeyState.updating.getAccessibility = PrivateKeyAccessibility.available
• PrivateKeyState.deceased.getAccessibility = PrivateKeyAccessibility.unknown
• PrivateKeyState.under_guardianship.getAccessibility = PrivateKeyAccessibility.available

structure IdentityDocument : Type

実世界の身分証明書情報

信頼継承の基盤となる情報。 本人確認プロセスで使用される実物の身分証明書の記録。

• docType : String

  身分証明書の種類

• documentNumber : String

  証明書番号

• issuerName : String

  発行者名

• verifiedAt : Timestamp

  検証日時

instance instReprIdentityDocument : Repr IdentityDocument

Equations

• instReprIdentityDocument = { reprPrec := reprIdentityDocument✝ }

structure ValidNormalPerson : Type

健常な生存者（本人確認済み）

Trust Anchor境界: このstructureのインスタンスが存在すること自体が、 物理世界での本人確認プロセスが完了したことを型レベルで保証する。

生成条件（Trust Anchorの要件）:

• 対面での身分証明書確認が完了
• 実世界の身分証明書（運転免許証、マイナンバーカードなど）が有効
• 信頼されたIssuer（警察署、市役所など）による本人確認プロセス

設計の核心: この型のインスタンスが作られた瞬間、「Trust Anchorを超えた」ことになる。 以降は暗号学的に証明可能な領域で処理される。

• did : ValidDID

  本人のDID

• identityDocument : IdentityDocument

  実世界の身分証明書（本人確認の根拠）

• verifiedAt : Timestamp

  本人確認完了日時

instance instReprValidNormalPerson : Repr ValidNormalPerson

Equations

• instReprValidNormalPerson = { reprPrec := reprValidNormalPerson✝ }

structure ValidWardPerson : Type

被後見人（本人確認済み + 後見制度確認済み）

生成条件（Trust Anchorの要件）:

• 対面での本人確認完了
• 有効な後見人VCが存在（後見開始審判書、登記事項証明書の確認）
• 家庭裁判所の審判確定

法的根拠: 民法第7条～第876条の9（成年後見制度）

重要な特性: 被後見人本人は秘密鍵にアクセス可能だが、法的制限により 後見人の同意が必要な行為が存在する。

設計上の注意: GuardianCredentialは後で定義されるため、ここでは後見制度の確認が 完了していることを型レベルで表現するに留める。具体的な後見人情報は 後見登記番号で参照可能。

• did : ValidDID

  被後見人のDID

• guardianDID : ValidDID

  後見人のDID

• guardianshipRegistrationNumber : String

  後見登記番号（後見人VCを参照するための識別子）

• identityDocument : IdentityDocument

  実世界の身分証明書

• verifiedAt : Timestamp

  本人確認完了日時

instance instReprValidWardPerson : Repr ValidWardPerson

Equations

• instReprValidWardPerson = { reprPrec := reprValidWardPerson✝ }

inductive ValidLivingPerson : Type

正規に検証された生存者

本人確認プロセスを完了した生存者の和型。

Trust Anchorの境界:

• ValidNormalPerson または ValidWardPerson のインスタンスが存在 → Trust Anchorを超えた（物理世界での本人確認完了）
• 以降は暗号学的に証明可能な領域

• normal : ValidNormalPerson → ValidLivingPerson
• ward : ValidWardPerson → ValidLivingPerson

instance instReprValidLivingPerson : Repr ValidLivingPerson

Equations

• instReprValidLivingPerson = { reprPrec := reprValidLivingPerson✝ }

structure InvalidLivingPerson : Type

検証されていない/不正な生存者

本人確認プロセスが失敗した、または不正な生存者の記録。

生成理由の例:

• 実世界の身分証明書が偽造
• 本人確認プロセスが不完全
• 身分証明書が失効済み

• did : ValidDID

  DID（検証失敗）

• reason : String

  検証失敗の理由

instance instReprInvalidLivingPerson : Repr InvalidLivingPerson

Equations

• instReprInvalidLivingPerson = { reprPrec := reprInvalidLivingPerson✝ }

inductive UnknownLivingPerson : Type

未検証の生存者

本人確認プロセスの結果を表す和型。 VC.lean, ZKP.leanと同じパターン。

設計の利点:

• 本人確認の暗号的詳細（対面確認プロセスなど）を抽象化
• プロトコルレベルでは「本人確認済み/未確認」の区別のみが重要
• 不正な本人確認はinvalidとして表現され、プロトコルの安全性には影響しない

• valid : ValidLivingPerson → UnknownLivingPerson
• invalid : InvalidLivingPerson → UnknownLivingPerson

instance instReprUnknownLivingPerson : Repr UnknownLivingPerson

Equations

• instReprUnknownLivingPerson = { reprPrec := reprUnknownLivingPerson✝ }

instance instReprUnknownLivingPerson_1 : Repr UnknownLivingPerson

Equations

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

def UnknownLivingPerson.isValid : UnknownLivingPerson → Bool

本人確認が成功したかどうか（定義として実装）

設計の核心:

• 正規の生存者（valid）: 常に本人確認成功
• 不正な生存者（invalid）: 常に本人確認失敗

Equations

• (UnknownLivingPerson.valid a).isValid = true
• (UnknownLivingPerson.invalid a).isValid = false

theorem UnknownLivingPerson.valid_living_person_verified (vp : ValidLivingPerson) : (valid vp).isValid = true

Theorem: 正規の生存者は常に本人確認成功

theorem UnknownLivingPerson.invalid_living_person_not_verified (ip : InvalidLivingPerson) : ¬(invalid ip).isValid = true

Theorem: 不正な生存者は常に本人確認失敗

structure ValidDeadPerson : Type

死亡者（死亡証明済み）

生成条件（Trust Anchorの要件）:

• 有効な死亡証明VCが存在
• 自治体による死亡登録完了（戸籍への死亡記載）

重要な特性: ValidDeadPersonのインスタンスが存在すること自体が、 公的機関による死亡確認が完了したことを型レベルで保証する。

設計上の注意: DeathCertificateは後で定義されるため、ここでは死亡登録番号を 保持することで死亡証明VCを参照可能にする。

• did : ValidDID

  死亡者のDID

• deathDate : Timestamp

  死亡日

• deathRegistrationNumber : String

  死亡登録番号（死亡証明VCを参照するための識別子）

instance instReprValidDeadPerson : Repr ValidDeadPerson

Equations

• instReprValidDeadPerson = { reprPrec := reprValidDeadPerson✝ }

structure InvalidDeadPerson : Type

検証されていない/不正な死亡者記録

死亡証明の検証が失敗した記録。

生成理由の例:

• 死亡証明VCの署名が不正
• 死亡登録番号が存在しない
• 死亡証明書が偽造

• did : ValidDID

  DID

• reason : String

  検証失敗の理由

instance instReprInvalidDeadPerson : Repr InvalidDeadPerson

Equations

• instReprInvalidDeadPerson = { reprPrec := reprInvalidDeadPerson✝ }

inductive UnknownDeadPerson : Type

未検証の死亡者

死亡証明の検証結果を表す和型。

• valid : ValidDeadPerson → UnknownDeadPerson
• invalid : InvalidDeadPerson → UnknownDeadPerson

instance instReprUnknownDeadPerson : Repr UnknownDeadPerson

Equations

• instReprUnknownDeadPerson = { reprPrec := reprUnknownDeadPerson✝ }

instance instReprUnknownDeadPerson_1 : Repr UnknownDeadPerson

Equations

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

def UnknownDeadPerson.isValid : UnknownDeadPerson → Bool

死亡証明が有効かどうか（定義として実装）

Equations

• (UnknownDeadPerson.valid a).isValid = true
• (UnknownDeadPerson.invalid a).isValid = false

theorem UnknownDeadPerson.valid_dead_person_verified (vd : ValidDeadPerson) : (valid vd).isValid = true

Theorem: 正規の死亡者は常に死亡証明有効

theorem UnknownDeadPerson.invalid_dead_person_not_verified (id : InvalidDeadPerson) : ¬(invalid id).isValid = true

Theorem: 不正な死亡者記録は常に死亡証明無効

inductive UnknownPerson : Type

人の状態

生存者と死亡者を統合する最上位の和型。

設計の核心:

• ValidLivingPerson: Trust Anchorを超えた「本人確認済み」の生存者
• ValidDeadPerson: 死亡証明済みの死亡者
• この型により、Trust Anchorが型の境界に明示化される

Trust Anchor境界の明確化:

物理世界（Trust Anchor）
  ↓ 対面確認、身分証明書検証、死亡登録確認
UnknownPerson.living (valid _) または UnknownPerson.dead (valid _)
  ↓ ここから先は暗号学的に証明可能
VC発行、DID移行、失効処理など

• living : UnknownLivingPerson → UnknownPerson
• dead : UnknownDeadPerson → UnknownPerson

instance instReprUnknownPerson : Repr UnknownPerson

Equations

• instReprUnknownPerson = { reprPrec := reprUnknownPerson✝ }

instance instReprUnknownPerson_1 : Repr UnknownPerson

Equations

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

inductive IdentityVCAvailability : Type

身分証明VCの有無

信頼継承の可否を決定する重要な要素。 身分証明VCがない場合、数学的に安全な復旧方法が存在しない。

• available : IdentityVCAvailability
• unavailable : IdentityVCAvailability

instance instReprIdentityVCAvailability : Repr IdentityVCAvailability

Equations

• instReprIdentityVCAvailability = { reprPrec := reprIdentityVCAvailability✝ }

instance instBEqIdentityVCAvailability : BEq IdentityVCAvailability

Equations

• instBEqIdentityVCAvailability = { beq := beqIdentityVCAvailability✝ }

inductive KeyManagementScenario : Type

秘密鍵管理シナリオ

シナリオ分類:

• leakage: 秘密鍵漏洩（旧秘密鍵で署名可能、決定的に対応可能）
• loss_with_abuse_risk: 秘密鍵紛失（悪用懸念あり）
• loss_no_abuse: 秘密鍵紛失（悪用懸念なし、身分証明VCの有無で対応可否が決まる）
• planned_update: 計画的な秘密鍵更新（マルチデバイス対応など）
• death_with_family: 本人死亡（家族あり、遺族が代理VC取得可能）
• death_no_family: 本人死亡（家族なし、自治体のみ対応可能）
• guardianship: 被後見人（後見人VCによる管理）

• leakage : KeyManagementScenario
• loss_with_abuse_risk : KeyManagementScenario
• loss_no_abuse : IdentityVCAvailability → KeyManagementScenario
• planned_update : KeyManagementScenario
• death_with_family : KeyManagementScenario
• death_no_family : KeyManagementScenario
• guardianship : KeyManagementScenario

instance instReprKeyManagementScenario : Repr KeyManagementScenario

Equations

• instReprKeyManagementScenario = { reprPrec := reprKeyManagementScenario✝ }

inductive ResponseCapability : Type

シナリオの対応可能性レベル

各シナリオで達成できる対応の確実性。

• deterministic : ResponseCapability
• limited : ResponseCapability
• impossible : ResponseCapability
• dependent_on_execution : ResponseCapability

instance instReprResponseCapability : Repr ResponseCapability

Equations

• instReprResponseCapability = { reprPrec := reprResponseCapability✝ }

instance instBEqResponseCapability : BEq ResponseCapability

Equations

• instBEqResponseCapability = { beq := beqResponseCapability✝ }

structure ValidRevocationEvidence : Type

正規の失効要求 (Valid Revocation Request)

署名検証が成功する失効要求。 旧秘密鍵による署名により、鍵の利用を示すのみで、正当な本人性を証明しない。

構造:

• oldDID: 漏洩した（または更新前の）DID
• newDID: 新しいDID（オプション）
• timestamp: 失効要求のタイムスタンプ
• revocationReason: 失効理由
• signatureByOldKey: 旧秘密鍵による署名（決定性の根拠）

暗号学的保証: Wire signatures use RequestBinding.keyBytes, including operation, recipient, scope and expiry. 漏洩鍵を持つ攻撃者も署名できる。緊急停止と個人資格再発行は別手続き。

不変条件:

• 署名検証が成功済み（旧秘密鍵の正当な所有者による要求）

• oldDID : ValidDID

  失効対象のDID

• newDID : Option ValidDID

  新しいDID（オプション）

• timestamp : Timestamp

  失効要求のタイムスタンプ

• revocationReason : String

  失効理由

• signatureByOldKey : Signature

  旧秘密鍵による署名（決定性の根拠）

instance instReprValidRevocationEvidence : Repr ValidRevocationEvidence

Equations

• instReprValidRevocationEvidence = { reprPrec := reprValidRevocationEvidence✝ }

structure InvalidRevocationEvidence : Type

不正な失効要求 (Invalid Revocation Request)

署名検証が失敗する失効要求。 以下のいずれかの理由で不正：

• 旧秘密鍵を持たない第三者による偽造
• 署名が改ざんされている
• 署名検証に失敗する

• oldDID : ValidDID

  失効対象のDID

• newDID : Option ValidDID

  新しいDID（オプション）

• timestamp : Timestamp

  失効要求のタイムスタンプ

• revocationReason : String

  失効理由

• signatureByOldKey : Signature

  旧秘密鍵による署名（決定性の根拠）

• reason : String

  不正な理由

instance instReprInvalidRevocationEvidence : Repr InvalidRevocationEvidence

Equations

• instReprInvalidRevocationEvidence = { reprPrec := reprInvalidRevocationEvidence✝ }

inductive UnknownRevocationEvidence : Type

未検証の失効要求 (Unknown Revocation Request)

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

• valid: 正規の失効要求（署名検証が成功）
• invalid: 不正な失効要求（署名検証が失敗）

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

• 署名検証の暗号的詳細を抽象化
• プロトコルレベルでは「正規/不正」の区別のみが重要
• 第三者の偽造はinvalidとして表現され、プロトコルの安全性には影響しない

• valid : ValidRevocationEvidence → UnknownRevocationEvidence
• invalid : InvalidRevocationEvidence → UnknownRevocationEvidence

instance instReprUnknownRevocationEvidence : Repr UnknownRevocationEvidence

Equations

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

def UnknownRevocationEvidence.verifySignature : UnknownRevocationEvidence → Bool

失効要求の署名検証（定義として実装）

設計の核心:

• 正規の失効要求（valid）: 常に検証成功（署名が有効）
• 不正な失効要求（invalid）: 常に検証失敗（署名が無効）

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

Equations

• (UnknownRevocationEvidence.valid a).verifySignature = true
• (UnknownRevocationEvidence.invalid a).verifySignature = false

def UnknownRevocationEvidence.isValid (req : UnknownRevocationEvidence) : Prop

失効要求が有効かどうかを表す述語

Equations

• req.isValid = (req.verifySignature = true)

def UnknownRevocationEvidence.isDeterministic : UnknownRevocationEvidence → Bool

失効要求が決定的に検証可能かどうか

旧秘密鍵による署名があるため、常に決定的に検証可能。 ValidRevocationEvidenceの場合、決定的に検証可能。

Equations

• (UnknownRevocationEvidence.valid a).isDeterministic = true
• (UnknownRevocationEvidence.invalid a).isDeterministic = false

theorem UnknownRevocationEvidence.valid_revocation_request_passes (vreq : ValidRevocationEvidence) : (valid vreq).isValid

Theorem: 正規の失効要求は常に検証成功

暗号学的に正しく署名された失効要求は、署名検証が成功する。

theorem UnknownRevocationEvidence.invalid_revocation_request_fails (ireq : InvalidRevocationEvidence) : ¬(invalid ireq).isValid

Theorem: 不正な失効要求は常に検証失敗

暗号学的に不正な失効要求は、署名検証が失敗する。

structure DIDMigrationCredential : Type

DID移行証明VC (DIDMigrationCredential)

身分証明VCを持つHolderが秘密鍵を紛失した際、 実世界の身分証明書による本人確認を経て発行されるVC。

信頼継承の原理: 旧DID → 身分証明VC → 実世界の身分証明書 ↓ 新DID ← DID移行証明VC ← 実世界の身分証明書

重要な特性:

• 発行者: 信頼されたIssuer（警察署、市役所など）
• 本人確認方法: 実物の身分証明書による対面確認
• 検証可能性: 他のIssuerがこのVCを検証して新DIDへのVC再発行を判断

Trust Anchorの表現: person: ValidLivingPerson フィールドの存在により、本人確認プロセス （Trust Anchor）を超えたことが型レベルで保証される。 identityDocValid チェックが不要に！

• core : ValidVC

  VCのコア情報

• newDID : ValidDID

  新しいDID（移行先）

• oldDID : ValidDID

  古いDID（移行元）

• person : ValidLivingPerson

  本人（本人確認済みの生存者）

• migrationType : String

  移行の種類

• migrationReason : String

  移行理由

def DIDMigrationCredential.isTrustedIssuer (dmc : DIDMigrationCredential) (trustedIssuers : List ValidDID) : Bool

DID移行証明VCの発行者が信頼できるか

Trust Anchorの相対性: 「絶対的に信頼できるIssuer」は分散システムには存在しない。 各Holder/Verifier/Issuerが自分のWallet内に「信頼するIssuerのリスト」を管理。

例:

• 日本人のWallet: [日本の警察署, 日本の市役所, ...]
• アメリカ人のWallet: [アメリカ政府, 州政府, ...]
• 外国人が日本の警察を信頼するとは限らない（個人の自由）

実装: trustedIssuersリストにdmc.core.issuerが含まれているかチェック。 このリストはWallet所有者が管理する主観的なTrust Anchor。

Equations

• dmc.isTrustedIssuer trustedIssuers = trustedIssuers.contains dmc.core.issuerDID

def DIDMigrationCredential.verify (dmc : DIDMigrationCredential) (trustedIssuers : List ValidDID) : Bool

DID移行証明VCの検証

発行者の署名と移行種別の検証。

Trust Anchorによる簡略化: person: ValidLivingPerson フィールドの存在により、本人確認プロセスは 型レベルで保証される。identityDocValid チェックは不要！

検証項目:

1. VC署名の検証（ValidVCは型レベルで保証）
2. migrationType = "trustInheritance"
3. 発行者が信頼できるか（Walletのトラストアンカーリストと照合）

Equations

• dmc.verify trustedIssuers = ((UnknownVC.valid dmc.core).verifySignature && dmc.migrationType == "trustInheritance" && dmc.isTrustedIssuer trustedIssuers)

structure ValidDIDUpdateEvidence : Type

正規のDID更新要求 (Valid DID Update Request)

双方向署名検証が成功するDID更新要求。 oldDIDとnewDIDの両鍵管理者の同意を検証。同一人物性は発行者承認で保証。

構造:

• oldDID: 更新前のDID
• newDID: 更新後のDID
• timestamp: 更新要求のタイムスタンプ
• updateReason: 更新理由
• transitionPeriod: 移行期間（日数）
• signatureByOldKey: 旧秘密鍵による署名
• signatureByNewKey: 新秘密鍵による署名

暗号学的保証: Wire signatures use RequestBinding.keyBytes, including operation, recipient, scope and expiry. Old/new signer roles are distinct signed domains over the same operation payload. → 両方の署名は鍵管理者の同意のみを保証する

不変条件:

• 双方向署名検証が成功済み（本人移転承認とは別）

• oldDID : ValidDID

  更新前のDID

• newDID : ValidDID

  更新後のDID

• timestamp : Timestamp

  更新要求のタイムスタンプ

• updateReason : String

  更新理由

• transitionPeriod : ℕ

  移行期間（日数）

• signatureByOldKey : Signature

  旧秘密鍵による署名

• signatureByNewKey : Signature

  新秘密鍵による署名

instance instReprValidDIDUpdateEvidence : Repr ValidDIDUpdateEvidence

Equations

• instReprValidDIDUpdateEvidence = { reprPrec := reprValidDIDUpdateEvidence✝ }

structure InvalidDIDUpdateEvidence : Type

不正なDID更新要求 (Invalid DID Update Request)

双方向署名検証が失敗するDID更新要求。 以下のいずれかの理由で不正：

• 旧秘密鍵または新秘密鍵を持たない第三者による偽造
• 署名が改ざんされている
• 署名検証に失敗する

• oldDID : ValidDID

  更新前のDID

• newDID : ValidDID

  更新後のDID

• timestamp : Timestamp

  更新要求のタイムスタンプ

• updateReason : String

  更新理由

• transitionPeriod : ℕ

  移行期間（日数）

• signatureByOldKey : Signature

  旧秘密鍵による署名

• signatureByNewKey : Signature

  新秘密鍵による署名

• reason : String

  不正な理由

instance instReprInvalidDIDUpdateEvidence : Repr InvalidDIDUpdateEvidence

Equations

• instReprInvalidDIDUpdateEvidence = { reprPrec := reprInvalidDIDUpdateEvidence✝ }

inductive UnknownDIDUpdateEvidence : Type

未検証のDID更新要求 (Unknown DID Update Request)

構造的に正しくパースされたDID更新要求で、双方向署名検証の結果を表す和型。 AMATELUSプロトコルで扱われるDID更新要求は、暗号学的に以下のいずれか：

• valid: 正規のDID更新要求（双方向署名検証が成功）
• invalid: 不正なDID更新要求（双方向署名検証が失敗）

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

• 双方向署名検証の暗号的詳細を抽象化
• プロトコルレベルでは「正規/不正」の区別のみが重要
• 第三者の偽造はinvalidとして表現され、プロトコルの安全性には影響しない

• valid : ValidDIDUpdateEvidence → UnknownDIDUpdateEvidence
• invalid : InvalidDIDUpdateEvidence → UnknownDIDUpdateEvidence

instance instReprUnknownDIDUpdateEvidence : Repr UnknownDIDUpdateEvidence

Equations

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

def UnknownDIDUpdateEvidence.verifySignatures : UnknownDIDUpdateEvidence → Bool

DID更新要求の双方向署名検証（定義として実装）

設計の核心:

• 正規のDID更新要求（valid）: 常に検証成功（双方向署名が有効）
• 不正なDID更新要求（invalid）: 常に検証失敗（双方向署名が無効）

この単純な定義により、暗号的詳細（Dilithium2双方向署名検証など）を 抽象化しつつ、プロトコルの安全性を形式的に証明できる。

Equations

• (UnknownDIDUpdateEvidence.valid a).verifySignatures = true
• (UnknownDIDUpdateEvidence.invalid a).verifySignatures = false

def UnknownDIDUpdateEvidence.isValid (req : UnknownDIDUpdateEvidence) : Prop

DID更新要求が有効かどうかを表す述語

Equations

• req.isValid = (req.verifySignatures = true)

def UnknownDIDUpdateEvidence.isDeterministic : UnknownDIDUpdateEvidence → Bool

DID更新要求が決定的に検証可能かどうか

双方向署名があるため、常に決定的に検証可能。 ValidDIDUpdateEvidenceの場合、決定的に検証可能。

Equations

• (UnknownDIDUpdateEvidence.valid a).isDeterministic = true
• (UnknownDIDUpdateEvidence.invalid a).isDeterministic = false

theorem UnknownDIDUpdateEvidence.valid_did_update_request_passes (vreq : ValidDIDUpdateEvidence) : (valid vreq).isValid

Theorem: 正規のDID更新要求は常に検証成功

暗号学的に正しく双方向署名されたDID更新要求は、署名検証が成功する。

theorem UnknownDIDUpdateEvidence.invalid_did_update_request_fails (ireq : InvalidDIDUpdateEvidence) : ¬(invalid ireq).isValid

Theorem: 不正なDID更新要求は常に検証失敗

暗号学的に不正なDID更新要求は、署名検証が失敗する。

inductive LegalAuthority : Type

法的代理権限の種類

本人死亡後、遺族が行使できる権限。

• vc_revocation : LegalAuthority
• contract_cancellation : LegalAuthority
• property_management : LegalAuthority

instance instReprLegalAuthority : Repr LegalAuthority

Equations

• instReprLegalAuthority = { reprPrec := reprLegalAuthority✝ }

instance instBEqLegalAuthority : BEq LegalAuthority

Equations

• instBEqLegalAuthority = { beq := beqLegalAuthority✝ }

structure LegalRepresentativeCredential : Type

代理VC (Legal Representative Credential)

本人死亡時に自治体が遺族に対して発行するVC。 遺族が民間Issuerに対してVC失効を依頼する際に使用。

重要な特性:

• 発行者: 信頼されたIssuer（市役所など）
• 本人確認方法: 実物の身分証明書および戸籍謄本による確認
• 権限: VC失効手続き、契約取り消しなど

• core : ValidVC

  VCのコア情報

• representativeID : ValidDID

  代理人のDID

• representativeOf : ValidDID

  代理対象者（死亡者）のDID

• relationship : String

  続柄

• authority : List LegalAuthority

  権限のリスト

• deathDate : Timestamp

  死亡情報

• deathRegistrationNumber : String

  死亡登録番号

• verificationMethod : String

  本人確認方法

def LegalRepresentativeCredential.isTrustedIssuer (lrc : LegalRepresentativeCredential) (trustedIssuers : List ValidDID) : Bool

代理VCの発行者が信頼できるか

Trust Anchorの相対性: 「絶対的に信頼できるIssuer」は分散システムには存在しない。 各Holder/Verifier/Issuerが自分のWallet内に「信頼するIssuerのリスト」を管理。

実装: trustedIssuersリストに含まれているかチェック。 このリストはWallet所有者が管理する主観的なTrust Anchor。

Equations

• lrc.isTrustedIssuer trustedIssuers = trustedIssuers.contains lrc.core.issuerDID

def LegalRepresentativeCredential.verify (lrc : LegalRepresentativeCredential) (trustedIssuers : List ValidDID) : Bool

代理VCの検証

検証項目:

1. VC署名の検証（ValidVCは型レベルで保証）
2. authorityに必要な権限が含まれているか
3. 発行者が信頼できるか（Walletのトラストアンカーリストと照合）

Equations

• lrc.verify trustedIssuers = ((UnknownVC.valid lrc.core).verifySignature && lrc.authority.contains LegalAuthority.vc_revocation && lrc.isTrustedIssuer trustedIssuers)

structure DeathCertificate : Type

死亡証明VC (Death Certificate)

本人死亡時に自治体が発行するVC。 他のIssuerが参照できる死亡情報。

重要な特性:

• 発行者: 信頼されたIssuer（市役所など）
• 内容: 死亡日、死亡登録番号など
• 用途: 民間Issuerが死亡事実を確認する際に使用

• core : ValidVC

  VCのコア情報

• deceasedID : ValidDID

  死亡者のDID

• status : String

  死亡状態

• deathDate : Timestamp

  死亡日

• deathRegistrationNumber : String

  死亡登録番号

• registrar : String

  登録機関

• revokeAllVCs : Bool

  全VCを失効するか

inductive GuardianAuthority : Type

後見人の権限

成年後見人が行使できる権限のリスト。

• vc_revocation : GuardianAuthority
• did_blacklist_registration : GuardianAuthority
• contract_cancellation : GuardianAuthority
• property_management : GuardianAuthority

instance instReprGuardianAuthority : Repr GuardianAuthority

Equations

• instReprGuardianAuthority = { reprPrec := reprGuardianAuthority✝ }

instance instBEqGuardianAuthority : BEq GuardianAuthority

Equations

• instBEqGuardianAuthority = { beq := beqGuardianAuthority✝ }

structure GuardianCredential : Type

後見人VC (Guardian Credential)

成年後見制度により被後見人となった場合に、 自治体が後見人に対して発行するVC。

重要な特性:

• 発行者: 信頼されたIssuer（市役所、家庭裁判所など）
• 本人確認方法: 後見開始審判書および登記事項証明書による確認
• 権限: VC失効依頼、契約取り消しなど
• 有効期限: 1年ごとの更新を推奨

• core : ValidVC

  VCのコア情報

• guardianID : ValidDID

  後見人のDID

• guardianOf : ValidDID

  被後見人のDID

• guardianType : String

  後見人の種類

• relationship : String

  続柄

• authority : List GuardianAuthority

  権限のリスト

• courtDecisionDate : Timestamp

  審判確定日

• courtCaseNumber : String

  裁判所の事件番号

• registrationNumber : String

  後見登記番号

• guardianshipStartDate : Timestamp

  後見開始日

• verificationMethod : String

  本人確認方法

• expirationDate : Timestamp

  有効期限

def GuardianCredential.isTrustedIssuer (gc : GuardianCredential) (trustedIssuers : List ValidDID) : Bool

後見人VCの発行者が信頼できるか

Trust Anchorの相対性: 「絶対的に信頼できるIssuer」は分散システムには存在しない。 各Holder/Verifier/Issuerが自分のWallet内に「信頼するIssuerのリスト」を管理。

実装: trustedIssuersリストに含まれているかチェック。 このリストはWallet所有者が管理する主観的なTrust Anchor。

Equations

• gc.isTrustedIssuer trustedIssuers = trustedIssuers.contains gc.core.issuerDID

def GuardianCredential.verify (gc : GuardianCredential) (trustedIssuers : List ValidDID) : Bool

後見人VCの検証

検証項目:

1. VC署名の検証（ValidVCは型レベルで保証）
2. authorityに必要な権限が含まれているか
3. 発行者が信頼できるか（Walletのトラストアンカーリストと照合）

Equations

• gc.verify trustedIssuers = ((UnknownVC.valid gc.core).verifySignature && gc.authority.contains GuardianAuthority.vc_revocation && gc.isTrustedIssuer trustedIssuers)

def GuardianCredential.isExpired (gc : GuardianCredential) (currentTime : Timestamp) : Bool

後見人VCが有効期限内かどうか

Equations

• gc.isExpired currentTime = decide (currentTime.unixTime > gc.expirationDate.unixTime)

structure ContractCancellationRequest : Type

契約取り消し要求

被後見人が不適切な契約をした場合、後見人が事後的に取り消す要求。

法的根拠: 民法第9条: 「成年被後見人の法律行為は、取り消すことができる。」

構造:

• guardianVC: 後見人VC
• targetContract: 取り消し対象の契約情報
• cancellationReason: 取り消し理由
• guardianSignature: 後見人の署名

• guardianVC : GuardianCredential

  後見人VC

• targetContractID : String

  取り消し対象の契約情報

• wardDID : ValidDID

  被後見人のDID

• cancellationReason : String

  取り消し理由

• guardianSignature : Signature

  後見人の署名

def getResponseCapability : KeyManagementScenario → ResponseCapability

シナリオの対応可能性を判定

各シナリオで達成できる対応の確実性を返す。

Equations

• getResponseCapability KeyManagementScenario.leakage = ResponseCapability.deterministic
• getResponseCapability KeyManagementScenario.loss_with_abuse_risk = ResponseCapability.limited
• getResponseCapability (KeyManagementScenario.loss_no_abuse IdentityVCAvailability.available) = ResponseCapability.limited
• getResponseCapability (KeyManagementScenario.loss_no_abuse IdentityVCAvailability.unavailable) = ResponseCapability.impossible
• getResponseCapability KeyManagementScenario.planned_update = ResponseCapability.deterministic
• getResponseCapability KeyManagementScenario.death_with_family = ResponseCapability.dependent_on_execution
• getResponseCapability KeyManagementScenario.death_no_family = ResponseCapability.dependent_on_execution
• getResponseCapability KeyManagementScenario.guardianship = ResponseCapability.deterministic

def isDeterministicScenario (scenario : KeyManagementScenario) : Bool

シナリオが決定的に対応可能かどうか

暗号署名により決定的に検証可能なシナリオを判定。

Equations

• isDeterministicScenario scenario = match getResponseCapability scenario with | ResponseCapability.deterministic => true | x => false

theorem valid_request_requires_key (req : UnknownRevocationEvidence) : req.verifySignature = true → req.isDeterministic = true → ∃ (vreq : ValidRevocationEvidence), req = UnknownRevocationEvidence.valid vreq

Theorem: 検証成功し決定的な失効要求は必ずValidRevocationEvidence

証明の核心: 秘密鍵がない状態は、そのDIDがInvalidDIDであることと同義。

• 秘密鍵がない = 検証できないDIDを持っている = 他人のDIDを知っているだけ
• InvalidDIDでは署名を生成できない → InvalidRevocationEvidenceしか作れない
• InvalidRevocationEvidenceはverifySignature = falseかつisDeterministic = false

結論: verifySignature = trueかつisDeterministic = trueである失効要求は、 必ずValidRevocationEvidence（秘密鍵を持っている場合のみ作成可能）。

逆に言えば: 秘密鍵がない場合、決定的な失効は不可能。

theorem loss_without_identity_vc_is_impossible : getResponseCapability (KeyManagementScenario.loss_no_abuse IdentityVCAvailability.unavailable) = ResponseCapability.impossible

Theorem: 身分証明VCなしでの秘密鍵紛失は復旧不可能

前提条件:

• scenario = loss_no_abuse unavailable（身分証明VCなし）

結論:

• getResponseCapability = impossible
• 数学的に安全な復旧方法が存在しない

証明の流れ:

1. 旧秘密鍵がない → 暗号署名による本人性証明は不可能
2. 身分証明VCがない → Issuerは「誰が」oldDIDの所有者だったか分からない
3. したがって、数学的に安全な方法で本人確認できない

theorem bidirectional_signature_proves_key_consent (req : UnknownDIDUpdateEvidence) : req.verifySignatures = true → req.isDeterministic = true

Theorem: 双方向署名によりDID更新への両鍵の同意を検証

前提条件:

• req.verifySignatures = true

結論:

• 両鍵による更新同意の検証成功。同一人物性は発行者の本人確認が必要

theorem death_does_not_establish_key_loss : PrivateKeyState.deceased.getAccessibility = PrivateKeyAccessibility.unknown

Death does not establish destruction of backups or stolen key copies.

theorem guardianship_deterministic_response : getResponseCapability KeyManagementScenario.guardianship = ResponseCapability.deterministic

Theorem: 被後見人のVC失効は決定的に対応可能

前提条件:

• scenario = guardianship
• gc.verify issuerPublicKey = true

結論:

• getResponseCapability = deterministic
• 後見人VCによりVC失効依頼・契約取り消しが決定的に可能

@[reducible, inline]

abbrev RevocationRequest : Type

Legacy *Evidence tagged unions above describe assumed outcomes only. They are not wire parsers, signature validators, or personal identity proofs. All incoming requests must go through these payload-bound checks.

Equations

• RevocationRequest = RequestBinding.KeyRequest

@[reducible, inline]

abbrev DIDUpdateRequest : Type

Equations

• DIDUpdateRequest = RequestBinding.KeyRequest

def verifyRevocationRequest (req : RevocationRequest) (issuer : ValidDID) (now : ℕ) (interactive : Bool) (checks : RequestBinding.KeyChecks) (budget : ResourceBudget) : Bool

Equations

• verifyRevocationRequest req issuer now interactive checks budget = RequestBinding.verifyKeyRequest req RequestBinding.KeyOperation.emergencyRevoke issuer now interactive checks budget

def verifyDIDUpdateRequest (req : DIDUpdateRequest) (issuer : ValidDID) (now : ℕ) (interactive : Bool) (checks : RequestBinding.KeyChecks) (budget : ResourceBudget) : Bool

Equations

• verifyDIDUpdateRequest req issuer now interactive checks budget = RequestBinding.verifyKeyRequest req RequestBinding.KeyOperation.rotate issuer now interactive checks budget

def verifyPersonalReissue (req : RequestBinding.KeyRequest) (issuer : ValidDID) (operation : RequestBinding.KeyOperation) (now : ℕ) (interactive : Bool) (checks : RequestBinding.KeyChecks) (budget : ResourceBudget) (identityRecords : ValidDID → ValidDID → ValidDID → RequestBinding.RevocationScope → Bool) : Bool

Revoke/rotate approval is distinct from approval to reissue personal VCs.

Equations

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

theorem personal_reissue_requires_identity_records (req : RequestBinding.KeyRequest) (issuer : ValidDID) (operation : RequestBinding.KeyOperation) (now : ℕ) (interactive : Bool) (checks : RequestBinding.KeyChecks) (budget : ResourceBudget) (records : ValidDID → ValidDID → ValidDID → RequestBinding.RevocationScope → Bool) (h : verifyPersonalReissue req issuer operation now interactive checks budget records = true) : RequestBinding.authorizePersonalReissue req.payload records = true

theorem recovered_resident_credential_preserves_ahi (old new : ResidentSeedCredential) (category : AuditSectionID) (continuity : SameSeedLineage old new) : residentAHI new category = residentAHI old category

紛失復旧・転居・通常再発行は既存の本人確認/発行記録照合フローを利用。 署名済み住民票VCに同じseedと履歴を引き継ぐ。端末紛失だけでseedを更新しない。 発行者はseed/履歴を復元できる記録を保管し、初回登録の偽装は住民管理で扱う。