research-article

Cap unification: application to protocol security modulo homomorphic encryption

Authors:

Siva Anantharaman,

Christopher Lynch,

Paliath Narendran,

Michael RusinowitchAuthors Info & Claims

ASIACCS '10: Proceedings of the 5th ACM Symposium on Information, Computer and Communications Security

Pages 192 - 203

https://doi.org/10.1145/1755688.1755713

Published: 13 April 2010 Publication History

Abstract

We address the insecurity problem for cryptographic protocols, for an active intruder and a bounded number of sessions. The protocol steps are modeled as rigid Horn clauses, and the intruder abilities as an equational theory. The problem of active intrusion -- such as whether a secret term can be derived, possibly via interaction with the honest participants of the protocol -- is then formulated as a Cap Unification problem. Cap Unification is an extension of Equational Unification: look for a cap to be placed on a given set of terms, so as to unify it with a given term modulo the equational theory. We give a decision procedure for Cap Unification, when the intruder capabilities are modeled as homomorphic encryption theory. Our procedure can be employed in a simple manner to detect attacks exploiting some properties of block ciphers.

References

[1]

S. Anantharaman, P. Narendran, M. Rusinowitch. "Intruders with Caps". In Proc. of Int. Conf. RTA'07, LNCS 4533, pp. 20--35, Springer-Verlag, June 2007.

Digital Library

[2]

S. Anantharaman, H. Lin, C. Lynch, P. Narendran, M. Rusinowitch. "Unification modulo Homomorphic Encryption". In Proc. of Int. Conf. FROCOS 2009, TRENTO-Italy, LNAI 5749, pp. 100--116, Springer-Verlag, September 2009.

Digital Library

[3]

A. Armando, L. Compagna. "SATMC: A SAT-based Model Checker for Security Protocols". In Proc. of JELIA 2004, LNCS 3229, pp. 730--733, Springer-Verlag, 2004.

[4]

D. Basin, S. Mödersheim, L. Viganó. "An On-The-Fly Model-Checker for Security Protocol Analysis". In Proc. of ESORICS'03, LNCS 2808, pp. 253--270. Springer-Verlag, 2003.

[5]

M. Baudet. "Deciding security of protocols against off-line guessing attacks". In Proc. of ACM Conf. on Computer and Communications Security, pp. 16--25, 2005.

Digital Library

[6]

Y. Chevalier, M. Kourjieh. "Key Substitution in the Symbolic Analysis of Cryptographic Protocols". In Proc. Int. Conf FSTTCS'07, LNCS 4855, pp. 121--132, Springer-Verlag, December 2007.

Digital Library

[7]

Y. Chevalier, R. Küsters, M. Rusinowitch, M. Turuani. "An NP Decision Procedure for Protocol Insecurity with XOR". In Proc. of the Logic In Computer Science Conference, LICS'03, pp. 261--270, 2003.

Digital Library

[8]

H. Comon-Lundh, R. Treinen. "Easy Intruder Deductions." Verification: Theory and Practice In LNCS 2772, pp. 225--242, Springer-Verlag, February 2004.

[9]

V. Cortier, S. Delaune, P. Lafourcade. "A Survey of Algebraic Properties Used in Cryptographic Protocols". In Journal of Computer Security 14(1): 1--43, 2006.

Digital Library

[10]

V. Cortier, M. Rusinowitch, E. Zalinescu. "A resolution strategy for verifying cryptographic protocols with CBC encryption and blind signatures". In Proc. of the 7th ACM SIGPLAN Symposium PPDP 2005, pp. 12--22.

Digital Library

[11]

S. Delaune, F. Jacquemard. "A decision procedure for the verification of security protocols with explicit destructors". In Proc. of the 11th ACM Conference on Computer and Communications Security (CCS'04), pp. 278--287, Washington, D.C., USA, October 2004. ACM Press.

Digital Library

[12]

S. Delaune, P. Lafourcade, D. Lugiez, R. Treinen, "Symbolic protocol analysis for monoidal equational theories." In Information and Computation 206(2--4), pp. 312--351, 2008.

Digital Library

[13]

S. Escobar, C. Meadows, J. Meseguer. "A Rewriting-Based Inference System for the NRL Protocol Analyzer and its Meta-Logical Properties." In Theoretical Computer Science, Vol. 367(1--2), pp. 162--202, 2006.

Digital Library

[14]

F. J.-T. Fabrega, J. C. Herzog, J. D. Guttman. "Strand Spaces: Why is a Security Protocol Correct?" In Proc. of IEEE Symposium on Security and Privacy, May 1998.

[15]

J. M. Hullot. "Canonical Forms and Unification". In Proc. of the Int. Conf. on Automated Deduction CADE-5, LNCS 87, pp. 318--334, Springer-Verlag, 1980.

Digital Library

[16]

S. Kremer, M. D. Ryan. "Analysing the vulnerability of protocols to produce known-pair and chosen-text attacks". In Proc. of the 2nd Int. Workshop on Security Issues in Coordination Models, Languages, and Systems (SecCo 2004), ENTCS, Vol. 128, Issue 5, pp. 87--104, 2004.

Digital Library

[17]

C. Meadows, P. Narendran. "A unification algorithm for the group Diffie-Hellman protocol". In Workshop on Issues in the Theory of Security (in conjunction with POPL'02), Portland, Oregon, USA, January 14--15, 2002.

[18]

J. Millen, V. Shmatikov. "Constraint Solving for Bounded-Process Cryptographic Protocol Analysis" In Proc. of the 8th ACM Conference on Computer and Communications Security pp. 166--175, 2001.

Digital Library

[19]

E. Tiden, S. Arnborg. "Unification Problems with One-sided Distributivity". In J. of Symb. Computation 3(1--2): 183--202, 1987.

Digital Library

[20]

C. Weidenbach. "Towards an automatic analysis of security protocols". In Proc. of the 16th Int. Conf. on Automated Deduction, CADE-16, LNAI 1632, pp. 378--382, Springer-Verlag, 1999.

Digital Library

Cited By

Cai LCai GLu SLi GWang Y(2024)Observational Equivalence and Security Games: Enhancing the Formal Analysis of Security ProtocolsComputers & Security10.1016/j.cose.2024.103785(103785)Online publication date: Feb-2024
https://doi.org/10.1016/j.cose.2024.103785
Lin HLynch C(2022)Local XOR Unification: Definitions, Algorithms and Application to CryptographyTheoretical Aspects of Computing – ICTAC 202210.1007/978-3-031-17715-6_18(272-289)Online publication date: 3-Oct-2022
https://doi.org/10.1007/978-3-031-17715-6_18
Eeralla ALynch C(2020)Bounded ACh unificationMathematical Structures in Computer Science10.1017/S0960129520000183(1-19)Online publication date: 16-Sep-2020
https://doi.org/10.1017/S0960129520000183
Show More Cited By

Index Terms

Cap unification: application to protocol security modulo homomorphic encryption
1. Computing methodologies

Recommendations

Unification Modulo Homomorphic Encryption

Encryption `distributing over pairs' is a technique employed in several cryptographic protocols. We show that unification is decidable for an equational theory HE specifying such an encryption. The method consists in transforming any given problem in ...
Decidability of bounded second order unification

It is well-known that first order unification is decidable, whereas second order (and higher order) unification is undecidable. Bounded second order unification is second order unification under the restriction that only a bounded number of bound ...
Undecidability of the unification and admissibility problems for modal and description logics

We show that the unification problem “is there a substitution instance of a given formula that is provable in a given logic?” is undecidable for basic modal logics K and K4 extended with the universal modality. It follows that the admissibility problem ...

Comments

Information & Contributors

Information

Published In

cover image ACM Conferences

ASIACCS '10: Proceedings of the 5th ACM Symposium on Information, Computer and Communications Security

April 2010

363 pages

ISBN:9781605589367

DOI:10.1145/1755688

General Chair:
Dengguo Feng
Chinese Academy of Sciences, China
,
Program Chairs:
David Basin
ETH Zurich, Switzerland
,
Peng Liu
Pennsylvania State University

Copyright © 2010 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Sponsors

SIGSAC: ACM Special Interest Group on Security, Audit, and Control

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 13 April 2010

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Funding Sources

Conference

ASIA CCS '10

Sponsor:

SIGSAC

ASIA CCS '10: 5th ACM Symposium on Information, Computer and Communications Security

April 13 - 16, 2010

Beijing, China

Acceptance Rates

ASIACCS '10 Paper Acceptance Rate 25 of 166 submissions, 15%;

Overall Acceptance Rate 418 of 2,322 submissions, 18%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

9
Total Citations
View Citations
236
Total Downloads

Downloads (Last 12 months)7
Downloads (Last 6 weeks)0

Reflects downloads up to 14 Sep 2024

Other Metrics

View Author Metrics

Citations

Cited By

Cai LCai GLu SLi GWang Y(2024)Observational Equivalence and Security Games: Enhancing the Formal Analysis of Security ProtocolsComputers & Security10.1016/j.cose.2024.103785(103785)Online publication date: Feb-2024
https://doi.org/10.1016/j.cose.2024.103785
Lin HLynch C(2022)Local XOR Unification: Definitions, Algorithms and Application to CryptographyTheoretical Aspects of Computing – ICTAC 202210.1007/978-3-031-17715-6_18(272-289)Online publication date: 3-Oct-2022
https://doi.org/10.1007/978-3-031-17715-6_18
Eeralla ALynch C(2020)Bounded ACh unificationMathematical Structures in Computer Science10.1017/S0960129520000183(1-19)Online publication date: 16-Sep-2020
https://doi.org/10.1017/S0960129520000183
Hanna ELynch CMyers DRichardson C(2019)Finding Intruder Knowledge with Cap-MatchingFoundations of Security, Protocols, and Equational Reasoning10.1007/978-3-030-19052-1_5(39-53)Online publication date: 28-Apr-2019
https://doi.org/10.1007/978-3-030-19052-1_5
Anantharaman SLin HLynch CNarendran PRusinowitch M(2018)Unification Modulo Homomorphic EncryptionJournal of Automated Reasoning10.1007/s10817-010-9205-y48:2(135-158)Online publication date: 28-Dec-2018
https://dl.acm.org/doi/10.1007/s10817-010-9205-y
Yang FEscobar SMeadows CMeseguer JNarendran PChitil OKing ADanvy O(2014)Theories of Homomorphic Encryption, Unification, and the Finite Variant PropertyProceedings of the 16th International Symposium on Principles and Practice of Declarative Programming10.1145/2643135.2643154(123-133)Online publication date: 8-Sep-2014
https://dl.acm.org/doi/10.1145/2643135.2643154
Anantharaman SBouchard CNarendran PRusinowitch M(2012)Unification modulo chainingProceedings of the 6th international conference on Language and Automata Theory and Applications10.1007/978-3-642-28332-1_7(70-82)Online publication date: 5-Mar-2012
https://dl.acm.org/doi/10.1007/978-3-642-28332-1_7
Escobar SKapur DLynch CMeadows CMeseguer JNarendran PSasse RSchneider-Kamp PHanus M(2011)Protocol analysis in Maude-NPA using unification modulo homomorphic encryptionProceedings of the 13th international ACM SIGPLAN symposium on Principles and practices of declarative programming10.1145/2003476.2003488(65-76)Online publication date: 20-Jul-2011
https://dl.acm.org/doi/10.1145/2003476.2003488
Narendran PMarshall AMahapatra B(2010)On the Complexity of the Tiden-Arnborg Algorithm for Unification modulo One-Sided DistributivityElectronic Proceedings in Theoretical Computer Science10.4204/EPTCS.42.542(54-63)Online publication date: 21-Dec-2010
https://doi.org/10.4204/EPTCS.42.5

View Options

Get Access

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Table of Contents