提示の主体・用途束縛とクレーム再包装

署名検証、鍵知識証明、委任検証の実暗号処理は引数の検証器に委ねる。 以下の定理はそれらの結果とフィールド照合の合成についての定理である。 主体や元資格参照は秘密witness。恒久的な共通公開IDを追加しない。

structure PresentationContext : Type

• verifier : ValidDID
• requestedPredicate : String
• challenge : List UInt8
• purpose : String

instance instReprPresentationContext : Repr PresentationContext

Equations

• instReprPresentationContext = { reprPrec := reprPresentationContext✝ }

instance instDecidableEqPresentationContext : DecidableEq PresentationContext

Equations

• instDecidableEqPresentationContext = decEqPresentationContext✝

structure ClaimConditions : Type

元発行者が署名する条件。外側のVCを自己署名しても変更できない。

• content : String
• subject : ValidDID
• issuer : ValidDID
• credentialRef : String
• expiresAt : Option ℕ
• revocationEnabled : Bool
• revocationRef : Option String
• delegationRefs : List String

instance instDecidableEqClaimConditions : DecidableEq ClaimConditions

Equations

• instDecidableEqClaimConditions = decEqClaimConditions✝

structure ClaimEnvelope : Type

自己署名による包装と、元発行者の署名対象を分離する。

• conditions : ClaimConditions
• originSignature : Signature
• packagingIssuer : ValidDID

def ClaimEnvelope.repackage (claim : ClaimEnvelope) (holder : ValidDID) : ClaimEnvelope

Equations

• claim.repackage holder = { conditions := claim.conditions, originSignature := claim.originSignature, packagingIssuer := holder }

theorem repackaging_preserves_origin (claim : ClaimEnvelope) (holder : ValidDID) : (claim.repackage holder).conditions = claim.conditions ∧ (claim.repackage holder).originSignature = claim.originSignature

inductive PresentationRole : Type

• sameSubjectReissue : PresentationRole
• delegatedPresentation : PresentationRole

instance instDecidableEqPresentationRole : DecidableEq PresentationRole

Equations

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

structure SubjectAuthorization : Type

発行者または権限を認められた主体が署名する移転/代理承認。 本人確認の保証水準は発行プロファイルで定義する。二重署名とは別の証拠。

• authority : ValidDID
• subject : ValidDID
• presenter : ValidDID
• credentialRefs : List String
• purpose : String
• expiresAt : ℕ
• revocationRef : String
• role : PresentationRole

instance instDecidableEqSubjectAuthorization : DecidableEq SubjectAuthorization

Equations

• instDecidableEqSubjectAuthorization = decEqSubjectAuthorization✝

structure BoundPresentation : Type

証明の秘密witnessを含む論理モデル。送信メッセージの型ではない。

• context : PresentationContext
• presenter : ValidDID
• subject : ValidDID
• claims : List ClaimEnvelope
• ahiSubject : Option ValidDID
• authorization : Option SubjectAuthorization

structure PresentationChecks : Type

実装で満たすべき検証器契約。結果は利用者が自己申告するフラグではない。 verifyClaimは元署名・信頼先・期限・委任範囲および要求属性条件を検証する。 失効の確認状態/鮮度は別途返し、業務受理と分離する。

• verifyClaim : ClaimEnvelope → PresentationContext → Bool
• verifyAuthorization : SubjectAuthorization → Bool
• verifyKeyKnowledge : ValidDID → PresentationContext → Bool
• verifySubjectLink : ValidDID → ValidDID → PresentationContext → Bool

  異なる署名済みsubjectを同一人物に結ぶ発行者承認を、この提示内で検証。 単なるDID文字列の違いや二重署名を同一人物証拠にしない。

def claimConditionsValidAt (c : ClaimConditions) (now : ℕ) : Bool

元条件の形式・期限チェック。失効の鮮度は別の観測結果で扱う。

Equations

• claimConditionsValidAt c now = ((match c.expiresAt with | none => true | some t => decide (now ≤ t)) && (!c.revocationEnabled || c.revocationRef.isSome))

def authorizationMatches (p : BoundPresentation) (a : SubjectAuthorization) (role : PresentationRole) (now : ℕ) : Bool

Equations

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

def verifySubjectAuthorization (p : BoundPresentation) (checks : PresentationChecks) (role : PresentationRole) (now : ℕ) : Bool

Equations

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

def subjectBound (subject : ValidDID) (p : BoundPresentation) (checks : PresentationChecks) : Bool

Equations

• subjectBound subject p checks = (decide (subject = p.subject) || checks.verifySubjectLink subject p.subject p.context)

def verifyBoundPresentation (p : BoundPresentation) (expected : PresentationContext) (checks : PresentationChecks) (role : PresentationRole) (now : ℕ) : Bool

Equations

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

theorem presentation_context_bound (p : BoundPresentation) (expected : PresentationContext) (checks : PresentationChecks) (role : PresentationRole) (now : ℕ) (h : verifyBoundPresentation p expected checks role now = true) : p.context = expected

theorem unapproved_other_presenter_rejected (p : BoundPresentation) (checks : PresentationChecks) (now : ℕ) (h : p.authorization = none) (hne : p.subject ≠ p.presenter) : verifySubjectAuthorization p checks PresentationRole.sameSubjectReissue now = false

theorem delegation_not_personal_reissue (p : BoundPresentation) (a : SubjectAuthorization) (checks : PresentationChecks) (now : ℕ) (ha : p.authorization = some a) (hr : a.role = PresentationRole.delegatedPresentation) : verifySubjectAuthorization p checks PresentationRole.sameSubjectReissue now = false

theorem ahi_subject_bound (p : BoundPresentation) (expected : PresentationContext) (checks : PresentationChecks) (role : PresentationRole) (now : ℕ) (s : ValidDID) (hs : p.ahiSubject = some s) (h : verifyBoundPresentation p expected checks role now = true) : s = p.subject ∨ checks.verifySubjectLink s p.subject p.context = true

theorem attributes_share_subject (p : BoundPresentation) (expected : PresentationContext) (checks : PresentationChecks) (role : PresentationRole) (now : ℕ) (claim : ClaimEnvelope) (member : claim ∈ p.claims) (h : verifyBoundPresentation p expected checks role now = true) : claim.conditions.subject = p.subject ∨ checks.verifySubjectLink claim.conditions.subject p.subject p.context = true