Name
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. |
Year | Venue | Keywords |
|---|---|---|
2011 | ITP | authentication protocol,precise logical formalisation,mifare classic card,precise documentation,key-retrieval attack,theorem prover,filter function,mifare classic smart card,smart card |
Field | DocType | Citations |
Linear feedback shift register,Programming language,Computer science,Automated theorem proving,Algorithm,Smart card,Exploit,Authentication protocol,Filter (function),Documentation | Conference | 2 |
PageRank | References | Authors |
0.37 | 9 | 2 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| B. Jacobs | 1 | 1046 | 100.09 |
| Ronny Wichers Schreur | 2 | 144 | 12.34 |