密码-解密分组链的模2-排序统一方程理论
Unification modulo a 2-sorted Equational theory for Cipher-Decipher Block Chaining
摘要：
我们调查的统一问题有关的密码块链（CBC）模式的加密。我们首先在一个简单的，收敛的，重写系统的签名与两个不相交的排序：列表和元素的链接模型。通过适当地解释该签名的特定符号，重写系统可以对感兴趣的几种实际情况进行建模。一个推理过程，提出了决定这个重写系统的统一问题模。这个过程在以下意义上是模块化的：任何给定的问题都由一个“列表推理”系统处理，因此在问题的元素项之间导出的方程组然后交给任何（“黑盒”）过程，该过程对于求解这些元素方程是完整的。该统一过程的应用的一个例子，作为攻击检测的Needham-Schroeder类协议，采用CBC加密模式的基础上的关联交换（AC）操作XOR。2排序的收敛重写系统，然后扩展到一个完全捕获块链接的解密模式在一个抽象的水平，不使用AC符号;和统一模这个扩展系统也被证明是可判定的。
英文摘要：
We investigate unification problems related to the Cipher Block Chaining (CBC) mode of encryption. We first model chaining in terms of a simple, convergent, rewrite system over a signature with two disjoint sorts: list and element. By interpreting a particular symbol of this signature suitably, the rewrite system can model several practical situations of interest. An inference procedure is presented for deciding the unification problem modulo this rewrite system. The procedure is modular in the following sense: any given problem is handled by a system of `list-inferences', and the set of equations thus derived between the element-terms of the problem is then handed over to any (`black-box') procedure which is complete for solving these element-equations. An example of application of this unification procedure is given, as attack detection on a Needham-Schroeder like protocol, employing the CBC encryption mode based on the associative-commutative (AC) operator XOR. The 2-sorted convergent rewrite system is then extended into one that fully captures a block chaining encryption-decryption mode at an abstract level, using no AC-symbols; and unification modulo this extended system is also shown to be decidable.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
