A system for analysing PIN-processing APIs for PIN recovery attacks.
You can download AnaBlock version 0.11. Look at the README file for installation instructions, and an explanation of what's in the directory.
To run AnaBlock, you need SICStus Prolog. To analyse the models, you need PRISM version 3.0. Both SICStus and PRISM should run on MS windows, but I have only tested the system running under GNU/Linux.
The journal paper describing AnaBlock is available from my publications page. An more informal presentation can be found on the PRISM case-studies page.
Thanks for your interest in AnaBlock.
Please email bug reports, queries etc. to: graham dot steel at ed dot ac dot uk.