安全协议理论课程笔记

第四章-可证明安全理论与方法

4.1 可证明安全理论与方法概述

4.1.1 基本思想

  • 启发式设计方法存在以下的问题:新的分析技术的产生时间是不确定的。使人们很难确信协议的安全性,反反复复地修补更增加了人们对安全性的担心,也增大了实现代价或成本。

  • 可证明安全理论就是为了解决上述问题而提出的一种解决方案。

  • 实际上,可证明安全性理论与方法是在一定的敌手模型下证明了安全方案或协议能够达到特定的安全目标,因此,合适的安全目标定义、适当的敌手模型是我们讨论可证明安全性的前提条件。

  • 可证明安全性是以某一假设为基础的,因此一旦该假设靠不住,安全性证明也就没有意义。

  • 所谓“极微本原(atomic primitives)”是指安全方案或协议的最基本组成构件或模块,也被称为密码原语,例如,某个基础密码算法或数学难题。人们普遍相信“极微本原”是难破译或难解决的。

4.1.2 可证明安全理论的三大要素

  • 可证明安全理论的三大要素为:困难问题假设、安全模型、规约论断。
    • 困难问题假设:是指能成功解决一个数学困难问题的概率是可忽略的。
    • 安全模型:在可证明安全框架下,一个方案的安全模型往往从两个方面定义:敌手的攻击目标和攻击行为。若敌手在某种攻击行为下无法达到他的预期攻击目标,那么方案就被定义为这种攻击下此攻击目标的安全。方案设计者需要的是让敌手的攻击能力最强,却无法达到最简单的攻击目标,这样的方案安全性最强,也最难实现。
    • 规约论断:规约论断是可证明安全理论的最基本工具或推理方法。

4.1.3 可证明安全理论与方法的优劣

  • 优势:
    • 可以把主要精力集中在“极微本原”的研究上。
    • 如果相信极微本原的安全性,不必进一步分析协议即可相信其安全性。
  • 局限性:
    • 必须注意模型的设计,即注意所建的模型都涵盖了哪些攻击。
    • 即使可证明安全性的方案,也可能有多种方式破坏安全性。(问题可能是错误的、可能应用了错误的模型、协议被错误操作、软件本身有错误)
    • 注意基本假设的选取。一旦某个假设靠不住,那么安全性证明也没有意义。
      • 选取基础假设的原则是“越弱越好”,通常称弱假设为标准假设。

4.2 要素一:困难问题假设

可证明安全协议的安全性依赖于困难问题假设。2个常见困难问题假设可以分为:单向函数的存在性、陷门单向函数的存在性。

  • 单向函数与陷门单向函数的区别:
    • 单向函数:任何人都容易计算函数值,但是给定$y=f(x)$,恢复$x$(或$y$的任何原像)在计算上是不可行的。
    • 陷门单向函数:与单向函数的不同是,其存在秘密信息(即陷门)有助于对函数进行求逆。

目前常用的困难问题假设有:

  • 整数分解与RSA问题

    • 描述:把两个素数$p$和$q$相乘得到$n=p·q$是容易的,而把合数$n$分解为素因子$p$和$q$则不是一件容易的事情。
  • 离散对数与Diffie-Hellman问题

    • 描述:设$(G,·)$表示一个阶为$q$的循环群,其中$q$是素数,$g$表示$G$的一个生成元,即$G=$。

      • 离散对数问题可以描述为:给定$y\in G$,计算$x\in Z^*_q$,使得$y=g^x$,记为$x=log_g^y$。
      • 计算Diffie-Hellman(CDH)问题:对于任意的整数$a,b\in Z^*_q$,给定$<g,g^a,g^b>$,计算$g^{ab}$。DH问题详解
      • 判定性Diffie-Hellman(DDH)问题:对于任意的整数$a,b,c\in Z^*_q$,给定$<g,g^a,g^b,g^c>$,判定是否有$c \equiv a b(\bmod q)$成立。

        Anki here

0%