@[reducible, inline]

abbrev ClaimTypeBasic : Type

クレームタイプを表す型

Equations

• ClaimTypeBasic = String

structure ClaimID : Type

クレーム識別子を表す型

VC発行者が定義するクレームの一意な識別子。 誰でもクレームを定義でき、受け取る側がどの発行者を信頼するかを決定する。 例: "政府_1" (住民票), "政府_2" (運転免許証), "友人_1" (推薦状)

• value : String

instance instReprClaimID : Repr ClaimID

Equations

• instReprClaimID = { reprPrec := reprClaimID✝ }

instance instDecidableEqClaimID : DecidableEq ClaimID

Equations

• instDecidableEqClaimID = decEqClaimID✝

instance instBEqClaimID : BEq ClaimID

Equations

• instBEqClaimID = { beq := beqClaimID✝ }

structure Claims : Type

クレーム（主張）を表す型

設計:

• data: 構造化データ（JSON等）
• claimID: クレームの識別子（発行者が定義）
  • Some claimID: 特定のクレームタイプ（住民票、運転免許証、推薦状等）
  • None: クレームIDが指定されていない（汎用クレーム）

AHI (Anonymous Hash Identifier) について: NationalID（マイナンバー等の個人番号）を含むクレームは、 AHI機能を使用する場合にのみ data フィールドに含まれます。

• AHI機能を使用する場合:

  • IssuerまたはVerifierが監査機能を要求する場合
  • data フィールドにNationalIDが含まれる
  • HolderはAHIを生成して提示する

• AHI機能を使用しない場合:

  • 通常のサービス利用（監査不要）
  • data フィールドにNationalIDは含まれない
  • 通常のVCとZKPのみで運用される

重要: 個人番号制度がない国でも、NationalIDを含まないVCで AMATELUSプロトコルは完全に機能します。

• data : String
• claimID : Option ClaimID

instance instReprClaims : Repr Claims

Equations

• instReprClaims = { reprPrec := reprClaims✝ }

instance instDecidableEqClaims : DecidableEq Claims

Equations

• instDecidableEqClaims = decEqClaims✝

def Claims.getClaimID (claims : Claims) : Option ClaimID

ClaimsからClaimIDを取得する関数（定義として実装）

Equations

• claims.getClaimID = claims.claimID

structure AuditSectionID : Type

監査区分識別子を表す型

• value : List UInt8

instance instReprAuditSectionID : Repr AuditSectionID

Equations

• instReprAuditSectionID = { reprPrec := reprAuditSectionID✝ }

instance instDecidableEqAuditSectionID : DecidableEq AuditSectionID

Equations

• instDecidableEqAuditSectionID = decEqAuditSectionID✝

structure NationalID : Type

国民識別番号（マイナンバー等）を表す型

• value : List UInt8

instance instReprNationalID : Repr NationalID

Equations

• instReprNationalID = { reprPrec := reprNationalID✝ }

instance instDecidableEqNationalID : DecidableEq NationalID

Equations

• instDecidableEqNationalID = decEqNationalID✝

structure AnonymousHashIdentifier : Type

匿名ハッシュ識別子 (Anonymous Hash Identifier)

AHI := H(AuditSectionID || NationalID)

オプショナル機能: AHIはAMATELUSプロトコルのオプショナル機能です。 使用するかどうかは、IssuerまたはVerifierが決定します。

• AHIが使用される場合:

  • 監査が必要なサービス（納税、給付、許認可等）
  • 多重アカウント防止が必要なサービス（SNS、チケット販売等）
  • 個人番号制度が存在する国・地域

• AHIが使用されない場合:

  • 通常のサービス利用（監査不要）
  • 個人番号制度がない国・地域
  • Holderが任意にAHIの提示を拒否することも可能

設計の重要な性質:

• ProtocolState.ahis: List は空リスト [] でも良い
• AHI機能を使用しなくても、AMATELUSは完全に機能する
• NationalIDSystemが存在しない場合、AHIは構築できない

• hash : Hash

instance instReprAnonymousHashIdentifier : Repr AnonymousHashIdentifier

Equations

• instReprAnonymousHashIdentifier = { reprPrec := reprAnonymousHashIdentifier✝ }

instance instDecidableEqAnonymousHashIdentifier : DecidableEq AnonymousHashIdentifier

Equations

• instDecidableEqAnonymousHashIdentifier = decEqAnonymousHashIdentifier✝

noncomputable def AnonymousHashIdentifier.fromComponents (auditSection : AuditSectionID) (nationalID : NationalID) : AnonymousHashIdentifier

AHIを生成する関数（定義として実装）

AHI := H(AuditSectionID || NationalID)

手順:

1. AuditSectionIDとNationalIDのバイト列を連結
2. 連結したバイト列をハッシュ化
3. ハッシュ値を持つAnonymousHashIdentifierを構築

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

• 決定性: 同じ入力からは常に同じAHIが生成される
• 不可逆性: AHIから元のNationalIDを復元することは計算量的に困難
• 一意性: 異なる入力は（高確率で）異なるAHIを生成する

Equations

• AnonymousHashIdentifier.fromComponents auditSection nationalID = { hash := hashForDID (auditSection.value ++ nationalID.value) }

def getIssuerDID (issuer : W3C.Issuer) : Option ValidDID

W3C.IssuerからDIDを取得する関数

W3C.IssuerのID文字列がDID形式（"did:amt:..."）の場合、DIDとして解釈します。

戻り値:

• None: DID形式でない、またはハッシュ情報が不明で検証できない

設計思想: W3C VCから抽出したDIDは、DIDDocumentのハッシュ情報が不明なため、 ValidDIDに変換できません。検証関数を使用するgetIssuerDIDWithValidationを 使用してください。

使用例:

• issuer: W3C.Issuer.uri "did:amt:123..." → None（ハッシュ不明）
• issuer: W3C.Issuer.uri "https://example.com" → None（URLはDIDではない）

Equations

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

def getIssuerDIDWithValidation (issuer : W3C.Issuer) (validateDID : W3C.DID → Option ValidDID) : Option ValidDID

W3C.IssuerからDIDを取得する関数（検証付き）

W3C.IssuerのID文字列をDIDとして解釈し、検証関数で検証します。

パラメータ:

• issuer: W3C.Issuer
• validateDID: DID文字列を検証し、ValidDIDを返す関数（例：Wallet内のDIDリストを参照）

戻り値:

• Some ValidDID: 検証に成功した場合
• None: DID形式でない、または検証に失敗した場合

使用例:

-- WalletからDIDを検証する関数
def validateWithWallet (wallet : Wallet) (didStr : W3C.DID) : Option ValidDID :=
  wallet.identities.find? (fun id => id.did.w3cDID == didStr)
    |>.map (fun id => id.did)

-- Issuerからvalidated DIDを取得
let issuerDID := getIssuerDIDWithValidation issuer (validateWithWallet myWallet)

Equations

• getIssuerDIDWithValidation issuer validateDID = if issuer.getId.startsWith "did:amt:" = true then let w3cDID := { value := issuer.getId }; validateDID w3cDID else none

def didToW3CIssuer (did : UnknownDID) : W3C.Issuer

DIDからW3C.Issuerを生成する関数

AMATELUSのDIDをW3C標準のIssuer型に変換します。

変換方法:

• DID.valid w3cDID → W3C.Issuer.uri (did文字列)
• DID.invalid w3cDID _ → W3C.Issuer.uri (did文字列)

使用例:

• did: DID.valid { value := "did:amt:123..." } → Issuer.uri "did:amt:123..."

Equations

• didToW3CIssuer (UnknownDID.valid v) = W3C.Issuer.uri v.w3cDID.value
• didToW3CIssuer (UnknownDID.invalid i) = W3C.Issuer.uri i.w3cDID.value

def getSubjectDID (subjects : List W3C.CredentialSubject) : Option ValidDID

W3C.CredentialSubjectからDIDを取得する関数

W3C.CredentialSubjectのid文字列がDID形式（"did:amt:..."）の場合、DIDとして解釈します。

戻り値:

• None: DID形式でない、idが存在しない、またはハッシュ情報が不明で検証できない

設計思想: W3C VCから抽出したDIDは、DIDDocumentのハッシュ情報が不明なため、 ValidDIDに変換できません。検証関数を使用するgetSubjectDIDWithValidationを 使用してください。

使用例:

• credentialSubject.id = Some "did:amt:123..." → None（ハッシュ不明）
• credentialSubject.id = Some "https://example.com" → None（URLはDIDではない）
• credentialSubject.id = None → None

Equations

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

def getSubjectDIDWithValidation (subjects : List W3C.CredentialSubject) (validateDID : W3C.DID → Option ValidDID) : Option ValidDID

W3C.CredentialSubjectからDIDを取得する関数（検証付き）

W3C.CredentialSubjectのid文字列をDIDとして解釈し、検証関数で検証します。

パラメータ:

• subjects: W3C.CredentialSubjectのリスト
• validateDID: DID文字列を検証し、ValidDIDを返す関数

戻り値:

• Some ValidDID: 検証に成功した場合
• None: DID形式でない、idが存在しない、または検証に失敗した場合

Equations

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

def didToCredentialSubject (did : UnknownDID) : W3C.CredentialSubject

DIDからW3C.CredentialSubjectを生成する関数

AMATELUSのDIDをW3C標準のCredentialSubject型に変換します。

変換方法:

• did → W3C.CredentialSubject with id = Some (did文字列) and empty claims

使用例:

• did: DID.valid { value := "did:amt:123..." } → CredentialSubject { id := Some "did:amt:123...", claims := [] }

注意: AMATELUSでは、claimsはValidVC.claimsフィールドに保存されます。 W3C.CredentialSubject.claimsはAMATELUSでは使用しません。

Equations

• didToCredentialSubject (UnknownDID.valid v) = { id := some v.w3cDID.value, claims := [] }
• didToCredentialSubject (UnknownDID.invalid i) = { id := some i.w3cDID.value, claims := [] }

structure DeLinkageInfo : Type

名寄せ回避情報 (De-linkage Information)

ZKPで証明される2つのDIDの関連付けに関する情報。

目的: Verifierに以下を証明する際、複数の身分証明用DIDを関連付けることを防ぐ

1. 身分証明用DID（Identity DID）の秘密鍵所有権
2. 通信用DID（Communication DID）の秘密鍵所有権

2つのDID名寄せ回避の原理:

• identityDID: 身分証明用DID（住民票、運転免許証など）
• communicationDID: 通信用DID（このサービスとの通信用）

ZKPは両方の秘密鍵所有権を証明するが、ZKP不学性により：

• ZKP自体からはidentityDIDとcommunicationDIDの対応関係を抽出困難
• 異なるサービスが異なるcommDIDを見ても、背後の共通identityDIDを推測困難

複数サービス間での名寄せ回避:

• サービスA観測: commDID_A（背後のidentityDID不明）
• サービスB観測: commDID_B（背後のidentityDID不明）
• commDID_AとcommDID_Bが同じentityからのものであることを推測困難 → 各通信で異なる通信用DIDを生成 + ZKP不学性

同一サービス内のプライバシー:

• 同じサービスに対しては、同じcommunicationDIDで複数回ログイン
• サービスはこのcommDIDの複数のアクセスを観測可能
• しかし、背後のidentityDIDが何であるかは不明（de-linkage infoでも推測不可）

クレーム提示の性質:

• VCで提示するクレーム（年齢>=20など）について
• ZKPでそのクレームの所有者がidentityDIDの所有者であることを証明
• 同時にcommunicationDIDも所有していることを証明
• 複数のクレームが同じidentityDIDに紐付いている場合、 Verifierはそれらが同一サービス内でのアクセスと判断可能 しかし 異なるサービス間での関連付けはZKP不学性により困難

• identityDID : ValidDID
• communicationDID : ValidDID

instance instReprDeLinkageInfo : Repr DeLinkageInfo

Equations

• instReprDeLinkageInfo = { reprPrec := reprDeLinkageInfo✝ }

instance instDecidableEqDeLinkageInfo : DecidableEq DeLinkageInfo

Equations

• instDecidableEqDeLinkageInfo = decEqDeLinkageInfo✝

structure ValidVC : Type

正規の検証可能資格情報 (Valid Verifiable Credential)

署名検証が成功するVC。 暗号学的に正しく発行されたVCは、署名検証に成功する。

一般的な属性情報（年齢、住所、資格など）を証明するVC。 汎用的なクレームタイプで、様々な発行者が発行できる。

設計の簡素化:

• すべての属性情報（検証者資格含む）を単一の型で表現
• w3cCredential.credentialSubject.claimsに委任チェーンを埋め込むことで、受託者認証として機能
• 各Walletの所有者が、どのDIDを信頼するか（Wallet.trustedAnchorsに登録）を自由に決定

階層制限（N階層対応）:

• 直接発行: claims配列に委任チェーンなし（0階層）
• N階層委譲発行: claims配列にDelegationChainを含む（N階層）
  • DelegationChainにより複数階層の委任を表現
  • 各delegationのmaxDepthにより階層制限を動的に設定
  • 循環委任をDID重複チェックで防止
  • 詳細はTrustChain.mdとTrustChainTypes.leanを参照

使用例: 自治体Aが政府から委譲された権限で住民票VCを発行する場合、 w3cCredential.credentialSubject.claimsには委任チェーン（DelegationChain）が含まれる。 詳細はTrustChainTypes.leanのDelegationChain型を参照。

名寄せ回避の設計: ZKPで証明する際、以下の2つのDIDが関連付けられる：

1. 身分証明用DID（Identity DID）: VCで提示するクレームに紐付いている
2. 通信用DID（Communication DID）: このサービスとの通信用DID

deLinkageInfoフィールドにより、ZKP検証時にこの情報を参照でき、 複数のクレームが関連していることを検証できつつ、 サービス間での名寄せは困難になる。

設計思想:

• VCの発行はIssuerの責任（署名は暗号ライブラリで生成）
• プロトコルレベルでは「正規に発行されたVC」として抽象化
• Verifierは署名検証のみに依存し、Issuer実装を信頼しない

抽象化の利点:

• Ed25519署名検証などの暗号的詳細を隠蔽
• プロトコルの安全性証明が簡潔になる
• Issuer実装の違いを抽象化（同じプロトコルで多様なIssuer実装が可能）

フィールド構成:

• w3cCredential: W3C標準Credential構造
• issuerDID: 発行者DID（型レベルで正規のDIDを保証）
• subjectDID: 主体DID（型レベルで正規のDIDを保証）
• signature: デジタル署名（型レベルで保証）
• claims: 属性固有のクレーム（任意の構造化クレーム）
• deLinkageInfo: 名寄せ回避情報（オプショナル）

権限証明の埋め込み方法: 委譲された権限で発行するVCでは、W3C.Credential.credentialSubject.claimsに以下を含める：

1. 主体の属性情報（本来のクレームデータ）
2. DelegationChain（N階層の委任チェーン）

これにより、VCが自己完結し、別VCの提示が不要になる。

• w3cCredential : W3C.Credential
• issuerDID : ValidDID
• subjectDID : ValidDID
• signature : Signature
• claims : Claims
• deLinkageInfo : Option DeLinkageInfo

instance instReprValidVC : Repr ValidVC

Equations

• instReprValidVC = { reprPrec := reprValidVC✝ }

def ValidVC.getDelegationChain (_vc : ValidVC) : Option DelegationChain

ValidVCから委任チェーンを取得

w3cCredential.credentialSubject.claimsから委任チェーン（DelegationChain）を抽出する。

戻り値:

• Some chain: 委任チェーンが見つかった場合（N階層委譲発行）
• None: 委任チェーンがない場合（直接発行）

使用例:

match getDelegationChain vc with
| none => -- 直接発行VC
| some chain =>
    -- N階層委譲発行VC
    -- chain.depthで階層数を取得
    -- chain.verifyで委任チェーンを検証

Equations

• _vc.getDelegationChain = none

structure InvalidVC : Type

不正な検証可能資格情報 (Invalid Verifiable Credential)

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

• 署名が改ざんされている
• 発行者の秘密鍵が不正
• VCの内容が改ざんされている
• 署名検証に失敗する

Issuerバグの影響:

• バグのあるIssuerが生成したVCはInvalidVCとして表現される
• プロトコルの安全性には影響しない（当該VCのみが無効になる）

• w3cCredential : W3C.Credential
• reason : String

inductive UnknownVC : Type

未検証の資格情報 (Unknown Verifiable Credential)

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

• valid: 正規に発行されたVC（署名検証が成功）
• invalid: 不正なVC（署名検証が失敗）

命名の意図:

• 「UnknownVC」= 構造的にパース成功したが、署名検証の状態は未確定または既知
• 「VerifiableCredential」から改名し、W3C標準との対応を明確化
• W3C.Credential（proof前）とは異なり、署名検証の結果を含む

設計の利点:

• VC検証の暗号的詳細（Ed25519署名検証など）を抽象化
• プロトコルレベルでは「正規/不正」の区別のみが重要
• Issuer実装のバグはinvalidとして表現され、プロトコルの安全性には影響しない

ZKPとの設計の一貫性:

• ZeroKnowledgeProofと同じパターン（Valid/Invalid + 和型）
• 統一された形式検証アプローチ

• valid : ValidVC → UnknownVC
• invalid : InvalidVC → UnknownVC

def UnknownVC.getIssuer (vc : UnknownVC) : UnknownDID

VCの発行者をDIDとして取得

def UnknownVC.getSubject (vc : UnknownVC) : UnknownDID

VCの主体をDIDとして取得

Equations

• One or more equations did not get rendered due to their size.
• (UnknownVC.valid vvc).getSubject = UnknownDID.valid vvc.subjectDID

def UnknownVC.getDelegationChain (vc : UnknownVC) : Option DelegationChain

VCから委任チェーンを取得

w3cCredential.credentialSubject.claimsから委任チェーン（DelegationChain）を抽出する。

戻り値:

• Some chain: 委任チェーンが見つかった場合（N階層委譲発行）
• None: 委任チェーンがない場合（直接発行）、またはInvalidVC

Equations

• (UnknownVC.valid vvc).getDelegationChain = vvc.getDelegationChain
• (UnknownVC.invalid ivc).getDelegationChain = none

def UnknownVC.verifySignature : UnknownVC → Bool

VC検証関数（定義として実装）

設計の核心:

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

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

Issuerバグの影響:

• バグのあるIssuerが生成したVCはinvalidとして表現される
• verifySignature (invalid _) = falseにより、検証は失敗する
• したがって、Issuerバグは当該VCのみに影響

Equations

• (UnknownVC.valid vvc).verifySignature = true
• (UnknownVC.invalid ivc).verifySignature = false

def UnknownVC.isValid (vc : UnknownVC) : Prop

VCが有効かどうかを表す述語

Equations

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

theorem UnknownVC.valid_vc_passes (vvc : ValidVC) : (valid vvc).isValid

Theorem: 正規のVCは常に検証成功

暗号学的に正しく発行されたVCは、署名検証が成功する。 これは定義から自明だが、明示的に定理として示す。

theorem UnknownVC.invalid_vc_fails (ivc : InvalidVC) : ¬(invalid ivc).isValid

Theorem: 不正なVCは常に検証失敗

暗号学的に不正なVCは、署名検証が失敗する。 これにより、Issuerバグや改ざんされたVCが受け入れられないことを保証。