inductive PrivateKeyAccessibility : Type

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

状態:

• available: 秘密鍵が手元にある（署名操作が可能）
• unavailable: 秘密鍵が手元にない（紛失、破損など）
• permanently_lost: 秘密鍵への物理的アクセスが永久に失われた（本人死亡）

• available : PrivateKeyAccessibility
• unavailable : 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.permanently_lost
• 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 ValidRevocationRequest : Type

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

署名検証が成功する失効要求。 旧秘密鍵による署名により、正当な所有者であることを決定的に証明。

構造:

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

暗号学的保証: signatureByOldKey = Sign(oldDID || newDID || timestamp, oldPrivateKey) → 第三者は旧秘密鍵を持たないため、この署名を偽造できない

不変条件:

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

• oldDID : ValidDID

  失効対象のDID

• newDID : Option ValidDID

  新しいDID（オプション）

• timestamp : Timestamp

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

• revocationReason : String

  失効理由

• signatureByOldKey : Signature

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

instance instReprValidRevocationRequest : Repr ValidRevocationRequest

Equations

• instReprValidRevocationRequest = { reprPrec := reprValidRevocationRequest✝ }

structure InvalidRevocationRequest : Type

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

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

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

• oldDID : ValidDID

  失効対象のDID

• newDID : Option ValidDID

  新しいDID（オプション）

• timestamp : Timestamp

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

• revocationReason : String

  失効理由

• signatureByOldKey : Signature

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

• reason : String

  不正な理由

instance instReprInvalidRevocationRequest : Repr InvalidRevocationRequest

Equations

• instReprInvalidRevocationRequest = { reprPrec := reprInvalidRevocationRequest✝ }

inductive UnknownRevocationRequest : Type

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

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

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

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

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

• valid : ValidRevocationRequest → UnknownRevocationRequest
• invalid : InvalidRevocationRequest → UnknownRevocationRequest

instance instReprUnknownRevocationRequest : Repr UnknownRevocationRequest

Equations

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

def UnknownRevocationRequest.verifySignature : UnknownRevocationRequest → Bool

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

設計の核心:

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

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

Equations

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

def UnknownRevocationRequest.isValid (req : UnknownRevocationRequest) : Prop

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

Equations

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

def UnknownRevocationRequest.isDeterministic : UnknownRevocationRequest → Bool

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

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

Equations

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

theorem UnknownRevocationRequest.valid_revocation_request_passes (vreq : ValidRevocationRequest) : (valid vreq).isValid

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

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

theorem UnknownRevocationRequest.invalid_revocation_request_fails (ireq : InvalidRevocationRequest) : ¬(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 ValidDIDUpdateRequest : Type

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

双方向署名検証が成功するDID更新要求。 oldDIDとnewDIDの所有者が同一人物であることを決定的に証明。

構造:

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

暗号学的保証: signatureByOldKey = Sign(oldDID || newDID || timestamp, oldPrivateKey) signatureByNewKey = Sign(newDID || oldDID || timestamp, newPrivateKey) → 両方の署名により、同一人物であることを決定的に証明

不変条件:

• 双方向署名検証が成功済み（同一人物性が証明済み）

• oldDID : ValidDID

  更新前のDID

• newDID : ValidDID

  更新後のDID

• timestamp : Timestamp

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

• updateReason : String

  更新理由

• transitionPeriod : ℕ

  移行期間（日数）

• signatureByOldKey : Signature

  旧秘密鍵による署名

• signatureByNewKey : Signature

  新秘密鍵による署名

instance instReprValidDIDUpdateRequest : Repr ValidDIDUpdateRequest

Equations

• instReprValidDIDUpdateRequest = { reprPrec := reprValidDIDUpdateRequest✝ }

structure InvalidDIDUpdateRequest : 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 instReprInvalidDIDUpdateRequest : Repr InvalidDIDUpdateRequest

Equations

• instReprInvalidDIDUpdateRequest = { reprPrec := reprInvalidDIDUpdateRequest✝ }

inductive UnknownDIDUpdateRequest : Type

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

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

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

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

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

• valid : ValidDIDUpdateRequest → UnknownDIDUpdateRequest
• invalid : InvalidDIDUpdateRequest → UnknownDIDUpdateRequest

instance instReprUnknownDIDUpdateRequest : Repr UnknownDIDUpdateRequest

Equations

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

def UnknownDIDUpdateRequest.verifySignatures : UnknownDIDUpdateRequest → Bool

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

設計の核心:

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

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

Equations

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

def UnknownDIDUpdateRequest.isValid (req : UnknownDIDUpdateRequest) : Prop

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

Equations

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

def UnknownDIDUpdateRequest.isDeterministic : UnknownDIDUpdateRequest → Bool

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

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

Equations

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

theorem UnknownDIDUpdateRequest.valid_did_update_request_passes (vreq : ValidDIDUpdateRequest) : (valid vreq).isValid

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

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

theorem UnknownDIDUpdateRequest.invalid_did_update_request_fails (ireq : InvalidDIDUpdateRequest) : ¬(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 deterministic_revocation_requires_key_access (state : PrivateKeyState) : state.getAccessibility = PrivateKeyAccessibility.available → ∃ (req : UnknownRevocationRequest), req.isDeterministic = true

Theorem: 秘密鍵が手元にある場合のみ決定的な失効が可能

前提条件:

• state.getAccessibility = available

結論:

• 失効要求に旧秘密鍵による署名を付けることができる
• Issuerは署名検証により、正当な所有者による要求であることを決定的に判定可能

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

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

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

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

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

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

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_identity (req : UnknownDIDUpdateRequest) : req.verifySignatures = true → req.isDeterministic = true

Theorem: 双方向署名によりDID更新の同一人物性を決定的に証明

前提条件:

• req.verifySignatures = true

結論:

• oldDIDとnewDIDの所有者が同一人物であることが決定的に証明される

theorem deceased_minimal_damage (state : PrivateKeyState) : state = PrivateKeyState.deceased → state.getAccessibility = PrivateKeyAccessibility.permanently_lost

Theorem: 本人死亡時のVC失効が不完全でも損害は極めて限定的

前提条件:

• state = deceased（本人死亡）
• state.getAccessibility = permanently_lost

結論:

• 秘密鍵が永久に使用不可能 → ZKP生成不可能
• VC失効が不完全でも、悪用リスクは実質的にゼロ

損害評価:

• Issuer側: 直接的損害なし
• Verifier側: 限定的（身分証明VCは自治体が失効）
• 社会全体: 極めて軽微

theorem guardianship_deterministic_response : getResponseCapability KeyManagementScenario.guardianship = ResponseCapability.deterministic

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

前提条件:

• scenario = guardianship
• gc.verify issuerPublicKey = true

結論:

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

def key_management_security_guarantees : String

鍵管理フローのセキュリティ保証

形式検証の効果:

• 秘密鍵が手元にある場合のみ決定的な失効が可能（deterministic_revocation_requires_key_access）
• 検証成功し決定的な失効要求は必ずValidRevocationRequest（valid_request_requires_key）
  • 逆に言えば: 秘密鍵がない = InvalidDIDを持っている = 決定的な失効は不可能
• 身分証明VCなしでの紛失は復旧不可能（loss_without_identity_vc_is_impossible）
• 双方向署名によりDID更新の同一人物性を証明（bidirectional_signature_proves_identity）
• 本人死亡時のVC失効が不完全でも損害は極めて限定的（deceased_minimal_damage）
• 被後見人のVC失効は決定的に対応可能（guardianship_deterministic_response）

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

• 決定性の原則: 秘密鍵が手元にある場合のみ、暗号学的に決定的な操作が可能
• InvalidDIDの本質: 秘密鍵がない = 検証できないDIDを持っている = 他人のDIDを知っているだけ
• 連絡可能性の限界: Issuerに連絡できない場合は対応不可能
• 数学的安全性の限界: 身分証明と紐づいていないDIDの紛失は復旧不可能
• 本人死亡時の特性: 秘密鍵が使用不可能なため、損害は極めて限定的
• 被後見人保護: 後見人VCにより法的保護と技術的管理を両立

型安全性によるプロトコル保証:

• 各シナリオの対応可能性が型で表現される
• 署名検証により正当性が保証される
• ValidDID/InvalidDIDの型区別により秘密鍵の有無を表現
• プロトコルの安全性が形式的に保証される

Equations

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