Verifying a delegation protocol for Grid systems

Benjamin Aziz; G. Hamilton

doi:10.1016/j.future.2010.12.003

Verifying a delegation protocol for Grid systems

Benjamin Aziz, G. Hamilton

School of Computing

Research output: Contribution to journal › Article › peer-review

142 Downloads (Pure)

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	https://doi.org/10.1016/j.future.2010.12.003
Publication status	Published - May 2011

Keywords

Delegation
Security
Protocol Veri�cation
Static Analysis
Grid Computing

Access to Document

10.1016/j.future.2010.12.003

AzizFGCS.pdfAccepted author manuscript (Post-print), 453 KB

http://www.sciencedirect.com/science/article/pii/S0167739X10002529

Cite this

@article{d73f479e465a4add99486f0b2fadb83f,

title = "Verifying a delegation protocol for Grid systems",

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.",

keywords = "Delegation, Security, Protocol Veri�cation, Static Analysis, Grid Computing",

author = "Benjamin Aziz and G. Hamilton",

note = "Projects: Security and Forensics.",

year = "2011",

month = may,

doi = "10.1016/j.future.2010.12.003",

language = "English",

volume = "27",

pages = "476--485",

journal = "Future Generation Computer Systems",

issn = "0167-739X",

publisher = "Elsevier BV",

number = "5",

}

TY - JOUR

T1 - Verifying a delegation protocol for Grid systems

AU - Aziz, Benjamin

AU - Hamilton, G.

N1 - Projects: Security and Forensics.

PY - 2011/5

Y1 - 2011/5

N2 - 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.

AB - 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.

KW - Delegation

KW - Security

KW - Protocol Veri�cation

KW - Static Analysis

KW - Grid Computing

U2 - 10.1016/j.future.2010.12.003

DO - 10.1016/j.future.2010.12.003

M3 - Article

SN - 0167-739X

VL - 27

SP - 476

EP - 485

JO - Future Generation Computer Systems

JF - Future Generation Computer Systems

IS - 5

ER -

Verifying a delegation protocol for Grid systems

Abstract

Keywords

Access to Document

Fingerprint

Cite this