研究シーズ共同研究・外部資⾦獲得実績研究キーワード暗号理論・形式的⼿法・定理証明・計算理論・数理論理・数理構造•形式的手法による暗号方式の安全性証明確率的関数の識別不能性の形式化アルゴリズムの形式化暗号方式の形式化計算量の形式化•暗号プロトコルの安全性自動検証暗号プリミティブの形式化暗号プロトコルの安全性検証（SSL/TLS等）IoTの通信プロトコル等も安全性検証できます•科研費(代表) 基盤（C）平成29年-32年形式手法による暗号の安全性証明自動検証システムの開発•科研費(分担)基盤（C）平成30年-32年情報セキュリティ人材育成のための暗号技術学習支援eラーニングシステムの開発•情報通信研究機構（NICT）委託研究課題(分担)平成25年-27年組織間機密通信のための公開鍵システムの研究開発•科研費(分担)基盤（B）平成22年-25年ＭＩＺＡＲ数学ライブラリの構築と大学数学向け高度遠隔教育用コンテンツ開発•科研費(分担) 基盤（A）平成21年-25年センサネットワークの安全・安心を保証する情報セキュリティ技術の研究•共同研究(エプソンアヴァシス株式会社)令和元年-令和2年IoTデバイス間相互認証方法の研究•暗号プロトコル評価技術コンソーシアム会員https://www.cellos-consortium.org/jp/最近の研究トピックス計算機援用による形式的定理証明システムMizar 上での共通鍵暗号方式AES(Advanced Encryption Standard)の形式化記述コード（一部抜粋）助教岡崎裕之研究から広がる未来卒業後の未来像岡崎研究室では暗号の研究をおこなっています。暗号はICT社会をささえるインフラの要素として重要となっています。しかし、暗号は情報理論、計算理論、あるいは数学など情報工学のさまざまな技術分野の上に成り立つ総合的な学問分野であり専門家の数は限られています。数理的技法を用いてコンピュータを使って暗号システムの安全性を検証する仕組みを作り、暗号の専門家でなくてもセキュリティバイデザインを実現するために暗号技術を正しく使い、安全な情報システムの設計・開発が行えるようにします。IoT,フィンテックをはじめとするSociety5.0を実現する様々なテクノロジーは暗号技術なくして成り立ちません。電子情報システムのすべてを支え、ブレイクスルーをもたらす根幹技術を開発しましょう。情報セキュリティ人材が不足しています。暗号に限らず情報セキュリティに関する理論、技術、法律やマネージメント等幅広い知識を習得し、情報セキュリティの専門家として活躍することを期待しています。博士（工学）（京都工芸繊維大学）信州大学大学院助手を経て2007年より信州大学大学院助教情報処理安全確保支援士（登録番号018816）暗号理論の研究に従事。数論アルゴリズム応用による暗号方式実装技術,形式的手法による暗号の安全性証明に取り組む。情報セキュリティの基礎理論暗号・論理・数理で実現するSociety 5.0電⼦情報システム⼯学科【私の学問へのきっかけ】もともと理論物理学をやりたかったのですが、数学が苦手だったので工学系の大学の実験物理学、特に電子顕微鏡の研究をやっていた電子情報工学科に入りました。電気、通信、情報など幅広く勉強しましたが、符号理論の先生が教鞭をとられていた情報数学の講義で苦手であった微分・積分をやらなくてもよい数学があると知りました。第5回実践的IT教育シンポジウムrePiT2019 in 愛媛において電子情報システム工学科3年次科目デザインプロジェクトⅠで行った暗号プロトコル設計演習の取り組みが優秀教育実践賞として表彰されました形式的安全性検証ツールProVerifによるCBCのパディングオラクル攻撃導出(抜粋)33
元のページ ../index.html#35