密码分析实验一（ProVerif/HandShake Protocol/Needham-Schroeder Protocol）

graphviz :

sudo apt install graphviz

到官网下载源码文件： http://proverif.inria.fr/   

解压：

tar -xzf proverif2.05.tar.gz

进入相应目录，安装Proverif：

cd ./proverif2.05
./build

-help参数可查看proverif可用：

2.验证hello.pv文件：

将hello.pv文件用proverif进行分析：

./proverif ./hello.pv

（二）HandShake Protocol

握手协议验证：

(* Symmetric Enc *) 
type key. 
fun senc(bitstring,key) : bitstring. 
reduc forall m:bitstring,k:key;sdec(senc(m,k),k) = m. 
(* Asymmetric Enc Structure *) 
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. 
(* Digital Signatures Structure *) 
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. 
(* HandShake Protocol *) 
free c:channel. 
free s:bitstring [private]. 
query attacker(s). 
let clientA(pkA:pkey,skA:skey,pkB:spkey) = 
out(c,pkA); 
in(c,x:bitstring); 
let y = adec(x,skA) in 
let (=pkB,k:key) = checksign(y,pkB) in 
out(c,senc(s,k)). 
let serverB(pkB:spkey,skB:sskey) = 
in(c,pkX:pkey); 
new k:key; 
out(c,aenc(sign((pkB,k),skB),pkX)); 
in(c,x:bitstring); 
let z = sdec(x,k) in 
0. 
process 
new skA:skey; 
new skB:sskey; 
let pkA = pk(skA) in out(c,pkA); 
let pkB = spk(skB) in out(c,pkB); 
( (!clientA(pkA,skA,pkB)) | (!serverB(pkB,skB)) )

将以上代码写入并保存为handshake.pv文件，具体操作如下：

sudo apt install vim

vim handshake

写入后进行验证：

分析ex_handshake.pv

（三）Needham-Schroeder Protocol