Skip to main content
Erschienen in: Journal of Automated Reasoning 4/2021

21.10.2020

A Decidable Class of Security Protocols for Both Reachability and Equivalence Properties

verfasst von: Véronique Cortier, Stéphanie Delaune, Vaishnavi Sundararajan

Erschienen in: Journal of Automated Reasoning | Ausgabe 4/2021

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config
loading …

Abstract

We identify a new decidable class of security protocols, both for reachability and equivalence properties. Our result holds for an unbounded number of sessions and for protocols with nonces. It covers all standard cryptographic primitives. Our class sets up three main assumptions. (i) Protocols need to be “simple”, meaning that an attacker can precisely identify from which participant and which session a message originates from. We also consider protocols with no else branches (only positive test). (ii) Protocols should be type-compliant, which is intuitively guaranteed as soon as two encrypted messages of the protocol cannot be confused. (iii) Finally, we define the notion of a dependency graph, which, given a protocol, characterises how actions depend on the other ones (both sequential dependencies and data dependencies are taken into account). Whenever the graph is acyclic, then the protocol falls into our class. We show that many protocols of the literature belong to our decidable class, including for example some of the protocols embedded in the biometric passport.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

Literatur
1.
Zurück zum Zitat Delignat-Lavaud, A., Fournet, C., Kohlweiss, M., Protzenko, J., Rastogi, A., Swamy, N., Béguelin, S.Z., Bhargavan, K., Pan, J., Zinzindohoue, J.K.: Implementing and proving the TLS 1.3 record layer. In: 2017 IEEE Symposium on Security and Privacy (S&P 2017), pp. 463–482 (2017) Delignat-Lavaud, A., Fournet, C., Kohlweiss, M., Protzenko, J., Rastogi, A., Swamy, N., Béguelin, S.Z., Bhargavan, K., Pan, J., Zinzindohoue, J.K.: Implementing and proving the TLS 1.3 record layer. In: 2017 IEEE Symposium on Security and Privacy (S&P 2017), pp. 463–482 (2017)
2.
Zurück zum Zitat Exigences techniques et administratives applicables au vote électronique. Chancellerie fédérale ChF (2014). Swiss recommendation on e-voting Exigences techniques et administratives applicables au vote électronique. Chancellerie fédérale ChF (2014). Swiss recommendation on e-voting
3.
Zurück zum Zitat Blanchet, B.: An efficient cryptographic protocol verifier based on prolog rules. In: Proceedings of 14th Computer Security Foundations Workshop (CSFW’01). IEEE Computer Society Press (2001) Blanchet, B.: An efficient cryptographic protocol verifier based on prolog rules. In: Proceedings of 14th Computer Security Foundations Workshop (CSFW’01). IEEE Computer Society Press (2001)
4.
Zurück zum Zitat Meier, S., Schmidt, B., Cremers, C., Basin, D.: The TAMARIN Prover for the Symbolic Analysis of Security Protocols. In: Computer Aided Verification, 25th International Conference, CAV 2013, Princeton, USA, Proceeding. LNCS, vol. 8044, pp. 696–701. Springer, Berlin (2013) Meier, S., Schmidt, B., Cremers, C., Basin, D.: The TAMARIN Prover for the Symbolic Analysis of Security Protocols. In: Computer Aided Verification, 25th International Conference, CAV 2013, Princeton, USA, Proceeding. LNCS, vol. 8044, pp. 696–701. Springer, Berlin (2013)
5.
Zurück zum Zitat Armando, A., Basin, D., Boichut, Y., Chevalier, Y., Compagna, L., Cuellar, J., Hankes Drielsma, P., Héam, P.C., Kouchnarenko, O., Mantovani, J., Mödersheim, S., von Oheimb, D., Rusinowitch, M., Santiago, J., Turuani, M., Viganò, L., Vigneron, L.: The AVISPA Tool for the automated validation of internet security protocols and applications. In: Etessami, K., Rajamani, S. (eds.) 17th International Conference on Computer Aided Verification, CAV’2005. Lecture Notes in Computer Science, vol. 3576, pp. 281–285. Springer, Edinburgh (2005)CrossRef Armando, A., Basin, D., Boichut, Y., Chevalier, Y., Compagna, L., Cuellar, J., Hankes Drielsma, P., Héam, P.C., Kouchnarenko, O., Mantovani, J., Mödersheim, S., von Oheimb, D., Rusinowitch, M., Santiago, J., Turuani, M., Viganò, L., Vigneron, L.: The AVISPA Tool for the automated validation of internet security protocols and applications. In: Etessami, K., Rajamani, S. (eds.) 17th International Conference on Computer Aided Verification, CAV’2005. Lecture Notes in Computer Science, vol. 3576, pp. 281–285. Springer, Edinburgh (2005)CrossRef
6.
Zurück zum Zitat Escobar, S., Meadows, C., Meseguer, J.: A rewriting-based inference system for the NRL protocol analyzer and its meta-logical properties. Theor. Comput. Sci. 367(1–2), 162–202 (2006)MathSciNetCrossRef Escobar, S., Meadows, C., Meseguer, J.: A rewriting-based inference system for the NRL protocol analyzer and its meta-logical properties. Theor. Comput. Sci. 367(1–2), 162–202 (2006)MathSciNetCrossRef
7.
Zurück zum Zitat Cremers, C.: The Scyther Tool: Verification, falsification, and analysis of security protocols. In: Proceedings 20th International Conference on Computer Aided Verification (CAV’08), Lecture Notes in Computer Science, pp. 414–418. Springer, Berlin (2008) Cremers, C.: The Scyther Tool: Verification, falsification, and analysis of security protocols. In: Proceedings 20th International Conference on Computer Aided Verification (CAV’08), Lecture Notes in Computer Science, pp. 414–418. Springer, Berlin (2008)
8.
Zurück zum Zitat Durgin, N., Lincoln, P., Mitchell, J., Scedrov, A.: Undecidability of bounded security protocols. In: Workshop on Formal Methods and Security Protocols. Trento, Italia (1999) Durgin, N., Lincoln, P., Mitchell, J., Scedrov, A.: Undecidability of bounded security protocols. In: Workshop on Formal Methods and Security Protocols. Trento, Italia (1999)
9.
Zurück zum Zitat Rusinowitch, M., Turuani, M.: Protocol insecurity with finite number of sessions and composed keys is NP-complete. Theor. Comput. Sci. 299, 451–475 (2003)MathSciNetCrossRef Rusinowitch, M., Turuani, M.: Protocol insecurity with finite number of sessions and composed keys is NP-complete. Theor. Comput. Sci. 299, 451–475 (2003)MathSciNetCrossRef
10.
Zurück zum Zitat Baudet, M.: Deciding security of protocols against off-line guessing attacks. In: Proceedings of 12th ACM Conference on Computer and Communications Security (CCS’05). ACM Press, Cambridge (2005) Baudet, M.: Deciding security of protocols against off-line guessing attacks. In: Proceedings of 12th ACM Conference on Computer and Communications Security (CCS’05). ACM Press, Cambridge (2005)
11.
Zurück zum Zitat Cheval, V., Kremer, S., Rakotonirina, I.: Deepsec: Deciding equivalence properties in security protocols—theory and practice. In: Proceedings 39th IEEE Symposium on Security and Privacy (S&P’18), pp. 525–542. IEEE Computer Society Press, San Francisco, CA, USA (2018) Cheval, V., Kremer, S., Rakotonirina, I.: Deepsec: Deciding equivalence properties in security protocols—theory and practice. In: Proceedings 39th IEEE Symposium on Security and Privacy (S&P’18), pp. 525–542. IEEE Computer Society Press, San Francisco, CA, USA (2018)
12.
Zurück zum Zitat Dawson, J., Tiu, A.: Automating open bisimulation checking for the spi-calculus. In: IEEE Computer Security Foundations Symposium (CSF 2010) (2010) Dawson, J., Tiu, A.: Automating open bisimulation checking for the spi-calculus. In: IEEE Computer Security Foundations Symposium (CSF 2010) (2010)
13.
Zurück zum Zitat Cheval, V.: APTE: an algorithm for proving trace equivalence. In: Proceedings of the 20th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’14), LNCS, vol. 8413, pp. 587–592 (2014) Cheval, V.: APTE: an algorithm for proving trace equivalence. In: Proceedings of the 20th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’14), LNCS, vol. 8413, pp. 587–592 (2014)
14.
Zurück zum Zitat Chadha, R., Ciobâcă, S., Kremer, S.: Automated verification of equivalence properties of cryptographic protocols. In: Programming Languages and Systems—Proceedings of the 21th European Symposium on Programming (ESOP’12), LNCS, vol. 7211, pp. 108–127. Springer, Berlin (2012) Chadha, R., Ciobâcă, S., Kremer, S.: Automated verification of equivalence properties of cryptographic protocols. In: Programming Languages and Systems—Proceedings of the 21th European Symposium on Programming (ESOP’12), LNCS, vol. 7211, pp. 108–127. Springer, Berlin (2012)
15.
Zurück zum Zitat Cortier, V., Delaune, S., Dallon, A.: SAT-Equiv: an efficient tool for equivalence properties. In: Proceedings of 30th IEEE Computer Security Foundations Symposium (CSF’17), pp. 481–494. IEEE Computer Society Press (2017) Cortier, V., Delaune, S., Dallon, A.: SAT-Equiv: an efficient tool for equivalence properties. In: Proceedings of 30th IEEE Computer Security Foundations Symposium (CSF’17), pp. 481–494. IEEE Computer Society Press (2017)
16.
Zurück zum Zitat Comon-Lundh, H., Cortier, V.: New decidability results for fragments of first-order logic and application to cryptographic protocols. In: Proceedings 14th International Conference on Rewriting Techniques and Applications (RTA’2003), LNCS, vol. 2706. Springer, Berlin (2003) Comon-Lundh, H., Cortier, V.: New decidability results for fragments of first-order logic and application to cryptographic protocols. In: Proceedings 14th International Conference on Rewriting Techniques and Applications (RTA’2003), LNCS, vol. 2706. Springer, Berlin (2003)
17.
Zurück zum Zitat Chrétien, R., Cortier, V., Delaune, S.: From security protocols to pushdown automata. In: Proceedings of 40th International Colloquium on Automata, Languages and Programming (ICALP’13) (2013) Chrétien, R., Cortier, V., Delaune, S.: From security protocols to pushdown automata. In: Proceedings of 40th International Colloquium on Automata, Languages and Programming (ICALP’13) (2013)
18.
Zurück zum Zitat Chrétien, R., Cortier, V., Delaune, S.: Typing messages for free in security protocols: the case of equivalence properties. In: Proceedings of 25th International Conference on Concurrency Theory (CONCUR’14), Lecture Notes in Computer Science, vol. 8704, pp. 372–386. Springer, Berlin (2014) Chrétien, R., Cortier, V., Delaune, S.: Typing messages for free in security protocols: the case of equivalence properties. In: Proceedings of 25th International Conference on Concurrency Theory (CONCUR’14), Lecture Notes in Computer Science, vol. 8704, pp. 372–386. Springer, Berlin (2014)
19.
Zurück zum Zitat Chrétien, R., Cortier, V., Delaune, S.: Decidability of trace equivalence for protocols with nonces. In: Proceedings of 28th IEEE Computer Security Foundations Symposium (CSF’15), pp. 170–184. IEEE Computer Society Press (2015) Chrétien, R., Cortier, V., Delaune, S.: Decidability of trace equivalence for protocols with nonces. In: Proceedings of 28th IEEE Computer Security Foundations Symposium (CSF’15), pp. 170–184. IEEE Computer Society Press (2015)
20.
Zurück zum Zitat Lowe, G.: Towards a completeness result for model checking of security protocols. In: Proceedings of the 11th Computer Security Foundations Workshop (CSFW’98). IEEE Computer Society Press (1998) Lowe, G.: Towards a completeness result for model checking of security protocols. In: Proceedings of the 11th Computer Security Foundations Workshop (CSFW’98). IEEE Computer Society Press (1998)
21.
Zurück zum Zitat Ramanujam, R., Suresh, S.P.: Tagging makes secrecy decidable with unbounded nonces as well. In: Proceedings of 23rd Conference of Foundations of Software Technology and Theoretical Computer Science (FST&TCS’03), LNCS, pp. 363–374. Springer, Berlin (2003) Ramanujam, R., Suresh, S.P.: Tagging makes secrecy decidable with unbounded nonces as well. In: Proceedings of 23rd Conference of Foundations of Software Technology and Theoretical Computer Science (FST&TCS’03), LNCS, pp. 363–374. Springer, Berlin (2003)
22.
Zurück zum Zitat Dougherty, D.J., Guttman, J.D.: Decidability for lightweight Diffie–Hellman protocols. In: Proceedings of 27th IEEE Symposium on Computer Security Foundations (CSF’14) (2014) Dougherty, D.J., Guttman, J.D.: Decidability for lightweight Diffie–Hellman protocols. In: Proceedings of 27th IEEE Symposium on Computer Security Foundations (CSF’14) (2014)
23.
Zurück zum Zitat Fröschle, S.: Leakiness is decidable for well-founded protocols? In: Proceedings of 4th Conference on Principles of Security and Trust (POST’15), Lecture Notes in Computer Science. Springer (2015) Fröschle, S.: Leakiness is decidable for well-founded protocols? In: Proceedings of 4th Conference on Principles of Security and Trust (POST’15), Lecture Notes in Computer Science. Springer (2015)
24.
Zurück zum Zitat Chrétien, R., Cortier, V., Dallon, A., Delaune, S.: Typing messages for free in security protocols. ACM Trans Comput Log 21(1), 1 (2019) MathSciNetCrossRef Chrétien, R., Cortier, V., Dallon, A., Delaune, S.: Typing messages for free in security protocols. ACM Trans Comput Log 21(1), 1 (2019) MathSciNetCrossRef
25.
Zurück zum Zitat Cortier, V., Dallon, A., Delaune, S.: Efficiently deciding equivalence for standard primitives and phases. In: Proceedings 23rd European Symposium on Research in Computer Security (ESORICS’18), Lecture Notes in Computer Science. Springer, Barcelona (2018) Cortier, V., Dallon, A., Delaune, S.: Efficiently deciding equivalence for standard primitives and phases. In: Proceedings 23rd European Symposium on Research in Computer Security (ESORICS’18), Lecture Notes in Computer Science. Springer, Barcelona (2018)
27.
Zurück zum Zitat Blanchet, B.: Vérification automatique de protocoles cryptographiques : modèle formel et modèle calculatoire. automatic verification of security protocols: formal model and computational model. Mémoire d’habilitation à diriger des recherches, Université Paris-Dauphine (2008). En français avec publications en anglais en annexe. In French with publications in English in appendix Blanchet, B.: Vérification automatique de protocoles cryptographiques : modèle formel et modèle calculatoire. automatic verification of security protocols: formal model and computational model. Mémoire d’habilitation à diriger des recherches, Université Paris-Dauphine (2008). En français avec publications en anglais en annexe. In French with publications in English in appendix
29.
Zurück zum Zitat Chadha, R., Ciobâcă, Ş., Kremer, S.: Automated verification of equivalence properties of cryptographic protocols. In: Proceedings of 21th European Symposium on Programming (ESOP’12), LNCS (2012) Chadha, R., Ciobâcă, Ş., Kremer, S.: Automated verification of equivalence properties of cryptographic protocols. In: Proceedings of 21th European Symposium on Programming (ESOP’12), LNCS (2012)
30.
Zurück zum Zitat Abadi, M., Gordon, A.D.: A calculus for cryptographic protocols: the spi calculus. Inf. Comput. 148, 1–70 (1999)MathSciNetCrossRef Abadi, M., Gordon, A.D.: A calculus for cryptographic protocols: the spi calculus. Inf. Comput. 148, 1–70 (1999)MathSciNetCrossRef
31.
Zurück zum Zitat Cortier, V., Dallon, A., Delaune, S.: Bounding the number of agents, for equivalence too. In: Piessens, F., Viganó, L. (eds.) Proceedings of the 5th International Conference on Principles of Security and Trust (POST’16), Lecture Notes in Computer Science, vol. 9635, pp. 211–232. Springer, Eindhoven (2016) Cortier, V., Dallon, A., Delaune, S.: Bounding the number of agents, for equivalence too. In: Piessens, F., Viganó, L. (eds.) Proceedings of the 5th International Conference on Principles of Security and Trust (POST’16), Lecture Notes in Computer Science, vol. 9635, pp. 211–232. Springer, Eindhoven (2016)
32.
Zurück zum Zitat PKI for machine readable travel documents offering ICC read-only access. Technical report, International Civil Aviation Organization (2004) PKI for machine readable travel documents offering ICC read-only access. Technical report, International Civil Aviation Organization (2004)
33.
Zurück zum Zitat Hirschi, L., Delaune, S.: Description of some case studies. Deliverable VIP 6.1, (ANR-11-JS02-0006) (2013), p. 14 Hirschi, L., Delaune, S.: Description of some case studies. Deliverable VIP 6.1, (ANR-11-JS02-0006) (2013), p. 14
Metadaten
Titel
A Decidable Class of Security Protocols for Both Reachability and Equivalence Properties
verfasst von
Véronique Cortier
Stéphanie Delaune
Vaishnavi Sundararajan
Publikationsdatum
21.10.2020
Verlag
Springer Netherlands
Erschienen in
Journal of Automated Reasoning / Ausgabe 4/2021
Print ISSN: 0168-7433
Elektronische ISSN: 1573-0670
DOI
https://doi.org/10.1007/s10817-020-09582-9

Premium Partner