1 0 0 0 OA 形式手法による暗号の安全性証明自動検証システムの開発
本研究では、形式的定理証明系Mizarとモデル検査器ProVerifを用いて、計算機援用による暗号システムの安全性形式的評価システムを開発した。Mizarでは暗号理論に関わる形式化数学ライブラリを開発した。本成果は確率、統計、関数解析、計算アルゴリズムや計算量等の計算機科学の基礎の形式化であるので、暗号理論以外にも応用できる。一方、ProVerifでは、基本的な暗号プロトコルのみならず、従来より抽象度が低くより現実のシステムや実装に近いモデルでの安全性検証手法を提案した。これにより暗号学的ハッシュ関数やブロック暗号の利用モード等の開発時の設計支援や形式的安全性検証を行うことが可能となった。
- 著者
- 藤岡 碧志 岡崎 裕之 鈴木 彦文
- 雑誌
- 研究報告インターネットと運用技術(IOT) (ISSN:21888787)
- 巻号頁・発行日
- vol.2021-IOT-54, no.7, pp.1-7, 2021-07-02
日々の研究データを管理するためのシステムとして Nii が GakuninRDM というサービスの提供を開始した.GakuninRDM は一般的なオンラインストレージサービスをと同様に扱うことができ,バージョン管理や外部サービスとの連携も可能となっている.しかし,同サービスが掲げている「研究データ管理による研究推進と研究公正」を達成するためには機能が不十分であると考えた.そこで我々は外部サービスとして NextCloud を選択し,その上にレビュー機能・RDM ヘ登録するファイルヘの署名付与を行うカスタムアプリケーションを構築し,運用することで研究データの再利用と研究公正に有用か検討を行う.
- 著者
- 岡崎 裕之 紫村 彰吾 宮本 樹 渡邊 樹 布田 裕一 村上 恭通
- 出版者
- 日本ソフトウェア科学会
- 雑誌
- コンピュータ ソフトウェア (ISSN:02896540)
- 巻号頁・発行日
- vol.37, no.1, pp.1_99-1_113, 2020-01-24 (Released:2020-02-22)
暗号技術は情報セキュリティを実現するための基盤要素である.暗号を専門とする研究者や技術者のみならずネットワークエンジニアや運用者等にとっても暗号技術に関する知識の習得は必須である.実際のシステムは,公開鍵暗号や電子署名等の複数の要素技術を組み合わせて構築する必要があるため,様々な攻撃について必要な対策を施しつつ安全性要件を満たすように実現しなければならない.しかしながら,システム構築を座学だけでは初学者に学ばせることは困難である.この課題を克服するために,報告者等は計算機援用による形式的暗号プロトコル安全性検証ツールを利用した暗号技術の基礎知識と利用方法を学習する教材を作成し,演習形式による授業を実践した.形式的暗号プロトコル安全性検証ツールの利用により,既存の教材では学習困難な実際の暗号技術の動作や攻撃を,学習者が設定した暗号システム上でシミュレーションしてインタラクティブに学ぶことが可能となった.本論文では,まず,実践した教育内容の概要とその成果を報告し,更に,現在進めている本教材を元とする CAI 教材開発方針の紹介と,その課題について報告する.