Event Based Formalization of Communication Properties for an E-Commerce Protocol: An Event-B Approach

Abstract:

The objective of this paper aims at modeling and analysis of communication properties of an E-commerce protocol with the Event-B language. NetBill protocol is developed for selling and buying of information and goods through the Internet. In this approach, we have used Event-B as proof-based development method which integrates proof techniques for writing specifications and building the model systematically using refinement, the key point is to start with a very abstract model of the system under development. Step by step details are added to this first model by building a series of more concrete ones. This strategy eases the proof of the correctness of requirements because only a small number of proof obligations are generated at each step. The aims are constructing a model with a clear and accurate formulation of the communication protocol properties and discharge of all proof obligations. The outcome of this procedure was that we achieved a very high degree of automatic proof. We reached a good degree of automatic proof. All interactive proofs involved a small number of steps and were straightforward to reach.

• Periodical: International Journal of Engineering Research in Africa (Volume 37)
• Pages: 78-90
• DOI: https://doi.org/10.4028/www.scientific.net/JERA.37.78
• Online since: August 2018
• Authors: Sanae El Mimouni*, Mohamed Bouhdadi
• Keywords: Event-B, Formal Modeling, Netbill Protocol, Refinement, Rodin

References

[1] Alistair Kelman. Secure electronic transactions - introduction and technical reference by loeb l. (1998). Journal of Information, Law and Technology, 1998(2), (1998).

[2] Sanae El Mimouni and Mohamed Bouhdadi. An incremental proof-based process of the netbill electronic commerce protocol. In Networked Systems - 4th International Conference, NETYS 2016, Marrakech, Morocco, May 18-20, 2016, Revised Selected Papers, pages 209-213, (2016).

DOI: 10.1007/978-3-319-46140-3_17

[3] Edmund M. Clarke and Jeannette M. Wing. Formal methods: State of the art and future directions. ACM Comput. Surv., 28(4):626-643, (1996).

DOI: 10.1145/242223.242257

[4] Mauricio Papa, Oliver Bremer, John Hale, and Sujeet Shenoi. Formal analysis of e-commerce protocols. In Fifth International Symposium on Autonomous Decentralized Systems, ISADS 2001, Dallas, Texas, USA, March 26-28, 2001, pages 19-28, (2001).

DOI: 10.1109/isads.2001.917391

[5] Shiyong Lu and Scott A. Smolka. Model checking the secure electronic transaction (set) protocol. In MASCOTS, pages 358-364, (1999).

[6] Michael Butler and Divakar Yadav. An incremental development of the mondex system in eventb. Formal Aspects of Computing, 20(1):61-77, January (2008).

DOI: 10.1007/s00165-007-0061-4

[7] J. R. Abrial. Modeling in Event-B: System and Software Engineering. Cambridge University Press, (2010).

[8] J. R. Abrial. The B-book: assigning programs to meanings. Cambridge University Press, New York and NY and USA, (1996).

[9] Thierry Lecomte. Safe and reliable metro platform screen doors control/command systems. In Jorge Cuéllar, T. S. E. Maibaum, and Kaisa Sere, editors, FM, volume 5014 of Lecture Notes in Computer Science, pages 430-434. Springer, (2008).

DOI: 10.1007/978-3-540-68237-0_32

[10] S. Gerhart, D. Craigen, and T. Ralston. Case study: Paris metro signaling system. IEEE Software, 11(1):32-28, Jan (1994).

DOI: 10.1109/ms.1994.1279941

[11] Willem P. De Roever and Kai Engelhardt. Data Refinement: Model-oriented Proof Theories and their Comparison, volume 46 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, (1998).

[12] Jean Raymond Abrial, Michael J. Butler, Stefan Hallerstede, Thai Son Hoang, Farhad Mehta, and Laurent Voisin. Rodin: an open toolset for modelling and reasoning in event-b. STTT, 12(6):447- 466, (2010).

DOI: 10.1007/s10009-010-0145-y

[13] J. R. Abrial. Summary of Event-B proof obligations, 2008 (accessed June 30,2017). http://www.docstoc.com/docs/7055755.

[14] Event-B and RODINs, (accessed July 20, 2017). http://wiki.event-b.org/index.php/MainPagef.

[15] Max Breitling and Jan Philipps. Transitions into Black Box Views -The NetBill Protocol Revisited-. Technical report, Institut fur Informatik Technische Universitat Munchen, (2000).