The VIP Approach for the Formal Verification of Electronic Commerce Protocols
by Dominique Bolignano
The VIP (Verified Internet Protocols) Project is a consortium of academic and industrial research teams whose aim is to develop tools and formal validation studies in the domain of the certification of secure communication protocols and architectures relevant to the Internet and Web technologies. The project is defined as a 3-year programme which has started in January 1996. The VIP Project is part of Dyade GIE, a Bull/INRIA Advanced Research Joint Venture. It involves the four INRIA research teams Coq, Lande, Cristal and Eureca, and a Bull team.
The VIP project has two main activities. One is the formal verification of cryptographic protocols. The other is concerned with formal method based evaluations of security architectures mainly in the context of mobile code (ie code downloading, Java based architectures, Javacard architecture, etc). In the sequel we focus on the first activity whose aim is to provide help in the design or evaluation of electronic commerce protocols.
Many electronic commerce protocols ie SET, C-SET, GlobeID, etc, have indeed been proposed recently to meet the demand for secure access for electronic shopping. Such protocols mainly use encryption and decryption functions to achieve security requirements. But the design of a cryptographic protocol is a difficult and error-prone task, and many popular and largely used cryptographic protocols have been shown to have flaws. For this reason the use of formal methods that are capable of verifying such protocols in a systematic and formal way has received increasing attention.
The VIP Project has developed its own approach to the formal verification of cryptographic protocols. The approach is based on the use of general purpose formal methods. It is complementary with modal logic-based approaches as it allows for a description of protocols, hypotheses and authentication properties at a finer level of precision and with more freedom. It uses a clear separation between the modeling of reliable agents and that of unreliable agents. It allows to express and verify very sophisticated properties. The formal verification is done using the Coq proof environment.
The approach has been applied successfully for expressing very elaborate properties in the context of electronic commerce protocols. The approach has been in particular applied under commercial contracts such as for the formal verification the C-SET (Chip-Secure Electronic Transactions) protocol, developed by the French Groupement des Cartes Bancaires CB, a joint venture, to implement, coordinate and promote inter-banking of bank cards acceptance (http://www.cardshow.com/eft/ CartesBancaires/about.html). This architecture allows for the payment of goods and services on the Internet using the smartcard technology, already in use with 25 millions CB payment cards, together with the SET protocol.
Another more recent but important use of formal verification within the VIP project is within the framework of a security evaluation (namely ITSEC, the Information Technology Security Evaluation Criteria). VIP is in particular currently participating in an ITSEC evaluation under a commercial contract. Formal models and verifications are of course provided as part of the required documents (eg the formal policy model). But the expression of properties as well as the precise identification of the hypotheses can also be used as a help in the carrying out of other tasks such as the identification of security target of evaluation, the design vulnerability analysis, etc. Such possible uses are currently under experimentation. Further information on the VIP project at: http://www.dyade.fr/actions/VIP/vip.html
Please contact:
Dominique Bolignano - INRIA/DYADE
Tel: + 33 1 39 63 58 72
E-mail: Dominique.Bolignano@dyade.fr
SET: the Secure Electronic Transaction (SET) protocol has been jointly developed by Visa and MasterCard as a method to secure payment card transactions over open networks. It is supported by GTE, IBM, Microsoft, Netscape, SAIC, Terisa, and Verisign...
C-SET: the Chip Secure Electronic Transaction (C-SET) developed by GIE Cartes Bancaires is a smartcard based secure payment card transactions over open networks.
Globe-ID: GlobeID Payment system allows electronic payments over the Internet for goods or services with prices from 1 cent (micropayment) to thousands of dollars.