Google DeepMind、Signal暗号の安全性を形式検証

Google DeepMindの研究者は、AIエージェントを使い、Signalプロトコルの主要な暗号学的保証の一部を形式検証しました。4週間の実証プロジェクトで、数学的な証明を通じて通信暗号の性質を確認したと報じられています。

SignalのプロトコルはSignalアプリのほか、GoogleメッセージやWhatsAppなどの通信保護にも関係します。独立した検証は、広く使われる暗号技術への追加の信頼材料となります。

今回の成果は暗号の検証だけでなく、AIが形式的な証明を進める能力を示す点でも注目されます。研究者は専用のAIシステムを使い、対象となる保証を数学的に記述・確認しました。

証明されたのはプロトコルの特定の性質であり、アプリ全体やあらゆる実装上の問題が安全と確認されたわけではありません。独立検証の範囲と実装との対応を理解することが重要です。