Anonymous and secure electronic transaction protocol

We present a new protocol for electronic transactions which is not only secure but also anonymous, the latter characteristic being obtained by associating an encryption device with a chip card. Security is ensured by the use of encryption, electronic signature and authentication. In order to check the validity of the security properties enforced by the protocol, a model and a specification are provided. The protocol modeling language is a process algebra with value passing extended by an observation mechanism allowing the specification of security levels, by cryptographic primitives, and by a function call feature on private channels allowing the modeling of interactions with the crypto-system. The anonymity is expressed by an information flow property. The verification method, based on cosimulation, is proved consistent and complete and analysis confirms that this approach ensures not only anonymity (thanks to the fact that the client never discloses to the merchant any information permitting his identification), but also the quasi-impossibility of any fraudulent transaction.