24-09-2016, 11:59 AM
1456053730-javaring.pdf (Size: 337.24 KB / Downloads: 7)
Abstract
N-Count is a system for oine value transfer. A prototype of an N-Count payment system has
been designed, and it has been implemented in Java. We have used the Java Ring with the Java
Card API as a secure device. The system has also been modelled using the Spin model checker. The
combined prototyping and model checking has made it possible to investigate safety properties of the
prototype, both formally and intuitively. Because of this model building activity, problems have been
identied and solved before an actual system has been built.
1 Introduction
N-Count [5] is an electronic value transfer system that can be used for fast payments with a secure purse.
The payments are secure, o-line and inexpensive. Like in all electronic payment systems [14], there are
three entities in an N-Count based payment system: the purse provider, the terminal and the purse. Value
is transferred between these entities by the use of N-Counters. The role of the purse provider is to load
the purse, and to clear N-Counters received from the terminal. The role of the terminal is to ask the purse
to (re-)value N-Counters during payment.
An N-Count purse stores the balance of its user as well as secret keys. The N-Count protocol and
an appropriate cryptographic one-way function ensure that the balance is increased (load) or decreased
(pay) as appropriate for the transactions made by the user. An implementation that oers overall security
therefore imposes three main requirements: (1) the device should be tamper resistant (to protect the
balance and the keys) and it should be based on a correct design and implementation of (2) the one-way
function and (3) the protocol.
Our ultimate aim is to design and build a system that satises all three requirements. As a rst step
towards achieving this goal we set out to build a prototype aimed at investigating the third aspect: the
study of the protocols. The present paper reports on this rst step.
To make a realistic prototype we used a Java Ring, with the Java Card API. The ring provides battery
powered, active tamper resistance, which we would expect to oer better security than a typical smart
card. The Java Card API oers an implementation of SHA-1 [15, Section 18.7] that is appropriate for use
as a one way function. We believe it to be a reasonable assumption (at least for now) that the Java Ring
and Java Card together satisfy our requirements (1) and (2) above. Therefore, we proceed to investigate
requirement (3), the correctness of the protocols in the prototype on this basis.
Model checking [11] is a technique that checks whether a state machine satises certain properties. In
the present context, the model describes the N-Count protocol, as well as the state of the three parties,
upon which the protocols act. A model is then an assignment of values to the components of the state.
Model checking veries that only states arise that are correct in some sense. We use the gold standard
model checker, SPIN [12], which uses a CSP like [10] notation for describing protocols, and a C-like
description of the state components and operations on the state components.
Using such a tool allows an appropriate formal model to be animated with relative ease. This helps
designers and programmers to understand what the system should do.
A formal model is unambiguous and it may therefore be used as a contract (at an appropriate level
of detail) between designers and programmers. A SPIN model is relatively easy to understand by a
good programmer.
A formal model can be used to state and verify that the system under consideration has certain desirable
properties (such as the conservation of electronic money, and guarantee of authentication). It
is also possible to prove the absence of undesirable properties (such as the whether certain deadlocks
may occur). Stating and proving properties requires some special training.
Our model is particularly useful as a contract between the customer who needs an N-count payment
system, and the engineer who designs and implements the system. The engineer can animate the
model, and show the animations to the customer to conrm the engineer's understanding of the
customer's intentions. This gives the engineer a deep understanding of the system requirements and
oers the customer increased condence in the product.
The next section discusses related work. In Section 3, we review the N-Count protocol. A summary of
the design and implementation of our prototype follows in Section 4. Section ?describes the SPIN model
of our system.In Section 6 we give the results from our modelling activity. The last section concludes.
2 Related work
Electronic payment systems have been proposed for various dierent purposes. The main driver in the
design of current systems is the cost of value transfer, which should be considerably lower than the `real'
value transferred. At one end of the spectrum micro payment systems, such as BT's Quickpay [9] avoid
cryptographic calculations and support even o line payments (but less securely so than on-line payments).
At the other extreme, systems such as the Inter-sector Electronic Purse (IEP) [6] dene complex transactions
aimed at mainly large value transfers. It is probably fair to say that most attention has been paid
to the security of the cryptography [15, pages 65-68]. Less attention has been paid to creating provably
correct implementations of such systems. An exception is the work of Anderson and Bezuidenhoudt, who
describe a design and implementation of an electronic pre-payment system for electricity meters [3]. The
success of their approach is attributed to the use of a simple, specialised logic [2] (an extension of BAN [4]
logic). Currently part of the executive card software for the Mondex electronic purse is in the process of
being evaluated at ITSEC level 6 [13], which implies the use of some formal method during the evaluation.
In previous work we have built a formal model of Quickpay [8], which enabled us to prove properties
of the protocol. Our model of the IEP [7] was geared towards animating and studying the protocol. Both
eorts helped to gain a better understanding of implementation choices for the security of the system.
The present paper complements our research portfolio in that it uses model checking, which in a sense
combines animation and automatic theorem proving.
3 N-Count protocol
An N-Counter is made up of a sequence of values X0; X1; : : :Xn. Here X0 represents the maximum value
possible: X0 is worth n u units. The actual value of a unit u can be decided as appropriate, and it may
dier between N-Counters. Xn represents the minimum value possible (i.e. 0 units).
The purse contains a secret key, k, and two functions, f and g. The most important is the one-way
function f , which is used to de-value an N-Counter. A block cipher or hash function like SHA-1 [15,
Section 18.7] can be used for f . The other function g, is used to create an initial N-Counter. It is quite
possible to implement g and f with same cryptographic algorithm. Table 1 shows the values in an NCounter,
initially created by an application of g at full value, and subsequently de-valued by repeated
applications of f .
Associated with every N-Counter is a unique random number r. To support more than one terminal
in the system, each N-Counter is related to a terminal identier t. In practice t and r may be combined
as an optimisation, but this does not concern us here.
X0 is generated by g(u; r; t; n; k) as can be seen at the top of Table 1. f n
(g(u; r; t; n; k); k) is evaluated
to get Xn, where the notation hn
(x) = h(hn1
(x)). The essential idea of the N-Count protocol is thus
that a counter is de-valued simply by applying the one-way function f . To re-value an N-Counter one has
to start from the beginning, (using g and the secret key k, etc.) and then to de-value as required.
The purse provider knows everything (f , g, u, r, n, t and k) for all N-Counters, terminals and purses.
The purses are trusted, but the terminals need not be trusted as they can not steal, reuse or generate any
values or N-Counters.
The purpose of the N-Count protocol is to pass N-Counters around and to authenticate them. Figure 1
shows some of the messages as they might be exchanged in the N-Count protocol. The first message,