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.
Wojciech Mostowski, and Erik Poll. Electronic Passports in a Nutshell. Technical report: ICIS-R10004, June, Radboud University Nijmegen, 2010.
This document tries to give concise, (semi)formal specifications for the second generation electronic passports as used by most EU countries, and for the closely related ISO18013 standard for electronic driving licenses. We developed these specifications as a follow-up to making open source Java Card implementations of these standards. Our aim is to provide useful information - implicit in the official specification, but crucial for the overall security - in a simple format that could be useful to anyone implementing these standards, performing security tests, or doing code reviews. More generally, we want to explore useful formats for rigorously specifying the typical complex combinations of security protocols that arise in real applications. In particular, we provide state diagrams which describe the state that are largely implicit in the official specifications, but which have to be explicit in any implementation, and which also provide a basis for systematic model-based testing.
Olha Shkaravska, and Marko van Eekelen. Univariate Polynomial Solutions of Nonlinear Polynomial Recurrence Relations. Technical report: ICIS-R10003, April, Radboud University Nijmegen, 2010.
Revised Version August 2013. Contrary to linear difference equations, there is no general theory of difference equations of the form G(P(x ? ?1),...,P(x ? ?s)) + G0(x)=0, with ?i ? K, G(x1,...,xs) ? K[x1,...,xs] of total degree D ? 2 and G0(x) ? K[x], where K is a field of characteristic zero. This article is concerned with the following problem: given ?i, G and G0, find an upper bound on the degree d of a polynomial solution P(x), if it exists. In the presented approach the problem is reduced to constructing a univariate polynomial for which d is a root. The authors formulate a sufficient condition under which such a polynomial exists. Using this condition, they give an effective bound on d, for instance, for all difference equations of the form G(P (x ? a), P (x ? a ? 1), P (x ? a ? 2)) + G0(x) = 0 with quadratic G, and all difference equations of the form G(P(x),P(x ? ?)) + G0(x) = 0 with G having an arbitrary degree.