Determining a parallel session attack on a key distribution protocol using a model checker
Vladimir Paşca, Anca Delia Jurcut, Reiner Dojen, Tom Coffey · 2008
The use of security protocols to protect sensitive information is critical. However, flaws in the design of security protocols can make them ineffective. This paper discusses various attacks against security protocols that exploit weaknesses in their design and a key-distribution protocol is analysed using a model checker. The analysis reveals weaknesses in the protocol, which can be exploited in a parallel session attack that allows an attacker to impersonate a legitimate principal. Correction to the protocol are proposed and a formal analysis of the fix is presented. The results of this analysis provide confidence in the correctness and effectiveness of the proposed corrected protocol.