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 did the original protocol designers envisage.
Original language | English |
---|---|
Pages (from-to) | 476-485 |
Number of pages | 10 |
Journal | Future Generation Computer Systems |
Volume | 27 |
Issue number | 5 |
DOIs | |
Publication status | Published - May 2011 |
Keywords
- Delegation
- Security
- Protocol Veri�cation
- Static Analysis
- Grid Computing