DID CommのFormal Verificationとセキュリティ強化

こんにちは、富士榮です。

クレデンシャル交換のプロトコルとして適しているのはDID CommなのかOpenID for Verifiable Credentials（OID4VC）なのか、という議論がひところ各所で聞かれましたが最近はそんな議論も落ち着いてきているのかな？と思っている今日この頃です（エコーチェンバー）。

当時、DID Commを否定的に捉える論拠の一つにFormal Verificationもすんでないじゃん、という話がありましたが、ようやく？やったみたいです。

What Did Come Out of It? Analysis and Improvements of DIDComm Messaging

https://eprint.iacr.org/2024/1361

Abstractにはこんなことが書いてあります。

Self-Sovereign Identity (SSI) empowers individuals and organizations with full control over their data. Decentralized identifiers (DIDs) are at its center, where a DID contains a collection of public keys associated with an entity, and further information to enable entities to engage via secure and private messaging across different platforms. A crucial stepping stone is DIDComm, a cryptographic communication layer that is in production with version 2. Due to its widespread and active deployment, a formal study of DIDComm is highly overdue.

We present the first formal analysis of DIDComm’s cryptography, and formalize its goal of (sender-) anonymity and authenticity. We follow a composable approach to capture its security over a generic network, formulating the goal of DIDComm as a strong ideal communication resource. We prove that the proposed encryption modes reach the expected level of privacy and authenticity, but leak beyond the leakage induced by an underlying network (captured by a parameterizable resource).

We further use our formalism to propose enhancements and prove their security: first, we present an optimized algorithm that achieves simultaneously anonymity and authenticity, conforming to the DIDComm message format, and which outperforms the current DIDComm proposal in both ciphertext size and computation time by almost a factor of 2. Second, we present a novel DIDComm mode that fulfills the notion of anonymity preservation, in that it does never leak more than the leakage induced by the network it is executed over. We finally show how to merge this new mode into our improved algorithm, obtaining an efficient all-in-one mode for full anonymity and authenticity.

自己主権型アイデンティティ（SSI）は、個人や組織が自分のデータを完全にコントロールできるようにする。分散型識別子（DID）がその中心であり、DIDには、エンティティに関連する公開鍵のコレクションと、エンティティが異なるプラットフォーム間で安全かつプライベートなメッセージングを介して関与できるようにするためのさらなる情報が含まれている。その重要な足がかりとなるのがDIDCommであり、バージョン2で製品化された暗号通信レイヤーである。DIDCommは広く活発に展開されているため、DIDCommの正式な研究は非常に遅れている。

本稿では、DIDCommの暗号技術に関する初の形式的分析を行い、（送信者の）匿名性と真正性というDIDCommの目標を形式化する。DIDCommの目標を強力な理想的通信リソースとして定式化することで、一般的なネットワーク上での安全性を実現する。提案する暗号化モードは、期待されるプライバシーと真正性のレベルに達するが、（パラメータ化可能なリソースによって捕捉される）基礎となるネットワークによって誘発される漏洩を超えて漏洩することを証明する。

次に、匿名性と真正性を同時に達成し、DIDCommメッセージフォーマットに適合し、暗号文のサイズと計算時間の両方において、現在のDIDCommの提案をほぼ2倍上回る最適化アルゴリズムを提示する。最後に、この新しいモードを改良されたアルゴリズムにマージする方法を示し、完全な匿名性と真正性を実現する効率的なオールインワンモードを得る。

中身はまだ細かく見ていませんが、しっかりと分析を行うプロセスが実行された、ということなので良かったんじゃないかと思います。

いずれにしても特にIoTのユースケースなどDID Commの方が適しているものもある気がしますので、ちゃんと適切にプロトコルを選択していけると良いかと思います。