Searching for just a few words should be enough to get started. If you need to make more complex queries, use the tips below to guide you.
Issue title: Security Issues in Concurrency (SecCo'07)
Guest editors: Daniele GorlaGuest-Editor and Catuscia PalamidessiGuest-Editor
Article type: Research Article
Authors: Bodei, Chiaraa; ** | Brodo, Lindab | Degano, Pierpaoloa | Gao, Hanc
Affiliations: [a] Dipartimento di Informatica, Università di Pisa, Via Pontecorvo, I-56127 Pisa, Italia. E-mails: chiara@di.unipi.it, degano@di.unipi.it | [b] Dipartimento di Scienze dei Linguaggi, Università di Sassari, via Tempio, 9, I-07100 Sassari, Italia. E-mail: brodo@uniss.it | [c] Informatics and Mathematical Modelling, Technical University of Denmark, Richard Petersens Plads bldg 321, DK-2800 Kongens Lyngby, Denmark. E-mail: hg@imm.dtu.dk
Correspondence: [**] Corresponding author.
Note: [*] A preliminary version of this paper appeared in [6]. Research partially supported by the EU within the FET-GC II Integrated Project IST-2005-016004 SENSORIA and by Italian PRIN Project “SOFT”.
Abstract: A type flaw attack on a security protocol is an attack where an honest principal is cheated on interpreting a field in a message as the one with a type other than the intended one. In this paper, we shall present an extension of the LYSA calculus to cope with types, by using tags to represent the intended types of terms. We develop a Control Flow Analysis for this calculus which soundly over-approximates all the possible behaviour of a protocol and, in particular, is able to capture any type confusion that may occur during the protocol execution. The analysis acts in a descriptive way: it describes which violations may occur. In the same setting, our approach also offers a prescriptive usage: we can impose a type discipline, by forcing some data to be of the expected types. At this point, the analysis may statically check that type violations are not possible any longer. In other words, we instrument the code with the only checks necessary to enforce type security. Finally, we apply our framework to a multi-protocol setting, where the risk of having type flaw attacks is higher. Our analysis has been implemented and successfully applied to a number of security protocols, showing it is able to capture type flaw attacks. The implementation complexity of the analysis is low polynomial.
Keywords: Security of cryptographic protocols, Control Flow Analysis, type flaw attacks
DOI: 10.3233/JCS-2010-0361
Journal: Journal of Computer Security, vol. 18, no. 2, pp. 229-264, 2010
IOS Press, Inc.
6751 Tepper Drive
Clifton, VA 20124
USA
Tel: +1 703 830 6300
Fax: +1 703 830 2300
sales@iospress.com
For editorial issues, like the status of your submitted paper or proposals, write to editorial@iospress.nl
IOS Press
Nieuwe Hemweg 6B
1013 BG Amsterdam
The Netherlands
Tel: +31 20 688 3355
Fax: +31 20 687 0091
info@iospress.nl
For editorial issues, permissions, book requests, submissions and proceedings, contact the Amsterdam office info@iospress.nl
Inspirees International (China Office)
Ciyunsi Beili 207(CapitaLand), Bld 1, 7-901
100025, Beijing
China
Free service line: 400 661 8717
Fax: +86 10 8446 7947
china@iospress.cn
For editorial issues, like the status of your submitted paper or proposals, write to editorial@iospress.nl
如果您在出版方面需要帮助或有任何建, 件至: editorial@iospress.nl