A framework for compositional verification of security protocols

Suzana Andova; Cas Cremers; Kristian Gjøsteen; Sjouke Mauw; Stig F. Mjølsnes; Saša Radomirović

doi:10.1016/j.ic.2007.07.002

A framework for compositional verification of security protocols

Suzana Andova, Cas Cremers, Kristian Gjøsteen, Sjouke Mauw, Stig F. Mjølsnes, Saša Radomirović (Lead / Corresponding author)

Computing

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

44 Citations (Scopus)

195 Downloads (Pure)

Abstract

Automatic security protocol analysis is currently feasible only for small protocols. Since larger protocols quite often are composed of many small protocols, compositional analysis is an attractive, but non-trivial approach. We have developed a framework for compositional analysis of a large class of security protocols. The framework is intended to facilitate automatic as well as manual verification of large structured security protocols. Our approach is to verify properties of component protocols in a multi-protocol environment, then deduce properties about the composed protocol. To reduce the complexity of multi-protocol verification, we introduce a notion of protocol independence and prove a number of theorems that enable analysis of independent component protocols in isolation. To illustrate the applicability of our framework to real-world protocols, we study a key establishment sequence in WiMAX consisting of three subprotocols. Except for a small amount of trivial reasoning, the analysis is done using automatic tools.

Original language	English
Pages (from-to)	425-459
Number of pages	35
Journal	Information and Computation
Volume	206
Issue number	2-4
Early online date	28 Nov 2007
DOIs	https://doi.org/10.1016/j.ic.2007.07.002
Publication status	Published - 2008
Event	Joint Workshop on Foundations of Computer Security and Automated Reasoning for Security Protocol Analysis - Seattle, United States Duration: 15 Aug 2006 → 16 Aug 2006

Keywords

Authentication
Automatic verification
Compositionality
Confidentiality
Security properties
Security protocols
Semantics
WiMAX

ASJC Scopus subject areas

Theoretical Computer Science
Information Systems
Computer Science Applications
Computational Theory and Mathematics

Access to Document

10.1016/j.ic.2007.07.002Licence: Elsevier User Licence

Author Accepted ManuscriptAccepted author manuscript, 422 KB

Cite this

@article{4a00d19251444614bd2ef486f77b7655,

title = "A framework for compositional verification of security protocols",

abstract = "Automatic security protocol analysis is currently feasible only for small protocols. Since larger protocols quite often are composed of many small protocols, compositional analysis is an attractive, but non-trivial approach. We have developed a framework for compositional analysis of a large class of security protocols. The framework is intended to facilitate automatic as well as manual verification of large structured security protocols. Our approach is to verify properties of component protocols in a multi-protocol environment, then deduce properties about the composed protocol. To reduce the complexity of multi-protocol verification, we introduce a notion of protocol independence and prove a number of theorems that enable analysis of independent component protocols in isolation. To illustrate the applicability of our framework to real-world protocols, we study a key establishment sequence in WiMAX consisting of three subprotocols. Except for a small amount of trivial reasoning, the analysis is done using automatic tools.",

keywords = "Authentication, Automatic verification, Compositionality, Confidentiality, Security properties, Security protocols, Semantics, WiMAX",

author = "Suzana Andova and Cas Cremers and Kristian Gj{\o}steen and Sjouke Mauw and Mj{\o}lsnes, {Stig F.} and Sa{\v s}a Radomirovi{\'c}",

note = "S.A & S.R. This work was partially carried out during the tenure of an ERCIM Fellowship at NTNU; C.C. Supported in part by the Hasler Foundation project 2071; K. G. Supported in part by the Norwegian Research Council project 158597 NTNU Research Programme in Information Security; S.R. Supported in part by a Centre de Recerca Matem{\`a}tica Postdoctoral Fellowship.; Joint Workshop on Foundations of Computer Security and Automated Reasoning for Security Protocol Analysis , FCS-ARSPA {\textquoteright}06 ; Conference date: 15-08-2006 Through 16-08-2006",

year = "2008",

doi = "10.1016/j.ic.2007.07.002",

language = "English",

volume = "206",

pages = "425--459",

journal = "Information and Computation",

issn = "0890-5401",

publisher = "Elsevier",

number = "2-4",

}

TY - JOUR

T1 - A framework for compositional verification of security protocols

AU - Andova, Suzana

AU - Cremers, Cas

AU - Gjøsteen, Kristian

AU - Mauw, Sjouke

AU - Mjølsnes, Stig F.

AU - Radomirović, Saša

N1 - S.A & S.R. This work was partially carried out during the tenure of an ERCIM Fellowship at NTNU; C.C. Supported in part by the Hasler Foundation project 2071; K. G. Supported in part by the Norwegian Research Council project 158597 NTNU Research Programme in Information Security; S.R. Supported in part by a Centre de Recerca Matemàtica Postdoctoral Fellowship.

PY - 2008

Y1 - 2008

N2 - Automatic security protocol analysis is currently feasible only for small protocols. Since larger protocols quite often are composed of many small protocols, compositional analysis is an attractive, but non-trivial approach. We have developed a framework for compositional analysis of a large class of security protocols. The framework is intended to facilitate automatic as well as manual verification of large structured security protocols. Our approach is to verify properties of component protocols in a multi-protocol environment, then deduce properties about the composed protocol. To reduce the complexity of multi-protocol verification, we introduce a notion of protocol independence and prove a number of theorems that enable analysis of independent component protocols in isolation. To illustrate the applicability of our framework to real-world protocols, we study a key establishment sequence in WiMAX consisting of three subprotocols. Except for a small amount of trivial reasoning, the analysis is done using automatic tools.

AB - Automatic security protocol analysis is currently feasible only for small protocols. Since larger protocols quite often are composed of many small protocols, compositional analysis is an attractive, but non-trivial approach. We have developed a framework for compositional analysis of a large class of security protocols. The framework is intended to facilitate automatic as well as manual verification of large structured security protocols. Our approach is to verify properties of component protocols in a multi-protocol environment, then deduce properties about the composed protocol. To reduce the complexity of multi-protocol verification, we introduce a notion of protocol independence and prove a number of theorems that enable analysis of independent component protocols in isolation. To illustrate the applicability of our framework to real-world protocols, we study a key establishment sequence in WiMAX consisting of three subprotocols. Except for a small amount of trivial reasoning, the analysis is done using automatic tools.

KW - Authentication

KW - Automatic verification

KW - Compositionality

KW - Confidentiality

KW - Security properties

KW - Security protocols

KW - Semantics

KW - WiMAX

UR - http://www.scopus.com/inward/record.url?scp=40149109757&partnerID=8YFLogxK

U2 - 10.1016/j.ic.2007.07.002

DO - 10.1016/j.ic.2007.07.002

M3 - Article

AN - SCOPUS:40149109757

SN - 0890-5401

VL - 206

SP - 425

EP - 459

JO - Information and Computation

JF - Information and Computation

IS - 2-4

T2 - Joint Workshop on Foundations of Computer Security and Automated Reasoning for Security Protocol Analysis

Y2 - 15 August 2006 through 16 August 2006

ER -

A framework for compositional verification of security protocols

Abstract

Keywords

ASJC Scopus subject areas

Access to Document

Other files and links

Fingerprint

Cite this