Probabilistic Model Checking of Security Protocols without Perfect Cryptography Assumption | SpringerLink
Skip to main content
Springer Nature Link
Log in

Probabilistic Model Checking of Security Protocols without Perfect Cryptography Assumption

  • Conference paper
  • First Online:
Computer Networks (CN 2016)

Part of the book series: Communications in Computer and Information Science ((CCIS,volume 608))

Included in the following conference series:

Abstract

This paper presents the description of a new, probabilistic approach to model checking of security protocols. The protocol, beyond traditional verification, goes through a phase in which we resign from a perfect cryptography assumption. We assume a certain minimal, but measurable probability of breaking/gaining the cryptographic key, and explore how it affects the execution of the protocol. As part of this work we have implemented a tool, that helps to analyze the probability of interception of sensitive information by the Intruder, depending on the preset parameters (number of communication participants, keys, nonces, the probability of breaking a cipher, etc.). Due to the huge size of the constructed computational spaces, we use parallel computing to search for states that contain the considered properties.

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

Access this chapter

Log in via an institution

Subscribe and save

Springer+ Basic
¥17,985 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Chapter
JPY 3498
Price includes VAT (Japan)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
JPY 5719
Price includes VAT (Japan)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
JPY 7149
Price includes VAT (Japan)
  • 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

Similar content being viewed by others

References

  1. Paulson, L.: Inductive Analysis of the Internet Protocol TLS, TR440. University of Cambridge, Computer Laboratory (1998)

    Google Scholar 

  2. Burrows, M., Abadi, M., Needham, R.: A logic of authentication. Proc. R. Soc. Lond. A 426, 233–271 (1989)

    Article  MathSciNet  MATH  Google Scholar 

  3. Dolev, D., Yao, A.: On the security of public key protocols. IEEE Trans. Inf. Theory 29(2), 198–207 (1983)

    Article  MathSciNet  MATH  Google Scholar 

  4. Armando, A., et al.: The AVISPA tool for the automated validation of internet security protocols and applications. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 281–285. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  5. Cremers, C.J.F.: The Scyther tool: verification, falsification, and analysis of security protocols. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 414–418. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  6. Kurkowski, M., Penczek, W.: Verifying security protocols modeled by networks of automata. Fundamenta Informaticae 79(3–4), 453–471 (2007). IOS Press

    MathSciNet  MATH  Google Scholar 

  7. Kurkowski, M., Siedlecka-Lamch, O., Szymoniak, S., Piech, H.: Parallel bounded model checking of security protocols. In: Wyrzykowski, R., Dongarra, J., Karczewski, K., Waśniewski, J. (eds.) PPAM 2013, Part I. LNCS, vol. 8384, pp. 224–234. Springer, Heidelberg (2014)

    Chapter  Google Scholar 

  8. Kurkowski, M., Siedlecka-Lamch, O., Dudek, P.: Using backward induction techniques in (timed) security protocols verification. In: Saeed, K., Chaki, R., Cortesi, A., Wierzchoń, S. (eds.) CISIM 2013. LNCS, vol. 8104, pp. 265–276. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  9. 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)

    Chapter  Google Scholar 

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

    Article  MATH  Google Scholar 

  11. Kurkowski, M., Grosser, A., Piatkowski, J., Szymoniak, S.: ProToc - an universal language for security protocols specification. In: Wiliński, A., El Fray, I., Pejaś, J. (eds.) Soft Computing in Computer and Information Science. AISC, vol. 342, pp. 237–248. Springer, Heidelberg (2015)

    Google Scholar 

  12. El Fray, I., Hyla, T., Kurkowski, M., Maćków, W., Pejaś, J.: Practical authentication protocols for protecting and sharing sensitive information on mobile devices. In: Kotulski, Z., Księżopolski, B., Mazur, K. (eds.) CSS 2014. CCIS, vol. 448, pp. 153–165. Springer, Heidelberg (2014)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Institute of Computer and Information Sciences, Czestochowa University of Technology, Częstochowa, Poland

    Olga Siedlecka-Lamch & Jacek Piatkowski

  2. Institute of Computer Sciences, Cardinal Stefan Wyszynski University in Warsaw, Warsaw, Poland

    Miroslaw Kurkowski

Authors
  1. Olga Siedlecka-Lamch
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Miroslaw Kurkowski
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Jacek Piatkowski
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Olga Siedlecka-Lamch .

Editor information

Editors and Affiliations

  1. Silesian University of Technology, Gliwice, Poland

    Piotr Gaj

  2. Silesian University of Technology, Gliwice, Poland

    Andrzej Kwiecień

  3. Silesian University of Technology, Gliwice, Poland

    Piotr Stera

Rights and permissions

Reprints and permissions

Copyright information

© 2016 Springer International Publishing Switzerland

About this paper

Cite this paper

Siedlecka-Lamch, O., Kurkowski, M., Piatkowski, J. (2016). Probabilistic Model Checking of Security Protocols without Perfect Cryptography Assumption. In: Gaj, P., Kwiecień, A., Stera, P. (eds) Computer Networks. CN 2016. Communications in Computer and Information Science, vol 608. Springer, Cham. https://doi.org/10.1007/978-3-319-39207-3_10

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-39207-3_10

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-39206-6

  • Online ISBN: 978-3-319-39207-3

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation