{"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":"<p><svg xmlns=\"http:\/\/www.w3.org\/2000\/svg\" style=\"display: none;\"> \n <path stroke-linecap=\"round\" d=\"M5,0 0,2.5 5,5z\" id=\"raphael-marker-block\" style=\"-webkit-tap-highlight-color: rgba(0, 0, 0, 0);\"><\/path> \n<\/svg> <\/p>\n<h4>1 Reachability\u548cSecrecy<\/h4>\n<p>\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<span class=\"katex--inline\"><span class=\"katex\"><span class=\"katex-mathml\"> M M <\/span><span class=\"katex-html\"><span class=\"base\"><span class=\"strut\" style=\"height: 0.68333em; vertical-align: 0em;\"><\/span><span class=\"mord mathdefault\" style=\"margin-right: 0.10903em;\">M<\/span><\/span><\/span><\/span><\/span>\u5728\u6a21\u578b\u4e2d\u662f\u5426\u6ee1\u8db3Secrecy\uff0c\u5728\u4e3b\u8fdb\u7a0b\u524d\u4f7f\u7528\uff1a<br \/> <span class=\"katex--display\"><span class=\"katex-display\"><span class=\"katex\"><span class=\"katex-mathml\"> q u e r y &nbsp;&nbsp; a t t a c k e r ( M ) . \\bold{query} \\ \\ attacker(M). <\/span><span class=\"katex-html\"><span class=\"base\"><span class=\"strut\" style=\"height: 1em; vertical-align: -0.25em;\"><\/span><span class=\"mord\"><span class=\"mord mathbf\">q<\/span><span class=\"mord mathbf\">u<\/span><span class=\"mord mathbf\">e<\/span><span class=\"mord mathbf\">r<\/span><span class=\"mord mathbf\" style=\"margin-right: 0.01597em;\">y<\/span><\/span><span class=\"mspace\">&nbsp;<\/span><span class=\"mspace\">&nbsp;<\/span><span class=\"mord mathdefault\">a<\/span><span class=\"mord mathdefault\">t<\/span><span class=\"mord mathdefault\">t<\/span><span class=\"mord mathdefault\">a<\/span><span class=\"mord mathdefault\">c<\/span><span class=\"mord mathdefault\" style=\"margin-right: 0.03148em;\">k<\/span><span class=\"mord mathdefault\">e<\/span><span class=\"mord mathdefault\" style=\"margin-right: 0.02778em;\">r<\/span><span class=\"mopen\">(<\/span><span class=\"mord mathdefault\" style=\"margin-right: 0.10903em;\">M<\/span><span class=\"mclose\">)<\/span><span class=\"mord\">.<\/span><\/span><\/span><\/span><\/span><\/span><\/p>\n<p>\u5176\u4e2d<span class=\"katex--inline\"><span class=\"katex\"><span class=\"katex-mathml\"> M M <\/span><span class=\"katex-html\"><span class=\"base\"><span class=\"strut\" style=\"height: 0.68333em; vertical-align: 0em;\"><\/span><span class=\"mord mathdefault\" style=\"margin-right: 0.10903em;\">M<\/span><\/span><\/span><\/span><\/span>\u662f\u4e00\u4e2a\u6700\u57fa\u672c\u7684\u9879\uff0c\u5373\u4e0d\u5305\u542b\u6790\u6784\u5668\uff0c<span class=\"katex--inline\"><span class=\"katex\"><span class=\"katex-mathml\"> M M <\/span><span class=\"katex-html\"><span class=\"base\"><span class=\"strut\" style=\"height: 0.68333em; vertical-align: 0em;\"><\/span><span class=\"mord mathdefault\" style=\"margin-right: 0.10903em;\">M<\/span><\/span><\/span><\/span><\/span>\u53ef\u4ee5\u5305\u542b<code>free<\/code>\u5b9a\u4e49\u7684\u540d\u79f0\uff0c\u5f53\u7136\u4e5f\u53ef\u4ee5\u8bbe\u7f6e\u4e3a<code>[private]<\/code>\uff0c\u8fd9\u6837\u653b\u51fb\u8005\u6700\u5f00\u59cb\u662f\u4e0d\u77e5\u9053\u5b83\u7684\u3002<\/p>\n<h4>2 \u4e8b\u4ef6(event)\u76f8\u5173<\/h4>\n<p>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<br \/> <span class=\"katex--display\"><span class=\"katex-display\"><span class=\"katex\"><span class=\"katex-mathml\"> e v e n t &nbsp;&nbsp; e ( M 1 , . . . , M n ) ; &nbsp; P \\bold{event} \\ \\ e(M_1,...,M_n); \\ P <\/span><span class=\"katex-html\"><span class=\"base\"><span class=\"strut\" style=\"height: 1em; vertical-align: -0.25em;\"><\/span><span class=\"mord\"><span class=\"mord mathbf\">e<\/span><span class=\"mord mathbf\" style=\"margin-right: 0.01597em;\">v<\/span><span class=\"mord mathbf\">e<\/span><span class=\"mord mathbf\">n<\/span><span class=\"mord mathbf\">t<\/span><\/span><span class=\"mspace\">&nbsp;<\/span><span class=\"mspace\">&nbsp;<\/span><span class=\"mord mathdefault\">e<\/span><span class=\"mopen\">(<\/span><span class=\"mord\"><span class=\"mord mathdefault\" style=\"margin-right: 0.10903em;\">M<\/span><span class=\"msupsub\"><span class=\"vlist-t vlist-t2\"><span class=\"vlist-r\"><span class=\"vlist\" style=\"height: 0.301108em;\"><span class=\"\" style=\"top: -2.55em; margin-left: -0.10903em; margin-right: 0.05em;\"><span class=\"pstrut\" style=\"height: 2.7em;\"><\/span><span class=\"sizing reset-size6 size3 mtight\"><span class=\"mord mtight\">1<\/span><\/span><\/span><\/span><span class=\"vlist-s\">\u200b<\/span><\/span><span class=\"vlist-r\"><span class=\"vlist\" style=\"height: 0.15em;\"><span class=\"\"><\/span><\/span><\/span><\/span><\/span><\/span><span class=\"mpunct\">,<\/span><span class=\"mspace\" style=\"margin-right: 0.166667em;\"><\/span><span class=\"mord\">.<\/span><span class=\"mord\">.<\/span><span class=\"mord\">.<\/span><span class=\"mpunct\">,<\/span><span class=\"mspace\" style=\"margin-right: 0.166667em;\"><\/span><span class=\"mord\"><span class=\"mord mathdefault\" style=\"margin-right: 0.10903em;\">M<\/span><span class=\"msupsub\"><span class=\"vlist-t vlist-t2\"><span class=\"vlist-r\"><span class=\"vlist\" style=\"height: 0.151392em;\"><span class=\"\" style=\"top: -2.55em; margin-left: -0.10903em; margin-right: 0.05em;\"><span class=\"pstrut\" style=\"height: 2.7em;\"><\/span><span class=\"sizing reset-size6 size3 mtight\"><span class=\"mord mathdefault mtight\">n<\/span><\/span><\/span><\/span><span class=\"vlist-s\">\u200b<\/span><\/span><span class=\"vlist-r\"><span class=\"vlist\" style=\"height: 0.15em;\"><span class=\"\"><\/span><\/span><\/span><\/span><\/span><\/span><span class=\"mclose\">)<\/span><span class=\"mpunct\">;<\/span><span class=\"mspace\" style=\"margin-right: 0.166667em;\"><\/span><span class=\"mspace\">&nbsp;<\/span><span class=\"mord mathdefault\" style=\"margin-right: 0.13889em;\">P<\/span><\/span><\/span><\/span><\/span><\/span><\/p>\n<p>\u56e0\u4e3a\u4e8b\u4ef6\u4e0d\u4ea7\u751f\u4efb\u4f55\u5f71\u54cd\uff0c\u6240\u4ee5\u8fd9\u91cc\u9762\u7684\u9879<span class=\"katex--inline\"><span class=\"katex\"><span class=\"katex-mathml\"> M 1 , . . . , M n M_1,...,M_n <\/span><span class=\"katex-html\"><span class=\"base\"><span class=\"strut\" style=\"height: 0.87777em; vertical-align: -0.19444em;\"><\/span><span class=\"mord\"><span class=\"mord mathdefault\" style=\"margin-right: 0.10903em;\">M<\/span><span class=\"msupsub\"><span class=\"vlist-t vlist-t2\"><span class=\"vlist-r\"><span class=\"vlist\" style=\"height: 0.301108em;\"><span class=\"\" style=\"top: -2.55em; margin-left: -0.10903em; margin-right: 0.05em;\"><span class=\"pstrut\" style=\"height: 2.7em;\"><\/span><span class=\"sizing reset-size6 size3 mtight\"><span class=\"mord mtight\">1<\/span><\/span><\/span><\/span><span class=\"vlist-s\">\u200b<\/span><\/span><span class=\"vlist-r\"><span class=\"vlist\" style=\"height: 0.15em;\"><span class=\"\"><\/span><\/span><\/span><\/span><\/span><\/span><span class=\"mpunct\">,<\/span><span class=\"mspace\" style=\"margin-right: 0.166667em;\"><\/span><span class=\"mord\">.<\/span><span class=\"mord\">.<\/span><span class=\"mord\">.<\/span><span class=\"mpunct\">,<\/span><span class=\"mspace\" style=\"margin-right: 0.166667em;\"><\/span><span class=\"mord\"><span class=\"mord mathdefault\" style=\"margin-right: 0.10903em;\">M<\/span><span class=\"msupsub\"><span class=\"vlist-t vlist-t2\"><span class=\"vlist-r\"><span class=\"vlist\" style=\"height: 0.151392em;\"><span class=\"\" style=\"top: -2.55em; margin-left: -0.10903em; margin-right: 0.05em;\"><span class=\"pstrut\" style=\"height: 2.7em;\"><\/span><span class=\"sizing reset-size6 size3 mtight\"><span class=\"mord mathdefault mtight\">n<\/span><\/span><\/span><\/span><span class=\"vlist-s\">\u200b<\/span><\/span><span class=\"vlist-r\"><span class=\"vlist\" style=\"height: 0.15em;\"><span class=\"\"><\/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<span class=\"katex--inline\"><span class=\"katex\"><span class=\"katex-mathml\"> e v e n t &nbsp;&nbsp; e ( t 1 , . . . , t n ) . event \\ \\ e(t_1,...,t_n). <\/span><span class=\"katex-html\"><span class=\"base\"><span class=\"strut\" style=\"height: 1em; vertical-align: -0.25em;\"><\/span><span class=\"mord mathdefault\">e<\/span><span class=\"mord mathdefault\" style=\"margin-right: 0.03588em;\">v<\/span><span class=\"mord mathdefault\">e<\/span><span class=\"mord mathdefault\">n<\/span><span class=\"mord mathdefault\">t<\/span><span class=\"mspace\">&nbsp;<\/span><span class=\"mspace\">&nbsp;<\/span><span class=\"mord mathdefault\">e<\/span><span class=\"mopen\">(<\/span><span class=\"mord\"><span class=\"mord mathdefault\">t<\/span><span class=\"msupsub\"><span class=\"vlist-t vlist-t2\"><span class=\"vlist-r\"><span class=\"vlist\" style=\"height: 0.301108em;\"><span class=\"\" style=\"top: -2.55em; margin-left: 0em; margin-right: 0.05em;\"><span class=\"pstrut\" style=\"height: 2.7em;\"><\/span><span class=\"sizing reset-size6 size3 mtight\"><span class=\"mord mtight\">1<\/span><\/span><\/span><\/span><span class=\"vlist-s\">\u200b<\/span><\/span><span class=\"vlist-r\"><span class=\"vlist\" style=\"height: 0.15em;\"><span class=\"\"><\/span><\/span><\/span><\/span><\/span><\/span><span class=\"mpunct\">,<\/span><span class=\"mspace\" style=\"margin-right: 0.166667em;\"><\/span><span class=\"mord\">.<\/span><span class=\"mord\">.<\/span><span class=\"mord\">.<\/span><span class=\"mpunct\">,<\/span><span class=\"mspace\" style=\"margin-right: 0.166667em;\"><\/span><span class=\"mord\"><span class=\"mord mathdefault\">t<\/span><span class=\"msupsub\"><span class=\"vlist-t vlist-t2\"><span class=\"vlist-r\"><span class=\"vlist\" style=\"height: 0.151392em;\"><span class=\"\" style=\"top: -2.55em; margin-left: 0em; margin-right: 0.05em;\"><span class=\"pstrut\" style=\"height: 2.7em;\"><\/span><span class=\"sizing reset-size6 size3 mtight\"><span class=\"mord mathdefault mtight\">n<\/span><\/span><\/span><\/span><span class=\"vlist-s\">\u200b<\/span><\/span><span class=\"vlist-r\"><span class=\"vlist\" style=\"height: 0.15em;\"><span class=\"\"><\/span><\/span><\/span><\/span><\/span><\/span><span class=\"mclose\">)<\/span><span class=\"mord\">.<\/span><\/span><\/span><\/span><\/span>\u7684\u5f62\u5f0f\u58f0\u660e\uff0c\u5176\u4e2d\u7684<span class=\"katex--inline\"><span class=\"katex\"><span class=\"katex-mathml\"> t 1 , . . . , t n t_1,...,t_n <\/span><span class=\"katex-html\"><span class=\"base\"><span class=\"strut\" style=\"height: 0.80952em; vertical-align: -0.19444em;\"><\/span><span class=\"mord\"><span class=\"mord mathdefault\">t<\/span><span class=\"msupsub\"><span class=\"vlist-t vlist-t2\"><span class=\"vlist-r\"><span class=\"vlist\" style=\"height: 0.301108em;\"><span class=\"\" style=\"top: -2.55em; margin-left: 0em; margin-right: 0.05em;\"><span class=\"pstrut\" style=\"height: 2.7em;\"><\/span><span class=\"sizing reset-size6 size3 mtight\"><span class=\"mord mtight\">1<\/span><\/span><\/span><\/span><span class=\"vlist-s\">\u200b<\/span><\/span><span class=\"vlist-r\"><span class=\"vlist\" style=\"height: 0.15em;\"><span class=\"\"><\/span><\/span><\/span><\/span><\/span><\/span><span class=\"mpunct\">,<\/span><span class=\"mspace\" style=\"margin-right: 0.166667em;\"><\/span><span class=\"mord\">.<\/span><span class=\"mord\">.<\/span><span class=\"mord\">.<\/span><span class=\"mpunct\">,<\/span><span class=\"mspace\" style=\"margin-right: 0.166667em;\"><\/span><span class=\"mord\"><span class=\"mord mathdefault\">t<\/span><span class=\"msupsub\"><span class=\"vlist-t vlist-t2\"><span class=\"vlist-r\"><span class=\"vlist\" style=\"height: 0.151392em;\"><span class=\"\" style=\"top: -2.55em; margin-left: 0em; margin-right: 0.05em;\"><span class=\"pstrut\" style=\"height: 2.7em;\"><\/span><span class=\"sizing reset-size6 size3 mtight\"><span class=\"mord mathdefault mtight\">n<\/span><\/span><\/span><\/span><span class=\"vlist-s\">\u200b<\/span><\/span><span class=\"vlist-r\"><span class=\"vlist\" style=\"height: 0.15em;\"><span class=\"\"><\/span><\/span><\/span><\/span><\/span><\/span><\/span><\/span><\/span><\/span>\u662f\u53c2\u6570\u7c7b\u578b\u3002<\/p>\n<h5>2.1 Correspondence\u65ad\u8a00<\/h5>\n<p>\u67e5\u8be2Correspondence\u7684\u8bed\u6cd5\u5982\u4e0b\uff1a<br \/> <span class=\"katex--display\"><span class=\"katex-display\"><span class=\"katex\"><span class=\"katex-mathml\"> q u e r y &nbsp;&nbsp; x 1 : t 1 , . . . , x n : t n ; &nbsp; e v e n t ( e ( M 1 , . . . , M j ) ) = = &gt; 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)) ==&gt; \\bold{event}(e'(N_1,...,N_k)). <\/span><span class=\"katex-html\"><span class=\"base\"><span class=\"strut\" style=\"height: 0.63888em; vertical-align: -0.19444em;\"><\/span><span class=\"mord\"><span class=\"mord mathbf\">q<\/span><span class=\"mord mathbf\">u<\/span><span class=\"mord mathbf\">e<\/span><span class=\"mord mathbf\">r<\/span><span class=\"mord mathbf\" style=\"margin-right: 0.01597em;\">y<\/span><\/span><span class=\"mspace\">&nbsp;<\/span><span class=\"mspace\">&nbsp;<\/span><span class=\"mord\"><span class=\"mord mathdefault\">x<\/span><span class=\"msupsub\"><span class=\"vlist-t vlist-t2\"><span class=\"vlist-r\"><span class=\"vlist\" style=\"height: 0.301108em;\"><span class=\"\" style=\"top: -2.55em; margin-left: 0em; margin-right: 0.05em;\"><span class=\"pstrut\" style=\"height: 2.7em;\"><\/span><span class=\"sizing reset-size6 size3 mtight\"><span class=\"mord mtight\">1<\/span><\/span><\/span><\/span><span class=\"vlist-s\">\u200b<\/span><\/span><span class=\"vlist-r\"><span class=\"vlist\" style=\"height: 0.15em;\"><span class=\"\"><\/span><\/span><\/span><\/span><\/span><\/span><span class=\"mspace\" style=\"margin-right: 0.277778em;\"><\/span><span class=\"mrel\">:<\/span><span class=\"mspace\" style=\"margin-right: 0.277778em;\"><\/span><\/span><span class=\"base\"><span class=\"strut\" style=\"height: 0.80952em; vertical-align: -0.19444em;\"><\/span><span class=\"mord\"><span class=\"mord mathdefault\">t<\/span><span class=\"msupsub\"><span class=\"vlist-t vlist-t2\"><span class=\"vlist-r\"><span class=\"vlist\" style=\"height: 0.301108em;\"><span class=\"\" style=\"top: -2.55em; margin-left: 0em; margin-right: 0.05em;\"><span class=\"pstrut\" style=\"height: 2.7em;\"><\/span><span class=\"sizing reset-size6 size3 mtight\"><span class=\"mord mtight\">1<\/span><\/span><\/span><\/span><span class=\"vlist-s\">\u200b<\/span><\/span><span class=\"vlist-r\"><span class=\"vlist\" style=\"height: 0.15em;\"><span class=\"\"><\/span><\/span><\/span><\/span><\/span><\/span><span class=\"mpunct\">,<\/span><span class=\"mspace\" style=\"margin-right: 0.166667em;\"><\/span><span class=\"mord\">.<\/span><span class=\"mord\">.<\/span><span class=\"mord\">.<\/span><span class=\"mpunct\">,<\/span><span class=\"mspace\" style=\"margin-right: 0.166667em;\"><\/span><span class=\"mord\"><span class=\"mord mathdefault\">x<\/span><span class=\"msupsub\"><span class=\"vlist-t vlist-t2\"><span class=\"vlist-r\"><span class=\"vlist\" style=\"height: 0.151392em;\"><span class=\"\" style=\"top: -2.55em; margin-left: 0em; margin-right: 0.05em;\"><span class=\"pstrut\" style=\"height: 2.7em;\"><\/span><span class=\"sizing reset-size6 size3 mtight\"><span class=\"mord mathdefault mtight\">n<\/span><\/span><\/span><\/span><span class=\"vlist-s\">\u200b<\/span><\/span><span class=\"vlist-r\"><span class=\"vlist\" style=\"height: 0.15em;\"><span class=\"\"><\/span><\/span><\/span><\/span><\/span><\/span><span class=\"mspace\" style=\"margin-right: 0.277778em;\"><\/span><span class=\"mrel\">:<\/span><span class=\"mspace\" style=\"margin-right: 0.277778em;\"><\/span><\/span><span class=\"base\"><span class=\"strut\" style=\"height: 1.03611em; vertical-align: -0.286108em;\"><\/span><span class=\"mord\"><span class=\"mord mathdefault\">t<\/span><span class=\"msupsub\"><span class=\"vlist-t vlist-t2\"><span class=\"vlist-r\"><span class=\"vlist\" style=\"height: 0.151392em;\"><span class=\"\" style=\"top: -2.55em; margin-left: 0em; margin-right: 0.05em;\"><span class=\"pstrut\" style=\"height: 2.7em;\"><\/span><span class=\"sizing reset-size6 size3 mtight\"><span class=\"mord mathdefault mtight\">n<\/span><\/span><\/span><\/span><span class=\"vlist-s\">\u200b<\/span><\/span><span class=\"vlist-r\"><span class=\"vlist\" style=\"height: 0.15em;\"><span class=\"\"><\/span><\/span><\/span><\/span><\/span><\/span><span class=\"mpunct\">;<\/span><span class=\"mspace\" style=\"margin-right: 0.166667em;\"><\/span><span class=\"mspace\">&nbsp;<\/span><span class=\"mord\"><span class=\"mord mathbf\">e<\/span><span class=\"mord mathbf\" style=\"margin-right: 0.01597em;\">v<\/span><span class=\"mord mathbf\">e<\/span><span class=\"mord mathbf\">n<\/span><span class=\"mord mathbf\">t<\/span><\/span><span class=\"mopen\">(<\/span><span class=\"mord mathdefault\">e<\/span><span class=\"mopen\">(<\/span><span class=\"mord\"><span class=\"mord mathdefault\" style=\"margin-right: 0.10903em;\">M<\/span><span class=\"msupsub\"><span class=\"vlist-t vlist-t2\"><span class=\"vlist-r\"><span class=\"vlist\" style=\"height: 0.301108em;\"><span class=\"\" style=\"top: -2.55em; margin-left: -0.10903em; margin-right: 0.05em;\"><span class=\"pstrut\" style=\"height: 2.7em;\"><\/span><span class=\"sizing reset-size6 size3 mtight\"><span class=\"mord mtight\">1<\/span><\/span><\/span><\/span><span class=\"vlist-s\">\u200b<\/span><\/span><span class=\"vlist-r\"><span class=\"vlist\" style=\"height: 0.15em;\"><span class=\"\"><\/span><\/span><\/span><\/span><\/span><\/span><span class=\"mpunct\">,<\/span><span class=\"mspace\" style=\"margin-right: 0.166667em;\"><\/span><span class=\"mord\">.<\/span><span class=\"mord\">.<\/span><span class=\"mord\">.<\/span><span class=\"mpunct\">,<\/span><span class=\"mspace\" style=\"margin-right: 0.166667em;\"><\/span><span class=\"mord\"><span class=\"mord mathdefault\" style=\"margin-right: 0.10903em;\">M<\/span><span class=\"msupsub\"><span class=\"vlist-t vlist-t2\"><span class=\"vlist-r\"><span class=\"vlist\" style=\"height: 0.311664em;\"><span class=\"\" style=\"top: -2.55em; margin-left: -0.10903em; margin-right: 0.05em;\"><span class=\"pstrut\" style=\"height: 2.7em;\"><\/span><span class=\"sizing reset-size6 size3 mtight\"><span class=\"mord mathdefault mtight\" style=\"margin-right: 0.05724em;\">j<\/span><\/span><\/span><\/span><span class=\"vlist-s\">\u200b<\/span><\/span><span class=\"vlist-r\"><span class=\"vlist\" style=\"height: 0.286108em;\"><span class=\"\"><\/span><\/span><\/span><\/span><\/span><\/span><span class=\"mclose\">)<\/span><span class=\"mclose\">)<\/span><span class=\"mspace\" style=\"margin-right: 0.277778em;\"><\/span><span class=\"mrel\">=<\/span><\/span><span class=\"base\"><span class=\"strut\" style=\"height: 0.36687em; vertical-align: 0em;\"><\/span><span class=\"mrel\">=<\/span><\/span><span class=\"base\"><span class=\"strut\" style=\"height: 0.5782em; vertical-align: -0.0391em;\"><\/span><span class=\"mrel\">&gt;<\/span><span class=\"mspace\" style=\"margin-right: 0.277778em;\"><\/span><\/span><span class=\"base\"><span class=\"strut\" style=\"height: 1.05189em; vertical-align: -0.25em;\"><\/span><span class=\"mord\"><span class=\"mord mathbf\">e<\/span><span class=\"mord mathbf\" style=\"margin-right: 0.01597em;\">v<\/span><span class=\"mord mathbf\">e<\/span><span class=\"mord mathbf\">n<\/span><span class=\"mord mathbf\">t<\/span><\/span><span class=\"mopen\">(<\/span><span class=\"mord\"><span class=\"mord mathdefault\">e<\/span><span class=\"msupsub\"><span class=\"vlist-t\"><span class=\"vlist-r\"><span class=\"vlist\" style=\"height: 0.801892em;\"><span class=\"\" style=\"top: -3.113em; margin-right: 0.05em;\"><span class=\"pstrut\" style=\"height: 2.7em;\"><\/span><span class=\"sizing reset-size6 size3 mtight\"><span class=\"mord mtight\"><span class=\"mord mtight\">\u2032<\/span><\/span><\/span><\/span><\/span><\/span><\/span><\/span><\/span><span class=\"mopen\">(<\/span><span class=\"mord\"><span class=\"mord mathdefault\" style=\"margin-right: 0.10903em;\">N<\/span><span class=\"msupsub\"><span class=\"vlist-t vlist-t2\"><span class=\"vlist-r\"><span class=\"vlist\" style=\"height: 0.301108em;\"><span class=\"\" style=\"top: -2.55em; margin-left: -0.10903em; margin-right: 0.05em;\"><span class=\"pstrut\" style=\"height: 2.7em;\"><\/span><span class=\"sizing reset-size6 size3 mtight\"><span class=\"mord mtight\">1<\/span><\/span><\/span><\/span><span class=\"vlist-s\">\u200b<\/span><\/span><span class=\"vlist-r\"><span class=\"vlist\" style=\"height: 0.15em;\"><span class=\"\"><\/span><\/span><\/span><\/span><\/span><\/span><span class=\"mpunct\">,<\/span><span class=\"mspace\" style=\"margin-right: 0.166667em;\"><\/span><span class=\"mord\">.<\/span><span class=\"mord\">.<\/span><span class=\"mord\">.<\/span><span class=\"mpunct\">,<\/span><span class=\"mspace\" style=\"margin-right: 0.166667em;\"><\/span><span class=\"mord\"><span class=\"mord mathdefault\" style=\"margin-right: 0.10903em;\">N<\/span><span class=\"msupsub\"><span class=\"vlist-t vlist-t2\"><span class=\"vlist-r\"><span class=\"vlist\" style=\"height: 0.336108em;\"><span class=\"\" style=\"top: -2.55em; margin-left: -0.10903em; margin-right: 0.05em;\"><span class=\"pstrut\" style=\"height: 2.7em;\"><\/span><span class=\"sizing reset-size6 size3 mtight\"><span class=\"mord mathdefault mtight\" style=\"margin-right: 0.03148em;\">k<\/span><\/span><\/span><\/span><span class=\"vlist-s\">\u200b<\/span><\/span><span class=\"vlist-r\"><span class=\"vlist\" style=\"height: 0.15em;\"><span class=\"\"><\/span><\/span><\/span><\/span><\/span><\/span><span class=\"mclose\">)<\/span><span class=\"mclose\">)<\/span><span class=\"mord\">.<\/span><\/span><\/span><\/span><\/span><\/span><\/p>\n<p>\u8fd9\u4e2a\u67e5\u8be2\u6210\u7acb\u7684\u6761\u4ef6\u662f\uff0c\u5bf9\u4e8e\u6bcf\u6b21\u4e8b\u4ef6<span class=\"katex--inline\"><span class=\"katex\"><span class=\"katex-mathml\"> e ( M 1 , . . . , M j ) e(M_1,...,M_j) <\/span><span class=\"katex-html\"><span class=\"base\"><span class=\"strut\" style=\"height: 1.03611em; vertical-align: -0.286108em;\"><\/span><span class=\"mord mathdefault\">e<\/span><span class=\"mopen\">(<\/span><span class=\"mord\"><span class=\"mord mathdefault\" style=\"margin-right: 0.10903em;\">M<\/span><span class=\"msupsub\"><span class=\"vlist-t vlist-t2\"><span class=\"vlist-r\"><span class=\"vlist\" style=\"height: 0.301108em;\"><span class=\"\" style=\"top: -2.55em; margin-left: -0.10903em; margin-right: 0.05em;\"><span class=\"pstrut\" style=\"height: 2.7em;\"><\/span><span class=\"sizing reset-size6 size3 mtight\"><span class=\"mord mtight\">1<\/span><\/span><\/span><\/span><span class=\"vlist-s\">\u200b<\/span><\/span><span class=\"vlist-r\"><span class=\"vlist\" style=\"height: 0.15em;\"><span class=\"\"><\/span><\/span><\/span><\/span><\/span><\/span><span class=\"mpunct\">,<\/span><span class=\"mspace\" style=\"margin-right: 0.166667em;\"><\/span><span class=\"mord\">.<\/span><span class=\"mord\">.<\/span><span class=\"mord\">.<\/span><span class=\"mpunct\">,<\/span><span class=\"mspace\" style=\"margin-right: 0.166667em;\"><\/span><span class=\"mord\"><span class=\"mord mathdefault\" style=\"margin-right: 0.10903em;\">M<\/span><span class=\"msupsub\"><span class=\"vlist-t vlist-t2\"><span class=\"vlist-r\"><span class=\"vlist\" style=\"height: 0.311664em;\"><span class=\"\" style=\"top: -2.55em; margin-left: -0.10903em; margin-right: 0.05em;\"><span class=\"pstrut\" style=\"height: 2.7em;\"><\/span><span class=\"sizing reset-size6 size3 mtight\"><span class=\"mord mathdefault mtight\" style=\"margin-right: 0.05724em;\">j<\/span><\/span><\/span><\/span><span class=\"vlist-s\">\u200b<\/span><\/span><span class=\"vlist-r\"><span class=\"vlist\" style=\"height: 0.286108em;\"><span class=\"\"><\/span><\/span><\/span><\/span><\/span><\/span><span class=\"mclose\">)<\/span><\/span><\/span><\/span><\/span>\u53d1\u751f\uff0c\u90fd\u80fd\u5728\u6b64\u524d\u627e\u5230\u4e00\u4e2a\u4f4d\u7f6e\u6709\u4e8b\u4ef6<span class=\"katex--inline\"><span class=\"katex\"><span class=\"katex-mathml\"> e \u2032 ( N 1 , . . . , N k ) e'(N_1,...,N_k) <\/span><span class=\"katex-html\"><span class=\"base\"><span class=\"strut\" style=\"height: 1.00189em; vertical-align: -0.25em;\"><\/span><span class=\"mord\"><span class=\"mord mathdefault\">e<\/span><span class=\"msupsub\"><span class=\"vlist-t\"><span class=\"vlist-r\"><span class=\"vlist\" style=\"height: 0.751892em;\"><span class=\"\" style=\"top: -3.063em; margin-right: 0.05em;\"><span class=\"pstrut\" style=\"height: 2.7em;\"><\/span><span class=\"sizing reset-size6 size3 mtight\"><span class=\"mord mtight\"><span class=\"mord mtight\">\u2032<\/span><\/span><\/span><\/span><\/span><\/span><\/span><\/span><\/span><span class=\"mopen\">(<\/span><span class=\"mord\"><span class=\"mord mathdefault\" style=\"margin-right: 0.10903em;\">N<\/span><span class=\"msupsub\"><span class=\"vlist-t vlist-t2\"><span class=\"vlist-r\"><span class=\"vlist\" style=\"height: 0.301108em;\"><span class=\"\" style=\"top: -2.55em; margin-left: -0.10903em; margin-right: 0.05em;\"><span class=\"pstrut\" style=\"height: 2.7em;\"><\/span><span class=\"sizing reset-size6 size3 mtight\"><span class=\"mord mtight\">1<\/span><\/span><\/span><\/span><span class=\"vlist-s\">\u200b<\/span><\/span><span class=\"vlist-r\"><span class=\"vlist\" style=\"height: 0.15em;\"><span class=\"\"><\/span><\/span><\/span><\/span><\/span><\/span><span class=\"mpunct\">,<\/span><span class=\"mspace\" style=\"margin-right: 0.166667em;\"><\/span><span class=\"mord\">.<\/span><span class=\"mord\">.<\/span><span class=\"mord\">.<\/span><span class=\"mpunct\">,<\/span><span class=\"mspace\" style=\"margin-right: 0.166667em;\"><\/span><span class=\"mord\"><span class=\"mord mathdefault\" style=\"margin-right: 0.10903em;\">N<\/span><span class=\"msupsub\"><span class=\"vlist-t vlist-t2\"><span class=\"vlist-r\"><span class=\"vlist\" style=\"height: 0.336108em;\"><span class=\"\" style=\"top: -2.55em; margin-left: -0.10903em; margin-right: 0.05em;\"><span class=\"pstrut\" style=\"height: 2.7em;\"><\/span><span class=\"sizing reset-size6 size3 mtight\"><span class=\"mord mathdefault mtight\" style=\"margin-right: 0.03148em;\">k<\/span><\/span><\/span><\/span><span class=\"vlist-s\">\u200b<\/span><\/span><span class=\"vlist-r\"><span class=\"vlist\" style=\"height: 0.15em;\"><span class=\"\"><\/span><\/span><\/span><\/span><\/span><\/span><span class=\"mclose\">)<\/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<span class=\"katex--inline\"><span class=\"katex\"><span class=\"katex-mathml\"> x 1 , . . . , x n x_1,...,x_n <\/span><span class=\"katex-html\"><span class=\"base\"><span class=\"strut\" style=\"height: 0.625em; vertical-align: -0.19444em;\"><\/span><span class=\"mord\"><span class=\"mord mathdefault\">x<\/span><span class=\"msupsub\"><span class=\"vlist-t vlist-t2\"><span class=\"vlist-r\"><span class=\"vlist\" style=\"height: 0.301108em;\"><span class=\"\" style=\"top: -2.55em; margin-left: 0em; margin-right: 0.05em;\"><span class=\"pstrut\" style=\"height: 2.7em;\"><\/span><span class=\"sizing reset-size6 size3 mtight\"><span class=\"mord mtight\">1<\/span><\/span><\/span><\/span><span class=\"vlist-s\">\u200b<\/span><\/span><span class=\"vlist-r\"><span class=\"vlist\" style=\"height: 0.15em;\"><span class=\"\"><\/span><\/span><\/span><\/span><\/span><\/span><span class=\"mpunct\">,<\/span><span class=\"mspace\" style=\"margin-right: 0.166667em;\"><\/span><span class=\"mord\">.<\/span><span class=\"mord\">.<\/span><span class=\"mord\">.<\/span><span class=\"mpunct\">,<\/span><span class=\"mspace\" style=\"margin-right: 0.166667em;\"><\/span><span class=\"mord\"><span class=\"mord mathdefault\">x<\/span><span class=\"msupsub\"><span class=\"vlist-t vlist-t2\"><span class=\"vlist-r\"><span class=\"vlist\" style=\"height: 0.151392em;\"><span class=\"\" style=\"top: -2.55em; margin-left: 0em; margin-right: 0.05em;\"><span class=\"pstrut\" style=\"height: 2.7em;\"><\/span><span class=\"sizing reset-size6 size3 mtight\"><span class=\"mord mathdefault mtight\">n<\/span><\/span><\/span><\/span><span class=\"vlist-s\">\u200b<\/span><\/span><span class=\"vlist-r\"><span class=\"vlist\" style=\"height: 0.15em;\"><span class=\"\"><\/span><\/span><\/span><\/span><\/span><\/span><\/span><\/span><\/span><\/span>\u5728<span class=\"katex--inline\"><span class=\"katex\"><span class=\"katex-mathml\"> M 1 , . . . , M j M_1,...,M_j <\/span><span class=\"katex-html\"><span class=\"base\"><span class=\"strut\" style=\"height: 0.969438em; vertical-align: -0.286108em;\"><\/span><span class=\"mord\"><span class=\"mord mathdefault\" style=\"margin-right: 0.10903em;\">M<\/span><span class=\"msupsub\"><span class=\"vlist-t vlist-t2\"><span class=\"vlist-r\"><span class=\"vlist\" style=\"height: 0.301108em;\"><span class=\"\" style=\"top: -2.55em; margin-left: -0.10903em; margin-right: 0.05em;\"><span class=\"pstrut\" style=\"height: 2.7em;\"><\/span><span class=\"sizing reset-size6 size3 mtight\"><span class=\"mord mtight\">1<\/span><\/span><\/span><\/span><span class=\"vlist-s\">\u200b<\/span><\/span><span class=\"vlist-r\"><span class=\"vlist\" style=\"height: 0.15em;\"><span class=\"\"><\/span><\/span><\/span><\/span><\/span><\/span><span class=\"mpunct\">,<\/span><span class=\"mspace\" style=\"margin-right: 0.166667em;\"><\/span><span class=\"mord\">.<\/span><span class=\"mord\">.<\/span><span class=\"mord\">.<\/span><span class=\"mpunct\">,<\/span><span class=\"mspace\" style=\"margin-right: 0.166667em;\"><\/span><span class=\"mord\"><span class=\"mord mathdefault\" style=\"margin-right: 0.10903em;\">M<\/span><span class=\"msupsub\"><span class=\"vlist-t vlist-t2\"><span class=\"vlist-r\"><span class=\"vlist\" style=\"height: 0.311664em;\"><span class=\"\" style=\"top: -2.55em; margin-left: -0.10903em; margin-right: 0.05em;\"><span class=\"pstrut\" style=\"height: 2.7em;\"><\/span><span class=\"sizing reset-size6 size3 mtight\"><span class=\"mord mathdefault mtight\" style=\"margin-right: 0.05724em;\">j<\/span><\/span><\/span><\/span><span class=\"vlist-s\">\u200b<\/span><\/span><span class=\"vlist-r\"><span class=\"vlist\" style=\"height: 0.286108em;\"><span class=\"\"><\/span><\/span><\/span><\/span><\/span><\/span><\/span><\/span><\/span><\/span>\u548c<span class=\"katex--inline\"><span class=\"katex\"><span class=\"katex-mathml\"> N 1 , . . . , N k N_1,...,N_k <\/span><span class=\"katex-html\"><span class=\"base\"><span class=\"strut\" style=\"height: 0.87777em; vertical-align: -0.19444em;\"><\/span><span class=\"mord\"><span class=\"mord mathdefault\" style=\"margin-right: 0.10903em;\">N<\/span><span class=\"msupsub\"><span class=\"vlist-t vlist-t2\"><span class=\"vlist-r\"><span class=\"vlist\" style=\"height: 0.301108em;\"><span class=\"\" style=\"top: -2.55em; margin-left: -0.10903em; margin-right: 0.05em;\"><span class=\"pstrut\" style=\"height: 2.7em;\"><\/span><span class=\"sizing reset-size6 size3 mtight\"><span class=\"mord mtight\">1<\/span><\/span><\/span><\/span><span class=\"vlist-s\">\u200b<\/span><\/span><span class=\"vlist-r\"><span class=\"vlist\" style=\"height: 0.15em;\"><span class=\"\"><\/span><\/span><\/span><\/span><\/span><\/span><span class=\"mpunct\">,<\/span><span class=\"mspace\" style=\"margin-right: 0.166667em;\"><\/span><span class=\"mord\">.<\/span><span class=\"mord\">.<\/span><span class=\"mord\">.<\/span><span class=\"mpunct\">,<\/span><span class=\"mspace\" style=\"margin-right: 0.166667em;\"><\/span><span class=\"mord\"><span class=\"mord mathdefault\" style=\"margin-right: 0.10903em;\">N<\/span><span class=\"msupsub\"><span class=\"vlist-t vlist-t2\"><span class=\"vlist-r\"><span class=\"vlist\" style=\"height: 0.336108em;\"><span class=\"\" style=\"top: -2.55em; margin-left: -0.10903em; margin-right: 0.05em;\"><span class=\"pstrut\" style=\"height: 2.7em;\"><\/span><span class=\"sizing reset-size6 size3 mtight\"><span class=\"mord mathdefault mtight\" style=\"margin-right: 0.03148em;\">k<\/span><\/span><\/span><\/span><span class=\"vlist-s\">\u200b<\/span><\/span><span class=\"vlist-r\"><span class=\"vlist\" style=\"height: 0.15em;\"><span class=\"\"><\/span><\/span><\/span><\/span><\/span><\/span><\/span><\/span><\/span><\/span>\u4e2d\u662f\u6709\u76f8\u540c\u7684\u503c\u7684\u3002<\/p>\n<p>\u6ce8\u610f\uff0c\u5728<span class=\"katex--inline\"><span class=\"katex\"><span class=\"katex-mathml\"> = = &gt; ==&gt; <\/span><span class=\"katex-html\"><span class=\"base\"><span class=\"strut\" style=\"height: 0.36687em; vertical-align: 0em;\"><\/span><span class=\"mrel\">=<\/span><\/span><span class=\"base\"><span class=\"strut\" style=\"height: 0.36687em; vertical-align: 0em;\"><\/span><span class=\"mrel\">=<\/span><\/span><span class=\"base\"><span class=\"strut\" style=\"height: 0.5782em; vertical-align: -0.0391em;\"><\/span><span class=\"mrel\">&gt;<\/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 class=\"katex--inline\"><span class=\"katex\"><span class=\"katex-mathml\"> = = &gt; ==&gt; <\/span><span class=\"katex-html\"><span class=\"base\"><span class=\"strut\" style=\"height: 0.36687em; vertical-align: 0em;\"><\/span><span class=\"mrel\">=<\/span><\/span><span class=\"base\"><span class=\"strut\" style=\"height: 0.36687em; vertical-align: 0em;\"><\/span><span class=\"mrel\">=<\/span><\/span><span class=\"base\"><span class=\"strut\" style=\"height: 0.5782em; vertical-align: -0.0391em;\"><\/span><span class=\"mrel\">&gt;<\/span><\/span><\/span><\/span><\/span>\u4e4b\u540e\u7684\u4e8b\u4ef6\u4e2d\u51fa\u73b0\uff0c<strong>\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<br \/> <span class=\"katex--display\"><span class=\"katex-display\"><span class=\"katex\"><span class=\"katex-mathml\"> q u e r y &nbsp;&nbsp; x : t 1 , y : t 2 , z : t 3 ; e v e n t ( e ( x , y ) ) = = &gt; 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)) ==&gt; \\bold{event}(e'(y,z)). <\/span><span class=\"katex-html\"><span class=\"base\"><span class=\"strut\" style=\"height: 0.63888em; vertical-align: -0.19444em;\"><\/span><span class=\"mord\"><span class=\"mord mathbf\">q<\/span><span class=\"mord mathbf\">u<\/span><span class=\"mord mathbf\">e<\/span><span class=\"mord mathbf\">r<\/span><span class=\"mord mathbf\" style=\"margin-right: 0.01597em;\">y<\/span><\/span><span class=\"mspace\">&nbsp;<\/span><span class=\"mspace\">&nbsp;<\/span><span class=\"mord mathdefault\">x<\/span><span class=\"mspace\" style=\"margin-right: 0.277778em;\"><\/span><span class=\"mrel\">:<\/span><span class=\"mspace\" style=\"margin-right: 0.277778em;\"><\/span><\/span><span class=\"base\"><span class=\"strut\" style=\"height: 0.80952em; vertical-align: -0.19444em;\"><\/span><span class=\"mord\"><span class=\"mord mathdefault\">t<\/span><span class=\"msupsub\"><span class=\"vlist-t vlist-t2\"><span class=\"vlist-r\"><span class=\"vlist\" style=\"height: 0.301108em;\"><span class=\"\" style=\"top: -2.55em; margin-left: 0em; margin-right: 0.05em;\"><span class=\"pstrut\" style=\"height: 2.7em;\"><\/span><span class=\"sizing reset-size6 size3 mtight\"><span class=\"mord mtight\">1<\/span><\/span><\/span><\/span><span class=\"vlist-s\">\u200b<\/span><\/span><span class=\"vlist-r\"><span class=\"vlist\" style=\"height: 0.15em;\"><span class=\"\"><\/span><\/span><\/span><\/span><\/span><\/span><span class=\"mpunct\">,<\/span><span class=\"mspace\" style=\"margin-right: 0.166667em;\"><\/span><span class=\"mord mathdefault\" style=\"margin-right: 0.03588em;\">y<\/span><span class=\"mspace\" style=\"margin-right: 0.277778em;\"><\/span><span class=\"mrel\">:<\/span><span class=\"mspace\" style=\"margin-right: 0.277778em;\"><\/span><\/span><span class=\"base\"><span class=\"strut\" style=\"height: 0.80952em; vertical-align: -0.19444em;\"><\/span><span class=\"mord\"><span class=\"mord mathdefault\">t<\/span><span class=\"msupsub\"><span class=\"vlist-t vlist-t2\"><span class=\"vlist-r\"><span class=\"vlist\" style=\"height: 0.301108em;\"><span class=\"\" style=\"top: -2.55em; margin-left: 0em; margin-right: 0.05em;\"><span class=\"pstrut\" style=\"height: 2.7em;\"><\/span><span class=\"sizing reset-size6 size3 mtight\"><span class=\"mord mtight\">2<\/span><\/span><\/span><\/span><span class=\"vlist-s\">\u200b<\/span><\/span><span class=\"vlist-r\"><span class=\"vlist\" style=\"height: 0.15em;\"><span class=\"\"><\/span><\/span><\/span><\/span><\/span><\/span><span class=\"mpunct\">,<\/span><span class=\"mspace\" style=\"margin-right: 0.166667em;\"><\/span><span class=\"mord mathdefault\" style=\"margin-right: 0.04398em;\">z<\/span><span class=\"mspace\" style=\"margin-right: 0.277778em;\"><\/span><span class=\"mrel\">:<\/span><span class=\"mspace\" style=\"margin-right: 0.277778em;\"><\/span><\/span><span class=\"base\"><span class=\"strut\" style=\"height: 1em; vertical-align: -0.25em;\"><\/span><span class=\"mord\"><span class=\"mord mathdefault\">t<\/span><span class=\"msupsub\"><span class=\"vlist-t vlist-t2\"><span class=\"vlist-r\"><span class=\"vlist\" style=\"height: 0.301108em;\"><span class=\"\" style=\"top: -2.55em; margin-left: 0em; margin-right: 0.05em;\"><span class=\"pstrut\" style=\"height: 2.7em;\"><\/span><span class=\"sizing reset-size6 size3 mtight\"><span class=\"mord mtight\">3<\/span><\/span><\/span><\/span><span class=\"vlist-s\">\u200b<\/span><\/span><span class=\"vlist-r\"><span class=\"vlist\" style=\"height: 0.15em;\"><span class=\"\"><\/span><\/span><\/span><\/span><\/span><\/span><span class=\"mpunct\">;<\/span><span class=\"mspace\" style=\"margin-right: 0.166667em;\"><\/span><span class=\"mord\"><span class=\"mord mathbf\">e<\/span><span class=\"mord mathbf\" style=\"margin-right: 0.01597em;\">v<\/span><span class=\"mord mathbf\">e<\/span><span class=\"mord mathbf\">n<\/span><span class=\"mord mathbf\">t<\/span><\/span><span class=\"mopen\">(<\/span><span class=\"mord mathdefault\">e<\/span><span class=\"mopen\">(<\/span><span class=\"mord mathdefault\">x<\/span><span class=\"mpunct\">,<\/span><span class=\"mspace\" style=\"margin-right: 0.166667em;\"><\/span><span class=\"mord mathdefault\" style=\"margin-right: 0.03588em;\">y<\/span><span class=\"mclose\">)<\/span><span class=\"mclose\">)<\/span><span class=\"mspace\" style=\"margin-right: 0.277778em;\"><\/span><span class=\"mrel\">=<\/span><\/span><span class=\"base\"><span class=\"strut\" style=\"height: 0.36687em; vertical-align: 0em;\"><\/span><span class=\"mrel\">=<\/span><\/span><span class=\"base\"><span class=\"strut\" style=\"height: 0.5782em; vertical-align: -0.0391em;\"><\/span><span class=\"mrel\">&gt;<\/span><span class=\"mspace\" style=\"margin-right: 0.277778em;\"><\/span><\/span><span class=\"base\"><span class=\"strut\" style=\"height: 1.05189em; vertical-align: -0.25em;\"><\/span><span class=\"mord\"><span class=\"mord mathbf\">e<\/span><span class=\"mord mathbf\" style=\"margin-right: 0.01597em;\">v<\/span><span class=\"mord mathbf\">e<\/span><span class=\"mord mathbf\">n<\/span><span class=\"mord mathbf\">t<\/span><\/span><span class=\"mopen\">(<\/span><span class=\"mord\"><span class=\"mord mathdefault\">e<\/span><span class=\"msupsub\"><span class=\"vlist-t\"><span class=\"vlist-r\"><span class=\"vlist\" style=\"height: 0.801892em;\"><span class=\"\" style=\"top: -3.113em; margin-right: 0.05em;\"><span class=\"pstrut\" style=\"height: 2.7em;\"><\/span><span class=\"sizing reset-size6 size3 mtight\"><span class=\"mord mtight\"><span class=\"mord mtight\">\u2032<\/span><\/span><\/span><\/span><\/span><\/span><\/span><\/span><\/span><span class=\"mopen\">(<\/span><span class=\"mord mathdefault\" style=\"margin-right: 0.03588em;\">y<\/span><span class=\"mpunct\">,<\/span><span class=\"mspace\" style=\"margin-right: 0.166667em;\"><\/span><span class=\"mord mathdefault\" style=\"margin-right: 0.04398em;\">z<\/span><span class=\"mclose\">)<\/span><span class=\"mclose\">)<\/span><span class=\"mord\">.<\/span><\/span><\/span><\/span><\/span><\/span><\/p>\n<p>\u8fd9\u8868\u793a\u5bf9\u4e8e<span class=\"katex--inline\"><span class=\"katex\"><span class=\"katex-mathml\"> x , y x,y <\/span><span class=\"katex-html\"><span class=\"base\"><span class=\"strut\" style=\"height: 0.625em; vertical-align: -0.19444em;\"><\/span><span class=\"mord mathdefault\">x<\/span><span class=\"mpunct\">,<\/span><span class=\"mspace\" style=\"margin-right: 0.166667em;\"><\/span><span class=\"mord mathdefault\" style=\"margin-right: 0.03588em;\">y<\/span><\/span><\/span><\/span><\/span>\u7684\u6bcf\u6b21\u51fa\u73b0<span class=\"katex--inline\"><span class=\"katex\"><span class=\"katex-mathml\"> e ( x , y ) e(x,y) <\/span><span class=\"katex-html\"><span class=\"base\"><span class=\"strut\" style=\"height: 1em; vertical-align: -0.25em;\"><\/span><span class=\"mord mathdefault\">e<\/span><span class=\"mopen\">(<\/span><span class=\"mord mathdefault\">x<\/span><span class=\"mpunct\">,<\/span><span class=\"mspace\" style=\"margin-right: 0.166667em;\"><\/span><span class=\"mord mathdefault\" style=\"margin-right: 0.03588em;\">y<\/span><span class=\"mclose\">)<\/span><\/span><\/span><\/span><\/span>\uff0c\u603b\u662f\u5b58\u5728\u4e00\u4e2a<span class=\"katex--inline\"><span class=\"katex\"><span class=\"katex-mathml\"> z z <\/span><span class=\"katex-html\"><span class=\"base\"><span class=\"strut\" style=\"height: 0.43056em; vertical-align: 0em;\"><\/span><span class=\"mord mathdefault\" style=\"margin-right: 0.04398em;\">z<\/span><\/span><\/span><\/span><\/span>\u4f7f\u5f97<span class=\"katex--inline\"><span class=\"katex\"><span class=\"katex-mathml\"> e \u2032 ( y , z ) e'(y,z) <\/span><span class=\"katex-html\"><span class=\"base\"><span class=\"strut\" style=\"height: 1.00189em; vertical-align: -0.25em;\"><\/span><span class=\"mord\"><span class=\"mord mathdefault\">e<\/span><span class=\"msupsub\"><span class=\"vlist-t\"><span class=\"vlist-r\"><span class=\"vlist\" style=\"height: 0.751892em;\"><span class=\"\" style=\"top: -3.063em; margin-right: 0.05em;\"><span class=\"pstrut\" style=\"height: 2.7em;\"><\/span><span class=\"sizing reset-size6 size3 mtight\"><span class=\"mord mtight\"><span class=\"mord mtight\">\u2032<\/span><\/span><\/span><\/span><\/span><\/span><\/span><\/span><\/span><span class=\"mopen\">(<\/span><span class=\"mord mathdefault\" style=\"margin-right: 0.03588em;\">y<\/span><span class=\"mpunct\">,<\/span><span class=\"mspace\" style=\"margin-right: 0.166667em;\"><\/span><span class=\"mord mathdefault\" style=\"margin-right: 0.04398em;\">z<\/span><span class=\"mclose\">)<\/span><\/span><\/span><\/span><\/span>\u51fa\u73b0\u3002<\/p>\n<h5>2.2 Injective Correspondence\u65ad\u8a00<\/h5>\n<p>\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\u4e48<code>2.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<br \/> <span class=\"katex--display\"><span class=\"katex-display\"><span class=\"katex\"><span class=\"katex-mathml\"> q u e r y &nbsp;&nbsp; x 1 : t 1 , . . . , x n : t n ; &nbsp; i n j \u2212 e v e n t ( e ( M 1 , . . . , M j ) ) = = &gt; 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)) ==&gt; \\bold{inj\u2212event}(e'(N_1,...,N_k)). <\/span><span class=\"katex-html\"><span class=\"base\"><span class=\"strut\" style=\"height: 0.63888em; vertical-align: -0.19444em;\"><\/span><span class=\"mord\"><span class=\"mord mathbf\">q<\/span><span class=\"mord mathbf\">u<\/span><span class=\"mord mathbf\">e<\/span><span class=\"mord mathbf\">r<\/span><span class=\"mord mathbf\" style=\"margin-right: 0.01597em;\">y<\/span><\/span><span class=\"mspace\">&nbsp;<\/span><span class=\"mspace\">&nbsp;<\/span><span class=\"mord\"><span class=\"mord mathdefault\">x<\/span><span class=\"msupsub\"><span class=\"vlist-t vlist-t2\"><span class=\"vlist-r\"><span class=\"vlist\" style=\"height: 0.301108em;\"><span class=\"\" style=\"top: -2.55em; margin-left: 0em; margin-right: 0.05em;\"><span class=\"pstrut\" style=\"height: 2.7em;\"><\/span><span class=\"sizing reset-size6 size3 mtight\"><span class=\"mord mtight\">1<\/span><\/span><\/span><\/span><span class=\"vlist-s\">\u200b<\/span><\/span><span class=\"vlist-r\"><span class=\"vlist\" style=\"height: 0.15em;\"><span class=\"\"><\/span><\/span><\/span><\/span><\/span><\/span><span class=\"mspace\" style=\"margin-right: 0.277778em;\"><\/span><span class=\"mrel\">:<\/span><span class=\"mspace\" style=\"margin-right: 0.277778em;\"><\/span><\/span><span class=\"base\"><span class=\"strut\" style=\"height: 0.80952em; vertical-align: -0.19444em;\"><\/span><span class=\"mord\"><span class=\"mord mathdefault\">t<\/span><span class=\"msupsub\"><span class=\"vlist-t vlist-t2\"><span class=\"vlist-r\"><span class=\"vlist\" style=\"height: 0.301108em;\"><span class=\"\" style=\"top: -2.55em; margin-left: 0em; margin-right: 0.05em;\"><span class=\"pstrut\" style=\"height: 2.7em;\"><\/span><span class=\"sizing reset-size6 size3 mtight\"><span class=\"mord mtight\">1<\/span><\/span><\/span><\/span><span class=\"vlist-s\">\u200b<\/span><\/span><span class=\"vlist-r\"><span class=\"vlist\" style=\"height: 0.15em;\"><span class=\"\"><\/span><\/span><\/span><\/span><\/span><\/span><span class=\"mpunct\">,<\/span><span class=\"mspace\" style=\"margin-right: 0.166667em;\"><\/span><span class=\"mord\">.<\/span><span class=\"mord\">.<\/span><span class=\"mord\">.<\/span><span class=\"mpunct\">,<\/span><span class=\"mspace\" style=\"margin-right: 0.166667em;\"><\/span><span class=\"mord\"><span class=\"mord mathdefault\">x<\/span><span class=\"msupsub\"><span class=\"vlist-t vlist-t2\"><span class=\"vlist-r\"><span class=\"vlist\" style=\"height: 0.151392em;\"><span class=\"\" style=\"top: -2.55em; margin-left: 0em; margin-right: 0.05em;\"><span class=\"pstrut\" style=\"height: 2.7em;\"><\/span><span class=\"sizing reset-size6 size3 mtight\"><span class=\"mord mathdefault mtight\">n<\/span><\/span><\/span><\/span><span class=\"vlist-s\">\u200b<\/span><\/span><span class=\"vlist-r\"><span class=\"vlist\" style=\"height: 0.15em;\"><span class=\"\"><\/span><\/span><\/span><\/span><\/span><\/span><span class=\"mspace\" style=\"margin-right: 0.277778em;\"><\/span><span class=\"mrel\">:<\/span><span class=\"mspace\" style=\"margin-right: 0.277778em;\"><\/span><\/span><span class=\"base\"><span class=\"strut\" style=\"height: 1.03611em; vertical-align: -0.286108em;\"><\/span><span class=\"mord\"><span class=\"mord mathdefault\">t<\/span><span class=\"msupsub\"><span class=\"vlist-t vlist-t2\"><span class=\"vlist-r\"><span class=\"vlist\" style=\"height: 0.151392em;\"><span class=\"\" style=\"top: -2.55em; margin-left: 0em; margin-right: 0.05em;\"><span class=\"pstrut\" style=\"height: 2.7em;\"><\/span><span class=\"sizing reset-size6 size3 mtight\"><span class=\"mord mathdefault mtight\">n<\/span><\/span><\/span><\/span><span class=\"vlist-s\">\u200b<\/span><\/span><span class=\"vlist-r\"><span class=\"vlist\" style=\"height: 0.15em;\"><span class=\"\"><\/span><\/span><\/span><\/span><\/span><\/span><span class=\"mpunct\">;<\/span><span class=\"mspace\" style=\"margin-right: 0.166667em;\"><\/span><span class=\"mspace\">&nbsp;<\/span><span class=\"mord\"><span class=\"mord mathbf\">i<\/span><span class=\"mord mathbf\">n<\/span><span class=\"mord mathbf\">j<\/span><span class=\"mord mathbf\">\u2212<\/span><span class=\"mord mathbf\">e<\/span><span class=\"mord mathbf\" style=\"margin-right: 0.01597em;\">v<\/span><span class=\"mord mathbf\">e<\/span><span class=\"mord mathbf\">n<\/span><span class=\"mord mathbf\">t<\/span><\/span><span class=\"mopen\">(<\/span><span class=\"mord mathdefault\">e<\/span><span class=\"mopen\">(<\/span><span class=\"mord\"><span class=\"mord mathdefault\" style=\"margin-right: 0.10903em;\">M<\/span><span class=\"msupsub\"><span class=\"vlist-t vlist-t2\"><span class=\"vlist-r\"><span class=\"vlist\" style=\"height: 0.301108em;\"><span class=\"\" style=\"top: -2.55em; margin-left: -0.10903em; margin-right: 0.05em;\"><span class=\"pstrut\" style=\"height: 2.7em;\"><\/span><span class=\"sizing reset-size6 size3 mtight\"><span class=\"mord mtight\">1<\/span><\/span><\/span><\/span><span class=\"vlist-s\">\u200b<\/span><\/span><span class=\"vlist-r\"><span class=\"vlist\" style=\"height: 0.15em;\"><span class=\"\"><\/span><\/span><\/span><\/span><\/span><\/span><span class=\"mpunct\">,<\/span><span class=\"mspace\" style=\"margin-right: 0.166667em;\"><\/span><span class=\"mord\">.<\/span><span class=\"mord\">.<\/span><span class=\"mord\">.<\/span><span class=\"mpunct\">,<\/span><span class=\"mspace\" style=\"margin-right: 0.166667em;\"><\/span><span class=\"mord\"><span class=\"mord mathdefault\" style=\"margin-right: 0.10903em;\">M<\/span><span class=\"msupsub\"><span class=\"vlist-t vlist-t2\"><span class=\"vlist-r\"><span class=\"vlist\" style=\"height: 0.311664em;\"><span class=\"\" style=\"top: -2.55em; margin-left: -0.10903em; margin-right: 0.05em;\"><span class=\"pstrut\" style=\"height: 2.7em;\"><\/span><span class=\"sizing reset-size6 size3 mtight\"><span class=\"mord mathdefault mtight\" style=\"margin-right: 0.05724em;\">j<\/span><\/span><\/span><\/span><span class=\"vlist-s\">\u200b<\/span><\/span><span class=\"vlist-r\"><span class=\"vlist\" style=\"height: 0.286108em;\"><span class=\"\"><\/span><\/span><\/span><\/span><\/span><\/span><span class=\"mclose\">)<\/span><span class=\"mclose\">)<\/span><span class=\"mspace\" style=\"margin-right: 0.277778em;\"><\/span><span class=\"mrel\">=<\/span><\/span><span class=\"base\"><span class=\"strut\" style=\"height: 0.36687em; vertical-align: 0em;\"><\/span><span class=\"mrel\">=<\/span><\/span><span class=\"base\"><span class=\"strut\" style=\"height: 0.5782em; vertical-align: -0.0391em;\"><\/span><span class=\"mrel\">&gt;<\/span><span class=\"mspace\" style=\"margin-right: 0.277778em;\"><\/span><\/span><span class=\"base\"><span class=\"strut\" style=\"height: 1.05189em; vertical-align: -0.25em;\"><\/span><span class=\"mord\"><span class=\"mord mathbf\">i<\/span><span class=\"mord mathbf\">n<\/span><span class=\"mord mathbf\">j<\/span><span class=\"mord mathbf\">\u2212<\/span><span class=\"mord mathbf\">e<\/span><span class=\"mord mathbf\" style=\"margin-right: 0.01597em;\">v<\/span><span class=\"mord mathbf\">e<\/span><span class=\"mord mathbf\">n<\/span><span class=\"mord mathbf\">t<\/span><\/span><span class=\"mopen\">(<\/span><span class=\"mord\"><span class=\"mord mathdefault\">e<\/span><span class=\"msupsub\"><span class=\"vlist-t\"><span class=\"vlist-r\"><span class=\"vlist\" style=\"height: 0.801892em;\"><span class=\"\" style=\"top: -3.113em; margin-right: 0.05em;\"><span class=\"pstrut\" style=\"height: 2.7em;\"><\/span><span class=\"sizing reset-size6 size3 mtight\"><span class=\"mord mtight\"><span class=\"mord mtight\">\u2032<\/span><\/span><\/span><\/span><\/span><\/span><\/span><\/span><\/span><span class=\"mopen\">(<\/span><span class=\"mord\"><span class=\"mord mathdefault\" style=\"margin-right: 0.10903em;\">N<\/span><span class=\"msupsub\"><span class=\"vlist-t vlist-t2\"><span class=\"vlist-r\"><span class=\"vlist\" style=\"height: 0.301108em;\"><span class=\"\" style=\"top: -2.55em; margin-left: -0.10903em; margin-right: 0.05em;\"><span class=\"pstrut\" style=\"height: 2.7em;\"><\/span><span class=\"sizing reset-size6 size3 mtight\"><span class=\"mord mtight\">1<\/span><\/span><\/span><\/span><span class=\"vlist-s\">\u200b<\/span><\/span><span class=\"vlist-r\"><span class=\"vlist\" style=\"height: 0.15em;\"><span class=\"\"><\/span><\/span><\/span><\/span><\/span><\/span><span class=\"mpunct\">,<\/span><span class=\"mspace\" style=\"margin-right: 0.166667em;\"><\/span><span class=\"mord\">.<\/span><span class=\"mord\">.<\/span><span class=\"mord\">.<\/span><span class=\"mpunct\">,<\/span><span class=\"mspace\" style=\"margin-right: 0.166667em;\"><\/span><span class=\"mord\"><span class=\"mord mathdefault\" style=\"margin-right: 0.10903em;\">N<\/span><span class=\"msupsub\"><span class=\"vlist-t vlist-t2\"><span class=\"vlist-r\"><span class=\"vlist\" style=\"height: 0.336108em;\"><span class=\"\" style=\"top: -2.55em; margin-left: -0.10903em; margin-right: 0.05em;\"><span class=\"pstrut\" style=\"height: 2.7em;\"><\/span><span class=\"sizing reset-size6 size3 mtight\"><span class=\"mord mathdefault mtight\" style=\"margin-right: 0.03148em;\">k<\/span><\/span><\/span><\/span><span class=\"vlist-s\">\u200b<\/span><\/span><span class=\"vlist-r\"><span class=\"vlist\" style=\"height: 0.15em;\"><span class=\"\"><\/span><\/span><\/span><\/span><\/span><\/span><span class=\"mclose\">)<\/span><span class=\"mclose\">)<\/span><span class=\"mord\">.<\/span><\/span><\/span><\/span><\/span><\/span><\/p>\n<p>\u8fd9\u4e2a\u610f\u601d\u662f<span class=\"katex--inline\"><span class=\"katex\"><span class=\"katex-mathml\"> = = &gt; ==&gt; <\/span><span class=\"katex-html\"><span class=\"base\"><span class=\"strut\" style=\"height: 0.36687em; vertical-align: 0em;\"><\/span><span class=\"mrel\">=<\/span><\/span><span class=\"base\"><span class=\"strut\" style=\"height: 0.36687em; vertical-align: 0em;\"><\/span><span class=\"mrel\">=<\/span><\/span><span class=\"base\"><span class=\"strut\" style=\"height: 0.5782em; vertical-align: -0.0391em;\"><\/span><span class=\"mrel\">&gt;<\/span><\/span><\/span><\/span><\/span>\u4e4b\u540e\u7684<span class=\"katex--inline\"><span class=\"katex\"><span class=\"katex-mathml\"> e \u2032 e' <\/span><span class=\"katex-html\"><span class=\"base\"><span class=\"strut\" style=\"height: 0.751892em; vertical-align: 0em;\"><\/span><span class=\"mord\"><span class=\"mord mathdefault\">e<\/span><span class=\"msupsub\"><span class=\"vlist-t\"><span class=\"vlist-r\"><span class=\"vlist\" style=\"height: 0.751892em;\"><span class=\"\" style=\"top: -3.063em; margin-right: 0.05em;\"><span class=\"pstrut\" style=\"height: 2.7em;\"><\/span><span class=\"sizing reset-size6 size3 mtight\"><span class=\"mord mtight\"><span class=\"mord mtight\">\u2032<\/span><\/span><\/span><\/span><\/span><\/span><\/span><\/span><\/span><\/span><\/span><\/span><\/span>\u7684<strong>\u53d1\u751f\u6b21\u6570\u5927\u4e8e\u7b49\u4e8e<\/strong><span class=\"katex--inline\"><span class=\"katex\"><span class=\"katex-mathml\"> = = &gt; ==&gt; <\/span><span class=\"katex-html\"><span class=\"base\"><span class=\"strut\" style=\"height: 0.36687em; vertical-align: 0em;\"><\/span><span class=\"mrel\">=<\/span><\/span><span class=\"base\"><span class=\"strut\" style=\"height: 0.36687em; vertical-align: 0em;\"><\/span><span class=\"mrel\">=<\/span><\/span><span class=\"base\"><span class=\"strut\" style=\"height: 0.5782em; vertical-align: -0.0391em;\"><\/span><span class=\"mrel\">&gt;<\/span><\/span><\/span><\/span><\/span>\u4e4b\u524d\u7684<span class=\"katex--inline\"><span class=\"katex\"><span class=\"katex-mathml\"> e e <\/span><span class=\"katex-html\"><span class=\"base\"><span class=\"strut\" style=\"height: 0.43056em; vertical-align: 0em;\"><\/span><span class=\"mord mathdefault\">e<\/span><\/span><\/span><\/span><\/span>\u7684\u53d1\u751f\u6b21\u6570\u7684\u3002\u53e6\u5916\u8981\u6ce8\u610f\uff0c<span class=\"katex--inline\"><span class=\"katex\"><span class=\"katex-mathml\"> = = &gt; ==&gt; <\/span><span class=\"katex-html\"><span class=\"base\"><span class=\"strut\" style=\"height: 0.36687em; vertical-align: 0em;\"><\/span><span class=\"mrel\">=<\/span><\/span><span class=\"base\"><span class=\"strut\" style=\"height: 0.36687em; vertical-align: 0em;\"><\/span><span class=\"mrel\">=<\/span><\/span><span class=\"base\"><span class=\"strut\" style=\"height: 0.5782em; vertical-align: -0.0391em;\"><\/span><span class=\"mrel\">&gt;<\/span><\/span><\/span><\/span><\/span>\u4e4b\u524d\u5199<span class=\"katex--inline\"><span class=\"katex\"><span class=\"katex-mathml\"> i n j \u2212 e v e n t inj-event <\/span><span class=\"katex-html\"><span class=\"base\"><span class=\"strut\" style=\"height: 0.85396em; vertical-align: -0.19444em;\"><\/span><span class=\"mord mathdefault\">i<\/span><span class=\"mord mathdefault\">n<\/span><span class=\"mord mathdefault\" style=\"margin-right: 0.05724em;\">j<\/span><span class=\"mspace\" style=\"margin-right: 0.222222em;\"><\/span><span class=\"mbin\">\u2212<\/span><span class=\"mspace\" style=\"margin-right: 0.222222em;\"><\/span><\/span><span class=\"base\"><span class=\"strut\" style=\"height: 0.61508em; vertical-align: 0em;\"><\/span><span class=\"mord mathdefault\">e<\/span><span class=\"mord mathdefault\" style=\"margin-right: 0.03588em;\">v<\/span><span class=\"mord mathdefault\">e<\/span><span class=\"mord mathdefault\">n<\/span><span class=\"mord mathdefault\">t<\/span><\/span><\/span><\/span><\/span>\u6216\u8005\u5199<span class=\"katex--inline\"><span class=\"katex\"><span class=\"katex-mathml\"> e v e n t event <\/span><span class=\"katex-html\"><span class=\"base\"><span class=\"strut\" style=\"height: 0.61508em; vertical-align: 0em;\"><\/span><span class=\"mord mathdefault\">e<\/span><span class=\"mord mathdefault\" style=\"margin-right: 0.03588em;\">v<\/span><span class=\"mord mathdefault\">e<\/span><span class=\"mord mathdefault\">n<\/span><span class=\"mord mathdefault\">t<\/span><\/span><\/span><\/span><\/span>\u90fd\u884c\uff0c\u53ea\u6709\u7bad\u5934\u4e4b\u540e\u5199\u4ec0\u4e48\u624d\u91cd\u8981\u3002<\/p>\n<h4>3 \u793a\u4f8b\uff1a\u63e1\u624b\u534f\u8bae\u4e2d\u7684\u4fdd\u5bc6\u6027\u548c\u8ba4\u8bc1\u6027<\/h4>\n<p>\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<ul>\n<li><code>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<li><code>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<li><code>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<li><code>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<p>\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<p>\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<span class=\"katex--inline\"><span class=\"katex\"><span class=\"katex-mathml\"> p k X = = p k A pkX==pkA <\/span><span class=\"katex-html\"><span class=\"base\"><span class=\"strut\" style=\"height: 0.88888em; vertical-align: -0.19444em;\"><\/span><span class=\"mord mathdefault\">p<\/span><span class=\"mord mathdefault\" style=\"margin-right: 0.03148em;\">k<\/span><span class=\"mord mathdefault\" style=\"margin-right: 0.07847em;\">X<\/span><span class=\"mspace\" style=\"margin-right: 0.277778em;\"><\/span><span class=\"mrel\">=<\/span><\/span><span class=\"base\"><span class=\"strut\" style=\"height: 0.36687em; vertical-align: 0em;\"><\/span><span class=\"mrel\">=<\/span><span class=\"mspace\" style=\"margin-right: 0.277778em;\"><\/span><\/span><span class=\"base\"><span class=\"strut\" style=\"height: 0.88888em; vertical-align: -0.19444em;\"><\/span><span class=\"mord mathdefault\">p<\/span><span class=\"mord mathdefault\" style=\"margin-right: 0.03148em;\">k<\/span><span class=\"mord mathdefault\">A<\/span><\/span><\/span><\/span><\/span>\uff09\uff0c\u90a3\u4e48A\u5bf9B\u7684\u8ba4\u8bc1\u5c31\u5e94\u8be5\u4fdd\u6301\u3002<\/p>\n<p>\u5c06\u4e0a\u9762\u4e24\u6761\u8ba4\u8bc1\u6027\u8d28\u5f62\u5f0f\u5316\uff0c\u4e66\u5199\u4e3a\uff1a<br \/> <span class=\"katex--display\"><span class=\"katex-display\"><span class=\"katex\"><span class=\"katex-mathml\"> q u e r y &nbsp;&nbsp; x : k e y , y : s p k e y ; &nbsp; e v e n t ( t e r m C l i e n t ( x , y ) ) = = &gt; 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 &nbsp;&nbsp; x : k e y ; &nbsp; i n j \u2212 e v e n t ( t e r m S e r v e r ( x ) ) = = &gt; 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} \\ \\ &amp; x:key,y:spkey; \\ \\bold{event}(termClient(x,y))==&gt;\\bold{event}(acceptsServer(x,y)). \\\\ \\bold{query} \\ \\ &amp; x:key; \\ \\bold{inj-event}(termServer(x))==&gt;\\bold{inj-event}(acceptsClient(x)). \\end{aligned} <\/span><span class=\"katex-html\"><span class=\"base\"><span class=\"strut\" style=\"height: 3em; vertical-align: -1.25em;\"><\/span><span class=\"mord\"><span class=\"mtable\"><span class=\"col-align-r\"><span class=\"vlist-t vlist-t2\"><span class=\"vlist-r\"><span class=\"vlist\" style=\"height: 1.75em;\"><span class=\"\" style=\"top: -3.91em;\"><span class=\"pstrut\" style=\"height: 3em;\"><\/span><span class=\"mord\"><span class=\"mord\"><span class=\"mord mathbf\">q<\/span><span class=\"mord mathbf\">u<\/span><span class=\"mord mathbf\">e<\/span><span class=\"mord mathbf\">r<\/span><span class=\"mord mathbf\" style=\"margin-right: 0.01597em;\">y<\/span><\/span><span class=\"mspace\">&nbsp;<\/span><span class=\"mspace\">&nbsp;<\/span><\/span><\/span><span class=\"\" style=\"top: -2.41em;\"><span class=\"pstrut\" style=\"height: 3em;\"><\/span><span class=\"mord\"><span class=\"mord\"><span class=\"mord mathbf\">q<\/span><span class=\"mord mathbf\">u<\/span><span class=\"mord mathbf\">e<\/span><span class=\"mord mathbf\">r<\/span><span class=\"mord mathbf\" style=\"margin-right: 0.01597em;\">y<\/span><\/span><span class=\"mspace\">&nbsp;<\/span><span class=\"mspace\">&nbsp;<\/span><\/span><\/span><\/span><span class=\"vlist-s\">\u200b<\/span><\/span><span class=\"vlist-r\"><span class=\"vlist\" style=\"height: 1.25em;\"><span class=\"\"><\/span><\/span><\/span><\/span><\/span><span class=\"col-align-l\"><span class=\"vlist-t vlist-t2\"><span class=\"vlist-r\"><span class=\"vlist\" style=\"height: 1.75em;\"><span class=\"\" style=\"top: -3.91em;\"><span class=\"pstrut\" style=\"height: 3em;\"><\/span><span class=\"mord\"><span class=\"mord\"><\/span><span class=\"mord mathdefault\">x<\/span><span class=\"mspace\" style=\"margin-right: 0.277778em;\"><\/span><span class=\"mrel\">:<\/span><span class=\"mspace\" style=\"margin-right: 0.277778em;\"><\/span><span class=\"mord mathdefault\" style=\"margin-right: 0.03148em;\">k<\/span><span class=\"mord mathdefault\">e<\/span><span class=\"mord mathdefault\" style=\"margin-right: 0.03588em;\">y<\/span><span class=\"mpunct\">,<\/span><span class=\"mspace\" style=\"margin-right: 0.166667em;\"><\/span><span class=\"mord mathdefault\" style=\"margin-right: 0.03588em;\">y<\/span><span class=\"mspace\" style=\"margin-right: 0.277778em;\"><\/span><span class=\"mrel\">:<\/span><span class=\"mspace\" style=\"margin-right: 0.277778em;\"><\/span><span class=\"mord mathdefault\">s<\/span><span class=\"mord mathdefault\">p<\/span><span class=\"mord mathdefault\" style=\"margin-right: 0.03148em;\">k<\/span><span class=\"mord mathdefault\">e<\/span><span class=\"mord mathdefault\" style=\"margin-right: 0.03588em;\">y<\/span><span class=\"mpunct\">;<\/span><span class=\"mspace\" style=\"margin-right: 0.166667em;\"><\/span><span class=\"mspace\">&nbsp;<\/span><span class=\"mord\"><span class=\"mord mathbf\">e<\/span><span class=\"mord mathbf\" style=\"margin-right: 0.01597em;\">v<\/span><span class=\"mord mathbf\">e<\/span><span class=\"mord mathbf\">n<\/span><span class=\"mord mathbf\">t<\/span><\/span><span class=\"mopen\">(<\/span><span class=\"mord mathdefault\">t<\/span><span class=\"mord mathdefault\">e<\/span><span class=\"mord mathdefault\" style=\"margin-right: 0.02778em;\">r<\/span><span class=\"mord mathdefault\">m<\/span><span class=\"mord mathdefault\" style=\"margin-right: 0.07153em;\">C<\/span><span class=\"mord mathdefault\" style=\"margin-right: 0.01968em;\">l<\/span><span class=\"mord mathdefault\">i<\/span><span class=\"mord mathdefault\">e<\/span><span class=\"mord mathdefault\">n<\/span><span class=\"mord mathdefault\">t<\/span><span class=\"mopen\">(<\/span><span class=\"mord mathdefault\">x<\/span><span class=\"mpunct\">,<\/span><span class=\"mspace\" style=\"margin-right: 0.166667em;\"><\/span><span class=\"mord mathdefault\" style=\"margin-right: 0.03588em;\">y<\/span><span class=\"mclose\">)<\/span><span class=\"mclose\">)<\/span><span class=\"mspace\" style=\"margin-right: 0.277778em;\"><\/span><span class=\"mrel\">=<\/span><span class=\"mrel\">=<\/span><span class=\"mrel\">&gt;<\/span><span class=\"mspace\" style=\"margin-right: 0.277778em;\"><\/span><span class=\"mord\"><span class=\"mord mathbf\">e<\/span><span class=\"mord mathbf\" style=\"margin-right: 0.01597em;\">v<\/span><span class=\"mord mathbf\">e<\/span><span class=\"mord mathbf\">n<\/span><span class=\"mord mathbf\">t<\/span><\/span><span class=\"mopen\">(<\/span><span class=\"mord mathdefault\">a<\/span><span class=\"mord mathdefault\">c<\/span><span class=\"mord mathdefault\">c<\/span><span class=\"mord mathdefault\">e<\/span><span class=\"mord mathdefault\">p<\/span><span class=\"mord mathdefault\">t<\/span><span class=\"mord mathdefault\">s<\/span><span class=\"mord mathdefault\" style=\"margin-right: 0.05764em;\">S<\/span><span class=\"mord mathdefault\">e<\/span><span class=\"mord mathdefault\" style=\"margin-right: 0.02778em;\">r<\/span><span class=\"mord mathdefault\" style=\"margin-right: 0.03588em;\">v<\/span><span class=\"mord mathdefault\">e<\/span><span class=\"mord mathdefault\" style=\"margin-right: 0.02778em;\">r<\/span><span class=\"mopen\">(<\/span><span class=\"mord mathdefault\">x<\/span><span class=\"mpunct\">,<\/span><span class=\"mspace\" style=\"margin-right: 0.166667em;\"><\/span><span class=\"mord mathdefault\" style=\"margin-right: 0.03588em;\">y<\/span><span class=\"mclose\">)<\/span><span class=\"mclose\">)<\/span><span class=\"mord\">.<\/span><\/span><\/span><span class=\"\" style=\"top: -2.41em;\"><span class=\"pstrut\" style=\"height: 3em;\"><\/span><span class=\"mord\"><span class=\"mord\"><\/span><span class=\"mord mathdefault\">x<\/span><span class=\"mspace\" style=\"margin-right: 0.277778em;\"><\/span><span class=\"mrel\">:<\/span><span class=\"mspace\" style=\"margin-right: 0.277778em;\"><\/span><span class=\"mord mathdefault\" style=\"margin-right: 0.03148em;\">k<\/span><span class=\"mord mathdefault\">e<\/span><span class=\"mord mathdefault\" style=\"margin-right: 0.03588em;\">y<\/span><span class=\"mpunct\">;<\/span><span class=\"mspace\" style=\"margin-right: 0.166667em;\"><\/span><span class=\"mspace\">&nbsp;<\/span><span class=\"mord\"><span class=\"mord mathbf\">i<\/span><span class=\"mord mathbf\">n<\/span><span class=\"mord mathbf\">j<\/span><span class=\"mspace\" style=\"margin-right: 0.222222em;\"><\/span><span class=\"mbin\">\u2212<\/span><span class=\"mspace\" style=\"margin-right: 0.222222em;\"><\/span><span class=\"mord mathbf\">e<\/span><span class=\"mord mathbf\" style=\"margin-right: 0.01597em;\">v<\/span><span class=\"mord mathbf\">e<\/span><span class=\"mord mathbf\">n<\/span><span class=\"mord mathbf\">t<\/span><\/span><span class=\"mopen\">(<\/span><span class=\"mord mathdefault\">t<\/span><span class=\"mord mathdefault\">e<\/span><span class=\"mord mathdefault\" style=\"margin-right: 0.02778em;\">r<\/span><span class=\"mord mathdefault\">m<\/span><span class=\"mord mathdefault\" style=\"margin-right: 0.05764em;\">S<\/span><span class=\"mord mathdefault\">e<\/span><span class=\"mord mathdefault\" style=\"margin-right: 0.02778em;\">r<\/span><span class=\"mord mathdefault\" style=\"margin-right: 0.03588em;\">v<\/span><span class=\"mord mathdefault\">e<\/span><span class=\"mord mathdefault\" style=\"margin-right: 0.02778em;\">r<\/span><span class=\"mopen\">(<\/span><span class=\"mord mathdefault\">x<\/span><span class=\"mclose\">)<\/span><span class=\"mclose\">)<\/span><span class=\"mspace\" style=\"margin-right: 0.277778em;\"><\/span><span class=\"mrel\">=<\/span><span class=\"mrel\">=<\/span><span class=\"mrel\">&gt;<\/span><span class=\"mspace\" style=\"margin-right: 0.277778em;\"><\/span><span class=\"mord\"><span class=\"mord mathbf\">i<\/span><span class=\"mord mathbf\">n<\/span><span class=\"mord mathbf\">j<\/span><span class=\"mspace\" style=\"margin-right: 0.222222em;\"><\/span><span class=\"mbin\">\u2212<\/span><span class=\"mspace\" style=\"margin-right: 0.222222em;\"><\/span><span class=\"mord mathbf\">e<\/span><span class=\"mord mathbf\" style=\"margin-right: 0.01597em;\">v<\/span><span class=\"mord mathbf\">e<\/span><span class=\"mord mathbf\">n<\/span><span class=\"mord mathbf\">t<\/span><\/span><span class=\"mopen\">(<\/span><span class=\"mord mathdefault\">a<\/span><span class=\"mord mathdefault\">c<\/span><span class=\"mord mathdefault\">c<\/span><span class=\"mord mathdefault\">e<\/span><span class=\"mord mathdefault\">p<\/span><span class=\"mord mathdefault\">t<\/span><span class=\"mord mathdefault\">s<\/span><span class=\"mord mathdefault\" style=\"margin-right: 0.07153em;\">C<\/span><span class=\"mord mathdefault\" style=\"margin-right: 0.01968em;\">l<\/span><span class=\"mord mathdefault\">i<\/span><span class=\"mord mathdefault\">e<\/span><span class=\"mord mathdefault\">n<\/span><span class=\"mord mathdefault\">t<\/span><span class=\"mopen\">(<\/span><span class=\"mord mathdefault\">x<\/span><span class=\"mclose\">)<\/span><span class=\"mclose\">)<\/span><span class=\"mord\">.<\/span><\/span><\/span><\/span><span class=\"vlist-s\">\u200b<\/span><\/span><span class=\"vlist-r\"><span class=\"vlist\" style=\"height: 1.25em;\"><span class=\"\"><\/span><\/span><\/span><\/span><\/span><\/span><\/span><\/span><\/span><\/span><\/span><\/span><\/p>\n<p>\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<p>\u52a0\u5165\u8fd9\u4e24\u6761\u8ba4\u8bc1\u6027\u8d28\u7684\u63e1\u624b\u534f\u8bae\u5982\u4e0b\uff1a<\/p>\n<pre class=\"language-java prettyprint linenums\"><code>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))==&gt;event(acceptsServer(x,y)). query x:key; inj-event(termServer(x))==&gt;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<p>\u6ce8\u610f\u5ba2\u6237\u7aef\u548c\u670d\u52a1\u5668\u7684<code>accepts*<\/code>\u4e8b\u4ef6\u548c<code>term*<\/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<br \/> <img decoding=\"async\" src=\"https:\/\/img-blog.csdnimg.cn\/20200813155824570.png\" =\"\" =\"\u5728\u8fd9\u91cc\u63d2\u5165\u56fe\u7247\u63cf\u8ff0\" alt=\"\u3010ProVerif\u5b66\u4e60\u7b14\u8bb0\u30114\uff1a\u4fe1\u606f\u5b89\u5168\u6027\u8d28(Security Property) (https:\/\/mushiming.com\/)  \u7b2c1\u5f20\" title=\"\u3010ProVerif\u5b66\u4e60\u7b14\u8bb0\u30114\uff1a\u4fe1\u606f\u5b89\u5168\u6027\u8d28(Security Property)  \u7b2c1\u5f20-\u7a46\u4e16\u660e\u535a\u5ba2\" ><\/p>\n<p>\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\u7acb<code>acceptsServer<\/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\u8ba4<code>termClient<\/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<p>\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\u7acb<code>acceptsClient<\/code>\u3011\u5e94\u8be5\u662f\u5728\u62ff\u5230<code>key<\/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\u8ba4<code>termServer<\/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\u67e5<code>pkX==pkA<\/code>\u624d\u884c\u3002<\/p>\n<hr>\n<p>\u624b\u518c\u91cc\u7ed9\u51fa\u4e86\u4e00\u4e9b\u6280\u5de7\uff0c\u5373\u901a\u5e38\u800c\u8a00<code>==&gt;<\/code>\u524d\u9762\u7684\u4e8b\u4ef6\u53ef\u4ee5\u653e\u5728\u8fdb\u7a0b\u672b\u5c3e\uff0c\u800c<code>==&gt;<\/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<p>\u8bbe<code>e==&gt;e'<\/code>\u5373\u4e0d\u540c\u8fdb\u7a0b\u4e2d\u7684\u4e24\u4e2a\u4e8b\u4ef6\u8fbe\u6210\u8ba4\u8bc1\u5173\u7cfb\uff0c\u901a\u5e38<code>e<\/code>\u6bd4\u8f83\u9760\u540e\uff0c<code>e'<\/code>\u6bd4\u8f83\u9760\u524d\uff0c\u4f46\u662f\u8ba9<code>e<\/code>\u5c3d\u91cf\u5f80\u4e0a\uff0c<code>e'<\/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<h4>\u53c2\u8003\u9605\u8bfb<\/h4>\n<p>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}]}}