- 安装ProVerif以及环境配置
作者使用的是LINUX系统,所以在网络上下载好对应系统的安装包进行安装,同时安装一并需要的环境配置软件如ocaml,graphviz。
安装完成后可以在命令行中输入help查看是否正确安装。
如图可见,安装成功。
- 测试ProVerif
**** 在ProVerif的文件夹下创建名为hello.pv的文件，使用ProVerif对其进行验证。****
- 验证Handshake Protocol协议
**** (* Symmetric key encryption )***
type key.
fun senc(bitstring, key): bitstring.
reduc forall m: bitstring, k: key; sdec(senc(m,k),k) = m.
(* Asymmetric key encryption *)
type skey.
type pkey.
fun pk(skey): pkey.
fun aenc(bitstring, pkey): bitstring.
reduc forall m: bitstring, sk: skey; adec(aenc(m,pk(sk)),sk) = m.
(* Digital signatures *)
type sskey.
type spkey.
fun spk(sskey): spkey.
fun sign(bitstring, sskey): bitstring.
reduc forall m: bitstring, ssk: sskey; getmess(sign(m,ssk)) = m.
reduc forall m: bitstring, ssk: sskey; checksign(sign(m,ssk),spk(ssk)) = m.
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)) )
****协议分析 ****
*这里首先分析一下上面的代码的工作，proverif从process标记的主进程开始分析，所以这里看***process ****
****后面的内容 ****
*首先是为clientA生成了非对称加密私钥skA，同时为serverB生成了签名用的私钥skB***，并分别为这两个 ****
*私钥生成对应的公钥（pkA，pkB），并通过公开信道c***将这两个公钥发送出去 ****
*接下来调用两个进程宏clientA和serverB来实现两个进程的并发执行（Line 64），这里用replication***的 ****
*方式让两个主体都以无限数量会话并发执行（Line 64的clientA和serverB***前面的感叹号表示重复无限多 ****
****个会话并发） ****
*然后关注clientA和serverB这两个模块，这里要把两个模块结合起来看，首先是A把自己公钥pkA***发出去 ****
*（Line 45），B会接收到这个公钥pkX（Line 52），同时创建一个对称密钥k（Line 53，k***这里起到临时 ****
****会话密钥的作用） ****
*然后B将这个临时密钥k和自己的公钥pkB一起打包成元组，先用自己的私钥skB签名（Line 54的sign***部 ****
*分），再用收到的公钥pkX加密，并通过公共信道发出去（Line 54的aenc部分，这里aenc***表示非对称加 ****
****密） ****
*A通过信道接收到这个发来的bitstring（Line 46），然后用自己私钥解密，解密成功之后得到y（***Line ****
47），之后用B的公钥pkB验证签名，如果验证通过了就会得到元组(m,k)，第一项就是pkB（Line 48********， ****
这里用****=pkB来匹配），第二项就是对称密钥k ****
*A再用这个k给消息s进行对称加密然后发出去（Line 49），B接收到发来的bitstring*****之后，用自己刚刚创 ****
*建的对称密钥k解密就得到了内容z，这应该和s***是一样的内容 ****
不难看出，这段代码很简单，所以也不难想到中间人攻击
可以看到存在中间人攻击。
****这里可以回顾中间人攻击的流程，攻击者需要同时维护两个会话（对应于上面的两个会话），将从与 ****
*server*****会话接收到的内容选择性的篡改（也可以不改，上面的协议需要解密，所以修改了），然后发送 ****
*到与client***的会话中 ****
*由于没有额外的方式完成鉴权（上述过程只有一个server的签名和认证），所以client和server***都认为它 ****
们与对方建立了加密会话，而实际上这个加密会话所使用的密钥已经被attacker获取到了。
改进后的代码
(* Symmetric key encryption *)
type key.
fun senc(bitstring, key): bitstring.
reduc forall m: bitstring, k: key; sdec(senc(m,k),k) = m.
(* Asymmetric key encryption *)
type skey.
type pkey.
fun pk(skey): pkey.
fun aenc(bitstring, pkey): bitstring.
reduc forall m: bitstring, sk: skey; adec(aenc(m,pk(sk)),sk) = m.
(* Digital signatures *)
type sskey.
type spkey.
fun spk(sskey): spkey.
fun sign(bitstring, sskey): bitstring.
reduc forall m: bitstring, ssk: sskey; getmess(sign(m,ssk)) = m.
reduc forall m: bitstring, ssk: sskey; checksign(sign(m,ssk),spk(ssk)) = m.
free c:channel.
free s:bitstring [private].
query attacker(s).
event acceptsClient(key).
event acceptsServer(key,pkey).
event termClient(key,pkey).
event termServer(key).
query x:key,y:pkey; event(termClient(x,y))==>event(acceptsServer(x,y)).
query x:key; inj-event(termServer(x))==>inj-event(acceptsClient(x)).
****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
event acceptsClient(k);
out(c,senc(s,k));
event termClient(k,pkA).
****let serverB(pkB:spkey,skB:sskey,pkA:pkey) = ****
in(c,pkX:pkey);
****new k:key; ****
event acceptsServer(k,pkX);
out(c,aenc(sign((pkB,k),skB),pkX));
****in(c,x:bitstring); ****
let z = sdec(x,k) in
if pkX = pkA then event termServer(k).
****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,pkA)) )
仍然存在中间人攻击，继续改进
type key.
fun 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.
reduc forall m: bitstring, sk: skey; adec(aenc(m,pk(sk)),sk) = m.
type sskey.
type spkey.
fun spk(sskey): spkey.
fun sign(bitstring, sskey): bitstring.
reduc forall m: bitstring, ssk: sskey; getmess(sign(m,ssk)) = m.
reduc forall m: bitstring, ssk: sskey; checksign(sign(m,ssk),spk(ssk)) = m.
free c:channel.
free s:bitstring [private].
query attacker(s).
event acceptsClient(key).
event acceptsServer(key,pkey).
event termClient(key,pkey).
event termServer(key).
query x:key,y:pkey; event(termClient(x,y))==>event(acceptsServer(x,y)).
query x:key; inj-event(termServer(x))==>inj-event(acceptsClient(x)).
****let clientA(pkA:pkey,skA:skey,pkB:spkey) = ****
out(c,pkA);
****in(c,x:bitstring); ****
let y = adec(x,skA) in
let (=pkA,=pkB,k:key) = checksign(y,pkB) in
event acceptsClient(k);
out(c,senc(s,k));
event termClient(k,pkA).
****let serverB(pkB:spkey,skB:sskey,pkA:pkey) = ****
in(c,pkX:pkey);
****new k:key; ****
event acceptsServer(k,pkX);
out(c,aenc(sign((pkX,pkB,k),skB),pkX));
****in(c,x:bitstring); ****
let z = sdec(x,k) in
if pkX = pkA then event termServer(k).
****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,pkA)) )
改进完成，没有漏洞。
四．Needham-Schroeder Protocol协议
Needham-Schroeder是一个基于对称加密算法的协议，它要求有可信任的第三方KDC参与，采用Challenge/Response的方式，使得A、B互相认证对方的身份。
1.NeedhamSchroederPK-var1.pv
free c: channel.
(* Public key encryption *)
type pkey.
type skey.
fun pk(skey): pkey.
fun aenc(bitstring, pkey): bitstring.
reduc forall x: bitstring, y: skey; adec(aenc(x, pk(y)),y) = x.
(* Signatures *)
type spkey.
type sskey.
fun spk(sskey): spkey.
fun sign(bitstring, sskey): bitstring.
reduc forall x: bitstring, y: sskey; getmess(sign(x,y)) = x.
reduc forall x: bitstring, y: sskey; checksign(sign(x,y), spk(y)) = x.
(* Shared key encryption *)
fun senc(bitstring,bitstring): bitstring.
reduc forall x: bitstring, y: bitstring; sdec(senc(x,y),y) = x.
(* Authentication queries *)
event beginBparam(pkey).
event endBparam(pkey).
event beginAparam(pkey).
event endAparam(pkey).
query x: pkey; inj-event(endBparam(x)) ==> inj-event(beginBparam(x)).
query x: pkey; inj-event(endAparam(x)) ==> inj-event(beginAparam(x)).
(* Secrecy queries *)
free secretANa, secretANb, secretBNa, secretBNb: bitstring [private].
query attacker(secretANa);
**** attacker(secretANb);****
**** attacker(secretBNa);****
**** attacker(secretBNb).****
(* Alice *)
let processA(pkB: pkey, skA: skey) =
in(c, pkX: pkey);
****event beginBparam(pkX); ****
****new Na: bitstring; ****
out(c, aenc((Na, pk(skA)), pkX));
****in(c, m: bitstring); ****
let (=Na, NX: bitstring) = adec(m, skA) in
out(c, aenc(NX, pkX));
if pkX = pkB then
event endAparam(pk(skA));
out(c, senc(secretANa, Na));
out(c, senc(secretANb, NX)).
(* Bob *)
let processB(pkA: pkey, skB: skey) =
in(c, m: bitstring);
let (NY: bitstring, pkY: pkey) = adec(m, skB) in
event beginAparam(pkY);
new Nb: bitstring;
out(c, aenc((NY, Nb), pkY));
in(c, m3: bitstring);
if Nb = adec(m3, skB) then
if pkY = pkA then
event endBparam(pk(skB));
out(c, senc(secretBNa, NY));
out(c, senc(secretBNb, Nb)).
(* Main *)
****process ****
new skA: skey; let pkA = pk(skA) in out(c, pkA);
new skB: skey; let pkB = pk(skB) in out(c, pkB);
( (!processA(pkB, skA)) | (!processB(pkA, skB)) )
漏洞分析
注入攻击检测不完善
查询 inj-event(endBparam(x)) ==> inj-event(beginBparam(x)) is false 表明系统在B参数结束时未能检测到注入攻击。这可能意味着系统对于某些情况下的注入攻击检测不够强大，需要进一步改进。
密钥泄漏问题
查询 not attacker(secretBNa[]) is false 和 not attacker(secretBNb[]) is false 表明攻击者能够获取B的某些密钥。这可能是系统中的一个重大漏洞，需要加强密钥管理和保护机制，以防止攻击者获取关键信息。
部分成功的注入攻击
查询 inj-event(endAparam(x)) ==> inj-event(beginAparam(x)) is true 表明系统在A参数结束时检测到了注入攻击。这可能表示在某些情况下系统能够成功地检测到攻击，但在其他情况下可能会失败。需要深入研究系统在各种场景下的注入攻击检测能力。
部分密钥保护
查询 not attacker(secretANa[]) is true 和 not attacker(secretANb[]) is true 表明攻击者无法获取A的某些密钥。这是系统的一个积极方面，但仍然需要确保所有关键密钥都得到足够的保护。
- NeedhamSchroederPK-var2.pv
free c: channel.
(* Public key encryption *)
type pkey.
type skey.
fun pk(skey): pkey.
fun aenc(bitstring, pkey): bitstring.
reduc forall x: bitstring, y: skey; adec(aenc(x, pk(y)),y) = x.
(* Signatures *)
type spkey.
type sskey.
fun spk(sskey): spkey.
fun sign(bitstring, sskey): bitstring.
reduc forall x: bitstring, y: sskey; getmess(sign(x,y)) = x.
reduc forall x: bitstring, y: sskey; checksign(sign(x,y), spk(y)) = x.
(* Shared key encryption *)
type nonce.
fun senc(bitstring,nonce): bitstring.
reduc forall x: bitstring, y: nonce; sdec(senc(x,y),y) = x.
(* Type converter *)
fun nonce_to_bitstring(nonce): bitstring [data,typeConverter].
(* Two honest host names A and B *)
type host.
free A, B: host.
(* Key table *)
table keys(host, pkey).
(* Authentication queries *)
event beginBparam(host).
event endBparam(host).
event beginAparam(host).
event endAparam(host).
query x: host; inj-event(endBparam(x)) ==> inj-event(beginBparam(x)).
query x: host; inj-event(endAparam(x)) ==> inj-event(beginAparam(x)).
(* Secrecy queries *)
free secretANa, secretANb, secretBNa, secretBNb: bitstring [private].
query attacker(secretANa);
**** attacker(secretANb);****
**** attacker(secretBNa);****
**** attacker(secretBNb).****
(* Alice *)
let processA(pkS: spkey, skA: skey) =
in(c, hostX: host);
****event beginBparam(hostX); ****
out(c, (A, hostX)); (* msg 1 *)
in(c, ms: bitstring); (* msg 2 *)
let (pkX: pkey, =hostX) = checksign(ms, pkS) in
****new Na: nonce; ****
out(c, aenc((Na, A), pkX)); (* msg 3 *)
in(c, m: bitstring); (* msg 6 *)
let (=Na, NX: nonce) = adec(m, skA) in
out(c, aenc(nonce_to_bitstring(NX), pkX)); (* msg 7 *)
if hostX = B then
event endAparam(A);
out(c, senc(secretANa, Na));
out(c, senc(secretANb, NX)).
(* Bob *)
let processB(pkS: spkey, skB: skey) =
in(c, m: bitstring); (* msg 3 *)
let (NY: nonce, hostY: host) = adec(m, skB) in
event beginAparam(hostY);
out(c, (B, hostY)); (* msg 4 *)
in(c,ms: bitstring); (* msg 5 *)
let (pkY: pkey,=hostY) = checksign(ms, pkS) in
new Nb: nonce;
out(c, aenc((NY, Nb), pkY)); (* msg 6 *)
in(c, m3: bitstring); (* msg 7 *)
if nonce_to_bitstring(Nb) = adec(m3, skB) then
if hostY = A then
event endBparam(B);
out(c, senc(secretBNa, NY));
out(c, senc(secretBNb, Nb)).
(* Trusted key server *)
****let processS(skS: sskey) = ****
****in(c,(a: host, b: host)); ****
get keys(=b, sb) in
out(c,sign((sb,b), skS)).
(* Key registration *)
let processK =
in(c, (h: host, k: pkey));
if h <> A && h <> B then insert keys(h,k).
(* Main *)
****process ****
new skA: skey; let pkA = pk(skA) in out(c, pkA); insert keys(A, pkA);
new skB: skey; let pkB = pk(skB) in out(c, pkB); insert keys(B, pkB);
new skS: sskey; let pkS = spk(skS) in out(c, pkS);
****( (!processA(pkS, skA)) | (!processB(pkS, skB)) | ****
**** (!processS(skS)) | (!processK) )****
- NeedhamSchroederPK-var3.pv
(* Loops if types are ignored *)
set ignoreTypes = false.
free c: channel.
type host.
type nonce.
type pkey.
type skey.
type spkey.
type sskey.
fun nonce_to_bitstring(nonce): bitstring [data,typeConverter].
(* Public key encryption *)
fun pk(skey): pkey.
fun encrypt(bitstring, pkey): bitstring.
reduc forall x: bitstring, y: skey; decrypt(encrypt(x,pk(y)),y) = x.
(* Signatures *)
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.
(* Shared key encryption *)
fun sencrypt(bitstring,nonce): bitstring.
reduc forall x: bitstring, y: nonce; sdecrypt(sencrypt(x,y),y) = x.
(* Secrecy assumptions *)
not attacker(new skA).
not attacker(new skB).
not attacker(new skS).
(* 2 honest host names A and B *)
free A, B: host.
table keys(host, pkey).
(* Queries *)
free secretANa, secretANb, secretBNa, secretBNb: bitstring [private].
query attacker(secretANa);
**** attacker(secretANb);****
**** attacker(secretBNa);****
**** attacker(secretBNb).****
event beginBparam(host, host).
event endBparam(host, host).
event beginAparam(host, host).
event endAparam(host, host).
event beginBfull(host, host, pkey, pkey, nonce, nonce).
event endBfull(host, host, pkey, pkey, nonce, nonce).
event beginAfull(host, host, pkey, pkey, nonce, nonce).
event endAfull(host, host, pkey, pkey, nonce, nonce).
****query x: host, y: host; ****
inj-event(endBparam(x,y)) ==> inj-event(beginBparam(x,y)).
****query x1: host, x2: host, x3: pkey, x4: pkey, x5: nonce, x6: nonce; ****
****inj-event(endBfull(x1,x2,x3,x4,x5,x6)) ****
==> inj-event(beginBfull(x1,x2,x3,x4,x5,x6)).
****query x: host, y: host; ****
inj-event(endAparam(x,y)) ==> inj-event(beginAparam(x,y)).
****query x1: host, x2: host, x3: pkey, x4: pkey, x5: nonce, x6: nonce; ****
****inj-event(endAfull(x1,x2,x3,x4,x5,x6)) ****
==> inj-event(beginAfull(x1,x2,x3,x4,x5,x6)).
(* Role of the initiator with identity xA and secret key skxA *)
let processInitiator(pkS: spkey, skA: skey, skB: skey) =
( The attacker starts the initiator by choosing identity xA,*
**** and its interlocutor xB0.****
**** We check that xA is honest (i.e. is A or B)****
**** and get its corresponding key. )***
in(c, (xA: host, hostX: host));
if xA = A || xA = B then
let skxA = if xA = A then skA else skB in
let pkxA = pk(skxA) in
(* Real start of the role *)
****event beginBparam(xA, hostX); ****
(* Message 1: Get the public key certificate for the other host *)
out(c, (xA, hostX));
(* Message 2 *)
****in(c, ms: bitstring); ****
let (pkX: pkey, =hostX) = checksign(ms,pkS) in
(* Message 3 *)
****new Na: nonce; ****
out(c, encrypt((Na, xA), pkX));
(* Message 6 *)
****in(c, m: bitstring); ****
let (=Na, NX2: nonce) = decrypt(m, skxA) in
event beginBfull(xA, hostX, pkX, pkxA, Na, NX2);
(* Message 7 *)
out(c, encrypt(nonce_to_bitstring(NX2), pkX));
(* OK *)
if hostX = B || hostX = A then
event endAparam(xA, hostX);
event endAfull(xA, hostX, pkX, pkxA, Na, NX2);
out(c, sencrypt(secretANa, Na));
out(c, sencrypt(secretANb, NX2)).
(* Role of the responder with identity xB and secret key skxB *)
let processResponder(pkS: spkey, skA: skey, skB: skey) =
( The attacker starts the responder by choosing identity xB.*
**** We check that xB is honest (i.e. is A or B). )***
in(c, xB: host);
if xB = A || xB = B then
let skxB = if xB = A then skA else skB in
let pkxB = pk(skxB) in
(* Real start of the role *)
(* Message 3 *)
in(c, m: bitstring);
let (NY: nonce, hostY: host) = decrypt(m, skxB) in
event beginAparam(hostY, xB);
(* Message 4: Get the public key certificate for the other host *)
out(c, (xB, hostY));
(* Message 5 *)
in(c,ms: bitstring);
let (pkY: pkey,=hostY) = checksign(ms,pkS) in
(* Message 6 *)
new Nb: nonce;
event beginAfull(hostY, xB, pkxB, pkY, NY, Nb);
out(c, encrypt((NY, Nb), pkY));
(* Message 7 *)
in(c, m3: bitstring);
if nonce_to_bitstring(Nb) = decrypt(m3, skB) then
(* OK *)
if hostY = A || hostY = B then
event endBparam(hostY, xB);
event endBfull(hostY, xB, pkxB, pkY, NY, Nb);
out(c, sencrypt(secretBNa, NY));
out(c, sencrypt(secretBNb, Nb)).
(* Server *)
****let processS(skS: sskey) = ****
****in(c,(a: host, b: host)); ****
get keys(=b, sb) in
out(c,sign((sb,b),skS)).
(* Key registration *)
let processK =
in(c, (h: host, k: pkey));
if h <> A && h <> B then insert keys(h,k).
(* Main *)
****process ****
new skA: skey; let pkA = pk(skA) in****out(c, pkA); insert keys(A, pkA);
new skB: skey; let pkB = pk(skB) in out(c, pkB); insert keys(B, pkB);
new skS: sskey; let pkS = spk(skS) in out(c, pkS);
(
(* Launch an unbounded number of sessions of the initiator *)
****(!processInitiator(pkS, skA, skB)) | ****
(* Launch an unbounded number of sessions of the responder *)
(!processResponder(pkS, skA, skB)) |
(* Launch an unbounded number of sessions of the server *)
(!processS(skS)) |
(* Key registration process *)
(!processK)
)
漏洞分析
A参数注入漏洞
漏洞分析： 可能存在未经过充分验证和过滤的A参数输入，导致在A参数结束时的注入事件影响了A参数的开始。
攻击方法： 攻击者可能会尝试通过在A参数结束时注入恶意代码或数据，来影响A参数的开始，执行未授权的操作或者篡改系统状态。
B参数比特串保护不足
漏洞分析： 暗示攻击者能够获取B参数的某些比特串，可能意味着存在对B参数比特串的不充分保护。
攻击方法： 攻击者可能会尝试通过拦截或者篡改B参数的比特串，来绕过安全控制，获取敏感信息或者执行未授权的操作。
A完整数据注入漏洞
漏洞分析： 暗示在A的完整数据结束时的注入事件可能影响A的完整数据的开始，表明存在对A完整数据注入的不足防护。
攻击方法： 攻击者可能会试图通过在A完整数据结束时注入恶意数据，来影响A完整数据的开始，导致数据不一致或者执行不当操作。
B完整数据注入漏洞
漏洞分析： 表明在B的完整数据结束时的注入事件无法有效防止在B的完整数据开始时的注入事件，存在B完整数据注入漏洞。
攻击方法： 攻击者可能会尝试通过在B完整数据结束时注入恶意数据，来绕过防护，影响B完整数据的开始，导致数据不一致或者执行不当操作。
引用参考
Needham-Schroeder协议原理及实现(Java)_needham-schroeder的原理-CSDN博客
密码协议形式化分析与可证明安全实验1——使用proverif来分析密码协议-CSDN博客
版权归原作者 m0_61001707 所有， 如有侵权，请联系我们删除。