References

The first generation of European e-passports will be issued in 2006. We discuss how borders are crossed regarding the security and privacy erosion of the proposed schemes, and show which borders need to be crossed to improve the security and the privacy protection of the next generation of e-passports. In particular we discuss attacks on Basic Access Control due to the low entropy of the data from which the access keys are derived, we sketch the European proposals for Extended Access Control and the weaknesses in that scheme, and show how fundamentally different design decisions can make e-passports more secure.

RIES stands for Rijnland Internet Election System. It is an online voting system that has been used twice in the fall of 2004 for in total over two million potential voters. In this paper we describe how this system works. Furthermore we describe how the system allowed us to independently verify the outcome of the elections-a key feature of RIES. To conclude the paper we evaluate possible threats to this system and describe some possible points for improvement.

This paper discusses an ambiguity in Sun's specification of the Java Card platform, which we noticed in the course of developing the precise formal description of the Java Card transaction mechanism presented in [HP03]. The ambiguity concerns the Java Card transaction mechanism, more in particular the interaction of the transaction mechanism and two Java Card API methods, the methods arrayCopyNonAtomic and arrayFillNonAtomic in the class javacard.framework.Util. The paper also describes the experiments we performed with smartcards of two different manufacturers to find out the behaviour actually implemented on these card. Interestingly, these experiments revealed some unexpected (and unexplainable) behaviour of these two methods on some cards.

This paper describes a case study in refining an abstract security protocol description down to a concrete implementation on a Java Card smart card. The aim is to consider the decisions that have to be made in the development of such an implementation in a systematic way, and to investigate the possibilities of formal specification and verification in the design process and for the final implementation.

The Java dialect Java Card for programming smartcards contains some features which do not exist in Java. Java Card distinguishes persistent and transient data (data stored in EEPROM and RAM, respectively). Because power to a smartcard can suddenly be interrupted by a so-called card tear, by someone removing the smartcard from the reader, Java Card provides a notion of transaction to ensure that updates of multiple fields in persistent memory can be performed atomically. This paper describes a way to reason about these Java Card specific language features.

The Java dialect Java Card for programming smartcards contains some features which do not exist in Java. Java Card distinguishes persistent and transient data (data stored in EEPROM and RAM, respectively). Because power to a smartcard can suddenly be interrupted by a so-called card tear, by someone removing the smartcard from the reader, Java Card provides a notion of transaction to ensure that updates of multiple fields in persistent memory can be performed atomically. This paper describes a way to reason about these Java Card specific language features.

In this paper we describe our findings after integrating several tools based upon the Java Modeling Language (JML), a specification language used to annotate Java programs. The tools we consider are Daikon, ESC/Java, JML runtime assertion checker, and Loop/PVS tool. The first one generates specifications; the others are used to verify them. We find that for the first three it is worthwhile to combine them because this is relatively easy and it improves the specifications. Combining Daikon and the Loop/PVS tool directly works in theory, but in practice it only works if the test suite is very good and hence it is not advisable.

This abstract provides some background information about the electronic voting experiment that is planned in the Netherlands for the European Elections of 2004, and about our own involvement in the infrastructure for this experiment. The talk will elaborate further about the computer security issues involved, especially with respect to the use of formal methods for vote counting software.

Back in 1994 Sergey Pinchuk has presented pairs of real polynomials in two variables that do have a nowhere vanishing Jacobian determinant but are not one-to-one. In this paper we examine a specific example F:=(P;Q) where deg(P)=10 and deg(Q)=25. We use a slightly modified version of the technique described by Bass, Connell and Wright to reduce this map to a cubic homogeneous map. Furthermore we transform this map into a cubic linear (or Druzkowski map) using the pairing-technique by Gorni and Zampieri. The result is an example in dimension 1999.

In this paper we explore two different methods to find a factorization of F^[m] by triangular automorphisms, showing that it is tame, for all F=X+H with H in H_n(A). Furthermore we give an explicit upperbound for this m in both methods.

In this paper we shall give a complete classification of all Druzkowski maps F:=X+(AX)³:k⁵->k⁵ for which J((AX)³) is nilpotent. Furthermore we use this classification to find all representatives of Meisters' cubic similarity relation in dimension five.

We show that the cubic linear polynomial automorphism F:C¹⁵->C¹⁵ given by Druzkowski has the property that for every λ>0 the dilation λF is not global analytic linearizable to its linear part.

In this paper we introduce a set, denoted by D_n(A), for every commutative ring A and every positive integer n. It is shown that the elements of this set can be used to give an explicit description of the class H_n(A). We deduce that each polynomial map of the form F=X+H with H in H_n(A) can be written as a finite product of automorphisms of the form exp(D), where each D is a locally nilpotent derivation satisfying D²(X_i)=0 for all i. Furthermore we deduce that all such F's are stably tame.

In this paper we present a new large class of polynomial maps F=X+H:Aⁿ->Aⁿ on every commutative ring A for which the Jacobian Conjecture is true. In particular H does not need to be homogeneous. We also show that for all H in this class satisfying H(0)=0 the n-th iterate Ho...oH=0.

We give a polynomial counterexample to both the Markus-Yamabe Conjecture and the discrete Markus-Yamabe problem for all dimensions >=3.

We give a polynomial counterexample to a discrete version of the Markus-Yamabe Conjecture and a conjecture of Deng, Meisters and Zampieri, asserting that if F:Cⁿ->Cⁿ is a polynomial map with det(JF) in C^*, then for all λ in R large enough λF is global analytic linearizable. These counterexamples hold in any dimension >=4.

Let H:kⁿ->kⁿ be a polynomial map. It is shown that the Jacobian matrix JH is strongly nilpotent if and only if JH is linearly triangularizable if and only if the polynomial map F=X+H is linearly triangularizable. Furthermore it is shown that for such maps F sF is linearizable for almost all s in k (except a finite number of roots of unity).