Proverif软件验证修改后的握手协议

Posted 2021-10-31 AnWen~

(*对称声明*)
type key.                                                                           (*用户定义类型，key是类型名称*)
fun senc(bitstring, key): bitstring.                                      (*定义对称加密函数（构造器）fun，定义一个密钥类型`key`，定义了一个对称加密函数`senc`，传入`bitstring`（内置的）和`key`，然后返回一个`bitstring`：*)
reduc forall m:bitstring, k:key; sdec(senc(m,k),k)=m.       (*析构器 解密操作 *)


(*非对称声明*)
type skey.    (*私钥*)
type pkey.   (*公钥*)

fun pk(skey): pkey.      (*输入私钥，得到公钥*)
fun aenc(bitstring, pkey): bitstring.   (*非对称加密，用公钥pkey加密*)

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


(*数字签名*)
type sskey.     (*私钥*)
type spkey.    (*公钥*)

fun spk(sskey): spkey.        (*输入私钥，得到公钥*)
fun sign(bitstring, sskey): bitstring.     (*签名操作，用私钥sskey签名*)

reduc forall  m: bitstring, k: sskey; getmess(sign(m,k))=m.   (*getmess就是直接从签名后的信息中提取到原信息*)
reduc forall  m: bitstring, k: sskey; checksign(sign(m,k),spk(k))=m. (*而checksign则是用公钥对签名进行验证，只有验证通过时才能返回原信息`m`。*)

free c:channel.     (*定义一个公共的信道，攻击者也可以得到的*)

free s:bitstring [private].   (*秘密值*)
query attacker(s).    (*对秘密值s的访问，实际查询的是not attacker (s)，即要判断命题  s不会被攻击者窃取  是否是成立的。*)

event acceptsClient(key).   (*客户端接受了   使用收到的key和服务器交互   这件事*)
event acceptsServer(key,pkey).   (*服务器接受了   使用key和公钥为pkey的客户端交互   这件事。*)
event termClient(key,pkey).    (*客户端认为已经完成了   使用key为会话密钥以及pkey作为客户端公钥，和服务器运行协议    这件事。*)
event termServer(key).    (*服务器认为已经完成了     使用key作为会话密钥，和客户端运行协议     这件事。*)

query x:key,y:pkey; event(termClient(x,y))==>event(acceptsServer(x,y)).   (*事件termClient(x,y)发生了，那么acceptsServer(x,y)一定发生*)
query x:key; inj-event(termServer(x))==>inj-event(acceptsClient(x)).         (* 事件termServer(x)发生了，那么acceptsClient(x)一定发生，并且是一对一的关系*)

let clientA(pkA:pkey,skA:skey,pkB:spkey) =    (*定义 进程宏，，clientA是宏的名字，等号后面的是子进程*)
	out(c,pkA);   (*通过信道c将 pkA 信息发出去*)
	in(c,x:bitstring);     (*通过信道c 得到信息 x*)
	let y = adec(x,skA) in    (*用自己的私钥skA解密消息x，如果能解密成功得到 y签名消息 ，就执行 下一步，这里实际省略了 else 0，0表示进程结束*)
	let (=pkA,=pkB,k:key) = checksign(y,pkB) in     (*利用 自己知道的 公钥pkB验证 签名，=pkB 模式匹配的是一个与项pkB相等的项，这个项是解密出来的*)
	event acceptsClient(k);   (*这个时候 定义一个事件，只有执行完前面的，这个事件才发生，表明 客户端A 已经 接收了 秘密值k*)
	out(c,senc(s,k));    (*用会话密钥k加密秘密值s，通过信道c发送出去*)
	event termClient(k,pkA).   (*上面事件执行完后，表明 使用了 会话密钥 k和自己的公钥pkA和服务器交互*)

let serverB(pkB:spkey,skB:sskey,pkA:pkey) =   (*定义 进程宏，，serverB是宏的名字，等号后面的是子进程*)
	in(c,pkX:pkey);  (*通过信道c 得到信息 pkX，也就是客户端A的公钥pkA*)
	new k:key;    (*定义一个新的进程中类型为key的变量k*)
	event acceptsServer(k,pkX);     (*上面事件执行完后，表明服务器使用 会话密钥k和公钥为 pkX的客户端进行交互*)
	out(c,aenc(sign((pkX,pkB,k),skB),pkX));    (*先利用自己的私钥进行签名，在利用pkX，也就是客户端A的公钥pkA进行加密，并将消息通过信道c将消息发送出去*)
	in(c,x:bitstring);      (*通过信道c 得到信息 x*)
	let z = sdec(x,k) in   (*如果服务器可以利用会话密钥k解密x,并得到消息 z，就执行下一个子进程，这里省略 else 0*)
	if pkX = pkA then  
	event termServer(k).   (*上面事件执行完后，表明服务器 已经完成了使用会话密钥k和客户端进行交互这件事*)

process   (*进程开始*)
	new skA:skey;      (*先建立客户端的私钥*)
	new skB:sskey;     (*建立服务器的私钥，用于签名的*)
	let pkA = pk(skA) in out(c,pkA);    (*如果 输入 客户端A 的私钥skA，成功得到一个公钥后pkA，后公布公钥pkA，保密私钥skA*)
	let pkB = spk(skB) in out(c,pkB);   (*如果 输入 服务端B 的私钥skB，成功得到一个公钥后pkB，后公布公钥pkB，保密私钥skB*)
	( (!clientA(pkA,skA,pkB)) | (!serverB(pkB,skB,pkA)) )  (*并发执行两个进程*)