信州大学HOMEENGLISH交通・キャンパス案内

研究者総覧研究者総覧

研究者、研究内容などで検索
項目別検索はこちら

岡﨑 裕之  オカザキ ヒロユキ

教員組織学術研究院(工学系)電話番号026-269-5503
教育組織大学院総合理工学研究科 工学専攻FAX番号
職名准教授メールアドレスokazaki@cs.shinshu-u.ac.jp
住所〒380-8553 長野県長野市若里4-17-1ホームページURL

更新日:2023/04/21

プロフィール

研究分野
情報セキュリティ(暗号理論)
形式検証
キーワード:暗号系 , 暗号・セキュリティ
現在の研究課題
形式的手法による暗号理論
キーワード:暗号理論 , 形式的手法 , cryptology
所属学会
所属学会
日本ソフトウェア科学会
日本応用数理学会
電子情報通信学会
学歴
出身大学院
2004 , 京都工芸繊維大学 , 工芸科学研究科 , 情報・生産科学専攻
2001 , 京都工芸繊維大学 , 工芸科学研究科 , 電子情報工学専攻

出身学校・専攻等(大学院を除く)
1999 , 京都工芸繊維大学 , 工芸学部 , 電子情報工学科

取得学位
博士(工学) , 京都工芸繊維大学(日本)

免許・資格等
20191001 , 情報処理安全確保支援士(登録番号 018816)
20160516 , 情報セキュリティマネージメント試験
20041216 , 情報セキュリティアドミニストレータ試験
受賞学術賞
2019 , 第5回 実践的IT教育シンポジウム rePiT2019 in 愛媛 優秀教育実践賞
研究職歴等
研究職歴
2007- , 信州大学大学院工学系研究科情報工学専攻(助教)
2005-2007 , 信州大学大学院工学系研究科情報工学専攻(助手)

研究活動業績

研究業績(著書・
発表論文等)
論文
The 3-Fold Product Space of Real Normed Spaces and its Properties
Formalized Mathematics,29(4):245-253 2021
Author:Hiroyuki Okazaki, Kazuhisa Nakasho


Finite Dimensional Real Normed Spaces are Proper Metric Spaces
Formalized Mathematics,29(4):177-186 2021
Author:Kazuhisa Nakasho, Hiroyuki Okazaki


Real Vector Space and Related Notions
Formalized Mathematics,29(3):117-127 2021
Author:Kazuhisa Nakasho,Hiroyuki Okazaki,Yasunari Shidama


Formal Verification of Merkle-Damgård Construction in ProVerif
Proc of The International Symposium on Information Theory and Its Applications(ISITA2020),:602-606 2021
Author:Mieno Takehiko, Yoshimura Togo, Hiroyuki Okazaki, Yuichi Futa, Kenichi Arai


Virtual Environment for Analysis and Evaluation of DDoS Attacks
Lecture Notes in Networks and Systems,227(3):459-468 2021
Author:Ryo Tokuyama, Yuichi Futa, Hikofumi Suzuki, Hiroyuki Okazaki


形式的安全性検証ツールを用いた暗号教育の実践とそのe-Learning教育化の課題について
コンピュータソフトウェア,37(1):99-113 2020
Author:岡崎 裕之, 紫村 彰吾,宮本 樹,渡邊 樹,布田 裕一,村上 恭通


Operations of Points on Elliptic Curve in Affine Coordinates
Formalized Mathematics,27(3):315-320 2019
Author:Yuichi Futa, Hiroyuki Okazaki, Yasunari Shidama


Formalization of Security Requirements and Attack Models for Cryptographic Hash Functions in ProVerif
The 2019 International Conference on Security and Management (SAM'19),:23-29 2019
Author:Togo Yoshimura, Kenichi Arai, Hiroyuki Okazaki, Yuichi Futa


Maximum Number of Steps Taken by Modular Exponentiation and Euclidean Algorithm
Formalized Mathematics,27(1):87-91 2019
Author:Hiroyuki Okazaki,Koh-ichi Nagao,Yuichi Futa


Suitable Models for Formal Security Verification of Cryptosystems in ProVerif
The International Symposium on Information Theory and Its Applications(ISITA2018),:326-330 2018
Author:Hiroyuki Okazaki, Yuichi Futa, Kenichi Arai


Binary Representation of Natural Numbers
Formalized Mathematics,26(3):223-229 2018
Author:Hiroyuki Okazaki


Formalization of Polynomially Bounded and Negligible Functions Using the Computer-Aided Proof-Checking System Mizar
2016 International Conference on Information and Knowledge Management (CIKM) FM4M/MathUI/ThEdu/DP/WIP@CIKM 2016,:117-131 2016
Author:Hiroyuki Okazaki, Yuichi Futa


Formalization of Statistical Indistinguishability of Probability Distribution Ensembles in Mizar
The International Symposium on Information Theory and Its Applications,:517-521 2016
Author:Hiroyuki Okazaki


Privacy Preserving Logic Formula Calculation in Cloud
2016 IEEE Tenth International Conference on Semantic Computing (ICSC),:329-332 2016
Author:Hiroshi Yamaguchi, Shigeo Tsujii, Hiroyuki Okazaki, Yasunari Shidama


Conservation Rules of Direct Sum Decomposition of Groups
Formalized Mathematics,24(1):81-94 2016
Author:Kazuhisa Nakasho, Hiroshi Yamazaki, Hiroyuki Okazaki, Yasunari Shidama


Algebra of Polynomially Bounded Sequences and Negligible Functions
Formalized Mathematics,23(4):371-378 2016
Author:Hiroyuki Okazaki


Torsion Part of ℤ-module
Formalized Mathematics,23(4):297-307 2016
Author:Yuichi Futa, Hiroyuki Okazaki, Yasunari Shidama


Polynomially Bounded Sequences and Polynomial Sequences
Formalized Mathematics,23(3):205-213 2015
Author:Hiroyuki Okazaki, Yuichi Futa


Equivalent Expressions of Direct Sum Decomposition of Groups
Formalized Mathematics,23(1):67-73 2015
Author:Kazuhisa Nakasho, Hiroyuki Okazaki, Hiroshi Yamazaki, Yasunari Shidama


Matrix of Z-module
Formalized Mathematics,23(1):29-49 2015
Author:Yuichi Futa, Hiroyuki Okazaki, Yasunari Shidama


Definition and Properties of Direct Sum Decomposition of Groups
Formalized Mathematics,23(1):15-27 2015
Author:Kazuhisa Nakasho, Hiroshi Yamazaki, Hiroyuki Okazaki, Yasunari Shidama


Torsion Z-module and Torsion-free Z-module
Formalized Mathematics,22(4):271-283 2014
Author:Yuichi Futa, Hiroyuki Okazaki, Kazuhisa Nakasho, Yasunari Shidama


Difference of Function on Vector Space over F
Formalized Mathematics,22(3):265-270 2014
Author:Kenichi Arai, Ken Wakabayashi, Hiroyuki Okazaki


Rank of Submodule, Linear Transformations and Linearly Independent Subsets of Z-module
Formalized Mathematics,22(3):189-198 2014
Author:Kazuhisa Nakasho, Yuichi Futa, Hiroyuki Okazaki, Yasunari Shidama


Formal definition of probability on finite and discrete sample space for proving security of cryptographic systems using Mizar
Artificial Intelligence Research,2(4):37-48 2013(Aug.)
Author:Okazaki, H; Futa, Y; Shidama, Y


Formalization of Definitions and Theorems Related to an Elliptic Curve Over a Finite Prime Field by Using Mizar
JOURNAL OF AUTOMATED REASONING,50(2):161-172 2013(Feb.)
Author:Futa, Y; Okazaki, H; Shidama, Y


Formalization of Binary Fields and N-dimensional Binary Vector Spaces Using the Mizar Proof Checker
2013 International Conference on Foundations of Computer Science (FCS'13),:71-77 2013
Author:Kenichi Arai, Hiroyuki Okazaki, Yasunari Shidama


Formalization Description of Huffman Coding Trees Using the Mizar
2013 International Conference on Foundations of Computer Science (FCS'13),:59-65 2013
Author:Takaya Ido, Hiroyuki Okazaki, Yasunari Shidama


Content Development for Distance Education in Advanced University Mathematics Using Mizar
The 2013 International Conference on e-Learning, e-Business, Enterprise Information Systems, and e-Government(EEE'13),:312-326 2013
Author:Takaya Ido, Hiroyuki Okazaki, Hiroshi YAMAZAKI, Pauline Naomi KAWAMOTO, Katsumi WASAKI, Yasunari Shidama


Submodule of free Z-module
Formalized Mathematics,21(4):273-282 2013
Author:Yuichi Futa, Hiroyuki Okazaki, Yasunari Shidama


Isomorphisms of Direct Products of Cyclic Groups of Prime-power Order
Formalized Mathematics,21(3):207-211 2013
Author:Hiroshi Yamazaki, Hiroyuki Okazaki, Kazuhisa Nakasho, Yasunari Shidama


Double Sequences and Limits
Formalized Mathematics,21(3):163-170 2013
Author:Noboru Endou, Hiroyuki Okazaki, Yasunari Shidama


Formalization of the Advanced Encryption Standard. Part I
Formalized Mathematics,21(3):171-184 2013
Author:Kenichi Arai, Hiroyuki Okazaki


Gaussian Integers
Formalized Mathematics,21(2):115-125 2013
Author:Yuichi Futa, Hiroyuki Okazaki, Daich Mizushima, Yasunari Shidama


Constructing Binary Huffman Tree
Formalized Mathematics,21(2):133-143 2013
Author:Hiroyuki Okazaki, Yuichi Futa, Yasunari Shidama


N-dimensional Binary Vector Spaces
Formalized Mathematics,21(2):75-81 2013
Author:Kenichi Arai, Hiroyuki Okazaki, Yasunari Shidama


Isomorphisms of Direct Products of Finite Commutative Groups
Formalized Mathematics,21(1):65-74 2013
Author:Hiroyuki Okazaki, Hiroshi Yamazaki, Yasunari Shidama


Random Variables and Product of Probability Spaces
Formalized Mathematics,21(1):33-39 2013
Author:Hiroyuki Okazaki, Yasunari Shidama


The C^k Space
Formalized Mathematics,21(1):25-31 2013
Author:Katuhiko Kanazashi, Hiroyuki Okazaki, Yasunari Shidama


Signature as Public Key Structured Cryptosystem and its Application
The 11th International Conference on Security and Management(SAM'12),:22-27 2012
Author:Kenichi Arai, Hiroyuki Okazaki


Formalization Verification of Number Theoretic Algorithms Using the Mizar Proof Checker
2012 International Conference on Foundations of Computer Science (FCS'12),:45-50 2012
Author:Hiroyuki Okazaki, Yoshiki Aoki, Yasunari Shidama


Formalization Verification of AES Using the Mizar Proof Checker
2012 International Conference on Foundations of Computer Science (FCS'12),:78-84 2012
Author:Hiroyuki Okazaki, Kenichi Arai, Yasunari Shidama


Formalization of Gaussian Integers, Gaussian Rational Numbers, and Their Algebraic Structures with Mizar
2012 International Symposium on Information Theory and its Applications (ISITA2012),:591-595 2012
Author:Yuichi Futa, Daichi Mizushima,Hiroyuki Okazaki


Banach's Continuous Inverse Theorem and Closed Graph Theorem
Formalized Mathematics,20(4):271-274 2012
Author:Hideki Sakurai, Hiroyuki Okazaki, Yasunari Shidama


Free Z-module
Formalized Mathematics,20(4):275-280 2012
Author:Yuichi Futa, Hiroyuki Okazaki, Yasunari Shidama


Isomorphisms of Direct Products of Finite Cyclic Groups
Formalized Mathematics,20(4):343-347 2012
Author:Kenichi Arai, Hiroyuki Okazaki, Yasunari Shidama


Posterior Probability on Finite Set
Formalized Mathematics,20(4):257-263 2012
Author:Hiroyuki Okazaki


Quotient Module of Z-module
Formalized Mathematics,20(3):205-214 2012
Author:Yuichi Futa, Hiroyuki Okazaki, Yasunari Shidama


Extended Euclidean Algorithm and CRT Algorithm
Formalized Mathematics,20(2):175-179 2012
Author:Hiroyuki Okazaki, Yoshiki Aoki,Yasunari Shidama


Higher-Order Partial Differentiation
Formalized Mathematics,20(2):113-124 2012
Author:Noboru Endou, Hiroyuki Okazaki, Yasunari Shidama


Formalization of the Data Encryption Standard
Formalized Mathematics,20(2):125-146 2012
Author:Hiroyuki Okazaki, Yasunari Shidama


Functional Space C(ω), C0(ω)
Formalized Mathematics,20(1):15-22 2012
Author:Katuhiko Kanazashi, Hiroyuki Okazaki, Yasunari Shidama


Z-modules
Formalized Mathematics,20(1):47-59 2012
Author:Yuichi Futa, Hiroyuki Okazaki, Yasunari Shidama


Operations of Points on Elliptic Curve in Projective Coordinates
Formalized Mathematics,20(1):87-95 2012
Author:Yuichi Futa, Hiroyuki Okazaki, Daichi Mizushima, Yasunari Shidama


Formalization Verification of DES Using the Mizar Proof Checker
2011 International Conference on Foundations of Computer Science,:63-68 2011(Jul.)
Author:Hiroyuki Okazaki, Kenichi Arai, Yasunari Shidama


Set of Points on Elliptic Curve in Projective Coordinates
Formalized Mathematics,19(3):131-138 2011
Author:Yuichi Futa, Hiroyuki Okazaki, Yasunari Shidama


Banach Algebra of Bounded Complex-Valued Functionals
Formalized Mathematics,19(2):121-126 2011
Author:Katuhiko Kanazashi, Hiroyuki Okazaki and Yasunari Shidama


Differentiable Functions into Real Normed Spaces
Formalized Mathematics,19(2):69-72 2011
Author:Hiroyuki Okazaki, Noboru Endou, Keiko Narita and Yasunari Shidama


Formalization of Integral Linear Space
Formalized Mathematics,19(1):61-64 2011
Author:Hiroyuki Okazaki, Noboru Endou and Yasunari Shidama


Cartesian Products of Family of Real Linear Spaces
Formalized Mathematics,19(1):51-59 2011
Author:Hiroyuki Okazaki, Noboru Endou and Yasunari Shidama


More on Continuous Functions on Normed Linear Spaces
Formalized Mathematics,19(1):45-49 2011
Author:Hiroyuki Okazaki, Noboru Endou and Yasunari Shidama


Normal Subgroup of Product of Groups
Formalized Mathematics,19(1):23-26 2011
Author:Hiroyuki Okazaki, Kenichi Arai, Yasunari Shidama


Formalization of Probability and Random Sampling on a Finite and Discrete Sample Space Using the Mizar Proof Checker
2010 International Conference on Foundations of Computer Science 2010(Jul.)
Author:Kenichi Arai, Nobuaki Kondo, Hiroyuki Okazaki


Probability Measure on Discrete Spaces and Algebra of Real Valued Random Variables
Formalized Mathematics,18(4):213-217 2010
Author:Hiroyuki Okazaki, Yasunari Shidama


Properties of Primes and Multiplicative Group of a Field
Formalized Mathematics,17(2):151-155 2009
Author:Kenichi Arai,Hiroyuki Okazaki


Probability on Finite Set and Real-Valued Random Variables
Formalized Mathematics,17(2):129-136 2009
Author:Hiroyuki Okazaki,Yasunari Shidama


Probability on Finite and Discrete Set and Uniform Distribution
Formalized Mathematics,17(2):173-178 2009
Author:Hiroyuki Okazaki


Hopf Extension Theorem of Measure
Formalized Mathematics,17(2):157-162 2009
Author:Noboru Endou, Hiroyuki Okazaki, Yasunari Shidama


Uniqueness of Factoring an Integer and Multiplicative Group Z/pZ*
Formalized Mathematics,16(2):103-107 2008
Author:Hiroyuki Okazaki,Yasunari Shidama


An evolutionary multiobjective approach to design highly non-linear Boolean functions
Genetic and Evolutionary Computation Conference (GECCO 2007),:749-756 2007
Author:Hernan E. Aguirre, Hiroyuki Okazaki, Yasushi Fuwa


A watermarking scheme using background pattern to protect printed documents
Proc. International Workshop on Nonlinear Circuits and Signal Processing (NCSP 2007) 2007
Author:Katsuki Kobayashi, Kiyoshi Tanaka, Hernan Aguirre, Hiroyuki Okazaki, Hisayoshi Kunimune,Katsumi Wasaki, Masaaki Niimura, Yasushi Fuwa


Preliminary Study on a Watermarking Scheme Using Background Pattern to Protect Printed Documents
Journal of Signal Processing,11(4):337-340 2007
Author:Katsuki Kobayashi,Heman Aguirre,Hiroyuki Okazaki,Kiyoshi Tanaka


Inferior Limit, Superior Limit and Convergence of Sequences of Extended Real Numbers
Formalized Mathematics,15(4):231-235 2007
Author:Hiroshi Yamazaki, Noboru Endou, Yasunari Shidama,Hiroyuki Okazaki


ヴェイユペアリングを用いた署名者の関連付けが可能なグループ署名方式
電子情報通信学会論文誌,J87-A(No.4):563~568 2004
Author:岡崎 裕之, 境 隆一, 柴山 潔, 笠原 正雄


合成数P^2Qの素因数分解に適した楕円曲線
日本応用数理学会論文誌,Vol.12(No.4):9~19 2002
Author:岡崎 裕之, 境 隆一, 笠原 正雄


講演・口頭発表等
オープンサイエンスにおける研究公正を追求するNextCloudカスタムアプリケーションの有用性の検討とGakuNinRDMとの比較
情報処理学会インターネットと運用技術研究会 2022(Mar. 08)
Presenter:藤岡碧志,岡崎裕之,鈴木彦文


ブロックチェーン技術を用いたDNSキャッシュポイズニング検知方式の評価
電子情報通信学会ICSS研究会 2022(Feb. 28)
Presenter:田中 健士朗, 布田 裕一, 岡崎裕之, 鈴木彦文


情報セキュリティ人材育成のための形式的安全性検証ツール学習用eラーニング環境の構築
第8回 実践的IT教育シンポジウム rePiT2022 2022
Presenter:大町 隆人, 岡崎 裕之, 布田 裕一, 村上 恭通


ProVerifによる検索可能暗号の形式的安全性検証について
2022年暗号と情報セキュリティシンポジウム(SCIS2022) 2022
Presenter:鈴木 孝誠, 山本 博章, 三重野 武彦, 荒井 研一, 岡崎 裕之, 布田 裕一


SVMによる工場ネットワークにおける偽装通信の検知手法のリアルタイム性の検証
2022年暗号と情報セキュリティシンポジウム(SCIS2022) 2022
Presenter:原田 雄基,布田 裕一, 岡崎 裕之


SDNを用いたDDoS攻撃に対する防御機構構築
2022年暗号と情報セキュリティシンポジウム(SCIS2022) 2022
Presenter:徳山 凌, 布田 裕一, 鈴木 彦文, 岡崎 裕之


SVMを用いた制御システムに対する偽装命令攻撃の検知
電子情報通信学会ISEC(研究会(ISEC2021-15) 2021(Jul. 19)
Presenter:原田雄基, 布田裕一, 岡崎裕之


GakuninRDMとオンプレミスNextCloudとの連携による研究不正対策基盤の構築と運用の提案
情報処理学会インターネットと運用技術研究会(IOT54) 2021(Jul. 09)
Presenter:藤岡碧志,岡崎裕之,鈴木彦文


第四世代鍵共有方式ID-NIKS IVを利用した新たな認証アーキテクチャ
第44回情報理論とその応用シンポジウム(SITA2021) 2021
Presenter:三重野 武彦, 岡崎 裕之, 布田 裕一, 村上 恭通


ProVerifを用いたスポンジ構造の形式化
2021年暗号と情報セキュリティシンポジウム(SCIS2021) 2021
Presenter:吉村 東悟,荒井 研一,岡崎 裕之,布田 裕一,三重野 武彦


制御システムにおける異常検知手法とデータセットの評価
2021年暗号と情報セキュリティシンポジウム(SCIS2021) 2021
Presenter:原田 雄基, 布田 裕一, 岡崎 裕之


モデル検査器ProVerifによるDES暗号の形式化
2020年電子情報通信学会総合大会 2020
Presenter:磯貝 百恵,岡崎 裕之,荒井 研一,布田 裕一,三重野武彦


協調型DNSによるキャッシュポイズニングの検知
2020年暗号と情報セキュリティシンポジウム(SCIS2020) 2020
Presenter:高橋 幸宏,布田 裕一,岡崎 裕之,鈴木 彦文


ProVerifを用いたMD変換の形式化
2020年暗号と情報セキュリティシンポジウム(SCIS2020) 2020
Presenter:吉村 東悟,荒井 研一,岡崎 裕之,布田 裕一,三重野 武彦


DRDoS攻撃の分析及び検証のための仮想環境構築
2020年暗号と情報セキュリティシンポジウム(SCIS2020) 2020
Presenter:徳山 凌,布田 裕一,鈴木 彦文,岡崎 裕之


ProVerifを用いたMD変換の形式化
日本応用数理学会 2020年度 年会 2020
Presenter:吉村 東悟,荒井 研一,岡崎 裕之,布田 裕一,三重野 武彦


Mizarによる離散確率分布の統計的識別不能性の形式化
日本応用数理学会 2019年度 年会 予稿集 2019
Presenter:岡崎 裕之, 布田 裕一, 師玉 康成


LLLアルゴリズムを用いたUTMトラフィックログの解析
信学技報,NS2019-124 27-30 2019
Presenter:森田 拓哉,鈴木 彦文, 岡崎 裕之


決定木を用いたUTMログ解析によるDDoS攻撃検知の試み
信学技報,NS2019-123 19-25 2019
Presenter:藤岡 碧志,岡崎 裕之,鈴木 彦文


ブロックチェーン技術を用いたDNSキャッシュポイズニング対策の検討
信学技報,ISEC2019-78 2019
Presenter:高橋 幸宏,布田 裕一,岡﨑 裕之,鈴木 彦文


Formalization of Security Requirements and Attack Models for Cryptographic Hash Functions in ProVerif
The 2019 International Conference on Security and Management (SAM'19) 2019
Presenter:Togo Yoshimura, Kenichi Arai, Hiroyuki Okazaki, Yuichi Futa


認証ログをライフログとして用いた安否確認システムの開発
ICSS研究会 ICSS2019 6 27-30 2019
Presenter:森田 拓哉, アサノ デービッド, 鈴木 彦文, 岡崎 裕之


形式的安全性検証ツールを用いた暗号教育の実践とそのe-Learning教材化の課題について
第5回 実践的IT教育シンポジウム rePiT2019 in 愛媛 2019
Presenter:紫村 彰吾, 岡崎 裕之, 宮本 樹, 渡邊 樹, 布田 裕一, 村上 恭通


ProVerifを用いたCT及びブロックチェーンの形式化
2019年 暗号と情報セキュリティシンポジウム 2019
Presenter:荒井 研一, 岡崎 裕之, 布田 裕一


Formalization of Security Requirements and Attack Models for Cryptographic Hash Functions in ProVerif
The 2019 International Conference on Security and Management (SAM'19) 2019
Presenter:Togo Yoshimura, Kenichi Arai, Hiroyuki Okazaki, Yuichi Futa


Moodleを用いたProverifのeラーニングシステム
第41回情報理論とその応用シンポジウム(SITA2018) 2018
Presenter:渡邊 樹,宮本 樹,紫村彰吾,岡崎裕之,布田裕一,村上恭通


e-Learning System for Cryptography on Moodle
Internet Conference 2018 (IC2018) 2018
Presenter:Tatsuki Miyamoto, Shogo Shimura, Tatsuki Watanabe, Hiroyuki Okazaki, Yuichi Futa, Yasuyuki Murakami


Suitable Models for Formal Security Verification of Cryptosystems in ProVerif
The International Symposium on Information Theory and Its Applications(ISITA2018) 2018
Presenter:Hiroyuki Okazaki, Yuichi Futa, Kenichi Arai


ProVerif を 用いたTLS1.3ハンドシェイクプロ トコルの形式検証
日本応用数理学会2018年度年会 2018
Presenter:荒井 研一, 岡崎 裕之, 布田 裕一


ProVerifを用いたCTの形式化
2018年 暗号と情報セキュリティシンポジウム 2018
Presenter:荒井 研一, 岡崎 裕之, 布田 裕一


ProVerifにおけるphaseについて
2017年 暗号と情報セキュリティシンポジウム 2017
Presenter:荒井 研一, 岡崎 裕之, 布田 裕一


Formalization of Polynomially Bounded and Negligible Functions Using the Computer-Aided Proof-Checking System Mizar
2016 International Conference on Information and Knowledge Management (CIKM) FM4M/MathUI/ThEdu/DP/WIP@CIKM 2016 2016
Presenter:Hiroyuki Okazaki, Yuichi Futa


ProVerifでの形式化における技術的な注意点について
日本応用数理学会2016年度年会 2016
Presenter:荒井 研一, 岡崎 裕之


Proverifを用いた暗号プリミティブの形式化
2016年 暗号と情報セキュリティシンポジウム 2016
Presenter:岡崎 裕之,荒井 研一


Formalization of Statistical Indistinguishability of Probability Distribution Ensembles in Mizar
The International Symposium on Information Theory and Its Applications 517-521 2016
Presenter:Hiroyuki Okazaki


Privacy Preserving Logic Formula Calculation in Cloud
2016 IEEE Tenth International Conference on Semantic Computing (ICSC) 2016
Presenter:Hiroshi Yamaguchi, Shigeo Tsujii, Hiroyuki Okazaki, Yasunari Shidama


MizarによるProbability Distribution Ensemble の形式定義について
日本応用数理学会2015年度年会 2015
Presenter:岡崎 裕之, 布田 裕一


Mizarによる多項式オーダー関数の形式化
2015年 暗号と情報セキュリティシンポジウム 2015
Presenter:岡崎裕之, 布田裕一, 師玉康成


Negligibleの形式定義に関する考察
2014年 暗号と情報セキュリティシンポジウム 2014
Presenter:岡崎 裕之, 布田 裕一


符号化の形式記述についての考察
2013年 暗号と情報セキュリティシンポジウム 2013
Presenter:岡崎裕之, 師玉康成


Formalization of Binary Fields and N-dimensional Binary Vector Spaces Using the Mizar Proof Checker
2013 International Conference on Foundations of Computer Science (FCS'13) 2013
Presenter:Kenichi Arai, Hiroyuki Okazaki, Yasunari Shidama


Formalization Description of Huffman Coding Trees Using the Mizar
2013 International Conference on Foundations of Computer Science (FCS'13) 2013
Presenter:Takaya Ido, Hiroyuki Okazaki, Yasunari Shidama


Content Development for Distance Education in Advanced University Mathematics Using Mizar
The 2013 International Conference on e-Learning, e-Business, Enterprise Information Systems, and e-Government(EEE'13) 2013
Presenter:Takaya Ido, Hiroyuki Okazaki, Hiroshi YAMAZAKI, Pauline Naomi KAWAMOTO, Katsumi WASAKI, Yasunari Shidama


Mizarによる離散確率の形式化についての考察
日本応用数理学会2012年度年会 2012
Presenter:岡崎裕之, 師玉康成


Mizarによる数論アルゴリズムの形式化と検証
2012年 暗号と情報セキュリティシンポジウム 2012
Presenter:青木祥希, 岡崎裕之, 師玉康成


形式化数学記述言語 Mizar による楕円曲線の形式化
2012年 暗号と情報セキュリティシンポジウム 2012
Presenter:水島大地, 布田裕一, 岡崎裕之


Mizarによる大学数学向け高度遠隔教育用コンテンツ開発
教育工学研究会 ET2012 55 13~17 2012
Presenter:井戸 貴也,岡崎 裕之,山崎 浩,師玉 康成


Signature as Public Key Structured Cryptosystem and its Application
The 11th International Conference on Security and Management(SAM'12) 2012
Presenter:Kenichi Arai, Hiroyuki Okazaki


Formalization Verification of Number Theoretic Algorithms Using the Mizar Proof Checker
2012 International Conference on Foundations of Computer Science (FCS'12) 2012
Presenter:Hiroyuki Okazaki, Yoshiki Aoki, Yasunari Shidama


Formalization Verification of AES Using the Mizar Proof Checker
2012 International Conference on Foundations of Computer Science (FCS'12) 2012
Presenter:Hiroyuki Okazaki, Kenichi Arai, Yasunari Shidama


Formalization of Gaussian Integers, Gaussian Rational Numbers, and Their Algebraic Structures with Mizar
2012 International Symposium on Information Theory and its Applications (ISITA2012) 2012
Presenter:Yuichi Futa, Daichi Mizushima,Hiroyuki Okazaki


ProVerif を用いたPolicy-based Chameleon Hashによる修正可能なブロックチェーンの形式化
日本応用数理学会 2021年度 年会 2011(Sep. 07)
Presenter:杉山 航平, 荒井 研一,岡崎 裕之,布田 裕一,三重野 武彦


Formalization Verification of DES Using the Mizar Proof Checker
2011 International Conference on Foundations of Computer Science 2011(Jul.)
Presenter:Hiroyuki Okazaki, Kenichi Arai, Yasunari Shidama


形式化数学記述言語 Mizar によるガウス整数環の形式化
第34回情報理論とその応用シンポジウム(SITA2011) 2011
Presenter:水島大地,布田裕一,岡崎裕之


Mizarによる素体上の楕円曲線の形式化
第 9 回「代数学と計算」研究集会 2011
Presenter:布田裕一, 岡崎裕之, 師玉康成


Mizarによる有限かつ離散的な標本空間における確率の形式化
2011年 暗号と情報セキュリティシンポジウム 2011
Presenter:岡崎 裕之,荒井 研一


Mizarによる数論アルゴリズムの形式化と検証
ライフインテリジェンスとオフィス情報システム研究会 LOIS2011 38 69~74 2011
Presenter:青木 祥希,岡崎 裕之,師玉 康成


Formalization of Probability and Random Sampling on a Finite and Discrete Sample Space Using the Mizar Proof Checker
2010 International Conference on Foundations of Computer Science 2010(Jul.)
Presenter:Kenichi Arai, Nobuaki Kondo, Hiroyuki Okazaki


形式化数学記述言語MizarによるDESの形式化
2010年 暗号と情報セキュリティシンポジウム 2010
Presenter:小林 亮太, 荒井 研一, 岡崎 裕之, 師玉 康成


電力線搬送通信における攻撃手法の考察
2010年 暗号と情報セキュリティシンポジウム 2010
Presenter:名取 諒, 岡崎 裕之


無線端末位置推定法Gomashioの改良
情報科学技術フォーラム講演論文集 8 4 383-386 2009
Presenter:武田 浩志 , 岡崎 裕之


署名公開鍵型公開鍵暗号方式に関する考察
2009年 暗号と情報セキュリティシンポジウム 2009
Presenter:荒井 研一, 岡崎 裕之


ペアリングを用いた三者間Diffie-Hellman プロトコルの安全性検証
2009年 暗号と情報セキュリティシンポジウム 2009
Presenter:清澤 勇貴,岡崎 裕之,荒井 研一


Mizarによる確率と分布の形式的定義
2009年 暗号と情報セキュリティシンポジウム 2009
Presenter:岡崎裕之


CryptoVerifのためのAuthenticated Encryptionの安全性の定式化に関する考察
2008年 暗号と情報セキュリティシンポジウム 2008
Presenter:荒井 研一,岡崎 裕之,不破 泰


IPアドレスを持たないネットワーク機器との通信手法について
2008年 暗号と情報セキュリティシンポジウム 2008
Presenter:清澤 勇貴,岡崎 裕之,荒井 研一,國宗 永佳,不破 泰


背景パターンを用いた印刷文書向け電子透かしの一手法
2007年 暗号と情報セキュリティシンポジウム 2007
Presenter:小林 克樹,田中 清,エルナン アギレ,岡崎 裕之,國宗 永佳,和崎 克己,新村 正明,不破 泰


An evolutionary multiobjective approach to design highly non-linear Boolean functions
Genetic and Evolutionary Computation Conference (GECCO 2007) 2007
Presenter:Hernan E. Aguirre, Hiroyuki Okazaki, Yasushi Fuwa


A watermarking scheme using background pattern to protect printed documents
Proc. International Workshop on Nonlinear Circuits and Signal Processing (NCSP 2007) 2007
Presenter:Katsuki Kobayashi, Kiyoshi Tanaka, Hernan Aguirre, Hiroyuki Okazaki, Hisayoshi Kunimune,Katsumi Wasaki, Masaaki Niimura, Yasushi Fuwa


メタ暗号系に関する考察
2007年 暗号と情報セキュリティシンポジウム 2007
Presenter:岡崎裕之


Mizarによる暗号技術教材の形式化記述について
日本Mizar学会秋季総会 2006
Presenter:岡崎裕之


署名者同一性検証についての考察
第 6 回「代数学と計算」 2005
Presenter:岡崎裕之


メタリング署名
情報セキュリティ研究会 ISEC2005 36 201~204 2005
Presenter:岡崎 裕之, 境 隆一, 笠原 正雄


匿名著作権署名
2005年暗号と情報セキュリティ・シンポジウム 2005
Presenter:岡崎 裕之, 境 隆一, 柴山 潔, 笠原 正雄


メタ署名に関する考察
2006年 暗号と情報セキュリティシンポジウム 2005
Presenter:岡崎裕之


ペアリングを用いた匿名著作権署名方式に関する2,3の考察
「数論アルゴリズムとその応用」研究部会第13回研究集会 2004
Presenter:岡崎裕之


ペアリングを用いた効率のよいグループ署名
2003年暗号と情報セキュリティ・シンポジウム 2003
Presenter:岡崎 裕之, 境 隆一, 柴山 潔, 笠原 正雄


リンク可能なグループ署名に関する考察
情報セキュリティ研究会 ISEC2003 55 35~38 2003
Presenter:岡崎 裕之, 境 隆一, 柴山 潔, 笠原 正雄


ヴェイユペアリングを用いたグループ署名
第5回「代数学と計算」研究集会 2003
Presenter:岡崎 裕之, 境 隆一, 柴山 潔,笠原 正雄


ペアリングを用いたグループ署名
2002年暗号と情報セキュリティ・シンポジウム 14B-2 2002
Presenter:岡崎 裕之, 境 隆一, 笠原 正雄


ペアリングを用いたグループ署名に関する2,3の考察
情報セキュリティ研究会 ISEC2002 64 53~60 2002
Presenter:岡崎 裕之, 境 隆一, 柴山 潔, 笠原 正雄


合成数p^2q の素因数分解に適した楕円曲線に関する二、三の考察
2001年暗号と情報セキュリティ・シンポジウム 14B-1 2001
Presenter:岡崎 裕之, 境 隆一, 笠原 正雄


乗算型公開鍵暗号に関する二,三の考察
2001年情報理論とその応用シンポジウム 2001
Presenter:岡崎 裕之, 村上 恭通, 笠原 正雄


ベイユ・テイトペアリングを用いたグループ署名
情報セキュリティ研究会 ISEC2001 108 105~108 2001
Presenter:境 隆一, 岡崎 裕之, 笠原 正雄


ある種の素因数分解に適した楕円曲線に関する二,三の考察
2000年暗号と情報セキュリティ・シンポジウム 2000
Presenter:岡崎 裕之, 堀内 啓次, 境 隆一, 笠原 正雄


MISC
Formal Definition of Probability and Probabilistic Function on Finite and Discrete Sample Space for Proving Security of Cryptographic Systems Using Mizar.
2011 Joint Mathematics Meetings (JMM2011),(1067-94-740):156 2011(Jan. 09)
Author:Hiroyuki Okazaki, Yasunari Shidama,Yuichi Futa


Meta Ring Signature Scheme
Cryptology ePrint Archive,(2005/310) 2005
Author:H. Okazaki, R. Sakai and M.Kasahara

研究費
共同研究
2019 - , IoTデバイス間相互認証方法の研究

科学研究費補助金(研究代表者)
2017 - 2020 , 形式手法による暗号の安全性証明自動検証システムの開発 , 基盤研究(C)

科学研究費補助金(研究分担者)
2018 - 2020 , 情報セキュリティ人材育成のための暗号技術学習支援eラーニングシステムの開発 , 基盤研究(C)
2010 - 2013 , MIZAR数学ライブラリの構築と大学数学向け高度遠隔教育用コンテンツ開発 , 基盤研究(B)
2009 - 2014 , センサネットワークの安全・安心を保証する情報セキュリティ技術の研究 , 基盤研究(A)
2007 - 2010 , 自学自習型e-Learningにおける学生サポートシステムの開発に関する研究 , 基盤研究(B)
研究諸活動
学術論文査読件数
2006- , 電子情報通信学会
2006- , 日本応用数理学会

管理運営実績

管理運営実績
学部内委員会等
2005 - , 環境委員会 , 情報工学科環境委員
内部監査委員会 , 環境ISO内部監査員