AMATELUS.MutualAuthentication

noncomputable def holderRespond (msg : VerifierInitialMessage) (holderWallet : Wallet) (holderIdentity : Identity) (humanApproval : Bool) (_h_has_identity : holderIdentity ∈ holderWallet.identities) :

Option HolderResponse

Holderの応答生成（人間の判断を外部入力として受け取る）

この関数は以下の決定的なステップで構成される：

Verifierメッセージの基本検証（決定的）
人間の判断を外部入力として受け取る（パラメータ）
両方がtrueならZKPと要求された属性データを生成

人間の判断（humanApproval）:

Wallet UIがクレーム情報と要求された属性スキーマを表示
Holderが「許可」または「拒否」ボタンを押す
その結果がBoolとして渡される

属性データの提供:

Verifierが requestedAttributes でスキーマを指定（必須）
Holderは自分のVCから該当する属性を抽出
スキーマ検証を行い、検証成功ならValidJSONValueを応答に含める
検証失敗または属性を提供できない場合、応答全体を返さない（none）
現在の実装では簡略化のためダミーデータを返す（TODO: 実装）

Equations

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

Instances For

source

theorem untrusted_issuer_rejected (msg : VerifierInitialMessage) (holderWallet : Wallet) :

(∃ (claim : VerifierClaim ), claim ∈ msg.presentedClaims ∧ match claim.issuerDID with | UnknownDID.valid validDID => (holderWallet.trustedAnchors.lookup validDID).isNone = true | UnknownDID.invalid a => True) → validateVerifierMessage msg holderWallet = false

Theorem: 信頼できない発行者のクレームを含むメッセージは拒否される

証明：validateVerifierMessage関数の定義により自明

source

theorem human_rejection_stops_protocol (msg : VerifierInitialMessage) (holderWallet : Wallet) (holderIdentity : Identity) (h_has_identity : holderIdentity ∈ holderWallet.identities) :

validateVerifierMessage msg holderWallet = true → holderRespond msg holderWallet holderIdentity false h_has_identity = none

Theorem: 人間が拒否した場合、応答は生成されない

証明：holderRespond関数の定義により自明

source

theorem trusted_and_approved_generates_response (msg : VerifierInitialMessage) (holderWallet : Wallet) (holderIdentity : Identity) (h_has_identity : holderIdentity ∈ holderWallet.identities) :

validateVerifierMessage msg holderWallet = true → (holderRespond msg holderWallet holderIdentity true h_has_identity).isSome = true

Theorem: 信頼できる発行者のみで、人間が許可した場合、応答が生成される

証明：holderRespond関数の定義により自明

source

theorem generated_zkp_is_valid (msg : VerifierInitialMessage) (holderWallet : Wallet) (holderIdentity : Identity) (h_has_identity : holderIdentity ∈ holderWallet.identities) (response : HolderResponse) :

holderRespond msg holderWallet holderIdentity true h_has_identity = some response → ∃ (relation : Relation ), response.holderZKP.isValid relation

Theorem: 生成されたZKPは有効である

証明：amtZKP.completenessにより、amtZKP.proverが生成したProofは検証に成功することが保証される

source

structure MutualAuthSession :

Type

相互認証セッション（簡略版）

Phase 1: Verifierがメッセージを送信 Phase 2: Holderが検証して応答（または拒否）

verifierMessage : VerifierInitialMessage
holderResponse : Option HolderResponse

Instances For

source

noncomputable def executeMutualAuth (verifierMessage : VerifierInitialMessage) (holderWallet : Wallet) (holderIdentity : Identity) (humanApproval : Bool) (h_has_identity : holderIdentity ∈ holderWallet.identities) :

MutualAuthSession

セッション実行関数

Equations

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

Instances For

source

def mutualAuthenticationRequirements :

String

実装要件: 相互認証プロトコル

Phase 1: Verifierの初期メッセージ

例1: 年齢制限サービス（酒類販売）

Verifier → Holder (DIDComm):
{
  presentedClaims: [
    {
      claimData: { data: "酒類販売許可", claimID: Some "liquor_license" },
      issuerDID: "did:amt:liquor_authority"
    }
  ],
  verifierDID: "did:amt:liquor_shop_xyz",
  requestedAttributes: {  // 必須：年齢証明
    type: ["object"],
    properties: {
      ageOver20: { type: ["boolean"], const: true },
      purchaseToken: { type: ["string"] }  // 購入トークン（名寄せ回避）
    },
    required: ["ageOver20", "purchaseToken"]
  },
  timestamp: now()
}

例2: Webサービスログイン（DIDComm認証）

**初回登録フロー:**
Holder → Service (DIDComm):
{
  presentedClaims: [
    {
      claimData: { data: "年齢確認", claimID: Some "age_verification" },
      issuerDID: "did:amt:trusted_authority"
    }
  ],
  verifierDID: "did:amt:service",
  requestedAttributes: {
    type: ["object"],
    properties: {
      ageOver18: { type: ["boolean"], const: true },
      serviceAccountID: { type: ["string"] }  // Service固有の識別子（名寄せ回避）
    },
    required: ["ageOver18"]
  },
  timestamp: now()
}

Holder → Verifier (DIDComm):
{
  holderZKP: ZKP,  // 属性証明（ageOver18など）
  providedAttributes: {
    ageOver18: true,
    serviceAccountID: "user_service_001"
  },
  timestamp: now()
}

Service検証ポイント:
1. DIDCommで通信認証済み（秘密鍵対応が確定的）
2. ZKPで属性を検証
3. providedAttributesがスキーマに適合か確認
4. (オプション) 本人による不正な再利用を防ぎたい場合、アプリケーション層でnonce管理を実装

**重要**: Nonceの生成・管理はアプリケーション層の責任

Phase 2: Holderの検証プロセス

Wallet UIが以下を表示：
- Verifierが提示したクレーム情報
- 各クレームの発行者（トラストアンカー名）
- Verifierが要求する属性スキーマ（requestedAttributes）例: 「年齢が20歳以上、日本国籍」
- 「このVerifierに以下の情報を提供しますか？」
Holderが判断：
- 自分が要求された属性を提供できるか確認
- 許可ボタン → humanApproval = true
- 拒否ボタン → humanApproval = false
許可された場合のみ応答生成
- Holderは自分のVCから該当する属性を抽出
- スキーマ検証を行い、ValidJSONValueとして構築

Phase 2: Holderの応答

例1: 年齢制限サービスへの応答

Holder → Verifier (DIDComm):
{
  holderZKP: {
    core: {
      proof: π,
      publicInput: <claimsData>,
      proofPurpose: "credential-presentation",
      created: now()
    },
    claimedAttributes: "Age verification for liquor purchase"
  },
  providedAttributes: {  // 必須：スキーマ検証済み
    value: {
      ageOver20: true,
      purchaseToken: "abc123xyz"  // 一時的な購入トークン
    },
    schema: <requestedAttributes>
  },
  timestamp: now()
}

注: Nonce処理が必要な場合、アプリケーション層で実装

例2: Webサービスログインへの応答

Holder → Verifier (DIDComm):
{
  holderZKP: {
    core: {
      proof: π,
      publicInput: <claimsData>,
      proofPurpose: "credential-presentation",
      created: now()
    },
    claimedAttributes: "Account ownership proof for SNS login"
  },
  providedAttributes: {  // 必須：スキーマ検証済み
    value: {
      serviceAccountID: "user_sns_001",  // Service専用ID
      loginSignature: "sig_..."  // チャレンジに対する署名
    },
    schema: <requestedAttributes>
  },
  timestamp: now()
}

Service検証:
1. DIDCommで受信認証済み（秘密鍵対応が確定的）
2. ZKPで属性を検証
3. serviceAccountIDとHolder DIDの紐付けを確認
4. (オプション) アプリケーション層でnonce機構を実装している場合、nonce一意性を確認

重要:

DIDは平文で送信されない（DIDCommで暗号化通信）
serviceAccountIDはService固有の識別子（所有権証明ではない）
loginSignatureでチャレンジ署名により初めてアカウント所有権が証明される

セキュリティ保証:

DIDComm認証: 通信路の認証・暗号化、秘密鍵対応の確定性
なりすまし攻撃防止: DIDCommによる秘密鍵対応確定でなりすまし攻撃を完全防止
チャレンジ署名: Holderの秘密鍵保持を検証、アカウント所有権を証明
トラストアンカー検証: Wallet内の辞書で検証
人間中心: 最終判断はHolderが行う
偽警官対策: 信頼できない発行者のクレームは拒否
リプレイ攻撃対策: アプリケーション層でnonce機構を実装（プロトコル層では規定なし）
スキーマ検証: 要求された属性データはJSONSchemaで検証済み（必須）
選択的開示: HolderはVerifierが要求した属性のみを提供
名寄せ回避: DIDを平文で送信せず、Service固有の識別子を使用
プライバシー保護: 属性を提供できない場合、応答全体を返さない
アカウント所有権証明: serviceAccountID単体ではなく、チャレンジ署名と組み合わせ

Equations

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

Instances For