Skip to main content
SpringerLink
Log in

Efficient Verification of Security Protocols Time Properties Using SMT Solvers

  • Conference paper
  • First Online:
International Joint Conference: 12th International Conference on Computational Intelligence in Security for Information Systems (CISIS 2019) and 10th International Conference on EUropean Transnational Education (ICEUTE 2019) (CISIS 2019, ICEUTE 2019)

Part of the book series: Advances in Intelligent Systems and Computing ((AISC,volume 951))

Abstract

In this paper, we present a novel method for the verification of security protocols time properties using SMT-based bounded model checking (SMT-BMC). In our approach, we model protocol users’ behaviours using networks of synchronized timed automata. Suitably specified correctness properties are defined as reachability property of some, chosen states in automata network. We consider most important time properties of protocols’ executions using specially constructed time conditions. These are checked by a quantifier-free SMT encoding and SMT solver using BMC algorithms. In our work, we have also implemented the proposed method and evaluated it for four, well-known security protocols. We also compared our new SMT-based technique with the corresponding SAT-based approach.

The project financed under the program of the Minister of Science and Higher Education under the name “Regional Initiative of Excellence” in 2019–2022 project number 020/RID/2018/19, the amount of financing 12,000,000 PLN.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 129.00
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 169.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Notes

  1. 1.

    Syntax of NSPK timed version in Common Language is as follow: \( \alpha _1 \) \(A \rightarrow B\) \( :\) \(\{T_A,I_A\}_{K_B}\); \( \alpha _2 \) \(B \rightarrow A\) \( :\) \(\{T_A,T_B\}_{K_A}\); \( \alpha _3 \) \(A \rightarrow B\) \( :\) \(\{T_B\}_{K_B}\).

  2. 2.

    Syntax of WLP timed version in Common Language is as follow: \( \alpha _1 \) \(A \rightarrow B\) \( :\) \(I_A\); \( \alpha _2 \) \(B \rightarrow A\) \( :\) \(T_B\); \( \alpha _3 \) \(A \rightarrow B\) \( :\) \(\{T_B\}_{K_{AS}}\); \( \alpha _4 \) \(B \rightarrow S\) \( :\) \(\{I_A, \{N_B\}_{K_{AS}}\}_{K_{BS}}\); \( \alpha _5 \) \(S \rightarrow B\) \( :\) \(\{T_B\}_{K_{BS}}\).

  3. 3.

    Syntax of WMF timed version in Common Language is as follow: \( \alpha _1 \) \(A \rightarrow S\) \( :\) \(I_A,\{T_A,I_B,K_{AB}\}_{K_{AS}}\); \( \alpha _2 \) \(S \rightarrow B\) \( :\) \(\{T_S,I_A,K_{AB}\}_{K_{BS}}\).

References

  1. Alur, R., Dill, D.L.: A theory of timed automata. Theor. Comput. Sci. 126, 183–235 (1994)

    Article  MathSciNet  Google Scholar 

  2. Armando, A., et al.: The AVISPA tool for the automated validation of internet security protocols and applications. In: CAV 2005, Edinburgh, Scotland, UK, 6–10 July 2005, pp. 281–285 (2005)

    Google Scholar 

  3. Basin, D., Cremers, C., Meadows, C.: Model Checking Security Protocols, pp. 727–762. Springer (2018)

    Google Scholar 

  4. Burrows, M., Abadi, M., Needham, R.: A logic of authentication. ACM Trans. Comput. Syst. 8(1), 18–36 (1990)

    Article  Google Scholar 

  5. Corin, R., Etalle, S., Hartel, P.H., Mader, A.: Timed model checking of security protocols. In: Proceedings of the ACM Workshop on FMSE. ACM (2004)

    Google Scholar 

  6. Corin, R., Etalle, S., Hartel, P.H., Mader, A.: Timed analysis of security protocols. J. Comput. Secur. 15(6), 619 (2007)

    Article  Google Scholar 

  7. Cremers, C.J.F.: The Scyther tool: verification, falsification, and analysis of security protocols. In: CAV 2008, Princeton, NJ, USA, 7–14 July 2008, pp. 414–418 (2008)

    Google Scholar 

  8. Genet, T., Klay, F.: Rewriting for cryptographic protocol verification. In: Automated Deduction - CADE-17, Pittsburgh, PA, USA, 17–20 June 2000, pp. 271–290 (2000)

    Google Scholar 

  9. Hess, A., Mödersheim, S.: A typing result for stateful protocols. In: 31st IEEE Computer Security Foundations Symposium, CSF 2018, Oxford, pp. 374–388 (2018)

    Google Scholar 

  10. Jakubowska, G., Penczek, W.: Modelling and checking timed authentication of security protocols. Fundam. Inform. 79(3–4), 363–378 (2007)

    MathSciNet  MATH  Google Scholar 

  11. Koymans, R.: Specifying real-time properties with metric temporal logic. Real-Time Syst. 2(4), 255–299 (1990)

    Article  Google Scholar 

  12. Kurkowski, M., Penczek, W.: Applying timed automata to model checking of security protocols. In: Handbook of Finite State Based Models and Applications, pp. 223–254 (2012)

    Google Scholar 

  13. Kurkowski, M., Srebrny, M.: A quantifier-free first-order knowledge logic of authentication. Fundam. Inform. 72(1–3), 263–282 (2006)

    MathSciNet  MATH  Google Scholar 

  14. Monniaux, D.: Abstracting cryptographic protocols with tree automata. In: Static Analysis, SAS 1999, Venice, Italy, Proceedings, pp. 149–163 (1999)

    Google Scholar 

  15. De Moura, L., Bjørner, N.: Z3: an efficient SMT solver. In: Proceedings of (TACAS’2008). LNCS, vol. 4963, pp. 337–340. Springer (2008)

    Google Scholar 

  16. Needham, R.M., Schroeder, M.D.: Using encryption for authentication in large networks of computers. Commun. ACM 21(12), 993–999 (1978)

    Article  Google Scholar 

  17. Penczek, W., Pólrola, A.: Advances in Verification of Time Petri Nets and Timed Automata: A Temporal Logic Approach. Studies in Computational Intelligence, vol. 20. Springer (2006)

    Google Scholar 

  18. Szymoniak, S., Kurkowski, M., Piątkowski, J.: Timed models of security protocols including delays in the network. J. Appl. Math. Comput. Mech. 14(3), 127–139 (2015)

    Article  Google Scholar 

  19. Szymoniak, S., Siedlecka-Lamch, O., Kurkowski, M.: Timed analysis of security protocols. In: ISAT 2016 - Part II, pp. 53–63 (2016)

    Google Scholar 

  20. Szymoniak, S., Siedlecka-Lamch, O., Kurkowski, M.: On some time aspects in security protocols analysis. In: CN 2018, Proceedings, pp. 344–356 (2018)

    Google Scholar 

  21. Woo, T.Y.C., Lam, S.S.: A lesson on authentication protocol design. SIGOPS Oper. Syst. Rev. 28(3), 24–37 (1994)

    Article  Google Scholar 

  22. Wozna-Szczesniak, B., Zbrzezny, A.M., Zbrzezny, A.: SMT-based searching for k-quasi-optimal runs in weighted timed automata. Fundam. Inform. 152(4), 411–433 (2017)

    Article  MathSciNet  Google Scholar 

  23. Zbrzezny, A.: Improvements in SAT-based reachability analysis for timed automata. Fundam. Inform. 60(1–4), 417–434 (2004)

    MathSciNet  MATH  Google Scholar 

  24. Zbrzezny, A.: SAT-based reachability checking for timed automata with diagonal constraints. Fundam. Inform. 67(1–3), 303–322 (2005)

    MathSciNet  MATH  Google Scholar 

  25. Zbrzezny, A.M., Wozna-Szczesniak, B., Zbrzezny, A.: SMT-based bounded model checking for weighted epistemic ECTL. In: EPIA 2015, Coimbra, Portugal, pp. 651–657 (2015)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Faculty of Mathematics and Computer Science, University of Warmia and Mazury in Olsztyn, Olsztyn, Poland

    Agnieszka M. Zbrzezny

  2. Institute of Computer and Information Sciences, Czȩstochowa University of Technology, Czȩstochowa, Poland

    Sabina Szymoniak

  3. Institute of Computer Science, Cardinal St. Wyszynski University, Warsaw, Poland

    Mirosław Kurkowski

Authors
  1. Agnieszka M. Zbrzezny
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Sabina Szymoniak
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Mirosław Kurkowski
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Sabina Szymoniak .

Editor information

Editors and Affiliations

  1. Data Science and Big Data Lab, Pablo de Olavide University, Seville, Spain

    Francisco Martínez Álvarez

  2. Data Science and Big Data Lab, Pablo de Olavide University, Seville, Spain

    Alicia Troncoso Lora

  3. University of Salamanca, Salamanca, Spain

    José António Sáez Muñoz

  4. Department of Industrial Engineering, University of A Coruña, A Coruña, Spain

    Héctor Quintián

  5. University of Salamanca, Salamanca, Spain

    Emilio Corchado

Rights and permissions

Reprints and permissions

Copyright information

© 2020 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Zbrzezny, A.M., Szymoniak, S., Kurkowski, M. (2020). Efficient Verification of Security Protocols Time Properties Using SMT Solvers. In: Martínez Álvarez, F., Troncoso Lora, A., Sáez Muñoz, J., Quintián, H., Corchado, E. (eds) International Joint Conference: 12th International Conference on Computational Intelligence in Security for Information Systems (CISIS 2019) and 10th International Conference on EUropean Transnational Education (ICEUTE 2019). CISIS ICEUTE 2019 2019. Advances in Intelligent Systems and Computing, vol 951. Springer, Cham. https://doi.org/10.1007/978-3-030-20005-3_3

Download citation

Publish with us

Policies and ethics

Search

Navigation