Home Results Security Formal Description of the NaDa Architecture
Formal Description of the NaDa Architecture PDF Print E-mail

The two most common NanoDataCenter use cases described in Deliverable D 3.2 were modeled and analysed using the SH-Verification Tool. The first use case is the process of putting nodes in to service. The second use case is the exchange of virtual goods. To prove that the fundamental security assumptions suit our requirements we have created a model to determine that our concept can't reach an illegal system state. This was done by creating a system specification using Asynchronous Product Automata to simulate and verify these use cases.

Beside the basic network functionality, the basic functionality for the management and the nodes was specified. The resulting model can simulate the behaviour of unlimited (only limited by the system resources of the analysing computer) count of nodes attached to one management. For certain system configurations the complete reachability graph (graph with all system states) was computed. The first use case, putting nodes in to service, involves the authentication between multiple nodes and the dedicated management. Furthermore takes the registration process also place in this use case. The first exchange of polices, which rule the behaviour of the later exchanged goods, or measurement data are also part of this process. The second use case describes the exchange of virtual goods over a peer to peer network in particular. It's also describes the usage of the ticket mechanism which is used to built up a trustworthy connection between two or more nodes.

We could prove that the system, represented by our model, lead always to a defined system state. All security related information's are distributed always right during the boot or the exchange process. We could also identify the management system as a possible bottleneck during those two scenarios.

The SH verification tool is provided by the Fraunhofer SIT and is available on request, the NaDa model is available here.