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.%Nous présentons un nouveau protocole de transaction électronique sécuritaire et surtout anonyme par l'association d'un logiciel de cryptage et d'une carte à puce. La sécurité du protocole est assurée par l'utilisation des techniques cryptographiques telles que le chiffrement, la signature électronique et l'authentification. En vue de s'assurer que les propriétés de sécurité que le protocole doit assumer sont vérifiées, un modèle du protocole et une spécification de l'anonymat sont donnés. Le langage de modélisation du protocole est une algèbre de processus avec passage de paramètres par valeur étendue d'un mécanisme appelé observation permettant de spécifier des niveaux de sécurité, de primitives cryptographiques et d'un mécanisme d'appel de fonction sur des canaux privés permettant la modélisation de l'interaction avec le crypto-système. L'anonymat est exprimé comme une propriété de flot d'information. La méthode de vérification, basée sur la cosimulation, est cohérente et complète. L'analyse confirme que l'anonymat est assuré par le fait que le client ne révèle au marchand aucune information pouvant l'identifier tout en garantissant la quasi-impossibilité d'une fraude.