other languages are known to be regular, and decision properties. The latter are algorithms to answer questions about automata or regular expressions, e.g., whether two automata or expressions represent the same language.

2.1 An Informal Picture of Finite Automata

In this section, wc shall study an extended example of a real-world problem whose solution uses finite automata in an important role. We investigate protocols that support electronic: money files that a customer can use to pay for goods on the internet, and that the seller can receive with assurance that the money is real. The seller must know that the file has not been forged, nor has it been copied and sent to the seller, wlnle the customer retains a copy of the same file to spend again.

The nonforgeability of the file is something that must be assured by a bank and by a cry])tograpliy policy. That is, a third player, the bank, must issue and encrypt the money files, so that forgery is not a problem. However, the bank has a second important job: it must keep a database of all the valid money that it has issued, so that it can verify to a store that the file it has received represents real money and can be credited to the stores account. We shall not address the cryptographic aspects of the problem, nor shall we worry about how the bank can store and retrieve what could be billions of electronic dollar bills. These problems are not likely to represent long-term impediments to the concept of electronic money, and examples of its small-scale use have existed since the late 1990s.

However, in order to use electronic money, protocols need to be devised to allow the manipulation of the money in a variety of ways that the users want. Because monetary systems always invite fraud, we must verify whatever policy we adopt regarding how money is used. That is, we need to prove the only things that can happen are things we intend to liappen - things that do not allow an unscrupulous user to steal from others or to manufacture money. In the balance of this section, wc shall introduce a very simple example of a (bad) electronic-money protocol, model it with finite automata, and shoлv how constructions on automata can be used to verify protocols (or, in this case, to discover that the protocol has a bug).

2.1.1 The Ground Rules

There are tliree participants; the customer, the store, and the bank. We assume for simplicity that there is only one money file in existence. The customer may decide to transfer this money file to the store, which will then redeem the file from the bank (i.e., get the bank to issue a new money file belonging to the store rather than the customer) and ship goods to the customer. In addition, the customer has the option to cancel the file. That is, the customer may ask the bank to place the money back in the customers account, making the money

no longer spendable. Interaction among the three participants is thus hmited to five events:

1. The customer may decide to pay. That is, the customer sends the money to the store.

2. The customer may decide to cancel. The money is sent to the bank with a message that the value of the money is to be added to tlie customers bank account.

3. The stort; may ship goods to the customer.

4. The store may redeem the money. That is, the money is sent to the bank with a request that its value be given to the store.

5. The bank may transfer the money- by creating a new, suitably encrypted money file and sending it to the store.

2,1.2 The Protocol

The three participants must design their behaviors carefully, or the wrong things may happen. In our example, we make the reasonable assumption that the customer cannot be relied upon to act responsibly. In particular, the customer may try to c!Opy the money file, use it to pay several times, or both pay and cancel the money, thus getting the goods for free.

The bank must behave responsibly, or it cannot be a bank. In particular, it must make sure that two stores cannot both redeem the same money file, and it must not allow money to be both canceled and redeemed. The store should be careful as well. In particular, it should not ship goods until it is sure it has been given valid money for the goods.

Protocols of this type can be represented as finite automata. Each state represents a situation that one of the participants could be in. That is, the state remembers that certain important events have happened and that others have not yet happened. Transitions between states occur when one of the five events described above occur. We shall think of these events as external to the automata representing the three participants, even though each participant is responsible for initiating one or more of the events. It turns out that what is important about the problem is what sequences of events can happen, not who is allowed to initiate them.

Figure 2.1 represents the three participants by automata. In that diagram, we show only the events that affect a participant. For example, the action pay affects only the customer and store. The bank does not know that the money has been sent by the customer to the store; it discovers that fact only when the store executes the action redeem.

Let us examine first the automaton (c) for the bank. The start state is state 1; it represents the situation where the bank has issued the money file in question but has not been requested either to redeem it or to cancel it. If a

Start pay . redeem. transfer.

(a) Store

redeem transfer

cancel

cancel

redeem transfer

Start

Start

(b) Customer (c) Bank

Figure 2.1: Finite automata representing a customer, a store, and a bank

cancel request is sent to the bank by the customer, then the bank restores the money to the customers account and enters state 2, The latter state represents the situation where the money has been cancelled. The bank, being responsible, will not leave state 2 once it is entered, since tlie bank must not allow the same money to be cancelled again or spent by the customer.

Alternatively, when in state 1 the bank may receive a redeem request from the store. If so, it goes to state 3, and shortly sends the store a trans/er message, with a new money file that now belongs to the store. After sending the transfer message, the bank goes to state 4. In that state, it will neither accept cancel or redeem requests nor will it perform any other actions regarding this particular money file.

Now-, let us consider Fig. 2.1(a), the automaton representing the actions of the store. While the bank always does the right thing, the stores system has some defects. Imagine that the shipping and financial operations are done by

You should remember that this entire discussion is about one single money file. The bank will ill fact be running the same protocol with a large number of electronic pieces of money, but the workings of the protocol are the same for each of them, so we can discuss the problem as if there were only one piece of electronic money in existence.