🔢 mathematics

Canonical Byte-String Encoding for Finite-Ring Cryptosystems

この論文は、有限環暗号系におけるバイト列から剰余リストへの標準的な変換（ベース m 長さコーデック）を提案し、その Rust 実装、Lean 4 による機械検証付きの形式化、および性能ベンチマークを通じて、その正確性と実用性を立証するものである。

原著者： Kyrylo Riabov, Serhii Kryvyi

公開日 2026-03-25

📖 1 分で読めます🧠 じっくり読む

CC BY 4.0

原著者： Kyrylo Riabov, Serhii Kryvyi

原論文は CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/) でライセンスされています。 ✨ これは以下の論文のAI生成解説です。著者が執筆または承認したものではありません。技術的な正確性については原論文を参照してください。免責事項の全文を読む

この論文は、**「コンピュータの言語（文字やデータ）を、暗号の世界で使える『数字の箱』にきれいに詰める方法」**について書かれたものです。

専門用語を排して、日常の生活に例えながら解説します。

1. 背景：なぜこんなものが必要なの？

Imagine you are sending a secret letter.
（想像してください。あなたは秘密の手紙を送ろうとしています。）

通常の暗号： 手紙を「鍵付きの金庫」に入れて送ります。
この論文の暗号（有限環暗号）： 手紙を「金庫」に入れる前に、まず**「数字の箱」**に詰め替える必要があります。

でも、ここで問題が起きます。
「手紙（文字や画像）」は 256 種類の記号（バイト）でできていますが、「数字の箱」は決まった数の数字（例えば 50 個や 257 個）しか入らないのです。
「A」や「B」という文字を、どうやって「0 から 49 までの数字」に変換すれば、後で100% 正確に元に戻せるのでしょうか？

これまでの方法は、小さなケース（辞書）を手作りで作って対応していましたが、これでは「どんなデータでも」対応できません。そこで、**「どんなデータでも、自動的に、正確に、箱詰めできる魔法のルール」**が必要だったのです。

2. この論文の解決策：「Base-m-len」codec（コーデック）

この論文が提案しているのは、**「Base-m-len」**という新しい箱詰めルールです。
これを「賢い郵便局員」に例えてみましょう。

① 手紙の長さを「ラベル」に書く（固定幅ヘッダ）

まず、郵便局員は手紙の長さを測ります。
「この手紙は 100 文字です！」と、決まった大きさのラベルに書いて、箱の一番上に貼ります。

ポイント： ラベルのサイズは、手紙が最大でどれくらい長くなっても（264 文字まで）、必ず収まるように設計されています。これにより、受け取り側は「あ、この箱には 100 文字が入っているんだ」と即座にわかります。

② 手紙を「数字の箱」に詰める（ペイロード変換）

次に、手紙の中身（文字）を、箱の数字に変えて詰めていきます。

仕組み： 文字を一つずつ読み取り、「256 倍して、次の文字を足す」という計算を繰り返しながら、箱の数字（0〜m-1）に変換していきます。
特徴： これは「圧縮」ではなく、**「変換」**です。元の情報が一切失われず、後で完全に復元できるように設計されています。

③ 最後の「状態」をラベルに書く

詰め終わったら、最後に「箱の残りの状態（計算の途中の値）」を、もう一枚の決まった大きさのラベルに書いて貼ります。
これで、箱の構造は完成です。
【長さのラベル】＋【状態のラベル】＋【変換された数字の列】

3. このルールがすごいところ（3 つのメリット）

① 100% 正確に元に戻る（完全な復元）

このルールは、数学的に「絶対に間違えない」ことが証明されています。
受け取り側は、ラベルの「長さ」を見て、必要な数の数字だけ読み取れば、元の文字（手紙）がピタリと再現されます。

例え： 「100 文字のラベル」がついていれば、101 文字目以降の数字は「余分なゴミ」として無視されます。つまり、箱に余計な数字がくっついていても、正しく開封できるのです。

② どのサイズの箱でも使える（柔軟性）

「数字の箱」のサイズ（m）は、25 個でも、50 個でも、257 個でも構いません。

小さな箱（m=25）： 数字が少し多くなりますが、使えます。
大きな箱（m=257）： ほぼ「文字 1 文字＝数字 1 個」の感覚で詰められ、非常に効率的です。
このルールは、箱のサイズに合わせて自動的に調整されます。

③ 数学的に「証明済み」である（信頼性）

この論文の最大の特徴は、**「コンピュータ（Lean 4 というツール）を使って、このルールが絶対に間違いないことを証明した」ことです。
人間が「たぶん大丈夫」と思っただけではなく、「数学的に間違いがないと確認された」**という点が、セキュリティにとって非常に重要です。

4. 現実世界での使い方

Rust という言語で実装済み： 実際に使えるプログラムとして作られています。
速い： 巨大なデータでも、一瞬で変換できます。
用途： 将来の高度な暗号技術（ホモモルフィック暗号など）や、複数の人が協力して計算するシステムで、データを安全にやり取りするための「共通言語」として使われます。

まとめ

この論文は、**「複雑な暗号の世界で、普通のデータ（文字や画像）を、数字の箱にきれいに詰めて、後で絶対に間違えずに開けるための『完璧な梱包マニュアル』」**を作ったものです。

問題： 文字を数字に変換するときに、元に戻せなかったり、サイズが合わなかったりする。
解決： 「長さのラベル」と「状態のラベル」を付けて、数学的に証明されたルールで変換する。
結果： どんなデータでも、どんな箱のサイズでも、100% 正確に、安全に扱えるようになった。

これにより、将来の「超安全なインターネット」や「秘密を隠したまま計算する技術」が、より現実的なものになるでしょう。

以下は、Kyrylo Riabov と Serhii Kryvyi による論文「Canonical Byte-String Encoding for Finite-Ring Cryptosystems（有限環暗号系のための標準バイト列エンコーディング）」の技術的サマリーです。

1. 背景と課題 (Problem)

有限環（ $\mathbb{Z}_m$ ）上で動作する暗号システム（リングマッピング暗号など）では、平文データを暗号化・復号する前に、バイト列を環の要素（剰余）に変換する必要がある。
既存の研究では、この変換層は手動で構築されたアルファベットや小さな固定符号表で処理されることが多かった。しかし、任意の UTF-8 テキストやバイナリデータを、環レベルの暗号化ステップに安全かつ標準的に渡すための一般的な解決策が欠けていた。
具体的には、以下の要件を満たす標準的なエンコーディングが必要とされていた：

任意の長さ（ $2^{64}$ 未満）のバイト列を扱えること。
復号時に元のバイト列を完全に再現できること（完全な可逆性）。
追加された有効な接尾辞（suffix）を無視できること（自己区切り性）。
形式検証（Formal Verification）による正しさが保証されていること。

2. 提案手法：Base- $m$ -Len コーデック (Methodology)

著者らは、バイト列を剰余のリスト（ $\mathbb{Z}_m$ の要素）に変換するための標準的なコーデック「base- $m$ -len」を提案した。これは Duda による rANS（range ANS）に基づくシステムの概念を応用・適応させたものであるが、目的はエントロピー符号化ではなく、決定論的かつ自己区切り的な表現層の構築にある。

ワイヤーフォーマット（送信形式）:
データは以下の 3 つのコンポーネントから構成される：

長さプレフィックス (len): バイト列の長さを固定幅でエンコード（ $k$ 桁の $m$ 進数）。
状態プレフィックス (state): 最終的なペイロード状態を固定幅でエンコード（ $k$ 桁の $m$ 進数）。
ペイロードストリーム (payload): 均一な $m$ 進変換によって生成された剰余の列。

アルゴリズムの概要:

エンコード:
- 入力バイト列を右から左にスキャンする。
- 各バイト $b$ に対して、状態 $x$ を $x \leftarrow 256x + b$ で更新する。
- 状態がエンコーダの閾値を超えた場合、 $x \mod m$ を出力し、 $x \leftarrow \lfloor x/m \rfloor$ で正規化する。
- 最終的に、長さ、最終状態、そして出力されたペイロード（FIFO 順）を連結する。
デコード:
- まず長さプレフィックスを読み取り、復号すべきバイト数を特定する。
- 次に状態プレフィックスを読み取り、初期状態を設定する。
- 宣言されたバイト数分だけ、ペイロードから剰余を読み取り、逆変換（ $x \leftarrow \lfloor x/256 \rfloor$ など）を適用して元のバイトを復元する。
- 復号が完了した後、残りの有効な接尾辞（suffix）は自動的に無視される。

3. 主な貢献 (Key Contributions)

標準コーデックの定義: 有限環プロトコル向けに、 $2^{64}$ 未満の長さを持つバイト列を $\mathbb{Z}_m$ のストリームにマッピングする標準的な「base- $m$ -len」形式を定義した。
厳密な正しさと保証:
- 支持されるすべての法 $m$ に対して、復号が元のバイト列を正確に再現すること（完全な可逆性）。
- 有効な接尾辞が付加されても正しく復号されること（接尾辞許容性）。
- 固定幅ヘッダの逆変換が常に成功すること。
- これらの性質は、Lean 4 による形式検証と機械検証済みの証明によって保証されている。
実装と形式仕様:
- 実用的な Rust ライブラリ（sym-adv-encoding）の公開。
- Lean 4 による抽象コーデックの形式仕様と、すべての定理の機械検証済み証明の公開。

4. 結果と評価 (Results)

正しさの証明: Lean 4 による形式検証により、ヘッダの逆変換、ペイロード状態の境界（ $L \le \text{state} < L \cdot m$ ）、およびストリームレベルの往復正しさが数学的に証明された。特に、ゼロ長さのケースや接尾辞の無視動作も厳密に扱われている。
パフォーマンス:
- 計算量: エンコード・デコードともにストリーム長に対して線形 $O(n)$ であり、作業状態は $O(1)$ である。
- 実測値: Apple M3 Pro 環境でのベンチマークによると、ネイティブ実装（Rust）は、大規模な入力における厳密な基数変換（BigUint ベースライン）よりも著しく高速である。
- 例: $m=257$ の設定では、バイトあたり約 1 個の剰余（1.0 桁）で表現でき、ヘッダのオーバーヘッドも最小限に抑えられる。
効率性: 法 $m$ が大きいほどペイロードの圧縮率（バイトあたりの桁数）は向上するが、固定ヘッダのサイズは $m$ の増加に伴って段階的に減少する。

5. 意義と限界 (Significance and Limitations)

意義:

このコーデックは、有限環暗号や形式検証された暗号プロトコル（SYMPZON プロジェクトなど）にとって不可欠な「メッセージ表現層」を提供する。
NTRU や ML-KEM などの格子暗号とは異なり、これは暗号学的な仮定に基づくものではなく、データ表現の標準化に焦点を当てている。
形式検証（Lean 4）と実装（Rust）の両方を提供することで、実運用における信頼性を高めている。

限界と注意点:

セキュリティ機能なし: このコーデック自体は暗号化や認証を提供しない。機密性、完全性、真正性は、これを囲む暗号プロトコルに依存する。
長さの露出: デフォルトの形式はバイト列の正確な長さを露出するため、長さ隠蔽が必要な場合はプロトコル層でパディングを適用する必要がある。
実装責任: Lean 4 は抽象仕様を証明しているが、Rust 実装の低レベルなパース処理やメモリ割り当ての安全性は実装者の責任となる。

結論

この論文は、有限環暗号系におけるバイト列から剰余への標準的な変換レイヤーを確立し、その正しさを形式検証で保証した点で画期的である。提案された「base- $m$ -len」コーデックは、実用的なパフォーマンスを持ちながら、数学的に厳密な保証を提供するため、次世代の対称鍵暗号やゼロ知識証明などのプロトコル実装において重要な基盤技術となる。