Article ID Journal Published Year Pages File Type
424697 Future Generation Computer Systems 2011 10 Pages PDF
Abstract

In this paper, we design a non-uniform static analysis for formally verifying a protocol used in large-scale Grid systems for achieving delegations from users to critical system services. The analysis reveals a few shortcomings in the protocol, such as the lack of token integrity and the possibility of repudiating a delegation session. It also reveals the vulnerability of non-deterministic delegation chains that was detected as a result of adopting a more precise analysis, which allows for more participants in the protocol than the original protocol designers envisaged.

Research highlights► Formal methods. ► Software engineering. ► Security. ► Verification. ► Large-scale distributed systems.

Related Topics
Physical Sciences and Engineering Computer Science Computational Theory and Mathematics
Authors
, ,