交换树自动机理论在系统设计中的应用-大崎仁

理论计算机科学电子笔记124（2005）97-111www.elsevier.com/locate/entcsACTAS：一个结合交换树自动机理论的系统设计大崎仁国家高级工业科学技术研究所&PRESTOohsaki@ni.aist.go.jp高井俊则CRESTtakai@ni.aist.go.jp摘要ACTAS是一个用于操作关联交换树自动机（AC- tree automata）的集成系统，它具有AC-tree自动机的布尔运算、重写后代计算、空性和成员问题求解等多种功能。为了在合理的时间内处理高复杂性问题，还配备了过近似和欠近似算法。这种功能使我们能够在有限状态模型中自动验证安全属性，这在网络安全等领域特别有用，对于允许等式性质的密码协议的安全问题。在模型构建过程中，为状态空间扩展分析提供了工具支持。计算的中间状态以数值数据表显示，并生成折线图。此外，该系统的图形用户界面为我们提供了一个方便的使用环境。关键词：项重写，AC树自动机，验证，密码协议1介绍树自动机是字符串有限自动机的对应物，在某种意义上，它们继承了有限自动机的大部分属性。已知树自动机识别的树语言在布尔运算下是封闭的，并且大多数可判定性结果是肯定的[4]。1571-0661 © 2005由Elsevier B. V.出版，CC BY-NC-ND许可下开放获取。doi：10.1016/j.entcs.2004.07.01798H. Ohsaki，T.Takai/Electronic Notes in Theoretical Computer Science 124（2005）97RRR树自动机框架在处理树（即术语）时很有用，并且已经研究了基于树自动机理论的几种验证技术[5，7]。例如，Kaji等人在[8]中指出，几个重要的密码协议可以用项重写系统（TRS，[2]）和树自动机来建模，而且树自动机的正可判定性结果和闭包性质允许我们设计一种自动演绎技术来推理安全问题。事实上，安全协议的验证工具已经通过使用树自动机框架开发出来[1，3]。 Genet和Viet Triem Tong提供了 一个树自动机库，称为Timbuk[5，6]，其中函数符号的结合和交换性质通过使用近似来处理。允许结合性和交换性的基于规则的方法也被研究，例如在[9]中。下面让我们简单地解释一下如何在实践中通过使用项重写和树自动机来处理无限状态转换系统的模型检查问题。 我们假设签名F上的TRSR指定转移系统M的转移关系。我们说M承认转变步骤s→Mt在初始状态空间L下，如果（1）s=C[lσ]和t=C[rσ]，对于R中的某个重写规则l→r，上下文C和替换σ，以及（2）存在L中的状态s0，使得s0→ s，其中→ s是自反的和传递的→M的闭包M MMR. 也就是说，. 应该注意到，系统M是F上所有基项的集合，并且M的状态空间要验证的是从L到R的可达状态。我们假设初始状态空间L可以用某个树自动机A来表示，使得t∈L当且仅当t被A接受。因此，在这种情况下，给定重写系统和指定M和L中的每一个的树自动机，转换系统的可达状态空间被认为是定义的。本文用L（A）表示树自动机A所接受的元素集，用[→]（L（A））可达状态的集合。设P是M的定义域的某个子集，它由我们不允许M从L中的任何初始状态过渡到的状态组成。 例如，在网络协议中，P是私有信息的集合， L是入侵者的初始知识，R是入侵者的可能操作。 因此入侵者可以获得的信息可以表示为（一）（二）（三）（四）（五）（五）（六）（六）（七）（八）（八）（入侵者可以通过某种方式获得的信息 换句话说就是交叉点的非空指示协议不安全。然而，可达状态的集合[→L]（L）不是正则树语言即使我R是一种正规的树语言。更糟糕的是，它通常是不可计算的树语言L称为正则语言，如果存在树自动机A，使得H. Ohsaki，T.Takai/Electronic Notes in Theoretical Computer Science 124（2005）9799FF→L被A识别。为了克服上述问题，已经进行了几项研究，例如：（1）找到R的一个子类，即保持正则性的充分条件，以及（2）扩展树自动机框架，可以处理更广泛种类的树语言。在[16，17]中已经研究了有效地保持正则性的这种TRS的可判定子类关于第二种方法，已知正则性不是AC闭的。准确地说，正则树语言的AC闭包不再是正则的。如果假设以下公理，则签名中的二元函数符号f是结合和交换的f（x，f（y，z））=f（f（x，y），z）f（x，y）=f（y，x）树语言L的AC-闭包是，给定F中二元函数符号的子集F AC，|s∈L. s = ACt}。这 里 = AC表示AC中所有函数符号的AC-公理所导出的等价关系。的上述否定的观察揭示了，对于像Di Jie-Hellman密钥交换协议那样的允许等式性质的密码协议的建模，标准树自动机不能处理可达状态空间。在本研究中，我们采用第二种方法。我们在[14]中提出了树自动机的一个扩展，称为等式树自动机。我们在[11，12]中也证明了，在某些有用的等式公理下，例如，结合性和/或交换性，方程树自动机接受的树语言在布尔运算下是封闭的。在这种程度上，可以处理以前的Difference-Hellman密钥交换协议，甚至验证过程也是自动化的[13]。AC-tree automata simulator（ACTAS）是一个计算树自动机的工具，它允许一些二元函数符号是关联的和可交换的。该系统的屏幕截图如图1所示。这类AC-树自动机在并和交下是有效封闭的，并且其成员和空性问题是可判定的。在常规情况下，空性检验在线性时间内可解。非正则情况下的空性问题的可判定性结果也是肯定的，但它在实际计算意义上是不可管理的，这可以从一个Petri网实例的可达性是EXPSPACE-难的这一事实来观察，非正则AC-树自动机在某种意义上是Petri网的推广。因此，我们在ACTAS中设计了过近似和欠近似算法，用于高效地计算重写后代[1]R/AC ]（L（A/A/C））AC树自动机A/AC和AC-TRSR/AC。100H. Ohsaki，T.Takai/Electronic Notes in Theoretical Computer Science 124（2005）97QF Q QQ一∈ F ∈ Qf（p1，. ，pn）→ q1f（p1，. ，pn）→ f（q1，...， qn）p1→q1（类型1）（类型2）（类型3）Fig. 1. ACTAS控制面板2AC树自动机我们从介绍AC树自动机开始这一节。然后，我们解释了如何操作ACTAS作为一个工具来操纵AC树自动机，甚至作为一个工具来支持自动验证。树自动机（简称TA）A是一个4元组（F，Q，Qfinn，F），其组成部分是签名F，即具有固定特征的函数符号的有限集合，称为状态的特殊常数符号的有限集合，= n，其元素被称为最终状态的子集fin，以及以下形式之一的过渡规则的有限集合fin使得f，arity（f）= n且p1，.，pn，q1，.，qn.在类型2中，左右两边的根函数符号必须相同。类型3中的转换规则被称为ε-规则（一个TA被称为正则的，如果TA只包含类型1的规则。类型2的规则在[4]中没有处理。然而，在考虑方程性质的情况下，类型2在以下意义上是必要的：我们定义的可识别树语言与单词语言层次结构有一个双射对应关系[11]。一位专家H. Ohsaki，T.Takai/Electronic Notes in Theoretical Computer Science 124（2005）97101→EF在[14]中提出的这种AC-树自动机的交集算法也是优点之一。A过渡移动→A是重写关系→A，将A作为TRS在签名上签名。F上的基项t被接受，如果t→f一对于某个qf∈ Qfinn。 树自动机A接受的项集是表示为L（A）。 树语言L是所有基本项的子集，如果存在树自动机A使得L=L（A），则可识别方程树自动机是一对树自动机A和方程理论E，记为A/E。过渡移动由关系A模定义。AC-树自动机是一种方程树自动机，其方程理论是结合性和交换性中的一些二元函数符号的公理。AC树自动机的基本性质如下所述：定理2.1 [12，14]（1）AC-树自动机可识别的树语言类在并和交下是闭的。（2）正则AC-树自动机可识别的树语言类在布尔运算下是封闭的。(3)AC-树自动机的成员问题和空问题是可判定的.Q我们考虑具有以下转移规则的树自动机Aa→qab→qbf（qa，qb）→qf（q，q）→q最后的状态Q。假设f是结合和交换的，那么AC树自动机A/AC接受这样的树t，|a =|不|B|b即，在同一棵树T中，A的出现次数与B的出现次数相同。人们应该注意到，上述语言是不可识别的任何树自动机。在ACTAS中，上述AC树自动机A/AC被指定为如下所示[签字]AC：fconst：a，b[T-规则（q）：A] a-> q_ab -> q_b f（q_a，q_b）->qf（q，q）->q术语模型的签名通过声明AC符号（例如，AC：f），同时声明常量函数符号（例如const：a，b）。根据该语法，将其它常量符号识别为状态符号。 树自动机A在第二个模块中指定，名为A，102H. Ohsaki，T.Takai/Electronic Notes in Theoretical Computer Science 124（2005）97ARCL C→{1}|||}R→i=11：[签名]7：[T规则（q）：A1]13：[T规则（q）：A2]2：AC：总和8：0 -> q_014：0 -> q3：const：09：q_0 -> q15：s（q）-> q_1第四章：10：s（q_0）-> q_116：s（q_1）-> q5：[R-规则：R]11：sum（q_1，q_1）-> q17：sum（q_1，q_1）-> q6：0 -> s（s（0））12：sum（q，q）-> q18：sum（q，q）-> q图二. ACTAS中的AC重写后代计算通过列出转换规则。T-规则的参数值q是树自动机A的最终状态。在目前的实施中，ACTAS配备了以下功能-（i）-（ii）布尔运算和（iii）重写后代计算的解，(i) 给定AC-树自动机A/AC和B/AC，构造一个AC-树自动机C/AC，使得L（C/AC）=L（A/AC）<$L（B/AC）.(ii) 给定AC-树自动机A/AC和B/AC，构造一个AC-树自动机C/AC，使得L（C/AC）=L（A/AC）<$L（B/AC）.(iii) 给定一个AC-树自动机/AC和一个重写规则不含AC-函数符号的AC-TRS /AC，构造AC-树自动机/AC，则（ /AC）=[R/AC ]（L（A/AC））。(iv) 给定AC树自动机A/AC和项t，确定是否t∈ L（A/AC）.(v) 给定一个AC树自动机A/AC，判断L（A/AC）是否= L。通过操作（i）-（iii）获得的计算结果可以重新用于新的对于自动验证，上述功能（iii）对于构建模型很有用。我们考虑图中的例子二、重写系统R由单个重写规则0→s（s（0））组成 树自动机A1接受树t，如果满足以下三个条件之一：（1）t = 0，（2）t =sum（s（0），s（0）），或（3）t=sum（t1，t2），使得t1，t2被A1/AC接受。由 于 声明AC：sum，二进制符号sum是结合和交换的。因此，上面的语言符合L=t ts（0）是偶数。这意味着t由三个分量sum，0，s（0）组成，并且s（0）在t中出现的次数是偶数。我们取L（A1/AC）（=L）作为初始状态空间，由/AC诱导的系统满足：s是[k]中R/AC ]（L）如果且只有当s = sum{s1，.，sn}，使得[[si]是偶数，其中[0]] = 0，H. Ohsaki，T.Takai/Electronic Notes in Theoretical Computer Science 124（2005）97103RA→一→ L A[[s（t）]]=[t]]+1。也就是说，只要在s中出现的自然数之和是偶数，s就是由/AC和1/AC生成的项。另一方面树语言[编辑]R/AC ]（L）可以用AC树自动机表示，例如，图2中定义的2/AC。但使用ACTAS的好处是，我们可以构造AC树自动机作为后代计算的结果可以观察到，在通过定点计算构造AC-树自动机时，经常需要有界计算，因为给定一个AC-TRSR/AC和nAC-三个子A/AC，（a）[→A]（L（A/AC））是AC/AC（2）如果（1）（ （/AC））可计算在一定条件下，它可能无法用AC-树自动机识别。这两种情况对应于非终止计算。根据上述观察，在ACTAS中，三个参数被安排在控制面板。 (See左下角的图。①的人。第1页限制算法中最外层循环的执行次数：通过设置1、A = 0（1）在函数（iii）中，我们可以执行只重写n个循环的后代计算。如果参数1为0，则程序检查给定的ACTAS代码在语法上是否正确，因为没有发生实质性的计算。为了计算过近似或欠近似的结果，我们为参数2和3选择适当的正整数。 如果非左线性重写规则为f（x，x）→x包含在重写系统中，我们需要检查，在算法的功能（iii），是否树自动机Ap1=（F，Q，{p1}，）和Ap2=（F，Q，{p2}，n）满足L（Ap1/AC）L（Ap2/AC）/=L对于Q中的某个p1，p2，其中p1/=p2.参数2和参数3的取值限制了上述问题决策过程的搜索深度和广度但如果参数2和3是最大值100，则忽略上限限制。如果计算终止，这反过来又会导致精确解 因此，通过为参数1本文讨论了[→A]（L（A/AC））在实际中的近似结果，有时间。另一方面，通过给出过度近似的结果。R/AC参数2和3 如果是0，3加密协议验证我们将在下面解释如何使用ACTAS验证网络协议。在图3所示的协议中，我们用E（x，y）表示由某个密钥x加密的消息y，用K（x）表示主体x 该协议的目标是在不丢失保密性的情况下从alice向bob发送秘密消息m104H. Ohsaki，T.Takai/Electronic Notes in Theoretical Computer Science 124（2005）97R设置[→R穴因此m用另一个密钥（随机数）r加密，因此r也被加密并传送给bob。在这个网络通信中，alice首先发送一个E（K（alice），r）的三元组，alice是发送者 在最后一步，Alice将E（K（bob），r）和E（r，m）的对发送给bob。后一个分量是通过用r加密m而生成的。接收方bob可以通过首先解密E（K（bob），r）来检索明文m。(1) E（K（alice），r），alice，bob_服务器爱丽丝，o（2）E（K（bob），r）鲍勃(3)E（K（bob），r），E（r，m）图三. 的密码协议现在我们假设入侵者夏娃拥有以下4种能力：1. 如果eve知道x和E（x，y），那么eve也知道y，2. Eve知道如何应用加密和解密函数E和D，也就是说，如果eve知道x和y，那么eve可以构造E（x，y）和D（x，y），3. eve知道其自己的秘密密钥K（eve）和所有其他主体的名称例如Alice和Bob，4. Eve可以窃听网络信道，即，Eve知道图1的网络中的所有信息3 .第三章。为了检测协议的安全性（否则保证协议的保密性），我们使用TRS和树自动机对协议进行了验证。我们首先通过树自动机对入侵者的初始知识进行建模。然后，我们通过以下TRS生成从初始知识可达到的状态集：Rcrypt={D（x，E（x，y））→y}TRS地穴对应于上述入侵者其他假设2-图四、树自动机A初始接受项t当且仅当t可由入侵者在不使用防解密公理Rcrypt的情况下获得。的地下室[1]（L（Ainitial））的可达状态对应于入侵者的知识 通过计算重写后代（函数（iii）），我们有一个树自动机Afixpoint，满足L（Afixpoint）=[→A]（L（Ainitial））如果存在的话。 因此，通过求解隶属约束（函数（iv）），H. Ohsaki，T.Takai/Electronic Notes in Theoretical Computer Science 124（2005）97105一曰：[签署]十五：k（q_e）-> q第二章：const：alice，bob，eve，m，r 十六日：eve -> q_e第三章：var：x，y十七：第四章：十八日：e（q_ka，q_r）-> q第五章：【R-rule：R_crypt】十九日：k（q_a）-> q_ka第六章：d（x，e（x，y））-> y二十：alice -> q_a第七章：二十一：第八章：【T规则（q）：A_initial】二十二：e（q_kb，q_r）-> q第九章：d（q，q）-> q二十三：k（q_b）-> q_kb第十章：e（q，q）-> q二十四：bob -> q_b十一：二十五：十二：爱丽丝-> q二十六：e（q_r，q_m）-> q十三日：bob -> q二十七：m-> q_m十四日：eve -> q二十八：r-> q_r见图4。 仅假设窃听的密码协议的规范代码一曰：[签署]二十：k（q_e）-> q第二章：const：alice，bob，eve，m，r二十一：eve -> q_e第三章：var：x，y，z二十二：第四章：二十三：s（q_kar，q_a，q_b）-> q第【R-rule：R_crypt2】二十e（q_ka，q_r）->106H. Ohsaki，T.Takai/Electronic Notes in Theoretical Computer Science 124（2005）97五章：四：q_kar第六章：d（x，e（x，y））-> y二十五：k（q_a）-> q_ka第七章：s（x，y，z）-> e（k（z），d（k（y），x））二十六：alice -> q_a第八章：s（x，y，z）-> x二十七：第九章：s（x，y，z）-> y二十八：e（q_kb，q_r）-> q第十章：s（x，y，z）-> z二十九日：k（q_b）-> q_kb十一：30日上午10：bob -> q_b十二：[T规则（q）：A_initial2]三十一：十三日：d（q，q）-> q三十二：e（q_r，q_m）-> q十四日：e（q，q）-> q三十三：m-> q_m十五：s（q，q，q）-> q三十四：r-> q_r十六日：十七：爱丽丝-> q十八日：bob -> q十九日：eve -> q图五.假设主动攻击的密码协议的规范代码m∈ L（A定点）？，可以确定该协议对于窃听是否安全。沿着类似的构造方案，我们可以检测到相同的协议对于假冒是不安全的。相关的树自动机和TRS在图5中示出，其表示假设入侵者的主动攻击的先前协议示例。通过允许每个主体（包括入侵者Eve）向服务器发送请求，我们添加了重写规则s（x，y，z）→E（k（z），D（k（y），x））H. Ohsaki，T.Takai/Electronic Notes in Theoretical Computer Science 124（2005）97107→回路（T规则）（州）时间（秒）0189-130163241161234416224441632见图6。 转换规则和状态符号的数量（循环0以及到先前码的转换规则s（q，q，q）q。 在左侧在重写规则的s（x，y，z）侧，变量x，y，z分别（倾向于）被分配给加密数据、发送者的ID和接收者的ID。更确切地说，发送方接收加密消息E（K（s1），D（K（s2），s3）），该消息在服务器站点用发送方的密钥解密一次我们还假设eve可以分解形式为s（t1，t2，t3）的任何数据，并且这种情况由其他三个重写规则表示。在实验中，通过使用ACTAS的函数（iii），其中PARR 1为4或更大（其他为任意正整数），我们得到了欠近似的结果。图6中示出了每个循环处的转换规则和状态符号的数量。该表格与线图一起自动生成。我们可以将显示的数据保存为HTML格式文件（图1）。7）。由此产生的树自动机接受秘密消息m，因此，我们知道该协议是不安全的。实际上，该协议允许以下安全规则：入侵者首先向服务器发送元组E（K（alice），r），alice，eve。由于假设3和假设4，这些要素包含在eve然后eve从服务器获得E（K（eve），r）作为响应。通过假设2和3，eve创建D（D（K（eve），E（K（eve），r）），E（r，m）），其产生m，因为Rcrypt是假设1。4D-H密钥交换协议下面描述的协议被称为Di Schie-Hellman密钥交换算法（例如第22.1节，[15]）：在图中，H（x，y）代表数据x和y的组合，即一个整数yx（modp，其中p是给定的）。为了简化H的性质，我们假设在这个模型中H被实现为H（x，y）=px+y（modq，其中p，q是给定的）。主体x的秘密密钥由K（x）表示。 该协议的目标是在不丢失保密性的情况下，通过在发起者（108H. Ohsaki，T.Takai/Electronic Notes in Theoretical Computer Science 124（2005）97见图7。 状态空间分析（1）H（K（alice），r），r(2) H（K（bob），r）爱丽丝 ，，(3) E（H（H（K（bob），r），K（alice）），m）鲍勃见图8。 Di-H密钥交换算法示例）和接收方（Bob），然后从发起方向接收方发送该协议由三个步骤组成：Alice首先选择一个数字r，并将其与整数H（K（Alice），r）一起发送给Bob。我们假设没有其他人可以从H（K（alice），r）中检索K在第二步，bob返回H（K（bob），r）给alice。由于H的实现中的幂运算，可以假设H是结合的和交换的：H（x，H（y，z））=H（H（x，y），z）H（x，y）=H（y，x）H. Ohsaki，T.Takai/Electronic Notes in Theoretical Computer Science 124（2005）97109一曰：[签署]第二章：第三章：第四章：AC：Hconst：alice，bob，eve，m，r var：x，y二十：二十一：二十二：h（q_ka，q_r）-> q k（q_a）-> q_kaalice -> q_a第五章：第六章：【R-rule：R_crypt】二十三：二十四：r-> q_r第七章：第八章：第九章：第十章：十一：十二：d（x，e（x，y））-> y[T规则（q）：假设]d（q，q）-> qe（q，q）-> qh（q，q）-> q二十五：二十六：二十七：二十八：二十九日：30日上午10：三十一：r ->qh（q_kb，q_r）-> q k（q_b）->q_kb bob -> q_be（q_kabr，q_m）-> q十三日：十四日：爱丽丝-> q三十二：三十三：h（q_kbr，q_ka）->q_kabrh（q_kb，q_r）->q_kbr十五：bob -> q三十四：m-> q_m十六日eve -> q110H. Ohsaki，T.Takai/Electronic Notes in Theoretical Computer Science 124（2005）97R：十七：十八日：k（q_e）-> q十九日：eve -> q_e见图9。 迪-赫尔曼密钥交换协议（假设仅窃听）由于前两个步骤，alice可以通过组合H（K（bob），r）和K（alice）来生成H（H （ K（ bob ） 后 一部 分 是 她的 密 钥 。 类似 地 ，bob 也 生 成H （H （K（alice），r），K（bob）），使得：H（H（K（alice），r），K（bob））=ACH（H（K（bob），r），K（alice））.因此，bob获得消息m如下。D（H（H（K（alice），r），K（bob）），E（H（H（K（bob），r），K（alice）），m））=ACD（H（H（K（bob），r），K（alice）），E（H（H（K（bob），r），K（alice）），m））→Rcryptm协议的假设可以指定为ACTAS代码，如图9所示。在这种情况下，我们假设（a）入侵者eve可以窃听网络信道，但（b）eve不会主动攻击协议。即使二元函数符号H是结合的和可交换的，AC重写后代也可以通过使用[16]的相同算法来计算，因为H不出现在重写规则中。 但由于crypt的左边有变量x的多次出现，AC-树自动机的交空问题必须在算法中处理在ACTAS中可以方便地计算AC-树自动机的交集。然而，在这种有效的构造中，所得到的AC-树自动机不再是AC-正则的，并且解决非正则AC-树自动机的空性问题是EXPSPACE困难的[12]。事实上，当完全自动计算精确解时，H. Ohsaki，T.Takai/Electronic Notes in Theoretical Computer Science 124（2005）97111一↓→非终止计算。然后，对于该示例有两个选择：过近似算法（通过将参数2设置为0）和欠近似（通过为参数2和3选择正整数）。过度近似在这种情况下，结果，即一个AC树自动机，是夏娃可获得的知识的某个超集也就是说，如果秘密消息m不被接受，则保证了协议的保密性通过取上面的输入（图9），我们得到一个AC树自动机作为输出，接受m。但是，这并不意味着协议的安全性。 在当前的实现中，没有选项来细化过度近似的结果。近似不足。在完全自动化模式下，也不会检测到协议的安全漏洞。这意味着，通过对参数2和3取几对正整数，得到了欠近似的结果，但是表示eve 尽管如此，我们有另一种可能性来处理AC树自动机框架中的这个协议示例。计算重写后代的基本思想是，给定树自动机A=（F，Q，Qfinn，n），找到重写规则l→r∈R以及赋值ρ ={xi <$→qi|1 ≤i≤n}，其中q，qi∈ Q且1 ≤i≤ n使得lρ→<$q但rρ/→ <$q。 然后我们添加新的状态和过渡A/ACA/ACj规则到A，使得新获得的系统A/AC满足rρ→AJ/ACq。该过程对应于对于somet∈L（A/AC）和dtJ∈/L（A/AC）的c a s e的一步重写后代计算a t t → R t j，suchthtt/o=lσ，tJ=s[rσ] o，p= σA/AC（即，p是σ关于/AC）。 此外，作为上述计算中的例外情况，如下处理非左线性重写规则。例如，我们考虑规则f（x，x）取两个（不同的）状态符号p1和p2，则我们检查是否L（A（p1）/AC）= L（A（p2）/AC）/上面的L（A（pi）/AC）是A/AC接受的树语言，其最终状态Qfinn被{pi}替换。 如果上面的问题得到了肯定的解决，我们对同一个变量x取不同的赋值x<$→ p1和x <$→ p2。形式上，非线性变量x被x1和x2替换，然后定义包含赋值x1→p1和x2→p2的替换ρ。假设A0/AC是最初提供的AC-树自动机。 则以下陈述。引理4.1对于A0/AC的每个状态符号p和q，112H. Ohsaki，T.Takai/Electronic Notes in Theoretical Computer Science 124（2005）97LA LAA/AC→（0（p）/AC）和（0（q）/AC）的空性是通过求解有限个隶属度问题来检验的.证据我们假设p/= q，其中q是图1中AC-树自动机的最终状态符号。9 .第九条。通过构造，L（A0（p）/AC）只接受有限棵树st1， . . . . ，tn，和dt1， . . ，由于K？nig的原因引理，例如在[10]中。因此，在这种情况下，交空性可以通过隶属度测试来解决。 剩下的情况是显而易见的。Q系统中的隶属函数帮助我们进行上述测试。理论上，正则AC树自动机的成员问题是NP完全的（推论4，[12]），但在这个例子中，树的大小最多为9。这意味着p和q的所有可能的组合都可以在合理的时间内计算。利用这个结果，我们可以检验下列性质是否正确。引理4.2设p1，p2，p3，p4是A0/AC的状态符号，使得L（A0（p1）/AC）<$L（A0（p2）/AC）<$，则D（p1，E（p2，p3））→n0p4当且仅当p1 = p2 = p3 = p4= q.Q定理4.3树语言[1]R穴/AC]（L（A0/AC））可与A0/AC。Q因此，A0/AC已经是定点，也就是说，该协议是安全的，不受窃听，因为m不在eve关于通过假设冒充的主动攻击，协议的安全性定理在[15]中指出例如，该协议允许以下攻击：(1) H（K（alice），r），r（2）H（K（eve），r），r爱丽丝(4) H（K（bob），r），，(5) E（H（H（K（bob），r），K（alice）），m）前夕（3）H（K（bob），r），，鲍勃见图10。 Di Chie-Hellman密钥交换协议确认作者感谢三位匿名的审稿人，感谢他们为改进论文早期版本提出的许多H. Ohsaki，T.Takai/Electronic Notes in Theoretical Computer Science 124（2005）97113引用[1] A. Armando，D. Basin，M. Bouallagui，Y.谢瓦利埃湖康帕尼亚，S.他 是 我 的 朋 友 。我 不 知 道 ， M 。 图 鲁 阿 尼 湖 。 维 加 诺 湖 。 Vigneron ：TheAVISSecurityProtocol Analysis Tool，Proc. of 14th CAV，Copenhagen（Denmark），LNCS2404，pp.349-[2] F. Baader和T.Nipkow：Term Rewriting and All That，Cambridge University Press，1998.[3] Y. Chevalier和L. Vigneron：Automated Unbounded Verification of Security Protocols，Proc. of14th CAV，Copenhagen（Denmark），LNCS 2404，pp. 324-[4] H. Comon，M. 多谢河Gilleron，F. Jacquemard，D. 卢吉斯，S. Tison 和M.Tommasi：Tree Automata Techniques and Applications，2002。草案可从http://l3ux02.univ-lille3.fr/tata/获得。[5] T. Genet和F. Klay：Rewriting for Cryptographic Protocol Verification，Proc. of 17th CADE，Pittsburgh（PA），LNCS 1831，pp. 271-[6] T. Genet和V. Viet Triem Tong：Timbuk项重写系统的可达性分析，第8届LPAR会议论文集，哈瓦那（古巴），LNAI 2250，pp. 691-[7] H. Hosoya ，J. J. Pierillon和B.C. Pierce ：Regular Expression Types for XML，Proc. of 5thICFP，Montreal（Canada），SIGPLAN Notices 35（9），pp. 11[8] Y. Kaji ， T. Fujiwara 和 T. Kasami ： Solving a Uni fication Problem Under ConstrainedSubstitutions Using Tree Automata，Journal of Symbolic Computation 23，pp.79[9] Jos'eMeseguer：SoftwareSpecicat i cionanddVericationinRewritingLogic，Proc. oNATO高级研究所模型，代数和工程软件逻辑，计算机和系统科学191，pp。133[10] 阴号莫绍瓦基斯：《集合论笔记》，数学本科教材，施普林格出版社，1994年.[11] H. Ohsaki ， H. Seki 和 T. Takai ： Recognizing Boolean Closed A-Tree Languages withMembership Conditional Rewriting Mechanism ， Proc. of 14th RTA ， Valencia （ Spain ） ，LNCS 2706，pp. 483-[12] H. Ohsaki和T. Takai：Decidability and Closure Properties of Equational Tree Languages，Proc.of 13th RTA，Copenhagen（Denmark），LNCS 2378，pp. 114-[13] H. Ohsaki 和 T. Takai ： A Tree Automata Theory for Uni fication Modulo EquationalRewriting，Proc. of 16th UNIF，Copenhagen（Denmark），2002.草案可从http://staff.aist.go.jp/hitoshi.ohsaki/获得。[14] H. Ohsaki：Beyond Regularity：Equational Tree Automata for Associative and CommutativeTheories，Proc. of 15th CSL，Paris（France），LNCS 2142，pp. 539-[15] B. Schneier：Applied Cryptography：Protocols，Algorithms，and Source Code in C，SecondEdition，John Wiley Sons，1996。[16] T. Takai ， Y. Kaji 和 H. Seki ： Right-Linearly Path overlapping Term Rewriting Systems ECompetitive Preserve Recognizability，Proc. of 11th RTA，Norwich（UK），LNCS 1833，pp.246[17] T. Takai，H. Seki，Y. Fujinaka和Y. Kaji：Layered Transducing Term Rewriting Systemand Its Recognizability Preserving Property ， IEICE Transactions on Information andSystems E86-D（2），pp. 285 http://www.ieice.org/。