TY - GEN
T1 - Theories of homomorphic encryption, unification, and the finite variant property
AU - Yang, Fan
AU - Escobar, Santiago
AU - Meadows, Catherine
AU - Meseguer, José
AU - Narendran, Paliath
N1 - Publisher Copyright:
© Copyright 2014 ACM.
PY - 2014/9/8
Y1 - 2014/9/8
N2 - Recent advances in the automated analysis of cryptographic protocols have aroused new interest in the practical application of unification modulo theories, especially theories that describe the algebraic properties of cryptosystems. However, this application requires unification algorithms that can be easily implemented and easily extended to combinations of different theories of interest. In practice this has meant that most tools use a version of a technique known as variant unification. This requires, among other things, that the theory be decomposable into a set of axioms B and a set of rewrite rules R such that R has the finite variant property with respect to B. Most theories that arise in cryptographic protocols have decompositions suitable for variant unification, but there is one major exception: the theory that describes encryption that is homomorphic over an Abelian group. In this paper we address this problem by studying various approximations of homomorphic encryption over an Abelian group. We construct a hierarchy of increasingly richer theories, taking advantage of new results that allow us to automatically verify that their decompositions have the finite variant property. This new verification procedure also allows us to construct a rough metric of the complexity of a theory with respect to variant unification, or variant complexity. We specify different versions of protocols using the different theories, and analyze them in the Maude-NPA cryptographic protocol analysis tool to assess their behavior. This gives us greater understanding of how the theories behave in actual application, and suggests possible techniques for improving performance.
AB - Recent advances in the automated analysis of cryptographic protocols have aroused new interest in the practical application of unification modulo theories, especially theories that describe the algebraic properties of cryptosystems. However, this application requires unification algorithms that can be easily implemented and easily extended to combinations of different theories of interest. In practice this has meant that most tools use a version of a technique known as variant unification. This requires, among other things, that the theory be decomposable into a set of axioms B and a set of rewrite rules R such that R has the finite variant property with respect to B. Most theories that arise in cryptographic protocols have decompositions suitable for variant unification, but there is one major exception: the theory that describes encryption that is homomorphic over an Abelian group. In this paper we address this problem by studying various approximations of homomorphic encryption over an Abelian group. We construct a hierarchy of increasingly richer theories, taking advantage of new results that allow us to automatically verify that their decompositions have the finite variant property. This new verification procedure also allows us to construct a rough metric of the complexity of a theory with respect to variant unification, or variant complexity. We specify different versions of protocols using the different theories, and analyze them in the Maude-NPA cryptographic protocol analysis tool to assess their behavior. This gives us greater understanding of how the theories behave in actual application, and suggests possible techniques for improving performance.
KW - Cryptographic protocol analysis
KW - Finite variant property
KW - Homomorphic encryption
KW - Unification
UR - http://www.scopus.com/inward/record.url?scp=84968782920&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=84968782920&partnerID=8YFLogxK
U2 - 10.1145/2643135.2643154
DO - 10.1145/2643135.2643154
M3 - Conference contribution
AN - SCOPUS:84968782920
T3 - PPDP 2014 - Proceedings of the 16th International Symposium on Principles and Practice of Declarative Programming
SP - 123
EP - 134
BT - PPDP 2014 - Proceedings of the 16th International Symposium on Principles and Practice of Declarative Programming
PB - Association for Computing Machinery
T2 - 16th International Symposium on Principles and Practice of Declarative Programming, PPDP 2014
Y2 - 8 September 2014 through 10 September 2014
ER -