|||Laboratoire LABRI. Visidia, 2008 and 2010. http://www.labri.fr/projet/visidia/. [ bib ]|
|||Laboratoire LABRI. B2visidia, 2010. http://www.labri.fr/projet/visidia/. [ bib ]|
|||ClearSy. BART. http://www.clearsy.com, 2010. [ bib ]|
N. Benaïssa and D. Méry.
Cryptologic protocols analysis using Event B.
In Alexander Marchuk, editor, Seventh International Andrei
Ershov Memorial Conference PERSPECTIVES OF SYSTEM INFORMATICS, volume 5947.
Springer, 15-19 June 2010.
[ bib ]
Abstract. We consider the proof-based development of cryptographic protocols satisfying security properties. For instance, the model of Dolev- Yao provides a way to integrate a description of possible attacks, when designing a protocol. We use existing protocols and want to provide a systematic way to prove but also to design cryptographic protocols; moreover, we would like to provide proof-based guidelines or patterns for integrating cryptographic elements in an existing protocol. The goal of the paper is to present a first attempt to mix design patterns (as in software engineering) and formal methods (as a verification tool). We illustrate the technique on the well known Needham-Schroeder public key protocol and Blake-Wilson-Menezes key transport protocol. The un- derlying modelling language is Event B and is supported by the RODIN platform, which is used to validate models.
Dominique Cansell and Dominique Méry.
Designing old and new distributed algorithms by replaying an
incremental proof-based development.
In Jean-Raymond Abrial and Uwe Glässer, editors, Rigorous
Methods for Software Construction and Analysis - Papers Dedicated to Egon
Börger on the Occasion of His 60th Birthday, number 5115, 2010.
[ bib ]
Abstract. The paper reports on practical experience with the event B method, when developing case studies, especially distributed algorithms, which are very complex to verify in practice. Using the event B method, we develop a famous distributed algorithm, namely the leader election protocol for an acyclic network, generally known as the IEEE 1394. The algorithm exists and the refinement helps us to model it entirely in an elegant way. The final model is very close to the real algorithm. Only the termination proof is missing, since it is a probabilistic algorithm, as well as the contention resolution, which is solved at a global abstract level. Modelling is clearly fundamental and complex; it should be carried out by persons able to use refinement and to manage abstractions or more precisely abstract models and proofs. Advantages of such an incremental development are multiple what we quote here and that will be explained in detail. We replay the development to improve the proof process and we obtain new distributed algorithms solving the leader election proto- col problem. Two strategies are used to build the new algorithms; a first strategy is called the contention resolution; a second strategy is called the contention prevention and is based on a priority among possible nodes of the network. The two resulting algorithms are cheaper than the original IEEE 1394 protocol and neither acknowledgement, nor confirmation is required. We show how the techniques of localisation help in deriving the final distributed algorithm. The paper is an extended version of the com- plete development of the two new algorithms and it aims to emphasize methodological aspects related to the event B development.
Keywords: Key-words: Formal method, B event-based method, refinement,safety, proofs, distributed systems.
|||A. El Hibaoui, J. M. Robson, N. Saheb-Djahromi, and A. Zemmari. Uniform election in trees and polyominoids. Discrete Appl. Math., 158(9):981-987, 2010. [ bib | DOI ]|
|||A. El Hibaoui, Y. Métivier, J.-M. Robson, N. Saheb-Djahromi, and A. Zemmari. Analysis of a randomized dynamic timetable handshake algorithm. Pure Mathematics and Applications (PuMA), 19(2-3):159-169, 2010. [ bib ]|
|||Dominique Méry. Refinement-based guidelines for constructing algorithms. In Jean-Raymond Abrial, Michael Butler, Rajeev Joshi, Elena Troubitsyna, and Jim C. P. Woodcock, editors, Refinement Based Methods for the Construction of Dependable Systems, number 09381 in Dagstuhl Seminar Proceedings, Dagstuhl, Germany, 2010. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, Germany. [ bib | http ]|
|||Nazim Benaissa. La composition des protocoles de sécurité avec la méthode B événementielle. PhD thesis, Université Henri Poincaré Nancy 1, May 2010. [ bib ]|
|||Joris Rehm. Proved development of the real-time properties of the ieee 1394 root contention protocol with the event-b method. International Journal on Software Tools for Technology Transfer (STTT), 12, fevrier 2010. [ bib ]|
|||Dominique Méry and Neeraj Kumar Singh. Real-time animation for formal specification. In Complex Systems Design & Management (CSDM), Paris, page (to appear), 2010. [ bib ]|
|||Dominique Méry and Neeraj Kumar Singh. Functional behavior of a cardiac pacing system (in Press). International Journal of Discrete Event Control Systems, 1, 2010. [ bib ]|
|||Dominique Méry and Neeraj Kumar Singh. Technical Report on Formal Development of Two-Electrode Cardiac Pacing System. (http://hal.archives-ouvertes.fr/inria-00465061/en/), LORIA, 2010. [ bib | http ]|
|||Nazim Benaissa and Dominique Méry. Cryptographic protocols analysis in event b. In PSI 2009, Russie Novosibisrk, 2009-11-11. Springer. [ bib | http ]|
|||Pierre Castéran and Vincent Filou. Tâches, types et tactiques pour les systèmes de calculs locaux. In Journées Francophones des Langages Applicatifs, pages 83-110, La Ciotat, Janvier 2010. Studia Informatica,Hermann Informatique. [ bib ]|
|||Nazim Benaissa and Dominique Méry. Proof-based design of security protocols. In Farid Ablayev and Ernst W. Mayr, editors, Computer Science- Theory and Applications 5th International Computer Science Symposium in Russia, CSR 2010, number 6072, RUSSIE, KAZAN, 2010. [ bib ]|
|||Projet ANR-RIMEL. Développement d'algorithmes répartis. Livrable RIMEL, LORIA, Janvier/Février 2008. [ bib ]|
|||Projet ANR-RIMEL. Intégration de contraintes temps-réel au sein d'un processus de développement incrémental basé sur la preuve. Livrable RIMEL, LORIA, Juillet 2008. [ bib ]|
|||Projet ANR-RIMEL. Proof-based design patterns. Livrable RIMEL, LORIA, Juillet 2008. [ bib ]|
|||Projet ANR-RIMEL. Probabilistic incremental proof-based development. Livrable RIMEL, LORIA, Décembre 2009. [ bib ]|
|||Projet ANR-RIMEL. Formal system engineering. Livrable RIMEL, LORIA, Juillet 2009. [ bib ]|
|||Projet ANR-RIMEL. Tools. Livrable RIMEL, LORIA, Juin 2010. [ bib ]|
|||D. Méry, M. Mosbah, and M. Tounsi. Integrating local computation models by refinement. In Symbolic Computation in Software Science (SCSS 2010), RISC, 2010. [ bib ]|
|||J. Chalopin and Y. Métivier. On the power of synchronizations between two adjacent vertices. Distributed computing, 2010. [ bib ]|
|||H. Hadj Kacem, M. Mosbah, N. Ouled Abdallah, and A. Zemmari. Broadcast in wireless mobile sensor networks with population protocols and extension with the rendezvous model. In 10th International Conference on New Technologies of Distributed Systems (NOTERE 2010), Tozeur, Tunisie, 31 mai - 2 juin 2010. [ bib ]|
|||Dominique Méry, Mohammed Mosbah, and Mohammed Tounsi. Proving Distributed Algorithms by Combining Refinement and Local Computations. In AVOCS 2010 10th International Workshop on Automated Verification of Critical Systems, 2010. [ bib ]|
This file has been generated by bibtex2html 1.87.