数理的技法による情報セキュリティの検証(<特集>数理的技法による情報セキュリティ)

概要

論文の詳細を見る
There are two approaches to verifying cryptographic protocols. One is the traditional computational approach in which an adversary is formulated as a polynomial-time probabilistic Turing machine and success probability of attack is estimated with respect to computational complexity. The other is the symbolic approach which applies formal methods such as automated theorem proving and model checking to formalize and verify cryptographic protocols. Recently, substantial effort is being made to merge the two approaches to enjoy the advantages of both. Such effort can be classified into direct and indirect methods. In the former, traditional computational arguments are formalized using appropriate frameworks from formal methods. In the latter, symbolic arguments, which usually rely on the Dolev-Yao assumption, are given probabilistic interpretation and justified computationally. The latter methods are applied to protocols in a level above cryptographic schemes, while the former are usually applied to verify cryptographic schemes or more basic cryptographic assumptions.
2007-12-26