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.
Mendeley helps you to discover research relevant for your work.
CITATION STYLE
Siedlecka-Lamch, O., Kurkowski, M., & Piatkowski, J. (2016). Probabilistic model checking of security protocols without perfect cryptography assumption. In Communications in Computer and Information Science (Vol. 608, pp. 107–117). Springer Verlag. https://doi.org/10.1007/978-3-319-39207-3_10