1 0 0 0 OA 形式手法による暗号の安全性証明自動検証システムの開発
本研究では、形式的定理証明系Mizarとモデル検査器ProVerifを用いて、計算機援用による暗号システムの安全性形式的評価システムを開発した。Mizarでは暗号理論に関わる形式化数学ライブラリを開発した。本成果は確率、統計、関数解析、計算アルゴリズムや計算量等の計算機科学の基礎の形式化であるので、暗号理論以外にも応用できる。一方、ProVerifでは、基本的な暗号プロトコルのみならず、従来より抽象度が低くより現実のシステムや実装に近いモデルでの安全性検証手法を提案した。これにより暗号学的ハッシュ関数やブロック暗号の利用モード等の開発時の設計支援や形式的安全性検証を行うことが可能となった。
- 著者
- 岡崎 裕之 紫村 彰吾 宮本 樹 渡邊 樹 布田 裕一 村上 恭通
- 出版者
- 日本ソフトウェア科学会
- 雑誌
- コンピュータ ソフトウェア (ISSN:02896540)
- 巻号頁・発行日
- vol.37, no.1, pp.1_99-1_113, 2020-01-24 (Released:2020-02-22)
暗号技術は情報セキュリティを実現するための基盤要素である.暗号を専門とする研究者や技術者のみならずネットワークエンジニアや運用者等にとっても暗号技術に関する知識の習得は必須である.実際のシステムは,公開鍵暗号や電子署名等の複数の要素技術を組み合わせて構築する必要があるため,様々な攻撃について必要な対策を施しつつ安全性要件を満たすように実現しなければならない.しかしながら,システム構築を座学だけでは初学者に学ばせることは困難である.この課題を克服するために,報告者等は計算機援用による形式的暗号プロトコル安全性検証ツールを利用した暗号技術の基礎知識と利用方法を学習する教材を作成し,演習形式による授業を実践した.形式的暗号プロトコル安全性検証ツールの利用により,既存の教材では学習困難な実際の暗号技術の動作や攻撃を,学習者が設定した暗号システム上でシミュレーションしてインタラクティブに学ぶことが可能となった.本論文では,まず,実践した教育内容の概要とその成果を報告し,更に,現在進めている本教材を元とする CAI 教材開発方針の紹介と,その課題について報告する.
1 0 0 0 IR 素数位数を有する楕円曲線の構成とその計算量評価
- 著者
- 堀内 啓次 布田 裕一 境 隆一 金子 昌信 笠原 正雄
- 出版者
- 電子情報通信学会
- 雑誌
- 電子情報通信学会論文誌. A, 基礎・境界 (ISSN:09135707)
- 巻号頁・発行日
- vol.82, no.8, pp.1269-1277, 1999-08
- 被引用文献数
- 7
楕円暗号において, 楕円曲線の群の位数は重要なパラメータである. 特に, その位数が素数であることが望ましい. 楕円曲線の位数を計算する方法としてSchoofのアルゴリズム及びそれを改良したElkies, Atkinのアルゴリズムが知られている. 本論文ではSchoofの改良アルゴリズムを用いた素数位数を有する楕円曲線の効率的な構成法を示す. 更に, 楕円曲線の位数分布及び位数が素数である確率を導出した後, 素数位数を有する楕円曲線の構成に必要な計算量を評価する. また, 法pの条件による計算時間の違いについて考察する.