Bart Jacobs, and Ronny Wichers Schreur. Logical Formalisation and Analysis of the Mifare Classic Card in PVS. Technical report: ICIS-R10002, March, Radboud University Nijmegen, 2010.
The way that Mifare Classic smart cards work has been uncovered recently [2,4] and several vulnerabilities and exploits have emerged. This paper gives a precise logical formalisation of the essentials of the Mifare Classic card, in the language of a theorem prover (PVS). The formalisation covers the LFSR, the filter function and (parts of) the authentication protocol, thus serving as precise documentation of the card`s ingredients and their properties. Additionally, the mathematics is described that makes two key-retrieval attacks from  work.