{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,30]],"date-time":"2025-07-30T15:40:24Z","timestamp":1753890024107,"version":"3.41.2"},"reference-count":1,"publisher":"Centre pour la Communication Scientifique Directe (CCSD)","license":[{"start":{"date-parts":[[2014,2,9]],"date-time":"2014-02-09T00:00:00Z","timestamp":1391904000000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/arxiv.org\/licenses\/nonexclusive-distrib\/1.0"}],"funder":[{"name":"National Science Foundation","award":["0905286"],"award-info":[{"award-number":["0905286"]}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"abstract":"<jats:p>We investigate unification problems related to the Cipher Block Chaining\n(CBC) mode of encryption. We first model chaining in terms of a simple,\nconvergent, rewrite system over a signature with two disjoint sorts: list and\nelement. By interpreting a particular symbol of this signature suitably, the\nrewrite system can model several practical situations of interest. An inference\nprocedure is presented for deciding the unification problem modulo this rewrite\nsystem. The procedure is modular in the following sense: any given problem is\nhandled by a system of `list-inferences', and the set of equations thus derived\nbetween the element-terms of the problem is then handed over to any\n(`black-box') procedure which is complete for solving these element-equations.\nAn example of application of this unification procedure is given, as attack\ndetection on a Needham-Schroeder like protocol, employing the CBC encryption\nmode based on the associative-commutative (AC) operator XOR. The 2-sorted\nconvergent rewrite system is then extended into one that fully captures a block\nchaining encryption-decryption mode at an abstract level, using no AC-symbols;\nand unification modulo this extended system is also shown to be decidable.<\/jats:p>","DOI":"10.2168\/lmcs-10(1:5)2014","type":"journal-article","created":{"date-parts":[[2014,7,15]],"date-time":"2014-07-15T09:40:14Z","timestamp":1405417214000},"source":"Crossref","is-referenced-by-count":1,"title":["Unification modulo a 2-sorted Equational theory for Cipher-Decipher Block Chaining"],"prefix":"10.46298","volume":"Volume 10, Issue 1","author":[{"given":"Siva","family":"Anantharaman","sequence":"first","affiliation":[]},{"given":"Christopher","family":"Bouchard","sequence":"additional","affiliation":[]},{"given":"Paliath","family":"Narendran","sequence":"additional","affiliation":[]},{"given":"Micha\u00ebl","family":"Rusinowitch","sequence":"additional","affiliation":[]}],"member":"25203","published-online":{"date-parts":[[2014,2,9]]},"reference":[{"key":"910:not-found"}],"container-title":["Logical Methods in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/lmcs.episciences.org\/808\/pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/lmcs.episciences.org\/808\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,4,11]],"date-time":"2023-04-11T19:56:34Z","timestamp":1681242994000},"score":1,"resource":{"primary":{"URL":"https:\/\/lmcs.episciences.org\/808"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,2,9]]},"references-count":1,"URL":"https:\/\/doi.org\/10.2168\/lmcs-10(1:5)2014","relation":{"is-same-as":[{"id-type":"arxiv","id":"1401.0445","asserted-by":"subject"},{"id-type":"doi","id":"10.48550\/arXiv.1401.0445","asserted-by":"subject"}]},"ISSN":["1860-5974"],"issn-type":[{"type":"electronic","value":"1860-5974"}],"subject":[],"published":{"date-parts":[[2014,2,9]]},"article-number":"808"}}