Timed properties of cryptographic security protocols - simulation approach

Modern communication systems require rigorous security solutions. This issue is multi-dimensional. Broadly understood security consists of many components. Security protocols (SP) ensure the confidentiality of transmitted or collected data and identify communicating parties - concurrent algorithms using cryptographic techniques appropriately implemented in communication systems. The exchange of information via a shared medium such as a computer network is always burdened with a certain degree of uncertainty due to the risk of eavesdropping, interception, or manipulation of transmitted information. SPs are challenging to analyze; therefore, their design is very demanding. The most difficult to study are the time properties of SP executions. Many works have been devoted to formal methods of examining these properties, defining what the dependencies between the time parameters used in a given protocol must be for it to work correctly. Until now, these studies have been conducted using formal methods abstracted from the real parameters of computer networks. In this work, we fill this gap by examining dependencies between the values of the time parameters of protocols using simulation methods. The values obtained by these dependencies will then be introduced into formal models to check the protocols’ security properties in real networks.