Detection of Data Breaches in Banking Transaction Processes

Organisation:	CNR-IIT (ITALY) CNR-IAC (ITALY) University of Molise (ITALY) University of Pisa (ITALY)
Method:	AUT XES
Tools used:	CADP (Construction and Analysis of Distributed Processes) ProM (Process Mining Workbench)
Domain:	Banking
Period:	2018
Size:	up to 434,073 states and 444,071 transitions
Description:	Usually, formal verification is applied to abstract models of a system, which might differ from the real implementation written in some programming language. To bridge this gap between the implementation and the model used for verification, the authors suggest to retrieve the formal model from concrete execution traces. Concretely, the authors proceed in three steps: gather execution traces in the XES (eXtensible Event Stream) format using an appropriately instrumented version of the application; construct an LTS (Labelled Transition System) using the ProM (Process Mining Workbench) tools, which implements model-learning techniques; model-check properties on the LTS using CADP; this step requires the conversion of the LTS into the AUT format. The approach is illustrated on a banking transaction process taken from the ProM database (thus the first step is skipped). This process contains various monetary checks, authority notifications, and logging, as required by the current economic environments. The authors focus on the property, that "serial numbers [of transactions] must be compared with an external database governed by a recognized international authority". This property has been expressed as a mu-calculus formula, plus eight additional properties, expressing preconditions of the original property, so as to provide more insights in the reason of an error. For each of four scenarios, 2000 LTSs were extracted, and for each of two additional scenarios, 10,000 LTSs were extracted. Then, all nine mu-calculus formulae were checked using CADP, counting, for each property, the number of LTSs were the property was not valid. This allowed to distinguish between correct and incorrect scenarios.
Conclusions:	The proposed combination of process mining and model checking was found a promising approach to bridge the gap between formal verification on abstract models and a concrete implementation.
Publications:	[Martinelli-Mercaldo-Nardone-et-al-18] Fabio Martinelli, Francesco Mercaldo, Vittoria Nardone, Albina Orlando, Antonella Santone, and Gigliola Vaglin. "Safety Critical Systems Formal Verification using Execution Traces". Proceedings of the 27th IEEE International Conference on Enabling Technologies: Infrastructure for Collaborative Enterprises (WETICE 2018), Paris, France, pages 247-250, IEEE, June 2018. Available on-line at: http://doi.org/10.1109/WETICE.2018.00054 or from the CADP Web site in PDF or PostScript
Contact:	Fabio Martinelli Istituto di Informatica e Telematica - IIT Area della Ricerca CNR di Pisa Via. G. Moruzzi 1 56124 Pisa, Italy Tel: +39 (0)50 315 3425 Fax: +39 (0)50 315 2593 E-mail: fabio.martinelli at iit.cnr.it
Further remarks:	This case-study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies

Back to the CADP case studies page