Formal Analysis of Symbolic Authenticity | SpringerLink
Skip to main content
Springer Nature Link
Log in

Formal Analysis of Symbolic Authenticity

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

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

Included in the following conference series:

Abstract

Authenticated encryption schemes are ways of encrypting messages which simultaneously assure the secrecy and authenticity of data. Designing authenticated encryption schemes can be error-prone. In this paper, we consider the authenticity of authenticated encryption schemes . We introduce the notion of symbolic authenticity, and present two inference systems for verifying symbolic authenticity. The first inference system works for authenticated encryption schemes for messages of fixed length. It is sound, complete and terminating. The second one works for authenticated encryption schemes for messages of arbitrary length. It is sound, terminating, and complete under some condition. These inference systems can be used to automatically synthesize authenticated encryption schemes.

The work is supported by NRL under contract N00173-19-1-G012.

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

Access this chapter

Log in via an institution

Subscribe and save

Springer+ Basic
¥17,985 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Chapter
JPY 3498
Price includes VAT (Japan)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
JPY 8579
Price includes VAT (Japan)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
JPY 10724
Price includes VAT (Japan)
  • 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

Similar content being viewed by others

References

  1. Akinyele, J.A., Green, M., Hohenberger, S.: Using SMT solvers to automate design tasks for encryption and signature schemes. In: Sadeghi, A.-R., Gligor, V.D., Yung, M. (eds.) 2013 ACM SIGSAC Conference on Computer and Communications Security (CCS 2013), Berlin, Germany, November 4–8 2013, pp. 399–410. ACM (2013)

    Google Scholar 

  2. Ambrona, M., Barthe, G., Schmidt, B.: Automated unbounded analysis of cryptographic constructions in the generic group model. In: Fischlin, M., Coron, J.-S. (eds.) EUROCRYPT 2016. LNCS, vol. 9666, pp. 822–851. Springer, Heidelberg (2016). https://doi.org/10.1007/978-3-662-49896-5_29

  3. Carmer, B., Rosulek, M.: Linicrypt: A model for practical cryptography. In: 36th Annual International Cryptology Conference, pp. 416–445 (2016)

    Google Scholar 

  4. Dworkin, M.: Recommendations for block cipher modes of operation: The CCM mode for authentication and confidentiality (2007)

    Google Scholar 

  5. Gligor, V.D., Donescu, P.: Fast encryption and authentication: XCBC encryption and XECB authentication modes. In: Matsui, M. (ed.) FSE 2001. LNCS, vol. 2355, pp. 92–108. Springer, Heidelberg (2002). https://doi.org/10.1007/3-540-45473-X_8

  6. Hoang, V.T., Katz, J., Malozemof, A.J.: Automated analysis and synthesis of authenticated encryption schemes. In: Proceedings of the 22nd ACM SIGSAC Conference on Computer and Communications Security, pp. 84–95 (2015)

    Google Scholar 

  7. Li, B., Micciancio, D.: Equational security proofs of oblivious transfer protocols. In: Abdalla, M., Dahab, R. (eds.) PKC 2018. LNCS, vol. 10769, pp. 527–553. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-76578-5_18

  8. Li, B., Micciancio, D.: Symbolic security of garbled circuits. In: 31st IEEE Computer Security Foundations Symposium (CSF 2018), Oxford, UK, July 9–12, 2018, pp. 147–161. IEEE Computer Society (2018)

    Google Scholar 

  9. Liskov, M., Rivest, R.L., Wagner, D.: Tweakable block ciphers. Adv. Cryptol.-Crypto 2002, 31–46 (2002)

    MathSciNet  MATH  Google Scholar 

  10. Malozemoff, A.J., Katz, J., Green, M.D.: Automated analysis and synthesis of block-cipher modes of operation. In: Computer Security Foundations Symposium (CSF), pp. 140–152 (2014)

    Google Scholar 

  11. Meadows, C.: Symbolic security criteria for blockwise adaptive secure modes of encryption. IACR Cryptol. ePrint Arch. 2020, 794 (2020)

    Google Scholar 

  12. Minematsu, K.: Parallelizable rate-1 authenticated encryption from pseudorandom functions. In: Nguyen, P.Q., Oswald, E. (eds.) EUROCRYPT 2014. LNCS, vol. 8441, pp. 275–292. Springer, Heidelberg (2014). https://doi.org/10.1007/978-3-642-55220-5_16

    Chapter  Google Scholar 

  13. Robinson, A., Voronkov. A.: Handbook of Automated Reasoning (2001)

    Google Scholar 

  14. Rogaway, P., Bellare, M., Black, J., Krovetz, T.: OCB: a block-cipher mode of operation for efficient authenticated encryption. In: 8th ACM Conference on Computer and Communications Security (CCS), pp. 196–205 (2001)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Clarkson University, Potsdam, NY, USA

    Hai Lin & Christopher Lynch

Authors
  1. Hai Lin
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Christopher Lynch
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Hai Lin .

Editor information

Editors and Affiliations

  1. University of Liverpool, Liverpool, UK

    Boris Konev

  2. The University of Manchester, Manchester, UK

    Giles Reger

Rights and permissions

Reprints and permissions

Copyright information

© 2021 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Lin, H., Lynch, C. (2021). Formal Analysis of Symbolic Authenticity. In: Konev, B., Reger, G. (eds) Frontiers of Combining Systems. FroCoS 2021. Lecture Notes in Computer Science(), vol 12941. Springer, Cham. https://doi.org/10.1007/978-3-030-86205-3_15

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-86205-3_15

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-86204-6

  • Online ISBN: 978-3-030-86205-3

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics