量子プロトコルの検証のための形式手法

• 研究課題/領域番号: 24700006
• 研究種目: 若手研究(B)
• 配分区分: 基金
• 研究分野: 情報学基礎
• 研究機関: 東京大学
• 研究代表者: 角谷 良彦 東京大学, 情報理工学(系)研究科, 助教 (70376614)
• 研究期間 (年度): 2012-04-01 – 2015-03-31
• 研究課題ステータス: 完了 (2014年度)
• 配分額: 4,160千円 (直接経費: 3,200千円、間接経費: 960千円); 2014年度: 1,300千円 (直接経費: 1,000千円、間接経費: 300千円); 2013年度: 1,300千円 (直接経費: 1,000千円、間接経費: 300千円); 2012年度: 1,560千円 (直接経費: 1,200千円、間接経費: 360千円)
• キーワード: 形式手法 / 量子プロトコル / セキュリティ検証 / プロセス計算 / 量子計算 / プロトコル

研究成果の概要

通常の計算の枠組みでは、プログラムやプロトコルの検証を行うための様々な形式手法が研究されている。本研究では、形式手法を量子計算に応用するための考察を行った。特に、量子プロトコルの安全性を検証することを目標に、量子プロセス計算の理論的考察を行った。その結果として、量子鍵配送プロトコルの安全性の証明を、量子プロセス計算の枠組みで形式化することに成功した。

研究成果

• [雑誌論文] Observational Equivalence Using Schedulers for Quantum Processes (2014)
  • 著者名/発表者名: K. Yasuda, T. Kubota, Y. Kakutani
  • 雑誌名: Electronic Proceedings in Theoretical Computer Science 巻: 172 ページ: 191-203
  • DOI: 10.4204/eptcs.172.13
  • NAID: 40020582250
  • 査読あり / オープンアクセス
• [雑誌論文] 猫にはわかる量子プログラミング (2014)
  • 著者名/発表者名: 本多健太郎, 角谷良彦, 久保田貴大
  • 雑誌名: コンピュータソフトウェア 巻: 31
  • NAID: 130004892304
  • オープンアクセス
• [学会発表] A Language for Topological Quantum Computation Based on Duality (Poster) (2014)
  • 著者名/発表者名: K. Honda, Y. Kakutani, K. Kumada
  • 学会等名: Asian Symposium on Programming Languages and Systems
  • 発表場所: National University of Singapore, Singapore
  • 年月日: 2014-11-17 – 2014-11-19
• [学会発表] Observational Equivalence Using Schedulers for Quantum Processes (2014)
  • 著者名/発表者名: 安田和矢, 久保田貴大, 角谷良彦
  • 学会等名: 日本ソフトウェア科学会大会
  • 発表場所: 名古屋大学, 愛知県
  • 年月日: 2014-09-07 – 2014-09-10
• [学会発表] 量子力学から量子計算へ (2014)
  • 著者名/発表者名: 角谷良彦, 本多健太郎
  • 学会等名: 情報科学技技術フォーラム
  • 発表場所: 筑波大学, 茨城県
  • 年月日: 2014-09-03 – 2014-09-05
  • 招待講演
• [学会発表] Observational Equivalence Using Schedulers for Quantum Processes (2014)
  • 著者名/発表者名: K. Yasuda, T. Kubota, Y. Kakutani
  • 学会等名: Quantum Physics and Logic
  • 発表場所: Kyoto University, Kyoto
  • 年月日: 2014-06-04 – 2014-06-06
• [学会発表] スケジューラを用いた量子プロセス間の観測同値 (ポスター) (2014)
  • 著者名/発表者名: 安田和矢, 久保田貴大, 角谷良彦
  • 学会等名: プログラミングおよびプログラミング言語ワークショップ
  • 発表場所: 阿蘇温泉阿蘇の司ビラパークホテル, 熊本県
• [学会発表] 量子暗号プロトコルの形式的検証のための確率双模倣 (2014)
  • 著者名/発表者名: 久保田貴大, 角谷良彦, 加藤豪, 河野泰人, 櫻田英樹
  • 学会等名: 日本応用数理学会春の研究部会連合発表会
  • 発表場所: 京都大学, 京都府
• [学会発表] スケジューラを用いた量子プロセス間の観測同値 (2014)
  • 著者名/発表者名: 安田和矢, 久保田貴大, 角谷良彦
  • 学会等名: 日本応用数理学会春の研究部会連合発表会
  • 発表場所: 京都大学, 京都府
• [学会発表] A Tool for Formal Verification of Equivalence on Quantum Cryptographic Protocols (2013)
  • 著者名/発表者名: 久保田貴大, 角谷良彦, 加藤豪, 河野泰人, 櫻田英樹
  • 学会等名: 量子情報技術研究会
  • 発表場所: 北海道大学, 北海道
• [学会発表] Induction by Coinduction and Control Operators in Call-by-Name (2013)
  • 著者名/発表者名: Y. Kakutani, D. Kimura
  • 学会等名: Control Operators and their Semantics
  • 発表場所: Eindhoven, Netherlands
• [学会発表] Automated Verification of Equivalence on Quantum Cryptographic Protocols (2013)
  • 著者名/発表者名: T. Kubota, Y. Kakutani, G. Kato, Y. Kawano, H. Sakurada
  • 学会等名: Symbolic Computation in Software Science
  • 発表場所: Castle of Hagenberg, Austria
• [学会発表] Towards Quantum Pseudo-telepathic Game Semantics (2013)
  • 著者名/発表者名: 本多健太郎, 角谷良彦
  • 学会等名: 代数, 論理, 幾何と情報科学, 記号論理と情報科学
  • 発表場所: 京都大学, 京都府
• [学会発表] Automated Proof of Equivalence on Quantum Cryptographic Protocols (2013)
  • 著者名/発表者名: 久保田貴大, 角谷良彦, 加藤豪, 河野泰人, 櫻田英樹
  • 学会等名: プログラミングおよびプログラミング言語
  • 発表場所: 東山温泉御宿東鳳, 会津若松
• [学会発表] 量子暗号のためのプロトコル等価性検証ツール (2013)
  • 著者名/発表者名: 久保田貴大, 角谷良彦, 加藤豪, 河野泰人, 櫻田英樹
  • 学会等名: 日本応用数理学会春の研究部会連合発表会
  • 発表場所: 東洋大学, 東京
• [学会発表] Application of a Process Calculus to Security Proofs of Quantum Protocols (2012)
  • 著者名/発表者名: T. Kubota, Y. Kakutani, G. Kato, Y. Kawano, H. Sakurada
  • 学会等名: Foundations of Computer Science in WORLDCOMP
  • 発表場所: Las Vegas, USA