中国移动 WebStorm 循环 Redis k8s centos8 selenium build mtu原理 ios5 vb6 formvalidator.js Draggabilly vue中文 vue注册组件 git视频 java多行注释 linux下载器 bootstrap滚动条 mysql分区表优劣分析 flutter项目案例 python3基础教程 python的array python命令行 java编程环境 java运算符 java方法调用 java抛出自定义异常 java判断 xp画图工具 phpqrcode saminside robotstudio 安卓刷机精灵 苹果放大镜 cubase下载 电脑书籍下载 华为动态照片 fireworks下载 圣武枪魂
当前位置: 首页 > 学习教程  > 编程语言

【ProVerif学习笔记】2:协议建模中的声明

2020/8/11 20:33:36 文章标签:

ProVerif验证的加密协议并发程序通过公共通道来进行信息较交互,最终实现一些目标。认为攻击者对这样的通道有完全的控制能力,包括阅读、修改、删除和注入消息,也可以解密自己持有密钥的消息(视解密为获取密文的唯一途径,不考虑攻击者用其它方式获取密文,所以如果自己没有解密的密钥就不行)。

1 握手协议

握手协议(Handshake protocol)是有一个客户端A和服务器B,假设每一方都有自己的公私钥对,然后A知道B的公钥pk(skB),协议的目的是让客户端A能向服务器B分享自己的私密信息s。

协议按照如下的方式工作。应客户端A的要求,B生成一个新的对称的密钥k,作为会话密钥,把这个k和自己的公钥pk(skB)打包,然后先用自己的私钥skB签名,再用A的公钥pk(skA)加密,也就是说要发送的是:
aenc(sign((pk(skB),k),skB),pk(skA))aenc(sign((pk(skB),k),skB),pk(skA))

其中sign是签名,aenc是非对称加密。

A收到消息后,先用自己的密钥skA解密,再用B的公钥pk(skB)验证一下内容无误,然后提取出会话密钥k,就能用这个k给自己的私密信息s加密然后发送了。

这个协议背后的基本原理在于,A收到的是用她的公钥非对称加密的结果,因此她应该是唯一能够解密其内容的人。而数字签名是用来确保B是这个消息的发起者。

整个过程如下:
AB:pk(skA)BA:aenc(sign((pk(skB),k),skB),pk(skA))AB:senc(s,k) \begin{aligned} A \to B &: pk(skA) \\ B \to A &: aenc(sign((pk(skB),k),skB),pk(skA)) \\ A \to B &: senc(s, k) \end{aligned}

上面的协议叙述还不够清晰,比如要检查每一步收到的格式是正确的,叙述里没有,但是协议建模到ProVerif时要做这些事。

用自然语言描述希望这个协议所具有的三个性质:

  1. 保密性:只有A和B知道s的值
  2. 认证性(A到B):如果B运行到了末尾,他认为和A共享了k,那么A确实是B的对话者,共享了这个k
  3. 认证性(B到A):如果B运行到了末尾,她认为和B共享了k,那么B确实是提供k的一方

这个协议可以受到中间人攻击,一个中间人I可以先和B通信,再冒充B和A通信:
IB:pk(skI)BI:aenc(sign((pk(skB),k),skB),pk(skI))AB:pk(skA)IA:aenc(sign((pk(skB),k),skB),pk(skA))AI:senc(s,k) \begin{aligned} I \to B &: pk(skI) \\ B \to I &: aenc(sign((pk(skB),k),skB),pk(skI)) \\ A \to B &: pk(skA) \\ I \to A &: aenc(sign((pk(skB),k),skB),pk(skA)) \\ A \to I &: senc(s, k) \end{aligned}

只要让服务器回传的信息中包含目标客户端的标识(这里是用公钥)就可以防止这种攻击发生了:
AB:pk(skA)BA:aenc(sign((pk(skA),pk(skB),k),skB),pk(skA))AB:senc(s,k) \begin{aligned} A \to B &: pk(skA) \\ B \to A &: aenc(sign((pk(skA),pk(skB),k),skB),pk(skA)) \\ A \to B &: senc(s, k) \end{aligned}

2 声明

用户定义类型,其中t是类型名称:

type t.

定义free的变量(原文是free names),其中n是变量名称,t是类型名:

free n : t.

定义一连串的free names,都是t类型的:

free n1,...,nk : t.

channel c.free c : channel.是同一个意思,都是声明一个公共信道c,如果要指定不被攻击者获取,使用:

free n : t [private].

构造器(函数)用来构建密码协议使用的建模原语,例如单向哈希、加密、数字签名等:

fun f(t1,...,tn) : t.

其中f是有n个参数的构造器,t是返回值类型,t1tn是参数。构造器默认是可以被攻击者使用的,如果要禁止攻击者使用,则要:

fun f(t1,...,tn) : t [private].

例如,这种私有的构造可以用在对服务器密钥表的建模上。


密码原语之间的关系由析构器指明,析构函数用于操作构造器组成的项。析构器使用如下的重写规则:

reduc forall x1,1 : t1,1,...,x1,n1 : t1,n1; g(M1,1,...,M1,k) = M1,0 ;
      ...
      forall xm,1 : tm,1,...,xm,nm : tm,nm;g(Mm,1,...,Mm,k) = Mm,0 .

其中gg是有k个参数的析构器,项M1,1,...,M1,k,M1,0M_{1,1},...,M_{1,k},M_{1,0}是将构造器作用于t1,1,...,t1,n1t_{1,1},...,t_{1,n_1}类型的x1,1,...,x1,n1x_{1,1},...,x_{1,n_1}上得到的。上面每一行重写规则,gg的返回值M1,0M_{1,0}Mm,0M_{m,0}都应该具有相同的类型,同样的,析构函数里每次传的参数表相应位置上也必须是相同的类型。

每次执行到g(M1,1,...,M1,k)g(M_{1,1},...,M_{1,k})或者这一项的实例时,都会找一条合适的重写规则将其变成对应的M1,0M_{1,0}。如果无法应用重写规则时,析构失败,进程会阻塞(除了let进程)。这和真实世界的密码原语是一致的。

如果多个变量有相同的类型,就只写最后一个的类型就行:

reduc forall x,y : t,z : t'; g(M_1,...,M_k)=M_0.

和构造器类似,析构器也可以加[private]声明为私有的。

3 示例:为握手协议声明加密原语

现在对握手协议中使用的密码学原语进行形式化。


首先是对称加密,这里定义一个密钥类型key,定义了一个对称加密函数senc,传入bitstring(内置的)和key,然后返回一个bitstring

type key.
fun senc(bitstring, key): bitstring.

再定义一个析构器,来对解密操作进行建模:

reduc forall m:bitstring, k:key; sdec(senc(m,k),k)=m.

其中m表示消息,k表示对称密钥。


对于非对称加密,使用一元构造器pk,传入私钥,返回公钥。也可以理解成是传入一个私钥就能生成对应的公钥,从而得到公私钥对。解密的析构器也是和前面类似的做法。

type skey.
type pkey.

fun pk(skey): pkey.
fun aenc(bitstring, pkey): bitstring.

reduc forall m: bitstring, k: skey; adec(aenc(m, pk(k)),k)=m.

对于数字签名,和非对称加密是类似的,需要有签名私钥sskey和签名公钥spkey,用私钥签名、公钥验证。下面是一种带有消息恢复的签名,getmess就是直接从签名后的信息中提取到原信息,而checksign则是用公钥对签名进行验证,只有验证通过时才能返回原信息m

type sskey.
type spkey.

fun spk(sskey): spkey.
fun sign(bitstring, sskey): bitstring.

reduc forall m: bitstring, k: sskey; getmess(sign(m,k))=m.
reduc forall m: bitstring, k: sskey; checksign(sign(m,k),spk(k))=m.

还支持元组,元组是n>=2n>=2(M1,...,Mn)(M_1,...,M_n)。如果允许攻击者访问某个元组,他可以取得其中的任何一项;反过来,如果攻击者有M1,...,MnM_1,...,M_n,他就可以构造元组。

元组中的每一项可以是任何类型,但是元组总是bitstring类型的,所以如果某个构造器的某个参数是bitstring类型的,那就可以传个元组进去。

需要注意元组一定是n>=2n>=2的,只有一个元素的(M1)(M_1)M1M_1没区别,不是元组。

参考阅读

ProVerif的manual第3~3.1.2章节


本文链接: http://www.dtmao.cc/news_show_100370.shtml

附件下载

相关教程

    暂无相关的数据...

共有条评论 网友评论

验证码: 看不清楚?