| 研究課題/領域番号 |
24700006
|
|---|
| 研究種目 |
若手研究(B)
|
| 研究機関 | 東京大学 |
|---|
研究代表者 |
角谷 良彦 東京大学, 情報理工学(系)研究科, 助教 (70376614)
|
|---|
| 研究期間 (年度) |
2012-04-01 – 2015-03-31
|
| キーワード | 形式手法 / 量子計算 / プロトコル |
|---|
| 研究概要 |
量子プロセス計算を量子鍵配送プロトコルの安全性証明に応用した。量子鍵配送プロトコルBB84には、ShorとPreskillによる安全性証明が既に存在する。この証明では、BB84の安全性をEDPを用いる別のプロトコルの安全性に帰着している。本研究では、プロトコルを量子プロセス計算におけるプロセスとして形式化し、プロトコル間の変換を双模倣として捉えることに成功した。元の安全性証明においては、プロトコルの変換は複数のステップからなっており、個々のステップの変換の前後でプロトコルが等価であることを保証している。対して、本研究の手法を利用すれば、最初と最後の2つのプロトコルが双模倣であることを直接示すことが可能となる。
プロトコルを量子プロセス計算の中で形式化するには、量子測定に関する問題が付随する。先行研究の量子プロセス計算の双模倣には、まだいくつか問題点が残されているが、最も大きな問題は、量子測定に対して複数の異なる形式化が存在することである。本研究では、等価なプロトコルの関係を双模倣として捉えるために、量子測定をどのように形式化するべきかについて考察を行った。この成果は、プロセス計算の研究分野と量子計算の研究分野を結ぶ上で、重要な結果だと考えられる。研究成果は、国際会議において発表され、論文として公開されている。
また、この双模倣を自動的に判別するツールについても開発中であり、実装はある程度の段階まで進んでいる。
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
2: おおむね順調に進展している
理由
量子鍵配送プロトコルを量子プロセス計算の枠組みで形式化するという点は、現在までにほぼ達成されている。実用的な応用を見越して、量子プロセス計算におけるプロセスの等価性を議論するという点においては、先行研究の問題点を認識し、プロトコルを適切に形式化するための指針を指針を示せたことから、研究は順調に進んでいると判断している。特に、量子測定に関して、外部から見えるかどうかの区別が双模倣に影響を与えるということが明らかになった点は重要である。
当初の計画では、対象となる量子プロセス計算として、量子π計算を利用するとなっていたが、実際には、量子CCSを利用している。量子的な部分においては、それらの2つの計算系に本質的な違いはないため、研究の進展としては問題ないと判断される。
|
| 今後の研究の推進方策 |
当初の計画では、次年度は理論的考察を続け、最終年度にツールの実装を行う予定であったが、既にツールの開発に着手しているため、ツールの実装を優先して進めることにする。ツールには理論的な裏付けが必要なので、理論的な考察も平行して行うのは当然である。これまでの研究で、量子測定の形式化の問題点が明らかになったので、今後はこの問題点を回避する新たな形式体系の考察も行なっていく予定である。もし新たな体系が得られた場合には、既に開発の進んでいるツールの方でもそれをサポートするように改良を行う。
また、BB84以外の鍵配送プロトコルの形式化も進めていく。BB84以外のプロトコルの安全性証明に本研究の手法を適用するためには、異なるプロトコルの安全性証明を比較し、その共通している枠組みや本質的な違いを考察する必要がある。プロトコルの種類は多岐に渡るので、広く様々な分野の研究者と議論を行っていく予定である。鍵配送プロトコル以外にも、等価性や双模倣と関係があるような量子プロトコルへの応用も視野に入れて研究を進めていくこととする。特に、量子非局所性ゲームはプロトコルと似た形式をしており、関連を調べる価値があると考えられる。
|
| 次年度の研究費の使用計画 |
今年度はパソコン関係の備品の整備があまり進まなかったため、その分は次年度に使用することとなった。パソコンの整備を進めるために、研究費は主に備品の購入に当てる予定である。
|
