| Article ID | Journal | Published Year | Pages | File Type |
|---|---|---|---|---|
| 424697 | Future Generation Computer Systems | 2011 | 10 Pages |
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
Benjamin Aziz, Geoff Hamilton,