暗号系の安全性検証 - 入門から計算機による証明まで  [in Japanese] Verification of Cryptosystems - from Introduction to Computer-Aided Security Proofs  [in Japanese]

Access this Article

Author(s)

Abstract

本論文では,暗号系の安全性を検証する方法について,暗号理論の初歩からコンピュータ上で安全性証明を書く最先端の研究までを解説する.暗号系の安全性は攻撃の確率や計算量を用いて定式化されるため,その数学的証明は煩雑であり,しばしば間違いも生じる.そこで,安全性証明を形式手法で記述し,証明の正しさをコンピュータ上で機械的に確かめる研究が盛んになっており,様々な検証ツールが開発されている.その中でも,検証ツールEasyCryptは,従来のツールよりも簡単に,厳密な安全性証明が得られる.本論文では,まず,確率的多項式時間チューリング機械の間のゲームとして暗号系の安全性を定式化し,ゲームの書き換えによって安全性を証明する手法を説明する.次に,確率関係ホーア論理を用いた安全性証明の形式化について述べ,検証ツールEasyCryptを用いて安全性証明を書く方法を紹介する.なお,本論文は暗号理論や定理証明支援系についての知識を仮定していない.

This paper gives an overview of verification methods for the security of cryptosystems from basic concepts of cryptography to advanced topics on computer-aided security proofs. The security of cryptosystems is formalized using probabilities and computational complexity of attacks while the mathematical proofs for such security tend to be complicated and error prone. To obtain rigorous security proofs there have been many studies on formalizing and machine-checking proofs using formal methods. Among various verification tools EasyCrypt is the most successful tool that can rigorously construct security proofs more easily than previous tools. In this paper we introduce a method for defining the security of cryptosystems as games among probabilistic polynomial-time (PPT) Turing machines and proving it by game transformation techniques. Then we explain how to formalize such security proofs in the framework of probabilistic relational Hoare logic (pRHL) and to write and machine-check proofs using EasyCrypt. Note that readers do not need to be familiar with cryptography or interactive theorem provers.

Journal

  • Computer Software

    Computer Software 33(4), 4_67-4_83, 2016

    Japan Society for Software Science and Technology

Codes

  • NII Article ID (NAID)
    130005290611
  • Text Lang
    JPN
  • ISSN
    0289-6540
  • Data Source
    J-STAGE 
Page Top