Efficient general AGH-unification. (English) Zbl 1360.94321
Summary: General \(E\)-unification is an important tool in cryptographic protocol analysis, where the equational theory \(E\) represents properties of the cryptographic algorithm, and uninterpreted function symbols represent other functions. The property of a homomorphism over an abelian group is common in encryption algorithms such as RSA. The general \(E\)-unification problem in this theory is NP-complete, and existing algorithms are highly nondeterministic. We give a mostly deterministic set of inference rules for solving general \(E\)-unification modulo a homomorphism over an abelian group, and prove that it is sound, complete and terminating. These inference rules have been implemented in Maude, and will be incorporated into the Maude-NRL Protocol Analyzer (Maude-NPA).
References:
| [1] | Meadows, C., Formal verification of cryptographic protocols: a survey, (Pieprzyk, J.; Safavi-Naini, R., ASIACRYPT. ASIACRYPT, Lect. Notes Comput. Sci., vol. 917 (1994), Springer), 135-150 · Zbl 0872.94035 |
| [2] | Escobar, S.; Meadows, C.; Meseguer, J., Maude-NPA: cryptographic protocol analysis modulo equational properties, (Aldini, A.; Barthe, G.; Gorrieri, R., FOSAD. FOSAD, Lect. Notes Comput. Sci., vol. 5705 (2007), Springer), 1-50 · Zbl 1252.94061 |
| [3] | Ryan, P. Y.A.; Bismark, D.; Heather, J.; Schneider, S.; Xia, Z., Prêt à voter: a voter-verifiable voting system, IEEE Trans. Inf. Forensics Secur., 4, 4, 662-673 (2009) |
| [4] | Kremer, S.; Ryan, M.; Smyth, B., Election verifiability in electronic voting protocols, (Gritzalis, D.; Preneel, B.; Theoharidou, M., ESORICS. ESORICS, Lect. Notes Comput. Sci., vol. 6345 (2010), Springer), 389-404 |
| [5] | Lankford, D.; Butler, G.; Brady, B., Abelian group unification algorithms for elementary terms, Contemp. Math., 29, 193-199 (1984) · Zbl 0555.68065 |
| [6] | Guo, Q.; Narendran, P.; Wolfram, D. A., Unification and matching modulo nilpotence, (McRobbie, M. A.; Slaney, J. K., Proceedings of the 13th International Conference on Automated Deduction on Automated Deduction. Proceedings of the 13th International Conference on Automated Deduction on Automated Deduction, New Brunswick, NJ, USA, CADE-13, July 30-August 3, 1996. Proceedings of the 13th International Conference on Automated Deduction on Automated Deduction. Proceedings of the 13th International Conference on Automated Deduction on Automated Deduction, New Brunswick, NJ, USA, CADE-13, July 30-August 3, 1996, Lect. Notes Comput. Sci., vol. 1104 (1996), Springer: Springer Berlin), 261-274 · Zbl 1412.68229 |
| [7] | Schulz, K. U., A criterion for intractability of \(E\)-unification with free function symbols and its relevance for combination algorithms, (Comon, H., RTA. RTA, Lect. Notes Comput. Sci., vol. 1232 (1997), Springer), 284-298 · Zbl 1379.68205 |
| [8] | Hermann, M.; Kolaitis, P. G., Unification algorithms cannot be combined in polynomial time, (McRobbie, M. A.; Slaney, J. K., Proceedings of the 13th International Conference on Automated Deduction on Automated Deduction. Proceedings of the 13th International Conference on Automated Deduction on Automated Deduction, New Brunswick, NJ, USA, CADE-13, July 30-August 3, 1996. Proceedings of the 13th International Conference on Automated Deduction on Automated Deduction. Proceedings of the 13th International Conference on Automated Deduction on Automated Deduction, New Brunswick, NJ, USA, CADE-13, July 30-August 3, 1996, Lect. Notes Comput. Sci., vol. 1104 (1996), Springer: Springer Berlin), 246-260 · Zbl 1412.68233 |
| [9] | Baader, F., Unification in commutative theories, J. Symb. Comput., 8, 5, 479-497 (1989) · Zbl 0689.68039 |
| [10] | Nutt, W., Unification in monoidal theories, (Stickel, M. E., CADE. CADE, Lect. Notes Comput. Sci., vol. 449 (1990), Springer), 618-632 · Zbl 1509.03045 |
| [11] | Schmidt-Schauß, M., Unification in a combination of arbitrary disjoint equational theories, J. Symb. Comput., 8, 1/2, 51-99 (1989) · Zbl 0691.03003 |
| [12] | Boudet, A.; Jouannaud, J.-P.; Schmidt-Schauß, M., Unification in Boolean rings and abelian groups, J. Symb. Comput., 8, 5, 449-477 (1989) · Zbl 0689.68040 |
| [13] | Dershowitz, N.; Plaisted, D. A., Rewriting, (Robinson, J. A.; Voronkov, A., Handbook of Automated Reasoning (in 2 volumes) (2001), Elsevier and MIT Press), 535-610, ISBN 0-444-50813-9, ISBN 0-262-18223-8 · Zbl 0992.68123 |
| [14] | (Clavel, M.; Durán, F.; Eker, S.; Lincoln, P.; Martí-Oliet, N.; Meseguer, J.; Talcott, C. L., All About Maude - A High-Performance Logical Framework, How to Specify, Program and Verify Systems in Rewriting Logic. All About Maude - A High-Performance Logical Framework, How to Specify, Program and Verify Systems in Rewriting Logic, Lect. Notes Comput. Sci., vol. 4350 (2007), Springer: Springer Berlin) · Zbl 1115.68046 |
| [15] | Liu, Z.; Lynch, C., Efficient general unification for XOR with homomorphism, (Bjørner, N.; Sofronie-Stokkermans, V., CADE. CADE, Lect. Notes Comput. Sci., vol. 6803 (2011), Springer), 407-421 · Zbl 1341.68195 |
| [16] | Baader, F.; Snyder, W., Unification theory, (Robinson, J. A.; Voronkov, A., Handbook of Automated Reasoning (in 2 volumes) (2001), Elsevier and MIT Press), 535-610, ISBN 0-444-50813-9, ISBN 0-262-18223-8 · Zbl 0964.00020 |
| [17] | Knuth, D., The Art of Computer Programming, vol. 2 (2004), Addison-Wesley |
| [18] | Maude: |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
