Compositional Verification of Secure Applet Interactions

Gilles Barthe; Dilian Gurov; Marieke Huisman

doi:10.1007/3-540-45923-52

Compositional Verification of Secure Applet Interactions

Gilles Barthe, Dilian Gurov, Marieke Huisman

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

11 Citations (Scopus)

7 Downloads (Pure)

Abstract

Recent developments in mobile code and embedded systems have led to an increased interest in open platforms, i.e. platforms which enable different applications to interact in a dynamic environment. However, the flexibility of open platforms presents major difficulties for the (formal) verification of secure interaction between the different applications. To overcome these difficulties, compositional verification techniques are required.

This paper presents a compositional approach to the specification and verification of secure applet interactions. This approach involves a compositional model of the interface behavior of applet interactions, a temporal logic property specification language, and a proof system for proving correctness of property decompositions. The usability of the approach is demonstrated on a realistic smartcard case study.

Original language	English
Title of host publication	Fundamental Approaches to Software Engineering, 5th International Conference, FASE 2002, held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2002, Grenoble, France, April 8-12, 2002, Proceedings
Editors	Ralf-Detlef Kutsche, Herbert Weber
Publisher	Springer
Pages	15-32
Number of pages	18
ISBN (Electronic)	978-3-540-45923-1
ISBN (Print)	978-3-540-43353-8
DOIs	https://doi.org/10.1007/3-540-45923-52
Publication status	Published - 2002
Externally published	Yes
Event	5th International Conference on Fundamental Approaches to Software Engineering, FASE 2002 - Grenoble, France Duration: 8 Apr 2002 → 12 Apr 2002 Conference number: 5

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer
Volume	2306

Conference

Conference	5th International Conference on Fundamental Approaches to Software Engineering, FASE 2002
Abbreviated title	FASE 2002
Country/Territory	France
City	Grenoble
Period	8/04/02 → 12/04/02

Access to Document

10.1007/3-540-45923-52

Barthe-2002-Compositional-verification-of-securAccepted author version, 273 KB

Cite this

Barthe, G., Gurov, D., & Huisman, M. (2002). Compositional Verification of Secure Applet Interactions. In R.-D. Kutsche, & H. Weber (Eds.), Fundamental Approaches to Software Engineering, 5th International Conference, FASE 2002, held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2002, Grenoble, France, April 8-12, 2002, Proceedings (pp. 15-32). (Lecture Notes in Computer Science; Vol. 2306). Springer. https://doi.org/10.1007/3-540-45923-52

Barthe, Gilles ; Gurov, Dilian ; Huisman, Marieke. / Compositional Verification of Secure Applet Interactions. Fundamental Approaches to Software Engineering, 5th International Conference, FASE 2002, held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2002, Grenoble, France, April 8-12, 2002, Proceedings. editor / Ralf-Detlef Kutsche ; Herbert Weber. Springer, 2002. pp. 15-32 (Lecture Notes in Computer Science).

@inproceedings{97c9b934b6df4f6fa67d0aee9573771c,

title = "Compositional Verification of Secure Applet Interactions",

abstract = "Recent developments in mobile code and embedded systems have led to an increased interest in open platforms, i.e. platforms which enable different applications to interact in a dynamic environment. However, the flexibility of open platforms presents major difficulties for the (formal) verification of secure interaction between the different applications. To overcome these difficulties, compositional verification techniques are required.This paper presents a compositional approach to the specification and verification of secure applet interactions. This approach involves a compositional model of the interface behavior of applet interactions, a temporal logic property specification language, and a proof system for proving correctness of property decompositions. The usability of the approach is demonstrated on a realistic smartcard case study.",

author = "Gilles Barthe and Dilian Gurov and Marieke Huisman",

year = "2002",

doi = "10.1007/3-540-45923-52",

language = "English",

isbn = "978-3-540-43353-8",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "15--32",

editor = "Ralf-Detlef Kutsche and Herbert Weber",

booktitle = "Fundamental Approaches to Software Engineering, 5th International Conference, FASE 2002, held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2002, Grenoble, France, April 8-12, 2002, Proceedings",

address = "Germany",

note = "5th International Conference on Fundamental Approaches to Software Engineering, FASE 2002, FASE 2002 ; Conference date: 08-04-2002 Through 12-04-2002",

}

Barthe, G, Gurov, D & Huisman, M 2002, Compositional Verification of Secure Applet Interactions. in R-D Kutsche & H Weber (eds), Fundamental Approaches to Software Engineering, 5th International Conference, FASE 2002, held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2002, Grenoble, France, April 8-12, 2002, Proceedings. Lecture Notes in Computer Science, vol. 2306, Springer, pp. 15-32, 5th International Conference on Fundamental Approaches to Software Engineering, FASE 2002, Grenoble, France, 8/04/02. https://doi.org/10.1007/3-540-45923-52

Compositional Verification of Secure Applet Interactions. / Barthe, Gilles; Gurov, Dilian; Huisman, Marieke.
Fundamental Approaches to Software Engineering, 5th International Conference, FASE 2002, held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2002, Grenoble, France, April 8-12, 2002, Proceedings. ed. / Ralf-Detlef Kutsche; Herbert Weber. Springer, 2002. p. 15-32 (Lecture Notes in Computer Science; Vol. 2306).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

TY - GEN

T1 - Compositional Verification of Secure Applet Interactions

AU - Barthe, Gilles

AU - Gurov, Dilian

AU - Huisman, Marieke

N1 - Conference code: 5

PY - 2002

Y1 - 2002

N2 - Recent developments in mobile code and embedded systems have led to an increased interest in open platforms, i.e. platforms which enable different applications to interact in a dynamic environment. However, the flexibility of open platforms presents major difficulties for the (formal) verification of secure interaction between the different applications. To overcome these difficulties, compositional verification techniques are required.This paper presents a compositional approach to the specification and verification of secure applet interactions. This approach involves a compositional model of the interface behavior of applet interactions, a temporal logic property specification language, and a proof system for proving correctness of property decompositions. The usability of the approach is demonstrated on a realistic smartcard case study.

AB - Recent developments in mobile code and embedded systems have led to an increased interest in open platforms, i.e. platforms which enable different applications to interact in a dynamic environment. However, the flexibility of open platforms presents major difficulties for the (formal) verification of secure interaction between the different applications. To overcome these difficulties, compositional verification techniques are required.This paper presents a compositional approach to the specification and verification of secure applet interactions. This approach involves a compositional model of the interface behavior of applet interactions, a temporal logic property specification language, and a proof system for proving correctness of property decompositions. The usability of the approach is demonstrated on a realistic smartcard case study.

U2 - 10.1007/3-540-45923-52

DO - 10.1007/3-540-45923-52

M3 - Conference contribution

SN - 978-3-540-43353-8

T3 - Lecture Notes in Computer Science

SP - 15

EP - 32

BT - Fundamental Approaches to Software Engineering, 5th International Conference, FASE 2002, held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2002, Grenoble, France, April 8-12, 2002, Proceedings

A2 - Kutsche, Ralf-Detlef

A2 - Weber, Herbert

PB - Springer

T2 - 5th International Conference on Fundamental Approaches to Software Engineering, FASE 2002

Y2 - 8 April 2002 through 12 April 2002

ER -

Barthe G, Gurov D, Huisman M. Compositional Verification of Secure Applet Interactions. In Kutsche RD, Weber H, editors, Fundamental Approaches to Software Engineering, 5th International Conference, FASE 2002, held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2002, Grenoble, France, April 8-12, 2002, Proceedings. Springer. 2002. p. 15-32. (Lecture Notes in Computer Science). doi: 10.1007/3-540-45923-52

Compositional Verification of Secure Applet Interactions

Abstract

Publication series

Conference

Access to Document

Fingerprint

Cite this