{"id":7576,"date":"2024-07-14T22:01:01","date_gmt":"2024-07-14T14:01:01","guid":{"rendered":""},"modified":"2024-07-14T22:01:01","modified_gmt":"2024-07-14T14:01:01","slug":"\u3010ProVerif\u5b66\u4e60\u7b14\u8bb0\u30114\uff1a\u4fe1\u606f\u5b89\u5168\u6027\u8d28(Security Property)","status":"publish","type":"post","link":"https:\/\/mushiming.com\/7576.html","title":{"rendered":"\u3010ProVerif\u5b66\u4e60\u7b14\u8bb0\u30114\uff1a\u4fe1\u606f\u5b89\u5168\u6027\u8d28(Security Property)"},"content":{"rendered":"

\n <\/path> \n<\/svg> <\/p>\n

1 Reachability\u548cSecrecy<\/h4>\n

\u8bc1\u660eReachability\u662f\u6700\u57fa\u672c\u7684\u80fd\u529b\uff0c\u56e0\u4e3a\u9700\u8981\u77e5\u9053\u653b\u51fb\u8005\u80fd\u8bbf\u95ee\u5230\u54ea\u4e9bterm\uff0c\u800cSecrecy\u5c31\u53ef\u4ee5\u6839\u636e\u8fd9\u4e2a\u6765\u8bc4\u4f30\u2014\u2014\u80fd\u8bbf\u95ee\u5230\u7684term\u4e0d\u6ee1\u8db3Secrecy\u3002\u8981\u6d4b\u8bd5\u9879 M M <\/span><\/span>M<\/span><\/span><\/span><\/span><\/span>\u5728\u6a21\u578b\u4e2d\u662f\u5426\u6ee1\u8db3Secrecy\uff0c\u5728\u4e3b\u8fdb\u7a0b\u524d\u4f7f\u7528\uff1a
q u e r y    a t t a c k e r ( M ) . \\bold{query} \\ \\ attacker(M). <\/span><\/span>q<\/span>u<\/span>e<\/span>r<\/span>y<\/span><\/span> <\/span> <\/span>a<\/span>t<\/span>t<\/span>a<\/span>c<\/span>k<\/span>e<\/span>r<\/span>(<\/span>M<\/span>)<\/span>.<\/span><\/span><\/span><\/span><\/span><\/span><\/p>\n

\u5176\u4e2d M M <\/span><\/span>M<\/span><\/span><\/span><\/span><\/span>\u662f\u4e00\u4e2a\u6700\u57fa\u672c\u7684\u9879\uff0c\u5373\u4e0d\u5305\u542b\u6790\u6784\u5668\uff0c M M <\/span><\/span>M<\/span><\/span><\/span><\/span><\/span>\u53ef\u4ee5\u5305\u542bfree<\/code>\u5b9a\u4e49\u7684\u540d\u79f0\uff0c\u5f53\u7136\u4e5f\u53ef\u4ee5\u8bbe\u7f6e\u4e3a[private]<\/code>\uff0c\u8fd9\u6837\u653b\u51fb\u8005\u6700\u5f00\u59cb\u662f\u4e0d\u77e5\u9053\u5b83\u7684\u3002<\/p>\n

2 \u4e8b\u4ef6(event)\u76f8\u5173<\/h4>\n

Correspondence Assertions\u5c31\u662f\u8bf4\u67d0\u4e2a\u7a0b\u5e8f\u70b9\u6267\u884c\u4e86\uff0c\u53e6\u4e00\u4e2a\u70b9\u4e00\u5b9a\u5728\u4e4b\u524d\u6267\u884c\u8fc7\u4e86\uff0c\u8981\u5b9a\u4e49\u8fd9\u79cd\u6027\u8d28\u5c31\u9700\u8981\u5f15\u5165\u4e8b\u4ef6(event)\u3002\u4e8b\u4ef6\u4e5f\u53ef\u4ee5\u5305\u542b\u53c2\u6570\uff0c\u4ee5\u7814\u7a76\u53c2\u6570\u4e4b\u95f4\u7684\u5173\u7cfb\u3002\u5b9a\u4e49\u7684\u4e8b\u4ef6\u53ea\u662f\u6807\u8bb0\u8fdb\u7a0b\u4e2d\u7684\u4e00\u4e2a\u91cd\u8981\u4f4d\u7f6e\uff0c\u5e76\u4e0d\u5bf9\u8fdb\u7a0b\u7684\u884c\u4e3a\u4ea7\u751f\u4efb\u4f55\u5f71\u54cd\uff0c\u4e8b\u4ef6\u6309\u5982\u4e0b\u65b9\u5f0f\u5b9a\u4e49\uff1a
e v e n t    e ( M 1 , . . . , M n ) ;   P \\bold{event} \\ \\ e(M_1,...,M_n); \\ P <\/span><\/span>e<\/span>v<\/span>e<\/span>n<\/span>t<\/span><\/span> <\/span> <\/span>e<\/span>(<\/span>M<\/span><\/span>1<\/span><\/span><\/span><\/span>\u200b<\/span><\/span><\/span><\/span><\/span><\/span><\/span><\/span>,<\/span><\/span>.<\/span>.<\/span>.<\/span>,<\/span><\/span>M<\/span><\/span>n<\/span><\/span><\/span><\/span>\u200b<\/span><\/span><\/span><\/span><\/span><\/span><\/span><\/span>)<\/span>;<\/span><\/span> <\/span>P<\/span><\/span><\/span><\/span><\/span><\/span><\/p>\n

\u56e0\u4e3a\u4e8b\u4ef6\u4e0d\u4ea7\u751f\u4efb\u4f55\u5f71\u54cd\uff0c\u6240\u4ee5\u8fd9\u91cc\u9762\u7684\u9879 M 1 , . . . , M n M_1,...,M_n <\/span><\/span>M<\/span><\/span>1<\/span><\/span><\/span><\/span>\u200b<\/span><\/span><\/span><\/span><\/span><\/span><\/span><\/span>,<\/span><\/span>.<\/span>.<\/span>.<\/span>,<\/span><\/span>M<\/span><\/span>n<\/span><\/span><\/span><\/span>\u200b<\/span><\/span><\/span><\/span><\/span><\/span><\/span><\/span><\/span><\/span><\/span><\/span>\u4e5f\u4e0d\u4f1a\u6269\u5c55\u8fd9\u4e2a\u8fdb\u7a0b\u7684\u77e5\u8bc6\u3002\u4e8b\u4ef6\u5fc5\u987b\u5728\u4f7f\u7528\u524d\u4ee5 e v e n t    e ( t 1 , . . . , t n ) . event \\ \\ e(t_1,...,t_n). <\/span><\/span>e<\/span>v<\/span>e<\/span>n<\/span>t<\/span> <\/span> <\/span>e<\/span>(<\/span>t<\/span><\/span>1<\/span><\/span><\/span><\/span>\u200b<\/span><\/span><\/span><\/span><\/span><\/span><\/span><\/span>,<\/span><\/span>.<\/span>.<\/span>.<\/span>,<\/span><\/span>t<\/span><\/span>n<\/span><\/span><\/span><\/span>\u200b<\/span><\/span><\/span><\/span><\/span><\/span><\/span><\/span>)<\/span>.<\/span><\/span><\/span><\/span><\/span>\u7684\u5f62\u5f0f\u58f0\u660e\uff0c\u5176\u4e2d\u7684 t 1 , . . . , t n t_1,...,t_n <\/span><\/span>t<\/span><\/span>1<\/span><\/span><\/span><\/span>\u200b<\/span><\/span><\/span><\/span><\/span><\/span><\/span><\/span>,<\/span><\/span>.<\/span>.<\/span>.<\/span>,<\/span><\/span>t<\/span><\/span>n<\/span><\/span><\/span><\/span>\u200b<\/span><\/span><\/span><\/span><\/span><\/span><\/span><\/span><\/span><\/span><\/span><\/span>\u662f\u53c2\u6570\u7c7b\u578b\u3002<\/p>\n

2.1 Correspondence\u65ad\u8a00<\/h5>\n

\u67e5\u8be2Correspondence\u7684\u8bed\u6cd5\u5982\u4e0b\uff1a
q u e r y    x 1 : t 1 , . . . , x n : t n ;   e v e n t ( e ( M 1 , . . . , M j ) ) = = > e v e n t ( e \u2032 ( N 1 , . . . , N k ) ) . \\bold{query} \\ \\ x_1 : t_1,...,x_n : t_n ; \\ \\bold{event}(e(M_1,...,M_j)) ==> \\bold{event}(e'(N_1,...,N_k)). <\/span><\/span>q<\/span>u<\/span>e<\/span>r<\/span>y<\/span><\/span> <\/span> <\/span>x<\/span><\/span>1<\/span><\/span><\/span><\/span>\u200b<\/span><\/span><\/span><\/span><\/span><\/span><\/span><\/span><\/span>:<\/span><\/span><\/span><\/span>t<\/span><\/span>1<\/span><\/span><\/span><\/span>\u200b<\/span><\/span><\/span><\/span><\/span><\/span><\/span><\/span>,<\/span><\/span>.<\/span>.<\/span>.<\/span>,<\/span><\/span>x<\/span><\/span>n<\/span><\/span><\/span><\/span>\u200b<\/span><\/span><\/span><\/span><\/span><\/span><\/span><\/span><\/span>:<\/span><\/span><\/span><\/span>t<\/span><\/span>n<\/span><\/span><\/span><\/span>\u200b<\/span><\/span><\/span><\/span><\/span><\/span><\/span><\/span>;<\/span><\/span> <\/span>e<\/span>v<\/span>e<\/span>n<\/span>t<\/span><\/span>(<\/span>e<\/span>(<\/span>M<\/span><\/span>1<\/span><\/span><\/span><\/span>\u200b<\/span><\/span><\/span><\/span><\/span><\/span><\/span><\/span>,<\/span><\/span>.<\/span>.<\/span>.<\/span>,<\/span><\/span>M<\/span><\/span>j<\/span><\/span><\/span><\/span>\u200b<\/span><\/span><\/span><\/span><\/span><\/span><\/span><\/span>)<\/span>)<\/span><\/span>=<\/span><\/span><\/span>=<\/span><\/span><\/span>><\/span><\/span><\/span><\/span>e<\/span>v<\/span>e<\/span>n<\/span>t<\/span><\/span>(<\/span>e<\/span><\/span>\u2032<\/span><\/span><\/span><\/span><\/span><\/span><\/span><\/span><\/span>(<\/span>N<\/span><\/span>1<\/span><\/span><\/span><\/span>\u200b<\/span><\/span><\/span><\/span><\/span><\/span><\/span><\/span>,<\/span><\/span>.<\/span>.<\/span>.<\/span>,<\/span><\/span>N<\/span><\/span>k<\/span><\/span><\/span><\/span>\u200b<\/span><\/span><\/span><\/span><\/span><\/span><\/span><\/span>)<\/span>)<\/span>.<\/span><\/span><\/span><\/span><\/span><\/span><\/p>\n

\u8fd9\u4e2a\u67e5\u8be2\u6210\u7acb\u7684\u6761\u4ef6\u662f\uff0c\u5bf9\u4e8e\u6bcf\u6b21\u4e8b\u4ef6 e ( M 1 , . . . , M j ) e(M_1,...,M_j) <\/span><\/span>e<\/span>(<\/span>M<\/span><\/span>1<\/span><\/span><\/span><\/span>\u200b<\/span><\/span><\/span><\/span><\/span><\/span><\/span><\/span>,<\/span><\/span>.<\/span>.<\/span>.<\/span>,<\/span><\/span>M<\/span><\/span>j<\/span><\/span><\/span><\/span>\u200b<\/span><\/span><\/span><\/span><\/span><\/span><\/span><\/span>)<\/span><\/span><\/span><\/span><\/span>\u53d1\u751f\uff0c\u90fd\u80fd\u5728\u6b64\u524d\u627e\u5230\u4e00\u4e2a\u4f4d\u7f6e\u6709\u4e8b\u4ef6 e \u2032 ( N 1 , . . . , N k ) e'(N_1,...,N_k) <\/span><\/span>e<\/span><\/span>\u2032<\/span><\/span><\/span><\/span><\/span><\/span><\/span><\/span><\/span>(<\/span>N<\/span><\/span>1<\/span><\/span><\/span><\/span>\u200b<\/span><\/span><\/span><\/span><\/span><\/span><\/span><\/span>,<\/span><\/span>.<\/span>.<\/span>.<\/span>,<\/span><\/span>N<\/span><\/span>k<\/span><\/span><\/span><\/span>\u200b<\/span><\/span><\/span><\/span><\/span><\/span><\/span><\/span>)<\/span><\/span><\/span><\/span><\/span>\u53d1\u751f\u3002\u66f4\u8fdb\u4e00\u6b65\uff0c\u4e8b\u4ef6\u7684\u53c2\u6570\u5fc5\u987b\u6ee1\u8db3\u6240\u5b9a\u4e49\u7684\u5173\u7cfb\uff0c\u4e5f\u5c31\u662f\u8bf4\u53d8\u91cf x 1 , . . . , x n x_1,...,x_n <\/span><\/span>x<\/span><\/span>1<\/span><\/span><\/span><\/span>\u200b<\/span><\/span><\/span><\/span><\/span><\/span><\/span><\/span>,<\/span><\/span>.<\/span>.<\/span>.<\/span>,<\/span><\/span>x<\/span><\/span>n<\/span><\/span><\/span><\/span>\u200b<\/span><\/span><\/span><\/span><\/span><\/span><\/span><\/span><\/span><\/span><\/span><\/span>\u5728 M 1 , . . . , M j M_1,...,M_j <\/span><\/span>M<\/span><\/span>1<\/span><\/span><\/span><\/span>\u200b<\/span><\/span><\/span><\/span><\/span><\/span><\/span><\/span>,<\/span><\/span>.<\/span>.<\/span>.<\/span>,<\/span><\/span>M<\/span><\/span>j<\/span><\/span><\/span><\/span>\u200b<\/span><\/span><\/span><\/span><\/span><\/span><\/span><\/span><\/span><\/span><\/span><\/span>\u548c N 1 , . . . , N k N_1,...,N_k <\/span><\/span>N<\/span><\/span>1<\/span><\/span><\/span><\/span>\u200b<\/span><\/span><\/span><\/span><\/span><\/span><\/span><\/span>,<\/span><\/span>.<\/span>.<\/span>.<\/span>,<\/span><\/span>N<\/span><\/span>k<\/span><\/span><\/span><\/span>\u200b<\/span><\/span><\/span><\/span><\/span><\/span><\/span><\/span><\/span><\/span><\/span><\/span>\u4e2d\u662f\u6709\u76f8\u540c\u7684\u503c\u7684\u3002<\/p>\n

\u6ce8\u610f\uff0c\u5728 = = > ==> <\/span><\/span>=<\/span><\/span><\/span>=<\/span><\/span><\/span>><\/span><\/span><\/span><\/span><\/span>\u4e4b\u524d\u7684\u4e8b\u4ef6\u4e2d\u51fa\u73b0\u7684\u53c2\u6570\u76f8\u5f53\u4e8e\u662f\u88ab\u5168\u79f0\u91cf\u8bcd\u4fee\u9970\u7684\uff1b\u800c\u5728 = = > ==> <\/span><\/span>=<\/span><\/span><\/span>=<\/span><\/span><\/span>><\/span><\/span><\/span><\/span><\/span>\u4e4b\u540e\u7684\u4e8b\u4ef6\u4e2d\u51fa\u73b0\uff0c\u4e14\u5728\u524d\u9762\u6ca1\u6709\u51fa\u73b0<\/strong>\u7684\u7684\u53c2\u6570\u662f\u88ab\u5b58\u5728\u91cf\u8bcd\u4fee\u9970\u7684\u3002\u4f8b\u5982\uff1a
q u e r y    x : t 1 , y : t 2 , z : t 3 ; e v e n t ( e ( x , y ) ) = = > e v e n t ( e \u2032 ( y , z ) ) . \\bold{query} \\ \\ x : t_1,y : t_2,z : t_3 ; \\bold{event}(e(x,y)) ==> \\bold{event}(e'(y,z)). <\/span><\/span>q<\/span>u<\/span>e<\/span>r<\/span>y<\/span><\/span> <\/span> <\/span>x<\/span><\/span>:<\/span><\/span><\/span><\/span>t<\/span><\/span>1<\/span><\/span><\/span><\/span>\u200b<\/span><\/span><\/span><\/span><\/span><\/span><\/span><\/span>,<\/span><\/span>y<\/span><\/span>:<\/span><\/span><\/span><\/span>t<\/span><\/span>2<\/span><\/span><\/span><\/span>\u200b<\/span><\/span><\/span><\/span><\/span><\/span><\/span><\/span>,<\/span><\/span>z<\/span><\/span>:<\/span><\/span><\/span><\/span>t<\/span><\/span>3<\/span><\/span><\/span><\/span>\u200b<\/span><\/span><\/span><\/span><\/span><\/span><\/span><\/span>;<\/span><\/span>e<\/span>v<\/span>e<\/span>n<\/span>t<\/span><\/span>(<\/span>e<\/span>(<\/span>x<\/span>,<\/span><\/span>y<\/span>)<\/span>)<\/span><\/span>=<\/span><\/span><\/span>=<\/span><\/span><\/span>><\/span><\/span><\/span><\/span>e<\/span>v<\/span>e<\/span>n<\/span>t<\/span><\/span>(<\/span>e<\/span><\/span>\u2032<\/span><\/span><\/span><\/span><\/span><\/span><\/span><\/span><\/span>(<\/span>y<\/span>,<\/span><\/span>z<\/span>)<\/span>)<\/span>.<\/span><\/span><\/span><\/span><\/span><\/span><\/p>\n

\u8fd9\u8868\u793a\u5bf9\u4e8e x , y x,y <\/span><\/span>x<\/span>,<\/span><\/span>y<\/span><\/span><\/span><\/span><\/span>\u7684\u6bcf\u6b21\u51fa\u73b0 e ( x , y ) e(x,y) <\/span><\/span>e<\/span>(<\/span>x<\/span>,<\/span><\/span>y<\/span>)<\/span><\/span><\/span><\/span><\/span>\uff0c\u603b\u662f\u5b58\u5728\u4e00\u4e2a z z <\/span><\/span>z<\/span><\/span><\/span><\/span><\/span>\u4f7f\u5f97 e \u2032 ( y , z ) e'(y,z) <\/span><\/span>e<\/span><\/span>\u2032<\/span><\/span><\/span><\/span><\/span><\/span><\/span><\/span><\/span>(<\/span>y<\/span>,<\/span><\/span>z<\/span>)<\/span><\/span><\/span><\/span><\/span>\u51fa\u73b0\u3002<\/p>\n

2.2 Injective Correspondence\u65ad\u8a00<\/h5>\n

\u5982\u679c\u671f\u671b\u534f\u8bae\u53cc\u65b9\u7684\u65f6\u95f4\u662f\u53ea\u53d1\u751f\u4e00\u6b21\u7684\uff08\u5373one-to-one\u7684\uff09\uff0c\u90a3\u4e482.1<\/code>\u4e2d\u5b66\u4e60\u7684Correspondence\u4e0d\u8db3\u4ee5\u8868\u8fbeAuthentication\uff08\u8ba4\u8bc1\u5173\u7cfb\uff09\u3002\u6bd4\u5982\u670d\u52a1\u5668\u5411\u5ba2\u6237\u7aef\u8bf7\u6c42\u7f34\u8d39\uff0c\u5ba2\u6237\u7aef\u7f34\u8d39\u4e00\u6b21\u5e94\u8be5\u5bf9\u5e94\u670d\u52a1\u5668\u6536\u8d39\u4e00\u6b21\uff0c\u5426\u5219\u5ba2\u6237\u7aef\u7f34\u8d39\u4e00\u6b21\u5bf9\u5e94\u670d\u52a1\u5668\u6536\u8d39\u591a\u6b21\u8fd9\u6837\u5c31\u4e0d\u6b63\u786e\u4e86\u3002Injective Correspondence\u65ad\u8a00\u53ef\u4ee5\u8868\u8fbe\u8fd9\u79cd\u4e00\u5bf9\u4e00\u5173\u7cfb\uff0c\u5176\u8bed\u6cd5\u5982\u4e0b\uff1a
q u e r y    x 1 : t 1 , . . . , x n : t n ;   i n j \u2212 e v e n t ( e ( M 1 , . . . , M j ) ) = = > i n j \u2212 e v e n t ( e \u2032 ( N 1 , . . . , N k ) ) . \\bold{query} \\ \\ x_1 : t_1,...,x_n : t_n ; \\ \\bold{inj\u2212event}(e(M_1,...,M_j)) ==> \\bold{inj\u2212event}(e'(N_1,...,N_k)). <\/span><\/span>q<\/span>u<\/span>e<\/span>r<\/span>y<\/span><\/span> <\/span> <\/span>x<\/span><\/span>1<\/span><\/span><\/span><\/span>\u200b<\/span><\/span><\/span><\/span><\/span><\/span><\/span><\/span><\/span>:<\/span><\/span><\/span><\/span>t<\/span><\/span>1<\/span><\/span><\/span><\/span>\u200b<\/span><\/span><\/span><\/span><\/span><\/span><\/span><\/span>,<\/span><\/span>.<\/span>.<\/span>.<\/span>,<\/span><\/span>x<\/span><\/span>n<\/span><\/span><\/span><\/span>\u200b<\/span><\/span><\/span><\/span><\/span><\/span><\/span><\/span><\/span>:<\/span><\/span><\/span><\/span>t<\/span><\/span>n<\/span><\/span><\/span><\/span>\u200b<\/span><\/span><\/span><\/span><\/span><\/span><\/span><\/span>;<\/span><\/span> <\/span>i<\/span>n<\/span>j<\/span>\u2212<\/span>e<\/span>v<\/span>e<\/span>n<\/span>t<\/span><\/span>(<\/span>e<\/span>(<\/span>M<\/span><\/span>1<\/span><\/span><\/span><\/span>\u200b<\/span><\/span><\/span><\/span><\/span><\/span><\/span><\/span>,<\/span><\/span>.<\/span>.<\/span>.<\/span>,<\/span><\/span>M<\/span><\/span>j<\/span><\/span><\/span><\/span>\u200b<\/span><\/span><\/span><\/span><\/span><\/span><\/span><\/span>)<\/span>)<\/span><\/span>=<\/span><\/span><\/span>=<\/span><\/span><\/span>><\/span><\/span><\/span><\/span>i<\/span>n<\/span>j<\/span>\u2212<\/span>e<\/span>v<\/span>e<\/span>n<\/span>t<\/span><\/span>(<\/span>e<\/span><\/span>\u2032<\/span><\/span><\/span><\/span><\/span><\/span><\/span><\/span><\/span>(<\/span>N<\/span><\/span>1<\/span><\/span><\/span><\/span>\u200b<\/span><\/span><\/span><\/span><\/span><\/span><\/span><\/span>,<\/span><\/span>.<\/span>.<\/span>.<\/span>,<\/span><\/span>N<\/span><\/span>k<\/span><\/span><\/span><\/span>\u200b<\/span><\/span><\/span><\/span><\/span><\/span><\/span><\/span>)<\/span>)<\/span>.<\/span><\/span><\/span><\/span><\/span><\/span><\/p>\n

\u8fd9\u4e2a\u610f\u601d\u662f = = > ==> <\/span><\/span>=<\/span><\/span><\/span>=<\/span><\/span><\/span>><\/span><\/span><\/span><\/span><\/span>\u4e4b\u540e\u7684 e \u2032 e' <\/span><\/span>e<\/span><\/span>\u2032<\/span><\/span><\/span><\/span><\/span><\/span><\/span><\/span><\/span><\/span><\/span><\/span><\/span>\u7684\u53d1\u751f\u6b21\u6570\u5927\u4e8e\u7b49\u4e8e<\/strong> = = > ==> <\/span><\/span>=<\/span><\/span><\/span>=<\/span><\/span><\/span>><\/span><\/span><\/span><\/span><\/span>\u4e4b\u524d\u7684 e e <\/span><\/span>e<\/span><\/span><\/span><\/span><\/span>\u7684\u53d1\u751f\u6b21\u6570\u7684\u3002\u53e6\u5916\u8981\u6ce8\u610f\uff0c = = > ==> <\/span><\/span>=<\/span><\/span><\/span>=<\/span><\/span><\/span>><\/span><\/span><\/span><\/span><\/span>\u4e4b\u524d\u5199 i n j \u2212 e v e n t inj-event <\/span><\/span>i<\/span>n<\/span>j<\/span><\/span>\u2212<\/span><\/span><\/span><\/span>e<\/span>v<\/span>e<\/span>n<\/span>t<\/span><\/span><\/span><\/span><\/span>\u6216\u8005\u5199 e v e n t event <\/span><\/span>e<\/span>v<\/span>e<\/span>n<\/span>t<\/span><\/span><\/span><\/span><\/span>\u90fd\u884c\uff0c\u53ea\u6709\u7bad\u5934\u4e4b\u540e\u5199\u4ec0\u4e48\u624d\u91cd\u8981\u3002<\/p>\n

3 \u793a\u4f8b\uff1a\u63e1\u624b\u534f\u8bae\u4e2d\u7684\u4fdd\u5bc6\u6027\u548c\u8ba4\u8bc1\u6027<\/h4>\n

\u63e1\u624b\u534f\u8bae\u4e2d\u662f\u6d89\u53ca\u8ba4\u8bc1\u6027\u8d28\u7684\uff0c\u5982\u5ba2\u6237\u7aefA\u8ba4\u4e3a\u5979\u5728\u548c\u670d\u52a1\u5668B\u901a\u4fe1\uff0c\u90a3\u4e48\u6027\u8d28\u5c31\u8981\u6c42\u786e\u5b9e\u662f\u5728\u548cB\u901a\u4fe1\uff0c\u53cd\u8fc7\u6765\u4e5f\u662f\u4e00\u6837\u3002\u8fd9\u91cc\u7684\u3010A\u8ba4\u4e3a\u3011\u610f\u601d\u5c31\u662fA\u6240\u63a5\u6536\u5230\u7684\u4fe1\u606f\u8868\u660e\u4e86\u8fd9\u4ef6\u4e8b\uff0c\u56e0\u6b64\u53ef\u4ee5\u58f0\u660e\u5982\u4e0b\u8fd9\u4e9b\u4e8b\u4ef6\uff1a<\/p>\n

    \n
  • event acceptsClient(key)<\/code>\uff1a\u5ba2\u6237\u7aef\u63a5\u53d7\u4e86\u3010\u4f7f\u7528\u6536\u5230\u7684key\u548c\u670d\u52a1\u5668\u4ea4\u4e92\u3011\u8fd9\u4ef6\u4e8b\u3002<\/li>\n
  • event acceptsServer(key,pkey)<\/code>\uff1a\u670d\u52a1\u5668\u63a5\u53d7\u4e86\u3010\u4f7f\u7528key\u548c\u516c\u94a5\u4e3apkey\u7684\u5ba2\u6237\u7aef\u4ea4\u4e92\u3011\u8fd9\u4ef6\u4e8b\u3002<\/li>\n
  • event termClient(key,pkey)<\/code>\uff1a\u5ba2\u6237\u7aef\u8ba4\u4e3a\u5df2\u7ecf\u5b8c\u6210\u4e86\u3010\u4f7f\u7528key\u4e3a\u4f1a\u8bdd\u5bc6\u94a5\u4ee5\u53capkey\u4f5c\u4e3a\u5ba2\u6237\u7aef\u516c\u94a5\uff0c\u548c\u670d\u52a1\u5668\u8fd0\u884c\u534f\u8bae\u3011\u8fd9\u4ef6\u4e8b\u3002<\/li>\n
  • event termServer(key)<\/code>\uff1a\u670d\u52a1\u5668\u8ba4\u4e3a\u5df2\u7ecf\u5b8c\u6210\u4e86\u3010\u4f7f\u7528key\u4f5c\u4e3a\u4f1a\u8bdd\u5bc6\u94a5\uff0c\u548c\u5ba2\u6237\u7aef\u8fd0\u884c\u534f\u8bae\u3011\u8fd9\u4ef6\u4e8b\u3002<\/li>\n<\/ul>\n

    \u5bf9\u5ba2\u6237\u7aefA\u800c\u8a00\uff0c\u5979\u53ea\u60f3\u548c\u670d\u52a1\u5668B\u5206\u4eab\u81ea\u5df1\u7684\u52a0\u5bc6\u4fe1\u606f\uff0c\u6240\u4ee5\u5982\u679c\u5979\u6267\u884c\u5b8c\u534f\u8bae\uff0cB\u5bf9A\u7684\u8ba4\u8bc1\u5c31\u5e94\u8be5\u4fdd\u6301\u3002<\/p>\n

    \u5bf9\u670d\u52a1\u5668B\u800c\u8a00\uff0c\u4ed6\u53ef\u4ee5\u548c\u5f88\u591a\u5ba2\u6237\u7aef\u4ea4\u4e92\uff0c\u6240\u4ee5\u5728\u8fd0\u884c\u5b8c\u534f\u8bae\u4e4b\u540e\uff0c\u5982\u679cB\u8ba4\u4e3aA\u662f\u4ed6\u7684\u5bf9\u8bdd\u8005\uff08 p k X = = p k A pkX==pkA <\/span><\/span>p<\/span>k<\/span>X<\/span><\/span>=<\/span><\/span><\/span>=<\/span><\/span><\/span><\/span>p<\/span>k<\/span>A<\/span><\/span><\/span><\/span><\/span>\uff09\uff0c\u90a3\u4e48A\u5bf9B\u7684\u8ba4\u8bc1\u5c31\u5e94\u8be5\u4fdd\u6301\u3002<\/p>\n

    \u5c06\u4e0a\u9762\u4e24\u6761\u8ba4\u8bc1\u6027\u8d28\u5f62\u5f0f\u5316\uff0c\u4e66\u5199\u4e3a\uff1a
    q u e r y    x : k e y , y : s p k e y ;   e v e n t ( t e r m C l i e n t ( x , y ) ) = = > e v e n t ( a c c e p t s S e r v e r ( x , y ) ) . q u e r y    x : k e y ;   i n j \u2212 e v e n t ( t e r m S e r v e r ( x ) ) = = > i n j \u2212 e v e n t ( a c c e p t s C l i e n t ( x ) ) . \\begin{aligned} \\bold{query} \\ \\ & x:key,y:spkey; \\ \\bold{event}(termClient(x,y))==>\\bold{event}(acceptsServer(x,y)). \\\\ \\bold{query} \\ \\ & x:key; \\ \\bold{inj-event}(termServer(x))==>\\bold{inj-event}(acceptsClient(x)). \\end{aligned} <\/span><\/span><\/span>q<\/span>u<\/span>e<\/span>r<\/span>y<\/span><\/span> <\/span> <\/span><\/span><\/span><\/span>q<\/span>u<\/span>e<\/span>r<\/span>y<\/span><\/span> <\/span> <\/span><\/span><\/span><\/span>\u200b<\/span><\/span><\/span><\/span><\/span><\/span><\/span><\/span><\/span>x<\/span><\/span>:<\/span><\/span>k<\/span>e<\/span>y<\/span>,<\/span><\/span>y<\/span><\/span>:<\/span><\/span>s<\/span>p<\/span>k<\/span>e<\/span>y<\/span>;<\/span><\/span> <\/span>e<\/span>v<\/span>e<\/span>n<\/span>t<\/span><\/span>(<\/span>t<\/span>e<\/span>r<\/span>m<\/span>C<\/span>l<\/span>i<\/span>e<\/span>n<\/span>t<\/span>(<\/span>x<\/span>,<\/span><\/span>y<\/span>)<\/span>)<\/span><\/span>=<\/span>=<\/span>><\/span><\/span>e<\/span>v<\/span>e<\/span>n<\/span>t<\/span><\/span>(<\/span>a<\/span>c<\/span>c<\/span>e<\/span>p<\/span>t<\/span>s<\/span>S<\/span>e<\/span>r<\/span>v<\/span>e<\/span>r<\/span>(<\/span>x<\/span>,<\/span><\/span>y<\/span>)<\/span>)<\/span>.<\/span><\/span><\/span><\/span><\/span>x<\/span><\/span>:<\/span><\/span>k<\/span>e<\/span>y<\/span>;<\/span><\/span> <\/span>i<\/span>n<\/span>j<\/span><\/span>\u2212<\/span><\/span>e<\/span>v<\/span>e<\/span>n<\/span>t<\/span><\/span>(<\/span>t<\/span>e<\/span>r<\/span>m<\/span>S<\/span>e<\/span>r<\/span>v<\/span>e<\/span>r<\/span>(<\/span>x<\/span>)<\/span>)<\/span><\/span>=<\/span>=<\/span>><\/span><\/span>i<\/span>n<\/span>j<\/span><\/span>\u2212<\/span><\/span>e<\/span>v<\/span>e<\/span>n<\/span>t<\/span><\/span>(<\/span>a<\/span>c<\/span>c<\/span>e<\/span>p<\/span>t<\/span>s<\/span>C<\/span>l<\/span>i<\/span>e<\/span>n<\/span>t<\/span>(<\/span>x<\/span>)<\/span>)<\/span>.<\/span><\/span><\/span><\/span>\u200b<\/span><\/span><\/span><\/span><\/span><\/span><\/span><\/span><\/span><\/span><\/span><\/span><\/span><\/span><\/p>\n

    \u8fd9\u4e24\u6761\u5f62\u5f0f\u4e0a\u6709\u5dee\u5f02\u7684\u539f\u56e0\u662f\u5ba2\u6237\u7aef\u548c\u670d\u52a1\u5668\u6240\u671f\u671b\u7684\u8eab\u4efd\u9a8c\u8bc1\u65b9\u5f0f\u662f\u4e0d\u540c\u7684\uff0c\u5176\u4e2d\u7b2c\u4e00\u6761\u4e0d\u662f\u5355\u5c04(injective)\u7684\uff0c\u56e0\u4e3a\u670d\u52a1\u5668\u6ca1\u6709\u5141\u8bb8\u5ba2\u6237\u7aef\u77e5\u9053\u5979\u6536\u5230\u7684\u6d88\u606f\u662f\u5426\u662f\u65b0\u7684\uff0c\u4ece\u670d\u52a1\u5668\u5411\u5ba2\u6237\u7aef\u53ef\u80fd\u53d1\u591a\u4e2a\u6d88\u606f\uff0c\u5c31\u4f1a\u5bfc\u81f4\u5355\u4e2a\u670d\u52a1\u5668session\u5bf9\u5e94\u591a\u4e2a\u5ba2\u6237\u7aefsession\u3002<\/p>\n

    \u52a0\u5165\u8fd9\u4e24\u6761\u8ba4\u8bc1\u6027\u8d28\u7684\u63e1\u624b\u534f\u8bae\u5982\u4e0b\uff1a<\/p>\n

    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)) ) <\/code><\/pre>\n
    \u6ce8\u610f\u5ba2\u6237\u7aef\u548c\u670d\u52a1\u5668\u7684accepts*<\/code>\u4e8b\u4ef6\u548cterm*<\/code>\u4e8b\u4ef6\u7684\u4f4d\u7f6e\u8981\u5728\u5404\u81ea\u7684\u8fdb\u7a0b\u5b8f\u4e2d\u5199\u51fa\u6765\u3002\u901a\u5e38\u4e8b\u4ef6\u653e\u7f6e\u7684\u4f4d\u7f6e\u6309\u7167\u5b83\u7684\u8bed\u4e49\u4e5f\u4e0d\u662f\u552f\u4e00\u7684\uff0c\u5bf9\u4e8e\u4e0a\u9762\u7684\u4e24\u6761\u8ba4\u8bc1\u6027\u8d28\u6d89\u53ca\u7684\u56db\u4e2a\u4e8b\u4ef6\uff0c\u6574\u4e2a\u903b\u8f91\u5c31\u662f\uff08\u53ef\u4ee5\u5206\u6210\u8fd9\u6837\u4e24\u7c7b\u90e8\u5206\u6765\u770b\uff09\uff1a
     \"\u3010ProVerif\u5b66\u4e60\u7b14\u8bb0\u30114\uff1a\u4fe1\u606f\u5b89\u5168\u6027\u8d28(Security<\/p>\n
    \u7eff\u8272\u7684\u90e8\u5206\u5c31\u662f\u3010\u670d\u52a1\u5668\u7ed9\u5ba2\u6237\u7aef\u53d1\u6d88\u606fn-1\u3011\uff0c\u6240\u4ee5\u3010\u670d\u52a1\u5668\u63a5\u53d7\u5173\u7cfb\u5efa\u7acbacceptsServer<\/code>\u3011\u5e94\u8be5\u653e\u5728\u8fd9\u4e2a\u53d1\u9001\u4e4b\u524d\uff0c\u53e6\u5916\u6309\u7167\u5b83\u7684\u8bed\u4e49\u8fd8\u5e94\u8be5\u5728\u3010\u83b7\u53d6\u5230\u5ba2\u6237\u7aef\u53d1\u6765\u7684\u516c\u94a5\u3011\u4e4b\u540e\uff1b\u3010\u5ba2\u6237\u7aef\u534f\u8bae\u786e\u8ba4termClient<\/code>\u3011\u53ef\u4ee5\u653e\u5728\u5ba2\u6237\u7aef\u8fd0\u884c\u672b\u5c3e\uff0c\u6309\u7167\u56fe\u4e0a\u4e00\u5b9a\u8981\u5728\u3010\u63a5\u6536\u5230\u6d88\u606f\u3011\u4e4b\u540e\u3002<\/p>\n
    \u84dd\u8272\u7684\u90e8\u5206\u5c31\u662f\u3010\u5ba2\u6237\u7aef\u7ed9\u670d\u52a1\u5668\u56de\u6d88\u606fn\u3011\uff0c\u6240\u4ee5\u3010\u5ba2\u6237\u7aef\u63a5\u53d7\u5173\u7cfb\u5efa\u7acbacceptsClient<\/code>\u3011\u5e94\u8be5\u662f\u5728\u62ff\u5230key<\/code>\u3001\u9a8c\u8bc1\u8eab\u4efd\u4e4b\u540e\uff0c\u800c\u4e14\u662f\u56de\u53d1\u6d88\u606f\u4e4b\u524d\uff1b\u3010\u670d\u52a1\u5668\u534f\u8bae\u786e\u8ba4termServer<\/code>\u3011\u4e5f\u53ef\u4ee5\u653e\u5728\u672b\u5c3e\uff0c\u4f46\u662f\u4e00\u5b9a\u8981\u5728\u3010\u6536\u5230\u521a\u521a\u7684\u5ba2\u6237\u7aef\u53d1\u6765\u7684\u6d88\u606f\u3011\u4e4b\u540e\uff0c\u6240\u4ee5\u4ee3\u7801\u91cc\u8981\u68c0\u67e5pkX==pkA<\/code>\u624d\u884c\u3002<\/p>\n
    \n
    \u624b\u518c\u91cc\u7ed9\u51fa\u4e86\u4e00\u4e9b\u6280\u5de7\uff0c\u5373\u901a\u5e38\u800c\u8a00==><\/code>\u524d\u9762\u7684\u4e8b\u4ef6\u53ef\u4ee5\u653e\u5728\u8fdb\u7a0b\u672b\u5c3e\uff0c\u800c==><\/code>\u540e\u9762\u7684\u4e8b\u4ef6\uff08\u5728\u53e6\u4e00\u4e2a\u8fdb\u7a0b\uff09\u7684\u4f4d\u7f6e\u540e\u9762\u81f3\u5c11\u5e94\u8be5\u6709\u4e00\u4e2a\u53d1\u9001\u6d88\u606f\u7684\u5730\u65b9\u3002<\/p>\n
    \u8bbee==>e'<\/code>\u5373\u4e0d\u540c\u8fdb\u7a0b\u4e2d\u7684\u4e24\u4e2a\u4e8b\u4ef6\u8fbe\u6210\u8ba4\u8bc1\u5173\u7cfb\uff0c\u901a\u5e38e<\/code>\u6bd4\u8f83\u9760\u540e\uff0ce'<\/code>\u6bd4\u8f83\u9760\u524d\uff0c\u4f46\u662f\u8ba9e<\/code>\u5c3d\u91cf\u5f80\u4e0a\uff0ce'<\/code>\u5c3d\u91cf\u5f80\u4e0b\uff0c\u53ef\u4ee5\u5f3a\u5316\u8fd9\u79cd\u8ba4\u8bc1\u5173\u7cfb\u3002\u8fd8\u6709\u5c31\u662f\u6dfb\u52a0\u4e8b\u4ef6\u7684\u53c2\u6570\u6765\u8fdb\u884c\u9650\u5b9a\u4e5f\u53ef\u4ee5\u5f3a\u5316\u8fd9\u79cd\u8ba4\u8bc1\u5173\u7cfb\u3002<\/p>\n
    \u53c2\u8003\u9605\u8bfb<\/h4>\n
    ProVerif\u7684manual\u7b2c3.2~3.2.3\u7ae0\u8282<\/p>\n","protected":false},"excerpt":{"rendered":"\u3010ProVerif\u5b66\u4e60\u7b14\u8bb0\u30114\uff1a\u4fe1\u606f\u5b89\u5168\u6027\u8d28(Security Property)1Reachability\u548cSecrecy\u8bc1\u660eReachability\u662f\u6700\u57fa\u672c\u7684\u80fd\u529b\uff0c\u56e0\u4e3a\u9700\u8981...","protected":false},"author":1,"featured_media":0,"comment_status":"open","ping_status":"open","sticky":false,"template":"","format":"standard","meta":{"footnotes":""},"categories":[],"tags":[],"_links":{"self":[{"href":"https:\/\/mushiming.com\/wp-json\/wp\/v2\/posts\/7576"}],"collection":[{"href":"https:\/\/mushiming.com\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/mushiming.com\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/mushiming.com\/wp-json\/wp\/v2\/users\/1"}],"replies":[{"embeddable":true,"href":"https:\/\/mushiming.com\/wp-json\/wp\/v2\/comments?post=7576"}],"version-history":[{"count":0,"href":"https:\/\/mushiming.com\/wp-json\/wp\/v2\/posts\/7576\/revisions"}],"wp:attachment":[{"href":"https:\/\/mushiming.com\/wp-json\/wp\/v2\/media?parent=7576"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/mushiming.com\/wp-json\/wp\/v2\/categories?post=7576"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/mushiming.com\/wp-json\/wp\/v2\/tags?post=7576"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}