More Web Proxy on the site http://driver.im/

Article

Combining intruder theories

Authors:

Yannick Chevalier,

Michaël RusinowitchAuthors Info & Claims

ICALP'05: Proceedings of the 32nd international conference on Automata, Languages and Programming

Pages 639 - 651

https://doi.org/10.1007/11523468_52

Published: 11 July 2005 Publication History

Abstract

Most of the decision procedures for symbolic analysis of protocols are limited to a fixed set of algebraic operators associated with a fixed intruder theory. Examples of such sets of operators comprise XOR, multiplication/exponentiation, abstract encryption/decryption. In this paper we give an algorithm for combining decision procedures for arbitrary intruder theories with disjoint sets of operators, provided that solvability of ordered intruder constraints, a slight generalization of intruder constraints, can be decided in each theory. This is the case for most of the intruder theories for which a decision procedure has been given. In particular our result allows us to decide trace-based security properties of protocols that employ any combination of the above mentioned operators with a bounded number of sessions.

References

[1]

M. Abadi, B. Blanchet, and C. Fournet. Just Fast Keying in the Pi Calculus. In David Schmidt, editor, Proceedings of ESOP'04, volume 2986 of Lecture Notes on Computer Science, pages 340-354, Barcelona, Spain, 2004. Springer Verlag.

[2]

R. Amadio, D. Lugiez, and V. Vanackère. On the symbolic reduction of processes with cryptographic functions. Theor. Comput. Sci., 290(1):695-740, 2003.

Digital Library

[3]

F. Baader and K. U. Schulz. Unification in the union of disjoint equational theories. combining decision procedures. J. Symb. Comput., 21(2):211-243, 1996.

Digital Library

[4]

D. Basin, S. Mödersheim, and L. Viganò. An On-The-Fly Model-Checker for Security Protocol Analysis. In Einar Snekkenes and Dieter Gollmann, editors, Proceedings of ESORICS'03, LNCS 2808, pages 253-270. Springer-Verlag, 2003.

[5]

M. Boreale. Symbolic trace analysis of cryptographic protocols. In Proceedings of the 28th ICALP'01, LNCS 2076, pages 667-681. Springer-Verlag, Berlin, 2001.

Digital Library

[6]

M. Boreale and M. Buscemi. Symbolic analysis of crypto-protocols based on modular exponentiation. In Proceedings of MFCS 2003, volume 2747 of Lecture Notes in Computer Science. Springer, 2003.

[7]

N. Borisov, I. Goldberg, and D. Wagner. Intercepting mobile communications: the insecurity of 802.11. In Proceedings of MOBICOM 2001, pages 180-189, 2001.

Digital Library

[8]

Y. Chevalier, R. Kuesters, M. Rusinowitch, and M. Turuani. An NP Decision Procedure for Protocol Insecurity with XOR. In Proceedings of the Logic In Computer Science Conference, LICS'03, June 2003.

Digital Library

[9]

Y. Chevalier and M. Rusinowitch. Combining intruder theories. Technical report, INRIA, 2005. http://www.inria.fr/rrrt/rr-5495.html.

[10]

Y. Chevalier and L. Vigneron. A Tool for Lazy Verification of Security Protocols. In Proceedings of the Automated Software Engineering Conference (ASE'01). IEEE Computer Society Press, 2001.

Digital Library

[11]

H. Comon-Lundh and V. Shmatikov. Intruder Deductions, Constraint Solving and Insecurity Decision in Presence of Exclusive or. In Proceedings of the Logic In Computer Science Conference, LICS'03, pages 271-280, 2003.

Digital Library

[12]

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

Digital Library

[13]

N. Dershowitz and J-P. Jouannaud. Rewrite systems. In Handbook of Theoretical Computer Science, Volume B, pages 243-320. Elsevier, 1990.

Digital Library

[14]

J. Hsiang and M. Rusinowitch. On word problems in equational theories. In ICALP, volume 267 of Lecture Notes in Computer Science, pages 54-71. Springer, 1987.

Digital Library

[15]

C. Meadows and 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.

[16]

J. Millen and V. Shmatikov. Constraint solving for bounded-process cryptographic protocol analysis. In ACM Conference on Computer and Communications Security, pages 166-175, 2001.

Digital Library

[17]

J. Millen and V. Shmatikov. Symbolic protocol analysis with an abelian group operator or Diffie-Hellman exponentiation. Journal of Computer Security, 2005.

Digital Library

[18]

M. Rusinowitch and M. Turuani. Protocol insecurity with finite number of sessions is NP-complete. In Proceedings of CSFW 2001. IEEE, 2001.

Digital Library

[19]

M. Schmidt-Schauß. Unification in a combination of arbitrary disjoint equational theories. J. Symb. Comput., 8(1/2):51-99, 1989.

Digital Library

Cited By

Avanesov TChevalier YRusinowitch MTuruani M(2017)Satisfiability of general intruder constraints with and without a set constructorJournal of Symbolic Computation10.1016/j.jsc.2016.07.00980:P1(27-61)Online publication date: 1-May-2017
https://dl.acm.org/doi/10.1016/j.jsc.2016.07.009
Delaune SLafourcade PLugiez DTreinen R(2008)Symbolic protocol analysis for monoidal equational theoriesInformation and Computation10.1016/j.ic.2007.07.005206:2-4(312-351)Online publication date: 1-Feb-2008
https://dl.acm.org/doi/10.1016/j.ic.2007.07.005
Chevalier YRusinowitch M(2008)Hierarchical combination of intruder theoriesInformation and Computation10.1016/j.ic.2007.07.004206:2-4(352-377)Online publication date: 1-Feb-2008
https://dl.acm.org/doi/10.1016/j.ic.2007.07.004
Show More Cited By

Index Terms

Combining intruder theories

Index terms have been assigned to the content through auto-classification.

Recommendations

Hierarchical combination of intruder theories

Recently automated deduction tools have proved to be very effective for detecting attacks on cryptographic protocols. These analysis can be improved, for finding more subtle weaknesses, by a more accurate modelling of operators employed by protocols. ...
Symbolic protocol analysis in the union of disjoint intruder theories: Combining decision procedures

Most of the decision procedures for symbolic analysis of protocols are limited to a fixed set of algebraic operators associated with a fixed intruder theory. Examples of such sets of operators comprise XOR, multiplication, abstract encryption/decryption. ...
Hierarchical combination of intruder theories
RTA'06: Proceedings of the 17th international conference on Term Rewriting and Applications

Recently automated deduction tools have proved to be very effective for detecting attacks on cryptographic protocols. These analysis can be improved, for finding more subtle weaknesses, by a more accurate modelling of operators employed by protocols. ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Guide Proceedings

ICALP'05: Proceedings of the 32nd international conference on Automata, Languages and Programming

July 2005

1476 pages

ISBN:3540275800

Editors:
Luís Caires
CITI / Departamento de Informática, Universidade Nova de Lisboa, Portugal
,
Giuseppe F. Italiano
Dipartimento di Informatica, Sistemi e Produzione, Università di Roma "Tor Vergata", via del Politecnico 1, Roma, Italy
,
Luís Monteiro
Departamento de Informatica, Universidade Nova de Lisboa, via del Politecnico 1, Caparica, Portugal
,
Catuscia Palamidessi
Departamento de Informatica, Ecole Polytechnique, Rue de Saclay, Palaiseau Cedex, France
,
Moti Yung
Computer Science Department, Google Inc. and Columbia University, 1214 Amsterdam Avenue, New York, France

Sponsors

Fundacao para a Ciencia e Tecnologia
FCT: Foundation for Science and Technology
Centro de Lógica e Computação/IST/UTL: Centro de Lógica e Computação/IST/UTL

Publisher

Springer-Verlag

Berlin, Heidelberg

Publication History

Published: 11 July 2005

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

16
Total Citations
View Citations
0
Total Downloads

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

Reflects downloads up to 13 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Avanesov TChevalier YRusinowitch MTuruani M(2017)Satisfiability of general intruder constraints with and without a set constructorJournal of Symbolic Computation10.1016/j.jsc.2016.07.00980:P1(27-61)Online publication date: 1-May-2017
https://dl.acm.org/doi/10.1016/j.jsc.2016.07.009
Delaune SLafourcade PLugiez DTreinen R(2008)Symbolic protocol analysis for monoidal equational theoriesInformation and Computation10.1016/j.ic.2007.07.005206:2-4(312-351)Online publication date: 1-Feb-2008
https://dl.acm.org/doi/10.1016/j.ic.2007.07.005
Chevalier YRusinowitch M(2008)Hierarchical combination of intruder theoriesInformation and Computation10.1016/j.ic.2007.07.004206:2-4(352-377)Online publication date: 1-Feb-2008
https://dl.acm.org/doi/10.1016/j.ic.2007.07.004
Comon-Lundh H(2008)Challenges in the Automated Verification of Security ProtocolsProceedings of the 4th international joint conference on Automated Reasoning10.1007/978-3-540-71070-7_34(396-409)Online publication date: 12-Aug-2008
https://dl.acm.org/doi/10.1007/978-3-540-71070-7_34
Bursuc SComon-Lundh HDelaune S(2007)Deducibility constraints, equational theory and electronic moneyRewriting Computation and Proof10.5555/2391276.2391289(196-212)Online publication date: 1-Jan-2007
https://dl.acm.org/doi/10.5555/2391276.2391289
Chevalier YKourjieh M(2007)Key substitution in the symbolic analysis of cryptographic protocolsProceedings of the 27th international conference on Foundations of software technology and theoretical computer science10.5555/1781794.1781806(121-132)Online publication date: 12-Dec-2007
https://dl.acm.org/doi/10.5555/1781794.1781806
Cortier VDelaune S(2007)Deciding knowledge in security protocols for monoidal equational theoriesProceedings of the 14th international conference on Logic for programming, artificial intelligence and reasoning10.5555/1779419.1779435(196-210)Online publication date: 15-Oct-2007
https://dl.acm.org/doi/10.5555/1779419.1779435
Lafourcade P(2007)Intruder Deduction for the Equational Theory of Exclusive-or with Commutative and Distributive EncryptionElectronic Notes in Theoretical Computer Science (ENTCS)10.1016/j.entcs.2007.02.054171:4(37-57)Online publication date: 1-Jul-2007
https://dl.acm.org/doi/10.1016/j.entcs.2007.02.054
Chevalier YKourjieh M(2007)Key Substitution in the Symbolic Analysis of Cryptographic ProtocolsFSTTCS 2007: Foundations of Software Technology and Theoretical Computer Science10.1007/978-3-540-77050-3_10(121-132)Online publication date: 12-Dec-2007
https://dl.acm.org/doi/10.1007/978-3-540-77050-3_10
Chevalier YLugiez DRusinowitch M(2007)Towards an Automatic Analysis of Web Service SecurityProceedings of the 6th international symposium on Frontiers of Combining Systems10.1007/978-3-540-74621-8_9(133-147)Online publication date: 10-Sep-2007
https://dl.acm.org/doi/10.1007/978-3-540-74621-8_9
Show More Cited By

View Options

View options

Media

Figures

Other

Tables

View Table of Contents