Copyright Information
The documents distributed by this server have been provided by the contributing authors as a means to ensure timely dissemination of
scholarly and technical work on a noncommercial basis. Copyright and all rights therein are maintained by the authors or by other
copyright holders, notwithstanding that they have offered their works here electronically. It is understood that all persons copying
this information will adhere to the terms and constraints invoked by each author's copyright. These works may not be reposted without
the explicit permission of the copyright holder.
show main publications
Detecting and Preventing Type Flaws: a Control Flow Analysis with tags
@ARTICLE{BBDG,
title = {{Detecting and Preventing Type Flaws: a Control Flow Analysis with tags}},
author = {{Chiara} {Bodei} and {Linda} {Brodo} and {Pierpaolo} {Degano} and {Han} {Gao}},
journal = {Proceeding of SecCO'07. ENTCS 194},
editor = {Elsevier},
pages = {3-22},
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 with
tags attached to each field, indicating the intended types. We
developed a control flow analysis for analysing the extended Lysa,
which over-approximates all the possible behaviour of a protocol
and hence is able to capture any type confusion that may happen
during the protocol execution. The control flow analysis has been
applied to a number of security protocols, either subject to type
flaw attacks or not. The results show that it is able to capture
type flaw attacks on those security protocols.},
url = {http://www.di.unipi.it/~chiara/publ-40/SecCO07.pdf},
address = {Informatics and Mathematical Modelling, Technical University},
institution = {University of Pisa},
keywords = {flow logic},
partner = {DTU, PISA},
school = {Tehnical University of Denmark, University of Pisa},
task = {T3.1},
}
|
