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.
