Investigating formal representations of PIN block attacks
Eirini Kaldeli · 2007
Abstract Financial security APIs control the use of tamper-proof hardware security mod-ules (HSMs) that are used in cash machine networks. The idea is that the APIkeeps the system secure even from corrupt insiders. Recently, several attacks havebeen found on these APIs, attracting the attention of formal methods researchersto the area. One family of attacks involves cracking PIN values by tweaking in-puts to API functions away from their usual values and watching for errors. Theseso-called “PIN block attacks” affect many APIs. A framework has been proposedfor modelling them as Markov Decision Processes, and analysing the resultingmodels using probabilistic model checking, in order to asses how vulnerable anAPI configuration is. One problem of this framework is that the models producedare very large, and thus it often takes considerable time to analyse them.The objective of this thesis is to investigate and implement alternative waysof representing the models of PIN block attacks, aiming at increasing their com-pactness, and consequently making their analysis more efficient in terms of timeand memory requirements. The great amount of symmetry inherent in the modelis one of the main characteristics that will draw our attention, since it is respon-sible for a lot of redundant operations. We experiment with our approaches ona number of different security API configurations, and evaluate the results. Weargue that the efficiency of the probabilistic model checker depends on a numberof issues, that should be taken into account during the modelling of real-worldsystems, in order to achieve faster performance and avoid memory overloads.iii