Modelling Attacker with Deciding Security Properties by Induction and Deduction

Formal methods for verifying cryptographic protocols are used to assist in ensuring that authentication protocols meet their specifications. Model checking techniques such as CSP and FDR checker, are widely acknowledged for effectively and efficiently revealing flaws in protocols faster than most other contemporaries. Essentially, model checking involves a detailed search of all the states reachable by the components of a protocol model. In the models that describe authentication protocols, the components, regarded as processes, are the principals including intruder (attacker) and parameters for authentication such as keys, nonces, tickets, and certificates. In this paper, transactions of proposed protocol models rely on trusted three-way authentication mechanisms while intruder capabilities are based on possible inductions and deductions of sequential processes. This research attempts to combine the two methods in model checking in order to realise an abstract description of intruder with enhanced capabilities.