Protocol security and algebraic properties: decision results for a bounded number of sessions. (English) Zbl 1242.94020
Treinen, Ralf (ed.), Rewriting techniques and applications. 20th international conference, RTA 2009, Brasília, Brazil, June 29–July 1, 2009. Proceedings. Berlin: Springer (ISBN 978-3-642-02347-7/pbk). Lecture Notes in Computer Science 5595, 133-147 (2009).
Summary: We consider the problem of deciding the security of cryptographic protocols for a bounded number of sessions, taking into account some algebraic properties of the security primitives, for instance abelian group properties. We propose a general method for deriving decision algorithms, splitting the task into four properties of the rewriting system describing the intruder capabilities: locality, conservativity, finite variant property and decidability of one-step deducibility constraints. We illustrate this method on a non trivial example, combining several abelian group properties, exponentiation and a homomorphism, showing a decidability result for this combination.
For the entire collection see [Zbl 1165.68021].
For the entire collection see [Zbl 1165.68021].
MSC:
| 94A60 | Cryptography |
| 03B25 | Decidability of theories and sets of sentences |
| 68P25 | Data encryption (aspects in computer science) |
References:
| [1] | Bursuc, S., Comon-Lundh, H.: Protocols, insecurity decision and combination of equational theories. Technical Report 02, Laboratoire Spécification et Vérification (February 2009), http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/rr-lsv-2009-02.pdf |
| [2] | Bursuc, S., Comon-Lundh, H., Delaune, S.: Associative-commutative deducibility constraints. In: Thomas, W., Weil, P. (eds.) STACS 2007. LNCS, vol. 4393, pp. 634–645. Springer, Heidelberg (2007) · Zbl 1186.68282 · doi:10.1007/978-3-540-70918-3_54 |
| [3] | Bursuc, S., Comon-Lundh, H., Delaune, S.: Deducibility constraints, equational theory and electronic money. In: Comon-Lundh, H., Kirchner, C., Kirchner, H. (eds.) Jouannaud Festschrift. LNCS, vol. 4600, pp. 196–212. Springer, Heidelberg (2007) · Zbl 1186.68283 · doi:10.1007/978-3-540-73147-4_10 |
| [4] | Chevalier, Y., Kuester, R., Rusinowitch, M., Turuani, M.: An NP decision procedure for protocol insecurity with xor. In: Kolaitis [15] · Zbl 1068.68057 · doi:10.1109/LICS.2003.1210066 |
| [5] | Chevalier, Y., Küsters, R., Rusinowitch, M., Turuani, M.: Deciding the security of protocols with Diffie-Hellman exponentiation and products in exponents. In: Pandya, P.K., Radhakrishnan, J. (eds.) FSTTCS 2003. LNCS, vol. 2914, pp. 124–135. Springer, Heidelberg (2003) · Zbl 1205.94078 · doi:10.1007/978-3-540-24597-1_11 |
| [6] | 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) · doi:10.1007/11523468_52 |
| [7] | Chevalier, Y., Rusinowitch, M.: Hierarchical combination of intruder theories. In: Pfenning, F. (ed.) RTA 2006. LNCS, vol. 4098, pp. 108–122. Springer, Heidelberg (2006) · Zbl 1151.68630 · doi:10.1007/11805618_9 |
| [8] | Comon-Lundh, H., Delaune, S.: The finite variant property: How to get rid of some algebraic properties. In: Giesl, J. (ed.) RTA 2005. LNCS, vol. 3467, pp. 294–307. Springer, Heidelberg (2005) · Zbl 1078.68059 · doi:10.1007/978-3-540-32033-3_22 |
| [9] | Comon-Lundh, H., Shmatikov, V.: Intruder deductions, constraint solving and insecurity decision in preence of exclusive or. In: Kolaitis [15] |
| [10] | Contejean, E., Marché, C.: Cime: Completion modulo e. In: Ganzinger, H. (ed.) RTA 1996. LNCS, vol. 1103, pp. 416–419. Springer, Heidelberg (1996) · doi:10.1007/3-540-61464-8_70 |
| [11] | Delaune, S.: An undecidability result for AGh. Theoretical Computer Science 368(1-2), 161–167 (2006) · Zbl 1171.94344 · doi:10.1016/j.tcs.2006.08.018 |
| [12] | Delaune, S., Lafourcade, P., Lugiez, D., Treinen, R.: Symbolic protocol analysis for monoidal equational theories. Information and Computation 206(2-4), 312–351 (2008) · Zbl 1148.68325 · doi:10.1016/j.ic.2007.07.005 |
| [13] | Dershowitz, N., Jouannaud, J.-P.: Rewrite systems. In: van Leeuwen, J. (ed.) Handbook of Theoretical Computer Science, vol. B, pp. 243–309. North-Holland, Amsterdam (1990) · Zbl 0900.68283 |
| [14] | Escobar, S., Meseguer, J., Sasse, R.: Effectively checking the finite variant property. In: Voronkov, A. (ed.) RTA 2008. LNCS, vol. 5117, pp. 79–93. Springer, Heidelberg (2008) · Zbl 1145.68444 · doi:10.1007/978-3-540-70590-1_6 |
| [15] | Kolaitis, P. (ed.): Eighteenth Annual IEEE Symposium on Logic in Computer Science, Ottawa, Canada. IEEE Computer Society, Los Alamitos (2003) |
| [16] | Millen, J., Shmatikov, V.: Constraint solving for bounded-process cryptographic protocol analysis. In: Proc. 8th ACM Conference on Computer and Communications Security (2001) · doi:10.1145/501983.502007 |
| [17] | Rusinowitch, M., Turuani, M.: Protocol insecurity with finite number of sessions is np-complete. In: Proc. 14th IEEE Computer Security Foundations Workshop, Cape Breton, Nova Scotia (June 2001) · Zbl 1042.68009 · doi:10.1109/CSFW.2001.930145 |
| [18] | Shmatikov, V.: Decidable analysis of cryptographic protocols with products and modular exponentiation. In: Schmidt, D. (ed.) ESOP 2004. LNCS, vol. 2986, pp. 355–369. Springer, Heidelberg (2004) · Zbl 1126.94341 · doi:10.1007/978-3-540-24725-8_25 |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
