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.
J. Kwisthout. Two new notions of abduction in Bayesian networks. Technical report: ICIS-R10005, November, Radboud University Nijmegen, 2010.
Most Probable Explanation and (Partial) MAP are well-known problems in Bayesian networks that correspond to Bayesian or probabilistic inference of the most probable explanation of observed phenomena, given full or partial evidence. These problems have been studied extensively, both from a knowledge-engineering starting point (see  for an overview) as well as a complexity-theoretic point of view (see  for an overview). Algorithms, both exact and approximate, are studied in e.g. [21, 25, 19, 28]. In this paper, we introduce two new notions of abduction-like problems in Bayesian networks, motivated from cognitive science, namely the problem of finding the most simple and the most informative explanation for a set of variables, given evidence. We define and motivate these problems, show that these problems are computationally intractable in general, but become tractable when some particular constraints are met.
J. Kwisthout. Most Probable Explanations in Bayesian Networks: complexity and tractability. Technical report: ICIS-R10001, March, Radboud University Nijmegen, 2010.
An overview is given of definitions and complexity results of a number of variants of the problem of probabilistic inference to the most probable explanation of a set of hypotheses given observed phenomana.
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.