Generic Modelにおける困難性仮定への攻撃の数式処理を用いた導出

摘要

The computational hardness of number-theoretic problems used in cryptography is generally proved in a generic model of the based mathematical structure such as a bilinear group. However, a proof often contains flaws due to miss of attacks. To assist proof, this paper proposes an automatic analysis method which derives attacks by solving simultaneous equations. We demonstrate the usefulness of the proposed method by using a computer algebra system called Maple. Specifically, we apply the proposed method to well-known easy/hard problems (M-LRSW/LIN) and confirm that it successfully derives an attack to M-LRSW within a second, which is a generalized version of the known attack, whereas LIN is decided that there is no attack.%暗号的な困難性仮定の妥当性を，基とする数学的構造を理想化したGeneric Model（GM）において証明する研究が活発に行われている.しかし，しばしば単純な誤解による誤り（仮定への攻撃の見逃し）が証明に含まれる.本研究では，困難性仮定のGMにおける妥当性証明の支援を目的とし，証明の議論で誤りが含まれやすい部分を数式処理を用いて自動化する手法を提案する.さらに，提案法を既存の数式処理システムを利用して実装し，その正しさと有効性を確認した.具体的には，Mapleを利用して，妥当な困難性仮定（LIN）と妥当でない困難性仮定（M-LRSW）に提案法を適用し，現実的な時間内で前者は攻撃無しと判定され，後者へは既知の攻撃を一般化した攻撃が導出されることを確認した.