Skip to main content
SpringerLink
Log in

On Asymmetric Unification for the Theory of XOR with a Homomorphism

  • Conference paper
  • First Online:
Frontiers of Combining Systems (FroCoS 2019)

Part of the book series: Lecture Notes in Computer Science ((LNAI,volume 11715))

Included in the following conference series:

  • 306 Accesses

Abstract

Asymmetric unification, or unification with irreducibility constraints, is a newly developed paradigm that arose out of the automated analysis of cryptographic protocols. However, there are still relatively few asymmetric unification algorithms. In this paper we address this lack by exploring the application of automata-based unification methods. We examine the theory of xor with a homomorphism, ACUNh, from the point of view of asymmetric unification, and develop a new automata-based decision procedure. Then, we adapt a recently developed asymmetric combination procedure to produce a general asymmetric-ACUNh decision procedure. Finally, we present a new approach for obtaining a solution-generating asymmetric-ACUNh unification automaton. We also compare our approach to the most commonly used form of asymmetric unification available today, variant unification.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 54.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 69.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Notes

  1. 1.

    This is the background theory.

  2. 2.

    The linear constant restrictions in Sect. 5 can also be handled this way: a constant restriction of the form \(a \; \not \in \; X\) can be taken care of by setting \(\mathsf {X^a} = 0\).

References

  1. Baader, F., Snyder, W.: Unification theory. Handb. Autom. Reasoning 1, 445–532 (2001)

    Article  Google Scholar 

  2. Büchi, J.R.: Weak second-order arithmetic and finite automata. Math. Logic Quart. 6(1–6), 66–92 (1960)

    Article  MathSciNet  Google Scholar 

  3. Chaum, D.: Blind signature system. In: Chaum, D. (ed.) Advances in Cryptology, p. 153. Springer, Boston (1984). https://doi.org/10.1007/978-1-4684-4730-9_14

    Chapter  Google Scholar 

  4. Comon-Lundh, H., Delaune, S.: The finite variant property: how to get rid of some algebraic properties. In: Giesl, J. (ed.) RTA 2005. LNCS, vol. 3467, pp. 294–307. Springer, Heidelberg (2005). https://doi.org/10.1007/978-3-540-32033-3_22

    Chapter  Google Scholar 

  5. Elgot, C.C.: Decision problems of finite automata design and related arithmetics. Trans. Am. Math. Soc. 98(1), 21–51 (1961)

    Article  MathSciNet  Google Scholar 

  6. Erbatur, S., et al.: Asymmetric unification: a new unification paradigm for cryptographic protocol analysis. In: Bonacina, M.P. (ed.) CADE 2013. LNCS (LNAI), vol. 7898, pp. 231–248. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-38574-2_16

    Chapter  Google Scholar 

  7. Erbatur, S., Kapur, D., Marshall, A.M., Meadows, C., Narendran, P., Ringeissen, C.: On asymmetric unification and the combination problem in disjoint theories. In: Muscholl, A. (ed.) FoSSaCS 2014. LNCS, vol. 8412, pp. 274–288. Springer, Heidelberg (2014). https://doi.org/10.1007/978-3-642-54830-7_18

    Chapter  MATH  Google Scholar 

  8. Escobar, S., Meseguer, J., Sasse, R.: Variant narrowing and equational unification. Electr. Notes Theor. Comput. Sci. 238(3), 103–119 (2009)

    Article  Google Scholar 

  9. Klaedtke, F., Ruess, H.: Parikh automata and monadic second-order logics with linear cardinality constraints, Technical report 177, Universität Freiburg (2002)

    Google Scholar 

  10. Lynch, C., Marshall, A.M., Meadows, C.A., Narendran, P., Ravishankar, V.: On asymmetric unification for the theory of xor with a homomorphism. Technical report, Clarkson University, University of Mary Washington, Naval Research Laboratory, University at Albany-SUNY (2019). https://www.marshallandrew.net/ach-asymmetric.pdf

  11. Narendran, P.: Solving linear equations over polynomial semirings. In: Proceedings, 11th Annual IEEE Symposium on Logic in Computer Science, New Brunswick, New Jersey, USA, 27–30 July 1996, pp. 466–472. IEEE Computer Society (1996)

    Google Scholar 

  12. Paillier, P.: Public-key cryptosystems based on composite degree residuosity classes. In: Stern, J. (ed.) EUROCRYPT 1999. LNCS, vol. 1592, pp. 223–238. Springer, Heidelberg (1999). https://doi.org/10.1007/3-540-48910-X_16

    Chapter  Google Scholar 

  13. Rivest, R.L., Shamir, A., Adleman, L.M.: A method for obtaining digital signatures and public-key cryptosystems. Commun. ACM 21(2), 120–126 (1978)

    Article  MathSciNet  Google Scholar 

  14. Vardi, M.Y., Wilke, T.: Automata: from logics to algorithms. Logic Automata 2, 629–736 (2008)

    MathSciNet  MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Clarkson University, Potsdam, NY, USA

    Christopher Lynch

  2. University of Mary Washington, Fredericksburg, VA, USA

    Andrew M. Marshall & Veena Ravishankar

  3. Naval Research Laboratory, Washington, D.C., USA

    Catherine Meadows

  4. University at Albany-SUNY, Albany, NY, USA

    Paliath Narendran

Authors
  1. Christopher Lynch
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Andrew M. Marshall
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Catherine Meadows
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Paliath Narendran
    View author publications

    You can also search for this author in PubMed Google Scholar

  5. Veena Ravishankar
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Veena Ravishankar .

Editor information

Editors and Affiliations

  1. CNRS, University of Toulouse, Toulouse, France

    Andreas Herzig

  2. Middlesex University London, London, UK

    Andrei Popescu

Rights and permissions

Reprints and permissions

Copyright information

© 2019 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Lynch, C., Marshall, A.M., Meadows, C., Narendran, P., Ravishankar, V. (2019). On Asymmetric Unification for the Theory of XOR with a Homomorphism. In: Herzig, A., Popescu, A. (eds) Frontiers of Combining Systems. FroCoS 2019. Lecture Notes in Computer Science(), vol 11715. Springer, Cham. https://doi.org/10.1007/978-3-030-29007-8_17

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-29007-8_17

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-29006-1

  • Online ISBN: 978-3-030-29007-8

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation