Formal analysis of the WAP Class 2 Wireless Transaction Protocol has
revealed several inconsistencies in the specification. These are
explained, and where possible, changes to the specification are
proposed to improve the protocol. The inconsistencies are: 1. The
counter RCR may be incremented to a value greater than RCR MAX; 2. Two
TR-Invoke.cnf primitives can be delivered to the Initiator user
(within the context of one transaction); 3. The TR-Result.req
primitive may immediately follow a TR-Invoke.ind primitive at the
Responder user when User Acknowledgement is on; 4. A transaction may
be aborted without the Responder user being notified; 5. The semantics
of Abort transaction in the state tables is not defined. Changes to
the state tables are proposed to remedy the first 4 problems. A
definition is required in the text for the final
problem. Typographical errors in the state tables are also pointed
out.