Protocol analysis in Maude-NPA using unification modulo homomorphic encryption

Santiago Escobar, Deepak Kapur, Christopher Lynch, Catherine Meadows, José Meseguer, Paliath Narendran, Ralf Sasse

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

A number of new cryptographic protocols are being designed to secure applications such as video-conferencing and electronic voting. Many of them rely upon cryptographic functions with complex algebraic properties that must be accounted for in order to be correctly analyzed by automated tools. Maude-NPA is a cryptographic protocol analysis tool based on narrowing and typed equational unification which takes into account these algebraic properties. It has already been used to analyze protocols involving bounded associativity, modular exponentiation, and exclusive-or. All of the above can be handled by the same general variant-based equational unification technique. However, there are important properties, in particular homomorphic encryption, that cannot be handled by variantbased unification in the same way. In these cases the best available approach is to implement specialized unification algorithms and combine them within a modular framework. In this paper we describe how we apply this approach within Maude-NPA, with respect to encryption homomorphic over a free operator. We also describe the use of Maude-NPA to analyze several protocols using such an encryption operation. To the best of our knowledge, this is the first implementation of homomorphic encryption of any sort in a tool for verifying the security of a protocol in the presence of active attackers.

Original languageEnglish (US)
Title of host publicationPPDP'11 - Proceedings of the 2011 Symposium on Principles and Practices of Declarative Programming
Pages65-76
Number of pages12
DOIs
StatePublished - Sep 2 2011
Event13th International ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming, PPDP 2011 - Odense, Denmark
Duration: Jul 20 2011Jul 22 2011

Publication series

NamePPDP'11 - Proceedings of the 2011 Symposium on Principles and Practices of Declarative Programming

Other

Other13th International ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming, PPDP 2011
CountryDenmark
CityOdense
Period7/20/117/22/11

Keywords

  • Homomorphism
  • Protocol verification
  • Unification

ASJC Scopus subject areas

  • Computational Theory and Mathematics
  • Applied Mathematics

Fingerprint Dive into the research topics of 'Protocol analysis in Maude-NPA using unification modulo homomorphic encryption'. Together they form a unique fingerprint.

Cite this