inductive Channel : Type

通信チャネルの種類

設計思想: AMATELUSでは統一されたDIDCommプロトコルを使用します。

DIDComm: DIDベースの相互認証通信プロトコル（did:amt仕様に準拠）

• 送信: ValidDID + Optional(ValidDIDDocument/VC/ZKP)
• 受信: UnknownDID + Optional(UnknownDIDDocument/VC/ZKP)
• did:amt制約: DID解決ができないため、Holderが明示的にDIDDocumentを送信
• すべてのデータが受信側でUnknownとして扱われ、検証が必要

• DIDComm : Channel

instance instReprChannel : Repr Channel

Equations

• instReprChannel = { reprPrec := reprChannel✝ }

instance instDecidableEqChannel : DecidableEq Channel

Equations

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

structure CommunicationDIDInfo : Type

通信用DID（Ephemeral Communication DID）

Holderが通信毎に作成する一時的なDID。 以下の性質を持つ：

ライフサイクル:

1. 各通信開始時に、新しい通信用DIDを生成
2. VCが発行された場合: Walletに保存し、通信相手DIDと紐づけて管理
3. VCが発行されなかった場合: 通信終了と同時にDIDを破棄（削除）

設計目的:

• 身分証明用DID（Identity DID）との名寄せ回避
• 通信毎の一時的な匿名性確保
• VC発行成功時のみ永続化

Wallet保存形式: 通信用DIDが保存される際、以下の情報を紐づけて保存：

• communicationDID: 通信用DID
• counterpartyDID: 通信相手のDID
• createdAt: 作成時刻
• vc: 発行されたVC（オプショナル）

このアソシエーション情報により、ログイン時に「この通信用DIDで そのサービスと通信していた」という履歴を参照できる。

• did : ValidDID
• counterpartyDID : UnknownDID
• issuedVC : Option ValidVC

instance instReprCommunicationDIDInfo : Repr CommunicationDIDInfo

Equations

• instReprCommunicationDIDInfo = { reprPrec := reprCommunicationDIDInfo✝ }

structure DIDCommMessageSend : Type

DIDCommメッセージ（送信側）

構造:

• senderDID: 送信者のValidDID（メッセージのfromフィールド）
  • 通常: 通信用DID（Ephemeral）
  • トラストアンカー: 固定DID
• senderDoc: オプショナルなValidDIDDocument（did:amt仕様に準拠）
• vcs: ValidVCのリスト（IssuerがHolderに発行する場合、Verifierが認証情報を送る場合など）
• zkp: オプショナルなValidZKP（相互認証時など）

ZKPに含まれる名寄せ回避メカニズム: ZKPは以下の2つのDID所有権を証明する：

1. 身分証明用DID（Identity DID）の秘密鍵所有権（提示したいクレーム関連）
2. 通信用DID（Communication DID）の秘密鍵所有権

ZKPがこの両方を証明することで、Verifierは 「クレームの所有者と通信相手は同じエンティティ」と確認できつつ、 複数の身分証明用DIDを同じ通信相手と関連付けることはできない。

秘密鍵対応の確定性（なりすまし攻撃の防止）: DIDCommメッセージで相手の公開鍵が明確に送信されるため：

• Verifierは「このZKPはこの公開鍵に対応する秘密鍵で生成されている」と確定的に知る
• 攻撃者が異なる秘密鍵でZKPを再利用することは暗号学的に不可能
• つまり、「異なる秘密鍵での署名」=「秘密鍵所有権の偽造」であり、完全ななりすまし
• ナンスにより本人によるリプレイは防止（これは秘密鍵の問題ではなく新鮮性の問題）

設計思想（DIDComm v2.1 + did:amt仕様に準拠）:

• メッセージにはDID文字列のみが含まれる
• did:amt特有の制約: DID文字列だけからDIDDocumentを解決できない
• そのため、Holderが明示的にDIDDocumentを送信する必要がある（Optional）
• 暗号化にはECDH-1PUを使用（送信者のSK + 受信者のPKで認証付き暗号化）

複数VC対応:

• Verifier認証メッセージなど、複数のVCを送信する必要がある場合に対応
• 単一VCの場合は、リストに1つだけ含める

did:amt仕様（Section 1.2.2 Read）:

The resolution of a did:amt is completed locally by a verifier who receives the [AMT Version Number, Public Key] pair from the owner and executes the same steps from 1.2.1, step 3 onwards.

つまり、HolderがVerifierに[AMT Version Number, Public Key]ペア （実質的にDIDDocument）を送信しない限り、VerifierはDIDを検証できない。

• senderDID : ValidDID
• senderDoc : Option ValidDIDDocument
• vcs : List ValidVC
• zkp : Option ValidZKP

structure DIDCommMessageReceive : Type

DIDCommメッセージ（受信側）

構造:

• senderDID: 送信者のUnknownDID（メッセージから取得、未検証）
• senderDoc: 送信者のオプショナルなUnknownDIDDocument（メッセージから取得、未検証）
• vcs: UnknownVCのリスト（受信側で検証が必要）
• zkp: オプショナルなUnknownZKP（受信側で暗号的検証が必要）

設計思想（信頼境界）:

• DID: メッセージから取得するが、未検証（UnknownDID）
• DIDDocument: メッセージから取得するが、所有権未検証（Option UnknownDIDDocument）
• VC/ZKP: 受信側はこれを信頼できないため、Unknownとして扱う

複数VC対応:

• Verifier認証メッセージなど、複数のVCを受信する必要がある場合に対応
• すべてのVCはUnknownとして扱われ、個別に検証が必要

実際のDIDComm + did:amt動作:

1. メッセージを受信（DID文字列 + オプショナルなDIDDocumentを取得）
2. did:amt制約: DID文字列だけからは解決できないため、送信側がDIDDocumentを含める必要がある
3. 受信したDIDDocumentから公開鍵を取得してメッセージを復号化
4. DIDとDIDDocumentの整合性検証（UnknownDID.isValid）
5. VC、ZKPをそれぞれ検証

理由（すべてUnknown）:

1. 通信経路での改ざんの可能性（中間者攻撃）
2. 送信側のバグによる不正なシリアライズ
3. ネットワークエラーによるデータ破損
4. 受信側のバグによる不正なデシリアライズ
5. 送信側が不正なDIDDocumentを送信する可能性

• senderDID : UnknownDID
• senderDoc : Option UnknownDIDDocument
• vcs : List UnknownVC
• zkp : Option UnknownZKP

noncomputable def Network.generateCommunicationDID : ValidDID

通信用DIDを生成する

プロセス:

1. 新しい秘密鍵ペア(SK, PK)を生成
2. DIDDocumentを作成（PKから生成）
3. ValidDIDDocumentを構築（所有権を検証済みとして扱う）
4. ValidDIDを生成

性質:

• 毎回異なるDIDが生成される（秘密鍵が異なる）
• 身分証明用DIDとは独立している

実装詳細: この関数は生成プロセスを抽象化しており、 実際の暗号操作（鍵生成等）は実装時に補完される。

Equations

• Network.generateCommunicationDID = { w3cDID := { value := "did:amt:communication:ephemeral" }, hash := { value := [] }, purpose := DIDPurpose.Communication }

noncomputable def Network.saveCommunicationDID (commDID : ValidDID) (counterpartyDID : UnknownDID) (issuedVC : Option ValidVC) : CommunicationDIDInfo

通信用DIDをWalletに保存する

パラメータ:

• commDID: 生成された通信用DID
• counterpartyDID: 通信相手のDID
• issuedVC: VC発行時のみSome vc、VCなしの場合は None

戻り値:

• CommunicationDIDInfo: 保存される情報

設計思想:

• VC発行時のみ永続化される
• VCなし（検証のみ）の場合は、破棄される
• Wallet内で「このサービスと通信したDID」を追跡可能

ログイン時の利用: 会員登録が必要なサービスの場合、以下のフロー：

1. Holder: 新しい通信用DIDを生成してサービスと通信
2. Issuer: VC（会員証など）を発行
3. Holder: 通信用DIDをWalletに保存
4. 次回ログイン: 同じ通信用DIDを使用してメッセージ認証

counterpartyDIDとdidの紐づけにより、 ログイン時に「どのサービスと通信していたか」が明確になる。

Equations

• Network.saveCommunicationDID commDID counterpartyDID issuedVC = { did := commDID, counterpartyDID := counterpartyDID, issuedVC := issuedVC }

noncomputable def Network.discardCommunicationDID (_commDID : ValidDID) : Unit

通信用DIDを破棄する（VC発行なし時）

タイミング:

• VC発行なし（検証のみ）で通信終了した場合
• 通信用DIDは生成したものの、発行されなかった場合

処理:

• Walletの通信用DID管理リストから削除
• メモリから破棄

型システムによる保証: VCが発行されなかった場合、通信は失敗を返す。 その場合、この関数が呼ばれて通信用DIDが破棄される。

実装詳細: この関数は破棄プロセスを抽象化しており、 実装時には、Walletから該当DIDを削除する処理が補完される。

Equations

• Network.discardCommunicationDID _commDID = ()

noncomputable def Network.sendViaDIDComm (senderDID : ValidDID) (senderDoc : Option ValidDIDDocument) (vcs : List ValidVC) (zkp : Option ValidZKP) : DIDCommMessageSend

DIDCommメッセージ送信: ValidDID + オプショナルなDIDDocument/VCs/ZKPを送信

設計思想（DIDComm v2.1 + did:amt仕様に準拠）:

• メッセージには送信者のDID文字列を含む
• did:amt制約: Holderは通常、DIDDocumentも送信する（Optionalだが推奨）
• ECDH-1PUで暗号化（送信者のSK + 受信者のPKで認証付き暗号化）

使用例:

1. Issuer → Holder: VCの発行

   let msg := Network.sendViaDIDComm issuerDID (some issuerDoc) [newVC] none
   

2. Verifier → Holder: Verifier認証（複数のVerifierVCを送信）

   let msg := Network.sendViaDIDComm verifierDID (some verifierDoc)
     verifierVCs (some verifierAuthZKP)
   

3. Holder → Verifier: HolderがVCに基づくZKPを送信

   let msg := Network.sendViaDIDComm holderDID (some holderDoc) [] (some holderCredentialZKP)
   

did:amt注意点:

• 受信側がDIDDocumentを持っていない場合、senderDocをsome docで送信する必要がある
• トラストアンカーのような公開されたDIDDocumentの場合は、noneでも可

Equations

• Network.sendViaDIDComm senderDID senderDoc vcs zkp = { senderDID := senderDID, senderDoc := senderDoc, vcs := vcs, zkp := zkp }

noncomputable def Network.receiveViaDIDComm (msg : DIDCommMessageSend) : DIDCommMessageReceive

DIDCommメッセージ受信: UnknownDID + オプショナルなUnknownDIDDocument + UnknownVCs/UnknownZKPを受信

設計思想（信頼境界）:

• DID: メッセージから取得するが、未検証（UnknownDID）
• DIDDocument: メッセージから取得するが、所有権未検証（Option UnknownDIDDocument）
• VCs/ZKP: 受信側はこれを信頼できないため、Unknownとして扱う

型システムによる保証: すべてのデータがUnknownとして受け取られるため、検証を忘れることができない。 型システムが検証を強制する。

実装: この関数は通信プロセスを抽象化したもの：

1. シリアライズ → DIDComm送信 → DIDComm受信 → デシリアライズ
2. 復号化（ECDH-1PU）
3. did:amt制約: DID解決は不可、送信側がDIDDocumentを含める必要がある

すべてのデータは受信側で未検証として扱われる。

Equations

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

def Network.verifyReceivedVC (vc : UnknownVC) : Option ValidVC

受信したVCを検証してValidVCに変換

DIDComm検証フロー:

1. DIDCommメッセージを受信
2. VCs（List UnknownVC）を取り出す
3. 各VCに対して署名検証を行う
4. 検証成功ならValidVCとして使用可能

使用例:

-- 受信側（Holder）
let receivedMsg := Network.receiveViaDIDComm sentMsg
-- 各VCを検証
let validVCs := receivedMsg.vcs.filterMap Network.verifyReceivedVC
-- 検証成功したVCのみを処理
for validVC in validVCs do
  Holder.storeCredential wallet validVC ...

Equations

• Network.verifyReceivedVC (UnknownVC.valid validVC) = some validVC
• Network.verifyReceivedVC (UnknownVC.invalid a) = none

def Network.verifyReceivedZKP (zkp : UnknownZKP) (_relation : Relation) : Option ValidZKP

受信したZKPを検証してValidZKPに変換

DIDComm検証フロー:

1. DIDCommメッセージを受信
2. ZKP（Option UnknownZKP）を取り出す
3. 暗号的検証を行う
4. 検証成功ならValidZKPとして使用可能

Equations

• Network.verifyReceivedZKP (UnknownZKP.valid validZKP) _relation = some validZKP
• Network.verifyReceivedZKP (UnknownZKP.invalid a) _relation = none

theorem Network.send_receive_didcomm_completeness (did : ValidDID) (doc : Option ValidDIDDocument) (vcs : List ValidVC) (zkp : Option ValidZKP) : let sentMsg := sendViaDIDComm did doc vcs zkp; let receivedMsg := receiveViaDIDComm sentMsg; receivedMsg.senderDID = UnknownDID.valid did ∧ (∀ (validDoc : ValidDIDDocument), doc = some validDoc → receivedMsg.senderDoc = some (UnknownDIDDocument.valid validDoc)) ∧ receivedMsg.vcs = List.map UnknownVC.valid vcs ∧ ∀ (validZKP : ValidZKP), zkp = some validZKP → receivedMsg.zkp = some (UnknownZKP.valid validZKP)

Theorem: 正しく送信されたDIDCommメッセージは正しく受信される（DIDCommの完全性）

設計思想（DIDComm v2.1 + did:amt仕様に準拠）:

• 送信側がValidなデータを送信し、改ざんされずに届いた場合、正しく受信される
• DID: メッセージから取得するが、未検証（UnknownDID）
• DIDDocument: メッセージから取得するが、所有権未検証（Option UnknownDIDDocument）
• VCs/ZKP: Unknownとして受信され、受信側で検証が必要

現実:

• 攻撃者が改ざんした場合、UnknownDID.invalid、UnknownDIDDocument.invalid、 UnknownVC.invalid、UnknownZKP.invalidが届く
• その場合、検証関数はnoneを返す（健全性）

theorem Network.didcomm_did_diddocument_safety (did : ValidDID) (doc : Option ValidDIDDocument) (vcs : List ValidVC) (zkp : Option ValidZKP) : let sentMsg := sendViaDIDComm did doc vcs zkp; let receivedMsg := receiveViaDIDComm sentMsg; receivedMsg.senderDID = UnknownDID.valid did ∧ ∀ (validDoc : ValidDIDDocument), doc = some validDoc → receivedMsg.senderDoc = some (UnknownDIDDocument.valid validDoc)

Theorem: DIDCommの型安全性（DID/DIDDocument）

保証（DIDComm v2.1 + did:amt仕様に準拠）: DIDCommでは、DIDもDIDDocumentも受信側でUnknownとして扱われるため、 検証を忘れることができない。型システムが検証を強制する。

形式化:

• sendViaDIDComm : ValidDID → Option ValidDIDDocument → List ValidVC → ... → DIDCommMessageSend
• receiveViaDIDComm : DIDCommMessageSend → DIDCommMessageReceive
• 受信側ではUnknownDIDとOption UnknownDIDDocumentとして扱う

theorem Network.didcomm_vc_zkp_type_safety : (∀ (did : ValidDID) (doc : Option ValidDIDDocument) (vcs : List ValidVC) (zkp : Option ValidZKP), let sentMsg := sendViaDIDComm did doc vcs zkp; let receivedMsg := receiveViaDIDComm sentMsg; receivedMsg.vcs = List.map UnknownVC.valid vcs) ∧ ∀ (did : ValidDID) (doc : Option ValidDIDDocument) (vcs : List ValidVC) (zkp : ValidZKP), let sentMsg := sendViaDIDComm did doc vcs (some zkp); let receivedMsg := receiveViaDIDComm sentMsg; ∃ (unknownZKP : UnknownZKP), receivedMsg.zkp = some unknownZKP ∧ ∀ (relation : Relation), verifyReceivedZKP unknownZKP relation = some zkp

Theorem: DIDCommの型安全性（VCs/ZKP）

保証: DIDCommでVCs/ZKPを送信する場合、受信側は必ずUnknownとして受け取るため、 検証を忘れることができない。型システムが検証を強制する。

形式化:

• VCs: List ValidVC → List UnknownVC（検証済み → 未検証）
• ZKP: Option ValidZKP → Option UnknownZKP（検証済み → 未検証）
• 受信側はverifyReceivedVC/verifyReceivedZKPで検証必須