Performance and cryptographic evaluation of security protocols in distributed networks using applied pi calculus and Markov Chain

Abstract

The development of cryptographic protocols goes through two stages, namely, security verification and performance analysis. The verification of the protocol’s security properties could be analytically achieved using threat modelling, or formally using formal methods and model checkers. The performance analysis could be mathematical or simulation-based. However, mathematical modelling is complicated and does not reflect the actual deployment environment of the protocol in the current state of the art. Simulation software provides scalability and can simulate complicated scenarios, however, there are times when it is not possible to use simulations due to a lack of support for new technologies or simulation scenarios. Therefore, this paper proposes a formal method and analytical model for evaluating the performance of security protocols using applied pi-calculus and Markov Chain processes. It interprets algebraic processes and associates cryptographic operatives with quantitative measures to estimate and evaluate cryptographic costs. With this approach, the protocols are presented as processes using applied pi-calculus, and their security properties are an approximate abstraction of protocol equivalence based on the verification from ProVerif and evaluated using analytical and simulation models for quantitative measures. The interpretation of the quantities is associated with process transitions, rates, and measures as a cost of using cryptographic primitives. This method supports users’ input in analysing the protocol’s activities and performance. As a proof of concept, we deploy this approach to assess the performance of security protocols designed to protect large-scale, 5G-based Device-to-Device communications. We also conducted a performance evaluation of the protocols based on analytical and network simulator results to compare the effectiveness of the proposed approach.