MultiLogin

Tag: register

The Multi-Login Systems we analyzed function similarly to a standard Login System with user IDs and password. The main difference is that passwords are generated as random values in outputs when a user registers, instead of being provided at input. You can view these outputs in a similar vein to session IDs or nonces. This complication makes such systems difficult to learn because of the inherent non-determinism exhibited by randomly generated output values, or so called fresh output values.

Tomte-0.4 can handle this behavior by way of a Determinizer function. Check the publication for more details on our algorithm. In a learning example Tomte 0.4 was used to infer models for instantiations of Multi-Login Systems with 1, 2 and 3 maximum registered users.

Description

In a our Login systems, a user can register, providing a login ID. Unless the maximum number of registered users, or regMax, is exceeded, the Register input will yield an OK output containing a password that can later be used to log into the system. After regMax users are registered, Register returns NOK, meaning an additional user could not be registered. If successfully registered the user can login using the user ID and password via the Login input. Logged in, the user can change their password (via ChangePassword) or log out (via Logout). There is no limit on the number of users that can be logged in at any point in time other than regMax.

The SUT

The implementation used for Multi-Login Systems with 1 and 2 users was generated automatically from a .xml specification model written in Uppaal. For the 3 user system we hand-crafted a java implementation because the system was too complex to draw manually.

Following Uppaal modelling conventions, we use LTS models extended with parameters, actions and guards. Below we show the Uppaal state machine we created for Multi-Login Systems with 1 and 2 users respectively:

Fig. 1: Uppaal SUT Model : Multi-Login with 1 user        

Fig. 1: Uppaal SUT Model : Multi-Login with 2 users        

Characteristics for MultiLogin n

Resources