The aim of this work is to develop unambiguous methods to verify algorithmically that webinos authentication methods do not contain deadlocks or similar critical states that can cause system crashes.
The present work was described in a scientific paper presented at the WISSE 2014 conference: Link to the paper.
One of the major problems encountered developing software, especially when the software is made up of a lot of components, is to verify that it does exactly what we expect from it. For this reason, the best way to verify the correctness of each module that makes up the software is to check out each part as a stand-alone component, and it is exactly what we did for webinos.
webinos is a project that wants to enable web applications and services to be used and shared consistently and securely over a broad spectrum of converged and connected devices, including mobile, PC, home media (TV) and in-car units.
It is made up of a lot of different modules and, more specifically, it plans to introduce some novel authentication methods, which should at the same time introduce user-friendly SSO (Single Sign-On) and preserve user privacy. So, this homework have the task to analyze algorithmically only the behaviour of the authentication modules and methods from a security point of view.
This purpose can be achieved using model checking, which is just a method created to let developers analyze algorithmically their own software. The verification is achieved by the definition of precise mathematical languages representing the system, its states, its transitions and its properties that can be verified by the model checker: a software that is able to check whether the properties are satisfied in a logic point of view.
The present work was described in a scientific paper presented at the WISSE 2014 conference: Link to the paper.
One of the major problems encountered developing software, especially when the software is made up of a lot of components, is to verify that it does exactly what we expect from it. For this reason, the best way to verify the correctness of each module that makes up the software is to check out each part as a stand-alone component, and it is exactly what we did for webinos.
webinos is a project that wants to enable web applications and services to be used and shared consistently and securely over a broad spectrum of converged and connected devices, including mobile, PC, home media (TV) and in-car units.
It is made up of a lot of different modules and, more specifically, it plans to introduce some novel authentication methods, which should at the same time introduce user-friendly SSO (Single Sign-On) and preserve user privacy. So, this homework have the task to analyze algorithmically only the behaviour of the authentication modules and methods from a security point of view.
This purpose can be achieved using model checking, which is just a method created to let developers analyze algorithmically their own software. The verification is achieved by the definition of precise mathematical languages representing the system, its states, its transitions and its properties that can be verified by the model checker: a software that is able to check whether the properties are satisfied in a logic point of view.
You can find the documentation related to this project at the following links:
Moreover you can find the attachments here:
Moreover you can find the attachments here:
Figure 1: Webinos logo - reprinted from Webinos site
Figure 2: Personal Zones - reprinted from Webinos Authentication