FUTA Yuichi 布田裕一

Researcher Number	50706223
Other IDs
Affiliation (Current)	2025: 東京工科大学, コンピュータサイエンス学部, 教授
Affiliation (based on the past Project Information) *help	2020 – 2023: 東京工科大学, コンピュータサイエンス学部, 教授 2016 – 2020: 東京工科大学, コンピュータサイエンス学部, 准教授 2015: 北陸先端科学技術大学院大学, 情報科学研究科, 准教授 2013: 北陸先端科学技術大学院大学, 情報科学研究科, 准教授
Review Section/Research Field	Principal Investigator Basic Section 60050:Software-related / Information security Except Principal Investigator Basic Section 60020:Mathematical informatics-related / Basic Section 09070:Educational technology-related / Information security / Educational technology
Keywords	Principal Investigator 観測等価性 / DDoS攻撃 / 仮想化技術 / セキュリティ評価 / 非線形変換 / 難読化技術 / ProVerif / 形式検証 / 耐タンパー技術 / White-Box Cryptography … More Except Principal Investigator … More ProVerif / Mizar / ICT技術者 / Virtual Programming Lab / Proverif / CAI教材 / 形式的暗号プロトコル安全性検証ツール / Virtual Programing Lab / Moodle / 安全性自動検証 / 形式化 / eラーニングシステム / 暗号技術学習支援 / 情報セキュリティ人材育成 / 応用数学 / 暗号・認証等 / 攻撃モデル形式化 / アルゴリズムのステップ数形式化 / 統計的識別不能性形式化 / 繰り返しおよび再帰形式化 / 安全性要件形式化 / アルゴリズムの計算量形式化 / 暗号システム / 安全性証明 / 形式検証 / モデル検査 / 形式的定理証明 / 形式的安全性検証 / 暗号理論 / 計算機による検査 / 証明記述問題 / プルーフチェッカー / e-learning教材 / moodle / 論理思考 / 定理証明支援系 / 形式化数学 / e-learning / プルーフチェッカ / eラーニング Less

形式手法を用いた数論アルゴリズムの設計支援システムの開発
- Principal Investigator
  
  長尾孝一
- Project Period (FY)
  2022 – 2025
- Research Category
  
  Grant-in-Aid for Scientific Research (C)
- Review Section
  
  Basic Section 60020:Mathematical informatics-related
- Research Institution
  Kanto Gakuin University
ネットワークシステムのセキュリティで等価な仮想評価環境の構築Principal Investigator
- Principal Investigator
  
  布田裕一
- Project Period (FY)
  2022 – 2025
- Research Category
  
  Grant-in-Aid for Scientific Research (C)
- Review Section
  
  Basic Section 60050:Software-related
- Research Institution
  Tokyo University of Technology
Development of e-learning system for human resource development in the information security field
- Principal Investigator
  
  Murakami Yasuyuki
- Project Period (FY)
  2018 – 2021
- Research Category
  
  Grant-in-Aid for Scientific Research (C)
- Review Section
  
  Basic Section 09070:Educational technology-related
- Research Institution
  Osaka Electro-Communication University
Developing Automated formal Verification System for Cryptology
- Principal Investigator
  
  Okazaki Hiroyuki
- Project Period (FY)
  2017 – 2020
- Research Category
  
  Grant-in-Aid for Scientific Research (C)
- Research Field
  
  Information security
- Research Institution
  Shinshu University
Study on tamper-resistant software technology with theoretic security evaluationPrincipal Investigator
- Principal Investigator
  
  FUTA Yuichi
- Project Period (FY)
  2015 – 2018
- Research Category
  
  Grant-in-Aid for Scientific Research (C)
- Research Field
  
  Information security
- Research Institution
  Tokyo University of Technology
  Japan Advanced Institute of Science and Technology
Content Development for Distance Education in Advanced University Mathematics Using Mizar
- Principal Investigator
  
  SHIDAMA Yasunari
- Project Period (FY)
  2010 – 2013
- Research Category
  
  Grant-in-Aid for Scientific Research (B)
- Research Field
  
  Educational technology
- Research Institution
  Shinshu University

All 2024 2023 2022 2021 2020 2019 2018 2017 2015 2014 2013 2012 2011

All Journal Article Presentation

[Journal Article] How to Formalize Loop Iterations in Cryptographic Protocols Using ProVerif2024
- Author(s)
  Takehiko MIENO, Hiroyuki OKAZAKI, Kenichi ARAI, Yuichi FUTA
- Journal Title
  
  IEEE Access
  
  Volume: 12 Pages: 31605-31625
- DOI
  10.1109/access.2024.3368453
- Peer Reviewed / Open Access
- Data Source
  KAKENHI-PROJECT-22K11982
[Journal Article] Inverse Function Theorem. Part I2021
- Author(s)
  Kazuhisa Nakasho, Yuichi Futa
- Journal Title
  
  FORMALIZED MATHEMATICS
  
  Volume: 29(1) Issue: 1 Pages: 9-20
- DOI
  10.2478/forma-2021-0002
- Peer Reviewed / Open Access
- Data Source
  KAKENHI-PROJECT-17K00182, KAKENHI-PROJECT-20K19863
[Journal Article] Formal Verification of Merkle-Damgård Construction in ProVerif2020
- Author(s)
  Takehiko Mieno, Togo Yoshimura, Hiroyuki Okazaki, Yuichi Futa, Kenichi Arai
- Journal Title
  
  IEICE Proceeding Series
  
  Volume: 65 Pages: 602-606
- DOI
  10.34385/proc.65.E03-2
- NAID
  230000012659
- ISSN
  2188-5079
- Year and Date
  2020-10-18
- Language
  English
- Peer Reviewed
- Data Source
  KAKENHI-PROJECT-18K02917
[Journal Article] Educating Cryptography using Formal Security Verification tool for Cryptographic Protocols2020
- Author(s)
  岡崎裕之、紫村彰吾、宮本樹、渡邊樹、布田裕一、村上恭通
- Journal Title
  
  Computer Software
  
  Volume: 37 Issue: 1 Pages: 1_99-1_113
- DOI
  10.11309/jssst.37.1_99
- NAID
  130007801473
- ISSN
  0289-6540
- Year and Date
  2020-01-24
- Language
  Japanese
- Peer Reviewed / Open Access
- Data Source
  KAKENHI-PROJECT-17K00182, KAKENHI-PROJECT-18K02917
[Journal Article] Maximum Number of Steps Taken by Modular Exponentiation and Euclidean Algorithm2019
- Author(s)
  Hiroyuki Okazaki, Koh-ichi Nagao and Yuichi Futa
- Journal Title
  
  Formalized Mathematics
  
  Volume: 27 Issue: 1 Pages: 87-91
- DOI
  10.2478/forma-2019-0009
- Peer Reviewed / Open Access
- Data Source
  KAKENHI-PROJECT-15K00183, KAKENHI-PROJECT-17K00182
[Journal Article] Operations of Points on Elliptic Curve in Affine Coordinates2019
- Author(s)
  Futa Yuichi、Okazaki Hiroyuki、Shidama Yasunari
- Journal Title
  
  Formalized Mathematics
  
  Volume: 27 Issue: 3 Pages: 315-320
- DOI
  10.2478/forma-2019-0026
- Peer Reviewed / Open Access
- Data Source
  KAKENHI-PROJECT-17K00182
[Journal Article] Continuity of Bounded Linear Operators on Normed Linear Spaces2018
- Author(s)
  Nakasho Kazuhisa、Futa Yuichi、Shidama Yasunari
- Journal Title
  
  Formalized Mathematics
  
  Volume: 26 Issue: 3 Pages: 231-237
- DOI
  10.2478/forma-2018-0021
- Peer Reviewed / Open Access
- Data Source
  KAKENHI-PROJECT-17K00182
[Journal Article] Dual Lattice of Z-module Lattice2017
- Author(s)
  Yuichi Futa and Yasunari Shidama
- Journal Title
  
  Formalized Mathematics
  
  Volume: 25 Issue: 2 Pages: 157-169
- DOI
  10.1515/forma-2017-0015
- Peer Reviewed / Open Access
- Data Source
  KAKENHI-PROJECT-15K00183
[Journal Article] Isomorphism Theorem on Vector Spaces over a Ring2017
- Author(s)
  Yuichi Futa and Yasunari Shidama
- Journal Title
  
  Formalized Mathematics
  
  Volume: 25 Issue: 3 Pages: 171-178
- DOI
  10.1515/forma-2017-0016
- Peer Reviewed / Open Access
- Data Source
  KAKENHI-PROJECT-15K00183
[Journal Article] Implicit Function Theorem. Part I2017
- Author(s)
  Nakasho Kazuhisa、Futa Yuichi、Shidama Yasunari
- Journal Title
  
  Formalized Mathematics
  
  Volume: 25 Issue: 4 Pages: 269-281
- DOI
  10.1515/forma-2017-0026
- Peer Reviewed / Open Access
- Data Source
  KAKENHI-PROJECT-17K00182
[Journal Article] Embedded Lattice and Properties of Gram Matrix2017
- Author(s)
  Yuichi Futa and Yasunari Shidama
- Journal Title
  
  Formalized Mathematics
  
  Volume: 25 Issue: 1 Pages: 73-86
- DOI
  10.1515/forma-2017-0007
- Peer Reviewed / Acknowledgement Compliant / Open Access / Int'l Joint Research
- Data Source
  KAKENHI-PROJECT-15K00183
[Journal Article] Submodule of free Z-module2014
- Author(s)
  Yuichi Futa, Hiroyuki Okazaki, Yasunari Shidama
- Journal Title
  
  Formalized Mathematics
  
  Volume: 21(4) Issue: 4 Pages: 275-284
- DOI
  10.2478/forma-2013-0029
- NAID
  120007101157
- Peer Reviewed
- Data Source
  KAKENHI-PROJECT-21240001, KAKENHI-PROJECT-22300285
[Journal Article] Constructing Binary Huffman Tree2013
- Author(s)
  Hiroyuki Okazaki, Yuichi Futa, Yasunari Shidama
- Journal Title
  
  Formalized Mathematics
  
  Volume: 21(2) Issue: 2 Pages: 133-143
- DOI
  10.2478/forma-2013-0015
- NAID
  120007101135
- Peer Reviewed
- Data Source
  KAKENHI-PROJECT-22300285
[Journal Article] Formalization of Definitions and Theorems Related to an Elliptic Curve Over a Finite Prime Field by Using Mizar2013
- Author(s)
  Yuichi Futa, Hiroyuki Okazaki, Yasunari Shidama
- Journal Title
  
  Journal of Automated Reasoning
  
  Volume: 50(2) Issue: 2 Pages: 161-172
- DOI
  10.1007/s10817-012-9265-2
- NAID
  120007105033
- Peer Reviewed
- Data Source
  KAKENHI-PROJECT-22300285
[Journal Article] Formal Definition of Probability on Finite and Discrete Sample Space for Proving Security of Cryptographic Systems Using Mizar2013
- Author(s)
  Hiroyuki Okazaki, Yuichi Futa, Yasunari Shidama
- Journal Title
  
  Artificial Intelligence Research
  
  Volume: 2(4) Issue: 4 Pages: 37-48
- DOI
  10.5430/air.v2n4p37
- NAID
  120007105032
- Peer Reviewed
- Data Source
  KAKENHI-PROJECT-21240001, KAKENHI-PROJECT-22300285
[Journal Article] Gaussian Integers2013
- Author(s)
  Yuichi Futa, Hiroyuki Okazaki, Daich Mizushima, Yasunari Shidama
- Journal Title
  
  Formalized Mathematics
  
  Volume: 21(2) Issue: 2 Pages: 115-125
- DOI
  10.2478/forma-2013-0013
- NAID
  120007101136
- Peer Reviewed
- Data Source
  KAKENHI-PROJECT-21240001, KAKENHI-PROJECT-22300285
[Journal Article] Isometric Differentiable Functions on Real Normed Space2013
- Author(s)
  Yuichi Futa, Noboru Endou, Yasunari Shidama
- Journal Title
  
  Formalized Mathematics
  
  Volume: 21(4) Issue: 4 Pages: 249-260
- DOI
  10.2478/forma-2013-0027
- NAID
  120007101146
- Peer Reviewed
- Data Source
  KAKENHI-PROJECT-22300285, KAKENHI-PROJECT-23500029
[Journal Article] Quotient Module of Z-module2012
- Author(s)
  Yuichi Futa, Hiroyuki Okazaki, Yasunari Shidama
- Journal Title
  
  Formalized Mathematics
  
  Volume: 20(3) Issue: 3 Pages: 205-214
- DOI
  10.2478/v10037-012-0024-y
- NAID
  120007101128
- Peer Reviewed
- Data Source
  KAKENHI-PROJECT-22300285
[Journal Article] Operations of Points on Elliptic Curve in Projective Coordinates2012
- Author(s)
  Yuichi Futa, Hiroyuki Okazaki, Daichi Mizushima, Yasunari Shidama
- Journal Title
  
  Formalized Mathematics
  
  Volume: 20(1) Issue: 1 Pages: 87-95
- DOI
  10.2478/v10037-012-0012-2
- NAID
  120007101132
- Peer Reviewed
- Data Source
  KAKENHI-PROJECT-22300285
[Journal Article] Free Z-module2012
- Author(s)
  Yuichi Futa, Hiroyuki Okazaki, Yasunari Shidama
- Journal Title
  
  Formalized Mathematics
  
  Volume: 20(4) Issue: 4 Pages: 257-280
- DOI
  10.2478/v10037-012-0033-x
- NAID
  120007101126
- Peer Reviewed
- Data Source
  KAKENHI-PROJECT-22300285
[Journal Article] Z-modules2012
- Author(s)
  Yuichi Futa, Hiroyuki Okazaki, Yasunari Shidama
- Journal Title
  
  Formalized Mathematics
  
  Volume: 20(1) Issue: 1 Pages: 47-59
- DOI
  10.2478/v10037-012-0007-z
- NAID
  120007101141
- Peer Reviewed
- Data Source
  KAKENHI-PROJECT-22300285
[Journal Article] Formalization of Integral Linear Space2011
- Author(s)
  Yuichi Futa, Hiroyuki Okazaki, Yasunari Shidama
- Journal Title
  
  Formalized Mathematics
  
  Volume: 19(1) Issue: 1 Pages: 61-64
- DOI
  10.2478/v10037-011-0010-9
- NAID
  120007101115
- Peer Reviewed
- Data Source
  KAKENHI-PROJECT-22300285
[Presentation] AES暗号処理装置に対する増分故障解析の攻撃検証と評価2023
- Author(s)
  玉川未蘭, 布田裕一, 三重野武彦, 岡崎裕之
- Organizer
  情報通信システムセキュリティ研究会 (ICSS), ICSS2023-56
- Data Source
  KAKENHI-PROJECT-22K11982
[Presentation] DNSログを用いたDNSキャッシュポイズニング攻撃検知手法のシミュレーション2023
- Author(s)
  田中健士朗, 布田裕一, 岡崎裕之, 鈴木彦文
- Organizer
  情報通信システムセキュリティ研究会 (ICSS), ICSS2023-64
- Data Source
  KAKENHI-PROJECT-22K11982
[Presentation] ブラウザフィンガープリントを用いた端末識別と特徴点の考察2023
- Author(s)
  塚崎崇至, 布田裕一, 岡崎裕之, 鈴木彦文
- Organizer
  情報通信システムセキュリティ研究会 (ICSS), ICSS2023-53
- Data Source
  KAKENHI-PROJECT-22K11982
[Presentation] 制御システムにおけるリプレイ攻撃に対するリアルタイム検知2023
- Author(s)
  西浩志, 布田裕一, 岡崎裕之
- Organizer
  情報通信システムセキュリティ研究会 (ICSS), ICSS2023-52
- Data Source
  KAKENHI-PROJECT-22K11982
[Presentation] DDoS攻撃によるSnortと正規ユーザーへの影響分析2023
- Author(s)
  鹿野湧生. 布田裕一, 鈴木彦文, 岡崎裕之
- Organizer
  情報通信システムセキュリティ研究会 (ICSS), ICSS2023-65
- Data Source
  KAKENHI-PROJECT-22K11982
[Presentation] DDoS攻撃によるSnortの影響分析2023
- Author(s)
  鹿野湧生. 布田裕一, 鈴木彦文, 岡崎裕之
- Organizer
  情報通信システムセキュリティ研究会 (ICSS), ICSS2023-30
- Data Source
  KAKENHI-PROJECT-22K11982
[Presentation] ブラウザフィンガープリントを用いたリスクベース認証における有効な特徴点の分析2023
- Author(s)
  塚崎崇至, 布田裕一, 岡崎裕之, 鈴木彦文
- Organizer
  情報通信システムセキュリティ研究会 (ICSS), ICSS2023-16
- Data Source
  KAKENHI-PROJECT-22K11982
[Presentation] リプレイ攻撃を含む通信データセットに対する機械学習を用いた異常検知2023
- Author(s)
  西浩志, 布田裕一, 岡崎裕之
- Organizer
  情報通信システムセキュリティ研究会 (ICSS), ISEC2023-52
- Data Source
  KAKENHI-PROJECT-22K11982
[Presentation] SVM による工場ネットワークにおける偽装通信の検知手法のリアルタイム性の検証2022
- Author(s)
  原田雄基. 布田裕一 , 岡崎裕之
- Organizer
  2022年暗号と情報セキュリティシンポジウム SCIS2022
- Data Source
  KAKENHI-PROJECT-18K02917
[Presentation] 制御システムにおける多地点パケットキャプチャを利用した異常検知2022
- Author(s)
  西浩志, 布田裕一, 鈴木智道, 岡崎裕之
- Organizer
  研究報告コンピュータセキュリティ（CSEC） , 2022-CSEC-99
- Data Source
  KAKENHI-PROJECT-22K11982
[Presentation] ブロックチェーン技術を用いたDNSキャッシュポイズニング検知方式の評価2022
- Author(s)
  田中健士朗, 布田裕一, 岡崎裕之, 鈴木彦文
- Organizer
  電子情報通信学会 ICSS研究会
- Data Source
  KAKENHI-PROJECT-18K02917
[Presentation] ブラウザフィンガープリンティングにおけるプライバシーを考慮したWebサイト利用者の識別・追跡2022
- Author(s)
  塚崎崇至, 布田裕一, 鈴木智道, 岡崎裕之
- Organizer
  信学技報, ISEC2022-28
- Data Source
  KAKENHI-PROJECT-22K11982
[Presentation] 情報セキュリティ人材育成のための形式的安全性検証ツール学習用eラーニング環境の構築2022
- Author(s)
  大町隆人, 岡崎裕之, 布田裕一, 村上恭通
- Organizer
  第8回実践的IT教育シンポジウムrePiT2022
- Data Source
  KAKENHI-PROJECT-18K02917
[Presentation] ブロックチェーン技術を用いたカミンスキー攻撃検知手法の提案2022
- Author(s)
  田中健士朗, 布田裕一, 岡崎裕之, 鈴木彦文
- Organizer
  信学技報, NS2022-116
- Data Source
  KAKENHI-PROJECT-22K11982
[Presentation] SDNを用いたDDoS攻撃に対する防御機構構築2022
- Author(s)
  徳山凌, 布田裕一 , 鈴木彦文, 岡崎裕之
- Organizer
  2022年暗号と情報セキュリティシンポジウム SCIS2022
- Data Source
  KAKENHI-PROJECT-18K02917
[Presentation] ProVerifを用いたスポンジ構造の形式化2021
- Author(s)
  吉村東悟,荒井研一,岡崎裕之,布田裕一,三重野武彦
- Organizer
  2021年暗号と情報セキュリティシンポジウム（SCIS2021)
- Data Source
  KAKENHI-PROJECT-17K00182
[Presentation] ブロックチェーンとフォグノードを用いたIoT機器の認証・認可2021
- Author(s)
  五十嵐孝洋, 布田裕一
- Organizer
  電子情報通信学会,ICSS研究会
- Data Source
  KAKENHI-PROJECT-17K00182
[Presentation] 制御システムにおける異常検知手法とデータセットの評価2021
- Author(s)
  原田雄基, 布田裕一, 岡崎裕之
- Organizer
  2021年暗号と情報セキュリティシンポジウム（SCIS2021)
- Data Source
  KAKENHI-PROJECT-17K00182
[Presentation] Virtual Environment for Analysis and Evaluation of DDoS Attacks2021
- Author(s)
  Ryo Tokuyama, Yuichi Futa, Hikofumi Suzuki, Hiroyuki Okazaki
- Organizer
  INTRICATE-SEC-2021, Proceedings of the 35th International Conference on Advanced Information Networking and Applications (AINA-2021)
- Int'l Joint Research
- Data Source
  KAKENHI-PROJECT-17K00182
[Presentation] ProVerifを用いたPolicy-based Chameleon Hashによる修正可能なブロックチェーンの形式化2021
- Author(s)
  杉山航平, 荒井研一,岡崎裕之,布田裕一,三重野武彦
- Organizer
  日本応用数理学会 2021年度年会
- Data Source
  KAKENHI-PROJECT-18K02917
[Presentation] 協調型DNSによるキャッシュポイズニングの検知2020
- Author(s)
  高橋幸宏,布田裕一,岡崎裕之,鈴木彦文
- Organizer
  2020年暗号と情報セキュリティシンポジウム（SCIS2020)
- Data Source
  KAKENHI-PROJECT-17K00182
[Presentation] ProVerifを用いたMD変換の形式化2020
- Author(s)
  吉村東悟,荒井研一,岡崎裕之,布田裕一,三重野武彦
- Organizer
  日本応用数理学会 2020年度年会
- Data Source
  KAKENHI-PROJECT-17K00182
[Presentation] モデル検査器ProVerifによるDES暗号の形式化2020
- Author(s)
  磯貝百恵,岡崎裕之,荒井研一,布田裕一,三重野武彦
- Organizer
  2020年電子情報通信学会総合大会
- Data Source
  KAKENHI-PROJECT-17K00182
[Presentation] Formal Verification of Merkle-Damgard Construction in ProVerif2020
- Author(s)
  Mieno Takehiko, Yoshimura Togo, Hiroyuki Okazaki, Yuichi Futa, Kenichi Arai
- Organizer
  The International Symposium on Information Theory and Its Applications(ISITA2020)
- Int'l Joint Research
- Data Source
  KAKENHI-PROJECT-17K00182
[Presentation] ブロックチェーンとフォグノードを用いたIoT機器の認証・認可2020
- Author(s)
  五十嵐孝洋, 布田裕一
- Organizer
  ICSS
- Data Source
  KAKENHI-PROJECT-18K02917
[Presentation] ProVerifを用いたMD変換の形式化2020
- Author(s)
  吉村　東悟,荒井　研一,岡崎　裕之,布田　裕一,三重野　武彦
- Organizer
  2020年暗号と情報セキュリティシンポジウム（SCIS2020)
- Data Source
  KAKENHI-PROJECT-17K00182
[Presentation] ProVerifを用いたスポンジ構造の形式化2020
- Author(s)
  吉村東悟,荒井研一,岡崎裕之,布田裕一,三重野武彦
- Organizer
  2021年暗号と情報セキュリティシンポジウム（SCIS2021)
- Data Source
  KAKENHI-PROJECT-18K02917
[Presentation] モデル検査器ProVerifによるDES暗号の形式化2020
- Author(s)
  磯貝百恵, 岡崎裕之, 荒井研一, 布田裕一, 三重野武彦
- Organizer
  2020年電子情報通信学会総合大会
- Data Source
  KAKENHI-PROJECT-18K02917
[Presentation] ProVerifを用いたMD変換の形式化2020
- Author(s)
  吉村東悟,荒井研一,岡崎裕之,布田裕一,三重野武彦
- Organizer
  日本応用数理学会 2020年度年会
- Data Source
  KAKENHI-PROJECT-18K02917
[Presentation] Mizarによる離散確率分布の統計的識別不能性の形式化2019
- Author(s)
  岡崎裕之, 布田裕一, 師玉康成
- Organizer
  日本応用数理学会 2019年度年会
- Data Source
  KAKENHI-PROJECT-17K00182
[Presentation] ProVerifを用いたCT及びブロックチェーンの形式化2019
- Author(s)
  荒井研一, 岡崎裕之, 布田裕一
- Organizer
  2019年暗号と情報セキュリティシンポジウム
- Data Source
  KAKENHI-PROJECT-17K00182
[Presentation] 形式的安全性検証ツールを用いた暗号教育の実践とそのe-Learning教材化の課題について2019
- Author(s)
  紫村彰吾, 岡崎裕之, 宮本樹, 渡邊樹, 布田裕一, 村上恭通
- Organizer
  第5回実践的IT教育シンポジウム rePiT2019 in 愛媛
- Data Source
  KAKENHI-PROJECT-17K00182
[Presentation] 形式的安全性検証ツールを用いた暗号教育の実践とそのe-Learning教材化の課題について2019
- Author(s)
  岡崎裕之, 紫村彰吾, 宮本樹, 渡邊樹, 布田裕一, 村上恭通
- Organizer
  第5回実践的IT教育シンポジウム rePiT2019
- Data Source
  KAKENHI-PROJECT-18K02917
[Presentation] 形式的安全性検証ツールを用いた暗号教育の実践とその e-Learning 教材化の課題について2019
- Author(s)
  紫村彰吾, 岡崎裕之, 宮本樹, 渡邊樹, 布田裕一, 村上恭通
- Organizer
  第5回実践的IT教育シンポジウム (rePiT2019)
- Data Source
  KAKENHI-PROJECT-18K02917
[Presentation] BGP経路における不正な経路情報の検知2019
- Author(s)
  高橋幸宏, 鈴木智道, 布田裕一, 田中覚
- Organizer
  暗号と情報セキュリティシンポジウム(SCIS2019)
- Data Source
  KAKENHI-PROJECT-15K00183
[Presentation] CAN-Ethernet変換における不正アクセスの検知2019
- Author(s)
  田付洋大, 布田裕一, 鈴木智道, 田中覚
- Organizer
  情報処理学会第81回全国大会
- Data Source
  KAKENHI-PROJECT-17K00182
[Presentation] Formalization of Security Requirements and Attack Models for Cryptographic Hash Functions in ProVerif2019
- Author(s)
  Togo Yoshimura, Kenichi Arai, Hiroyuki Okazaki, Yuichi Futa
- Organizer
  ProVerif,The 2019 International Conference on Security and Management (SAM'19)
- Int'l Joint Research
- Data Source
  KAKENHI-PROJECT-17K00182
[Presentation] ProVerifを用いたCT及びブロックチェーンの形式化2019
- Author(s)
  荒井研一, 岡崎裕之, 布田裕一
- Organizer
  暗号と情報セキュリティシンポジウム(SCIS2019)
- Data Source
  KAKENHI-PROJECT-15K00183
[Presentation] Mizarによる離散確率分布の統計的識別不能性の形式化2019
- Author(s)
  岡崎裕之, 布田裕一, 師玉康成
- Organizer
  日本応用数理学会 2019年度年会予稿集
- Data Source
  KAKENHI-PROJECT-18K02917
[Presentation] Formalization of Security Requirements and Attack Models for Cryptographic Hash Functions in ProVerif2019
- Author(s)
  Togo Yoshimura, Kenichi Arai, Hiroyuki Okazaki, Yuichi Futa
- Organizer
  The 2019 International Conference on Security and Management (SAM'19)
- Int'l Joint Research
- Data Source
  KAKENHI-PROJECT-18K02917
[Presentation] Moodle を用いた Proverifの e ラーニングシステム2018
- Author(s)
  渡邊樹, 宮本樹, 紫村彰吾, 岡崎裕之, 布田裕一, 村上恭通
- Organizer
  第41回情報理論とその応用シンポジウム (SITA2018)
- Data Source
  KAKENHI-PROJECT-18K02917
[Presentation] ProVerifを用いたCTの形式化2018
- Author(s)
  荒井　研一, 岡崎　裕之, 布田　裕一
- Organizer
  2018年暗号と情報セキュリティシンポジウム (SCIS2018)
- Data Source
  KAKENHI-PROJECT-15K00183
[Presentation] Suitable Symbolic Models for Cryptographic Verification of Secure Protocols in ProVerif2018
- Author(s)
  Okazaki Hiroyuki、Futa Yuichi、Arai Kenichi
- Organizer
  The International Symposium on Information Theory and Its Applications(ISITA2018)
- Int'l Joint Research
- Data Source
  KAKENHI-PROJECT-17K00182
[Presentation] e-Learning System for Cryptography on Moodle2018
- Author(s)
  Tatsuki Miyamoto, Shogo Shimura, Tatsuki Watanabe, Hiroyuki Okazaki, Yuichi Futa, Yasuyuki Murakami
- Organizer
  Internet Conference 2018 (IC2018),Poster session
- Int'l Joint Research
- Data Source
  KAKENHI-PROJECT-17K00182
[Presentation] Moodleを用いたProverifのeラーニングシステム2018
- Author(s)
  渡邊樹，宮本樹，紫村彰吾，岡崎裕之，布田裕一，村上恭通
- Organizer
  第41回情報理論とその応用シンポジウム(SITA2018), Poster session
- Data Source
  KAKENHI-PROJECT-17K00182
[Presentation] ProVerif を用いたTLS1.3ハンドシェイクプロトコルの形式検証2018
- Author(s)
  荒井研一, 岡崎裕之, 布田裕一
- Organizer
  日本応用数理学会 2018年度年会
- Invited
- Data Source
  KAKENHI-PROJECT-17K00182
[Presentation] e-Learning System for Cryptography on Moodle2018
- Author(s)
  Tatsuki Miyamoto, Shogo Shimura, Tatsuki Watanabe, Hiroyuki Okazaki, Yuichi Futa, Yasuyuki Murakami
- Organizer
  Internet Conference 2018 (IC2018)
- Int'l Joint Research
- Data Source
  KAKENHI-PROJECT-18K02917
[Presentation] ProVerifを用いたCTの形式化2018
- Author(s)
  荒井　研一、岡崎　裕之、布田　裕一
- Organizer
  2018年暗号と情報セキュリティシンポジウム (SCIS2018)
- Data Source
  KAKENHI-PROJECT-17K00182
[Presentation] ProVerifにおけるphaseについて2017
- Author(s)
  荒井　研一、岡崎　裕之、布田　裕一
- Organizer
  暗号と情報セキュリティシンポジウム(SCIS)
- Place of Presentation
  ロワジールホテル那覇(沖縄県那覇市)
- Year and Date
  2017-01-25
- Data Source
  KAKENHI-PROJECT-15K00183
[Presentation] 共通鍵暗号方式におけるLinear Obfuscationを用いた効果的な難読化手法2017
- Author(s)
  ステュワートギャビンレン，布田裕一，宮地充子
- Organizer
  IEICE Japan Tech. Rep. ISEC2017 (2017-03)
- Place of Presentation
  東海大学(東京都港区)
- Year and Date
  2017-03-10
- Data Source
  KAKENHI-PROJECT-15K00183
[Presentation] ProVerifにおける暗号プリミティブの安全性要件と攻撃モデルの形式化方法について2017
- Author(s)
  荒井　研一、岡崎　裕之、布田　裕一
- Organizer
  日本応用数理学会2017年度年会
- Data Source
  KAKENHI-PROJECT-17K00182
[Presentation] Symbolic Execution に対する難読化の評価2015
- Author(s)
  ステュワートギャヴィン, 宮地充子, 布田裕一
- Organizer
  コンピュータセキュリティシンポジウム
- Place of Presentation
  長崎ブリックホール(長崎県長崎市)
- Year and Date
  2015-10-22
- Data Source
  KAKENHI-PROJECT-15K00183
[Presentation] negligible function の形式定義について2014
- Author(s)
  岡崎裕之, 布田　裕一
- Organizer
  日本応用数理学会2014年研究部会連合発表会「数理的技法による情報セキュリティ」(FAIS)セッション
- Place of Presentation
  京都大学
- Data Source
  KAKENHI-PROJECT-22300285
[Presentation] Mizarによる素体上の楕円曲線の形式化2011
- Author(s)
  布田裕一, 岡崎裕之, 師玉康成
- Organizer
  第9回「代数学と計算」研究集会
- Place of Presentation
  首都大学東京
- Year and Date
  2011-11-07
- Data Source
  KAKENHI-PROJECT-22300285
[Presentation] Formal Definition of Probability and Probabilistic Function on Finite and Discrete Sample Space for Proving Security of Cryptographic Systems Using Mizar2011
- Author(s)
  Hiroyuki Okazaki, Yasunari Shidama, Yuichi Futa
- Organizer
  The 2011 Joint Mathematics Meetings
- Place of Presentation
  New Orleans
- Data Source
  KAKENHI-PROJECT-22300285

1. OKAZAKI Hiroyuki (50432167)

# of Collaborated Projects: 6 results

# of Collaborated Products: 62 results
2. SHIDAMA Yasunari (20226129)

# of Collaborated Projects: 2 results

# of Collaborated Products: 14 results
3. ARAI Kenichi (60645290)

# of Collaborated Projects: 2 results

# of Collaborated Products: 11 results
4. WASAKI Katsumi (70271492)

# of Collaborated Projects: 1 results

# of Collaborated Products: 0 results
5. KPAULINE Naomi (40283238)

# of Collaborated Projects: 1 results

# of Collaborated Products: 0 results
6. YAMAZAKI Hiroshi (00293522)

# of Collaborated Projects: 1 results

# of Collaborated Products: 0 results
7. Murakami Yasuyuki (50368172)

# of Collaborated Projects: 1 results

# of Collaborated Products: 5 results
8. 宮地充子 (10313701)

# of Collaborated Projects: 1 results

# of Collaborated Products: 2 results
9. CHEN Jiageng (90640748)

# of Collaborated Projects: 1 results

# of Collaborated Products: 0 results
10. 長尾孝一 (00308321)

# of Collaborated Projects: 1 results

# of Collaborated Products: 0 results
11. 鈴木彦文 (30300578)

# of Collaborated Projects: 1 results

# of Collaborated Products: 8 results
12. KAWAMOTO Pauline・Naomi

# of Collaborated Projects: 0 results

# of Collaborated Products: 8 results

FUTA Yuichi 布田 裕一

Research Projects

Research Products

Co-Researchers

形式手法を用いた数論アルゴリズムの設計支援システムの開発

Principal Investigator

Project Period (FY)

Research Category

Review Section

Research Institution

ネットワークシステムのセキュリティで等価な仮想評価環境の構築Principal Investigator

Principal Investigator

Project Period (FY)

Research Category

Review Section

Research Institution

Development of e-learning system for human resource development in the information security field

Principal Investigator

Project Period (FY)

Research Category

Review Section

Research Institution

Developing Automated formal Verification System for Cryptology

Principal Investigator

Project Period (FY)

Research Category

Research Field

Research Institution

Study on tamper-resistant software technology with theoretic security evaluationPrincipal Investigator

Principal Investigator

Project Period (FY)

Research Category

Research Field

Research Institution

Content Development for Distance Education in Advanced University Mathematics Using Mizar

Principal Investigator

Project Period (FY)

Research Category

Research Field

Research Institution

[Journal Article] How to Formalize Loop Iterations in Cryptographic Protocols Using ProVerif2024

Author(s)

Journal Title

DOI

Data Source

[Journal Article] Inverse Function Theorem. Part I2021

Author(s)

Journal Title

DOI

Data Source

[Journal Article] Formal Verification of Merkle-Damgård Construction in ProVerif2020

Author(s)

Journal Title

DOI

NAID

ISSN

Year and Date

Language

Data Source

[Journal Article] Educating Cryptography using Formal Security Verification tool for Cryptographic Protocols2020

Author(s)

Journal Title

DOI

NAID

ISSN

Year and Date

Language

Data Source

[Journal Article] Maximum Number of Steps Taken by Modular Exponentiation and Euclidean Algorithm2019

Author(s)

Journal Title

DOI

Data Source

[Journal Article] Operations of Points on Elliptic Curve in Affine Coordinates2019

Author(s)

Journal Title

DOI

Data Source

[Journal Article] Continuity of Bounded Linear Operators on Normed Linear Spaces2018

Author(s)

FUTA Yuichi 布田裕一