A Model Checker for the Verification of Browser Based Protocols

Authors

  • Victor Ferman Tecnológico de Monterrey, Escuela de Ingeniería y Ciencias
  • Raúl Monroy Tecnológico de Monterrey, Escuela de Ingeniería y Ciencias
  • Dieter Hutter German Research Center for Artificial Intelligence

DOI:

https://doi.org/10.13053/cys-21-1-2483

Keywords:

Model Checking, Browser Based Protocols, Security Protocols, Formal Methods

Abstract

A browser based protocol is the chief security component of a safety critical web application, such as e-banking. Accordingly, browser based protocols need to be thoroughly verified in order to guarantee they are up to comply with key security properties. To this end, we have developed WebMC, a model checker especially designed to consider web standards, with the aim of analyzing browser based protocol execution, as encompassed by the interactions of a typical user, a browser, and active attacker playing the role of the network, and one or more servers. In this paper, we shall show how to use WebMC in the design and the development of browser based protocols. Our tool has been successfully validated: WebMC has been able to reproduce a number of the verification results found in the literature, but fully automatically.

Author Biographies

Victor Ferman, Tecnológico de Monterrey, Escuela de Ingeniería y Ciencias

Victor Ferman is a PhD student working on the verification of browser based protocols under the supervision of Prof. Raul Monroy, at Tecnologico de Monterrey, Campus Estado de México.

Raúl Monroy, Tecnológico de Monterrey, Escuela de Ingeniería y Ciencias

Raúl Monroy obtained a PhD in Artificial Intelligence in 1998 from Edinburgh University, under the supervision of Prof. Alan Bundy. He is a (full) Professor in Computing at Tecnlogico de Monterrey, Campus Estado de México. Since 1998 he is a member of CONACyT’s National Research System, currently rank 2. He is the leader of the GIEE-ML (Machine Learning) research group at Tecnologico de Monterrey. Dr. Monroy’s research is concerned with the discovery and application of general search control strategies for uncovering and correcting errors in either a system or its specification; for detecting anomalies endangering information security; and for planning robot motion.

Dieter Hutter, German Research Center for Artificial Intelligence

Dieter Hutter received his PhD from Karlsruhe University working on inductive theorem proving. In 1991 he moved to the Saarland University and joined DFKI in 1993. He lead various projects in Formal Methods and Security. Moving to Bremen in 2008, he is now vice director of the Cyber-Physical System Department at DFKI and honorary professor at Bremen University.

Downloads

Published

2017-03-20

Issue

Vol. 21 No. 1 (2017): Thematic Issue: Topic Trends in Computing Research (Guest Editors: C.P. Ayala, S.N. González-Rocha)

Section

Articles

License 

Hereby I transfer exclusively to the Journal "Computación y 
Sistemas", published by the Computing Research Center (CIC-IPN),
the Copyright of the aforementioned paper. I also accept that these 
rights will not be transferred to any other publication, in any other 
format, language or other existing means of developing.
I certify that the paper has not been previously disclosed or simultaneo
usly submitted to any other publication, and that it does not contain 
material whose publication would violate the Copyright or other 
proprietary rights of any person, company or institution. I certify that 
I have the permission from the institution or company where I work or 
study to publish this work.
The representative author accepts the responsibility for the publication
of this paper on behalf of each and every one of the authors. 
This transfer is subject to the following conditions:
  • The authors retain all ownership rights (such as patent rights) of this work, except for the publishing rights transferred to the CIC, through this document.
  • Authors retain the right to publish the work in whole or in part in any book they are the authors or publishers. They can also make use of this work in conferences, courses, personal web pages, and so on.
  • Authors may include working as part of his thesis, for non-profit distribution only.