Informatics Report Series



Related Pages

Report (by Number) Index
Report (by Date) Index
Author Index
Institute Index

Title:Formal Analysis of PIN Block Attacks
Authors: Graham Steel
Date:Nov 2006
Publication Title:Theoretical Computer Science Volume 367, Issues 1-2 , 24 November 2006,
Publication Type:Journal Article Publication Status:Published
Volume No:367 Page Nos:257-270
PIN blocks are 64-bit strings that encode a PIN ready for encryption and secure transmission in banking networks. These networks employ tamper proof hardware security modules (HSMs) to perform sensitive cryptographic operations, such as checking the correctness of a PIN typed by a customer. The use of these HSMs is controlled by an API designed to enforce security. PIN block attacks are unanticipated sequences of API commands which allow an attacker to determine the value of a PIN in an encrypted PIN block. This paper describes a framework for formal analysis of such attacks. Our analysis is probabilistic, and is automated using constraint logic programming and probabilistic model checking.
Links To Paper
(C) Elsevier
2nd Link
Bibtex format
author = { Graham Steel },
title = {Formal Analysis of PIN Block Attacks},
journal = {Theoretical Computer Science Volume 367, Issues 1-2 , 24 November 2006,},
publisher = {Elsevier},
year = 2006,
month = {Nov},
volume = {367},
pages = {257-270},
doi = {doi:10.1016/j.tcs.2006.08.042},
url = {},

Home : Publications : Report 

Please mail <> with any changes or corrections.
Unless explicitly stated otherwise, all material is copyright The University of Edinburgh