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

Article

Combining Algorithms for Deciding Knowledge in Security Protocols

Authors:

Mathilde Arnaud,

Véronique Cortier,

Stéphanie DelauneAuthors Info & Claims

FroCoS '07: Proceedings of the 6th international symposium on Frontiers of Combining Systems

Pages 103 - 117

https://doi.org/10.1007/978-3-540-74621-8_7

Published: 10 September 2007 Publication History

Abstract

In formal approaches, messages sent over a network are usually modeled by terms together with an equational theory, axiomatizing the properties of the cryptographic functions (encryption, exclusive or, ...). The analysis of cryptographic protocols requires a precise understanding of the attacker knowledge. Two standard notions are usually considered: deducibility and indistinguishability. Those notions are well-studied and several decidability results already exist to deal with a variety of equational theories. However most of the results are dedicated to specific equational theories.

We show that decidability results can be easily combined for any disjoint equational theories: if the deducibility and indistinguishability relations are decidable for two disjoint theories, they are also decidable for their union. As an application, new decidability results can be obtained using this combination theorem.

References

[1]

Abadi, M., Baudet, M., Warinschi, B.: Guessing attacks and the computational soundness of static equivalence. In: Aceto, L., Ingólfsdóttir, A. (eds.) FOSSACS 2006 and ETAPS 2006. LNCS, vol. 3921, pp. 398-412. Springer, Heidelberg (2006)

Digital Library

[2]

Abadi, M., Cortier, V.: Deciding knowledge in security protocols under equational theories. Theoretical Computer Science 387(1-2), 2-32 (2006)

Digital Library

[3]

Abadi, M., Fournet, C.: Mobile values, new names, and secure communication. In: Proceedings of the 28th ACM Symposium on Principles of Programming Languages (POPL'01), pp. 104-115. ACM Press, New York (2001)

Digital Library

[4]

Arnaud, M., Cortier, V., Delaune, S.: Combining algorithms for deciding knowledge in security protocols. Research Report 6118, INRIA, p. 28 (February 2007)

[5]

Baader, F., Schulz, K.U.: Unification in the union of disjoint equational theories: Combining decision procedures. Journal of Symbolic Computation 21(2), 211-243 (1996)

Digital Library

[6]

Baudet, M., Cortier, V., Kremer, S.: Computationally sound implementations of equational theories against passive adversaries. In: Caires, L., Italiano, G.F., Monteiro, L., Palamidessi, C., Yung, M. (eds.) ICALP 2005. LNCS, vol. 3580, pp. 652-663. Springer, Heidelberg (2005)

Digital Library

[7]

Chevalier, Y., Küsters, R., Rusinowitch, M., Turuani, M.: An NP decision procedure for protocol insecurity with XOR. In: Proceedings of 18th Annual IEEE Symposium on Logic in Computer Science (LICS'03), Ottawa (Canada), IEEE Computer Society Press, Los Alamitos (2003)

Digital Library

[8]

Chevalier, Y., Rusinowitch, M.: Combining intruder theories. In: Caires, L., Italiano, G.F., Monteiro, L., Palamidessi, C., Yung, M. (eds.) ICALP 2005. LNCS, vol. 3580, pp. 639-651. Springer, Heidelberg (2005)

Digital Library

[9]

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

[10]

Chevalier, Y., Rusinowitch, M.: Hierarchical combination of intruder theories. In: Pfenning, F. (ed.) RTA 2006. LNCS, vol. 4098, pp. 108-122. Springer, Heidelberg (2006)

Digital Library

[11]

Comon-Lundh, H., Shmatikov, V.: Intruder deductions, constraint solving and insecurity decision in presence of exclusive or. In: Proceedings of 18th Annual IEEE Symposium on Logic in Computer Science (LICS'03), Ottawa (Canada), IEEE Computer Society Press, Los Alamitos (2003)

Digital Library

[12]

Cortier, V., Delaune, S.: Deciding knowledge in security protocols for monoidal equational theories. In: Proc. of the Joint Workshop on Foundations of Computer Security and Automated Reasoning for Security Protocol Analysis (FCSARSPA' 07), Wrocław, Poland (to appear, 2007)

[13]

Delaune, S.: Easy intruder deduction problems with homomorphisms. Information Processing Letters 97(6), 213-218 (2006)

Digital Library

[14]

Dershowitz, N., Jouannaud, J.-P.: Rewrite systems. In: Handbook of Theoretical Computer Science, vol. B, ch. 6, Elsevier, Amsterdam (1990)

Digital Library

[15]

Lafourcade, P., Lugiez, D., Treinen, R.: Intruder deduction for the equational theory of Abelian groups with distributive encryption. Information and Computation (to appear, 2007)

Digital Library

[16]

Lakhnech, Y., Mazaré, L., Warinschi, B.: Soundness of symbolic equivalence for modular exponentiation. In: Proceedings of the Second Workshop on Formal and Computational Cryptography (FCC'06), pp. 19-23, Venice, Italy (July 2006)

[17]

Lowe, G.: Breaking and fixing the Needham-Schroeder public-key protocol using FDR. In: Margaria, T., Steffen, B. (eds.) TACAS 1996. LNCS, vol. 1055, pp. 147- 166. Springer, Heidelberg (1996)

Digital Library

[18]

Millen, J., Shmatikov, V.: Constraint solving for bounded-process cryptographic protocol analysis. In: Proceedings of the 8th ACM Conference on Computer and Communications Security (CCS'01), ACM Press, New York (2001)

Digital Library

[19]

Paulson, L.C.: The inductive approach to verifying cryptographic protocols. Journal of Computer Security 6(1-2), 85-128 (1998)

Digital Library

[20]

Rusinowitch, M., Turuani, M.: Protocol insecurity with a finite number of sessions, composed keys is NP-complete. Theoretical Computer Science 1-3(299), 451-475 (2003)

Digital Library

[21]

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

Digital Library

Cited By

Chadha RCheval VCiobâcă ŞKremer S(2016)Automated Verification of Equivalence Properties of Cryptographic ProtocolsACM Transactions on Computational Logic (TOCL)10.1145/292671517:4(1-32)Online publication date: 20-Sep-2016
https://dl.acm.org/doi/10.1145/2926715
Baudet MCortier VDelaune S(2013)YAPAACM Transactions on Computational Logic (TOCL)10.1145/2422085.242208914:1(1-32)Online publication date: 1-Feb-2013
https://dl.acm.org/doi/10.1145/2422085.2422089
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
Show More Cited By

Combining Algorithms for Deciding Knowledge in Security Protocols

Recommendations

Deciding Knowledge in Security Protocols for Monoidal Equational Theories
Logic for Programming, Artificial Intelligence, and Reasoning
Abstract
In formal approaches, messages sent over a network are usually modeled by terms together with an equational theory, axiomatizing the properties of the cryptographic functions (encryption, exclusive or, ...). The analysis of cryptographic protocols ...
Deciding knowledge in security protocols for monoidal equational theories
LPAR'07: Proceedings of the 14th international conference on Logic for programming, artificial intelligence and reasoning

In formal approaches, messages sent over a network are usually modeled by terms together with an equational theory, axiomatizing the properties of the cryptographic functions (encryption, exclusive or, ...). The analysis of cryptographic protocols ...
Decidability and Combination Results for Two Notions of Knowledge in Security Protocols

In formal approaches, messages sent over a network are usually modeled by terms together with an equational theory, axiomatizing the properties of the cryptographic functions (encryption, exclusive or, ...). The analysis of cryptographic protocols ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Guide Proceedings

FroCoS '07: Proceedings of the 6th international symposium on Frontiers of Combining Systems

September 2007

282 pages

ISBN:9783540746201

Publisher

Springer-Verlag

Berlin, Heidelberg

Publication History

Published: 10 September 2007

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

4
Total Citations
View Citations
0
Total Downloads

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

Reflects downloads up to 12 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Chadha RCheval VCiobâcă ŞKremer S(2016)Automated Verification of Equivalence Properties of Cryptographic ProtocolsACM Transactions on Computational Logic (TOCL)10.1145/292671517:4(1-32)Online publication date: 20-Sep-2016
https://dl.acm.org/doi/10.1145/2926715
Baudet MCortier VDelaune S(2013)YAPAACM Transactions on Computational Logic (TOCL)10.1145/2422085.242208914:1(1-32)Online publication date: 1-Feb-2013
https://dl.acm.org/doi/10.1145/2422085.2422089
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
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

View Options

View options

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

Media

Figures

Other

Tables

View Table of Contents