任意のAHI監査プロファイル

暗号学的匿名性を衝突困難性や数値比較だけから証明しない。 自治体は本人とseedの対応を保持して照合できる。令状、アクセス権限、 アナログ初回登録の正当性は制度・運用前提であり、暗号学的保証ではない。

structure ResidentSeedCredential : Type

住民票VC内の秘密属性。変更履歴は古い順で、署名対象に含める。 seed/履歴はサービス公開入力、公開VC ID、状態URLに含めない。

• subject : ValidDID
• nationalID : NationalID
• seed : AHISeed
• previousSeeds : List AHISeed
• issuer : ValidDID
• credentialRef : String
• revocationRef : String
• signature : Signature

def SameSeedLineage (old new : ResidentSeedCredential) : Prop

通常の転居・再発行・紛失復旧で保存すべき属性。本人確認と旧発行記録の 照合は既存のDIDMigrationCredentialフローで実施する。

Equations

• SameSeedLineage old new = (new.nationalID = old.nationalID ∧ new.seed = old.seed ∧ new.previousSeeds = old.previousSeeds)

def SeedRotation (old new : ResidentSeedCredential) : Prop

例外更新では旧seedを履歴へ追加し、履歴の省略や分岐を認めない。 発行者署名・旧資格の処理・競合排除は別途発行手続きで検証する。

Equations

• SeedRotation old new = (new.nationalID = old.nationalID ∧ new.seed ≠ old.seed ∧ new.previousSeeds = old.previousSeeds ++ [old.seed])

noncomputable def residentAHI (vc : ResidentSeedCredential) (category : AuditSectionID) : AnonymousHashIdentifier

Equations

• residentAHI vc category = AnonymousHashIdentifier.fromComponents category vc.nationalID vc.seed

theorem routine_reissue_preserves_ahi (old new : ResidentSeedCredential) (category : AuditSectionID) (h : SameSeedLineage old new) : residentAHI new category = residentAHI old category

noncomputable def predecessorAHIs (vc : ResidentSeedCredential) (category : AuditSectionID) : List AnonymousHashIdentifier

移行時のカテゴリ内履歴。全履歴に対応させ、2回以上の更新も省略しない。 他カテゴリのIDや共通移行ID、seed自体は公開しない。

Equations

• predecessorAHIs vc category = List.map (AnonymousHashIdentifier.fromComponents category vc.nationalID) vc.previousSeeds

theorem rotation_preserves_predecessors (old new : ResidentSeedCredential) (category : AuditSectionID) (h : SeedRotation old new) : predecessorAHIs new category = predecessorAHIs old category ++ [residentAHI old category]

theorem different_audit_different_input (a b : AuditSectionID) (n : NationalID) (s : AHISeed) (h : a ≠ b) : (a, n, s) ≠ (b, n, s)

異なるカテゴリは異なる構造化入力。出力の非衝突や関連付け不能性ではない。

structure AHIPublicInputs : Type

• ahi : AnonymousHashIdentifier
• category : AuditSectionID
• context : PresentationContext
• predecessors : List AnonymousHashIdentifier

instance instDecidableEqAHIPublicInputs : DecidableEq AHIPublicInputs

Equations

• instDecidableEqAHIPublicInputs = decEqAHIPublicInputs✝

structure CategoryAuthorization : Type

Category authority is a signed VC checked through wallet-selected anchors. Shared categories are allowed; verifier identity is not added to the AHI hash.

• authority : ValidDID
• verifier : ValidDID
• category : AuditSectionID
• purpose : String
• credentialRef : String
• expiresAt : ℕ
• signature : Signature

def walletAuthorizesCategory (auth : CategoryAuthorization) (context : PresentationContext) (category : AuditSectionID) (now : ℕ) (verifyAuthority : CategoryAuthorization → Bool) (authenticateVerifier : PresentationContext → Bool) (consent : Bool) : Bool

Checks the signed authority chain, scope and status under wallet policy. Consent is separate and cannot substitute for authority. No online registry is required.

Equations

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

noncomputable def prepareAHIForPresentation (vc : ResidentSeedCredential) (auth : CategoryAuthorization) (context : PresentationContext) (category : AuditSectionID) (now : ℕ) (verifyAuthority : CategoryAuthorization → Bool) (authenticateVerifier : PresentationContext → Bool) (consent : Bool) : Option AHIPublicInputs

Wallet release boundary: neither current nor predecessor AHIs are returned until verifier/category authority and consent are established.

Equations

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

theorem unauthorized_category_not_released (vc : ResidentSeedCredential) (auth : CategoryAuthorization) (context : PresentationContext) (category : AuditSectionID) (now : ℕ) (verifyAuthority : CategoryAuthorization → Bool) (authenticateVerifier : PresentationContext → Bool) (consent : Bool) (h : walletAuthorizesCategory auth context category now verifyAuthority authenticateVerifier consent = false) : prepareAHIForPresentation vc auth context category now verifyAuthority authenticateVerifier consent = none

def AHIProofRelation (vc : ResidentSeedCredential) (pub : AHIPublicInputs) (presentation : BoundPresentation) (checks : PresentationChecks) (verifyResident : ResidentSeedCredential → BoundPresentation → Bool) (now : ℕ) : Prop

回路が証明すべき関係。ResidentSeedCredential署名は全秘密属性と履歴を保護。 presentation内に住民票VCの同じ元署名/参照が存在することも検証器が確認する。 この述語の証明を受け取る型モデルであり、暗号回路の実装ではない。

Equations

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

structure VerifiedAHIProof : Type

暗号検証器は、公開入力と同じ証明についてこの関係を確立する必要がある。 verify callbackの健全性は抽象化された実装契約。

• publicInputs : AHIPublicInputs
• resident : ResidentSeedCredential
• presentation : BoundPresentation
• checks : PresentationChecks
• verifyResident : ResidentSeedCredential → BoundPresentation → Bool
• now : ℕ
• valid : AHIProofRelation self.resident self.publicInputs self.presentation self.checks self.verifyResident self.now

def verifyServiceRequest (proof : VerifiedAHIProof) (expectedCategory : AuditSectionID) (expectedContext : PresentationContext) : Option AnonymousHashIdentifier

AMT-01: 外側AHIを引数に取らず、検証済み公開入力だけを返す。 検証済み型の構築は実装では検証器に限定する。

Equations

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

theorem service_request_uses_verified_ahi (proof : VerifiedAHIProof) (category : AuditSectionID) (context : PresentationContext) (ahi : AnonymousHashIdentifier) (h : verifyServiceRequest proof category context = some ahi) : ahi = proof.publicInputs.ahi

def registerAHI (registered : List AnonymousHashIdentifier) (ahi : AnonymousHashIdentifier) : Option (List AnonymousHashIdentifier)

登録/給付/BANはサービス側。検証済みカテゴリとAHIをキーに原子的に処理する。 並行要求の直列化はDBトランザクションの実装義務である。

Equations

• registerAHI registered ahi = if ahi ∈ registered then none else some (ahi :: registered)

theorem repeated_registration_rejected (registered : List AnonymousHashIdentifier) (ahi : AnonymousHashIdentifier) : registerAHI (ahi :: registered) ahi = none

structure NationalIDSystem : Type

同じ住民の登録隠蔽は自治体の発行記録と住民管理で扱う。 この型は国民番号制度に依存しない通常のVC/ZKPには不要。

• generate : Unit → NationalID
• validate : NationalID → Bool

theorem wrong_audit_category_rejected (proof : VerifiedAHIProof) (category : AuditSectionID) (context : PresentationContext) (h : proof.publicInputs.category ≠ category) : verifyServiceRequest proof category context = none

theorem incomplete_rotation_history_rejected (old new : ResidentSeedCredential) (h : new.previousSeeds ≠ old.previousSeeds ++ [old.seed]) : ¬SeedRotation old new