Formal Verification of Secure Evidence Collection Protocol using BAN Logic and AVISPA

The effect of digitization has led to an increased dependency on the internet. At the same time, cyber-attacks are on the rise due to this increased digitization. In cybercrime cases, digital evidence is of utmost importance. The forensic investigation process always begins after the incident occurred, by that time intelligent attackers got enough time to destroy the traces. This paper proposes a prior evidence capture protocol, that will help in the simultaneous collection of evidence when the crime has occurred. This collected evidence is in the form of device fingerprint which will uniquely identify the fingeprintee client device. In the future, if the dispute arises these prior captured device fingerprints can be used as legal evidence and help in the process of forensic investigation. The proposed protocol uses the concept of a trusted time stamping server (TTSS) to prove the integrity and nonrepudiation of the collected evidence. The timestamps are attached by the trusted third party TTSS with all collected evidence, these timestamps cannot be changed by local client devices. The paper also provides security validation of the proposed protocol by using Burrows Abadi Needham (BAN) logic. The formal verification is also done by using the AVISPA tool. The results of AVISPA shows that the proposed protocol is safe under OFMC and Cl-AtSe model. (C) 2020 The Authors. Published by Elsevier B.V.