| 研究課題/領域番号 |
26730067
|
|---|
| 研究種目 |
若手研究(B)
|
| 配分区分 | 基金 |
|---|
| 研究分野 |
情報セキュリティ
|
|---|
| 研究機関 | 長崎大学 (2015-2016)
東京理科大学 (2014) |
|---|
研究代表者 |
荒井 研一 長崎大学, 工学研究科, 助教 (60645290)
|
|---|
| 研究期間 (年度) |
2014-04-01 – 2017-03-31
|
| 研究課題ステータス |
完了 (2016年度)
|
| 配分額 *注記 |
1,950千円 (直接経費: 1,500千円、間接経費: 450千円)
2016年度: 650千円 (直接経費: 500千円、間接経費: 150千円)
2015年度: 650千円 (直接経費: 500千円、間接経費: 150千円)
2014年度: 650千円 (直接経費: 500千円、間接経費: 150千円)
|
|---|
| キーワード | 暗号プロトコル / 安全性 / フォーマルメソッド / 自動検証 / 自動証明 / ProVerif / Mizar / CryptoVerif |
|---|
| 研究成果の概要 |
近年、暗号プロトコルはさまざまな要求に答えるために日々複雑になってきている。暗号プロトコルが複雑になるにつれて安全性評価は困難になるため、人為的なミスが発生しやすくなる。そのため、評価に誤りがある論文が多数存在し問題となっている。そこで本研究では、計算機を用いた暗号プロトコルの安全性評価の有効性に着目し、暗号プロトコルの安全性評価を厳密に行うことができる手法の実現に向けた検討を行った。本研究の成果は、暗号プロトコルの複雑化に伴う評価の誤りの増加といった深刻な問題に対して、有効な解決手段を提供するものとなる。
|
