Abstract
The way that Mifare Classic smart cards work has been uncovered recently [6,8] 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 [6] work. © 2011 Springer-Verlag.
Cite
CITATION STYLE
Jacobs, B., & Wichers Schreur, R. (2011). Logical formalisation and analysis of the Mifare classic card in PVS. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 6898 LNCS, pp. 3–17). https://doi.org/10.1007/978-3-642-22863-6_3
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
