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.
Sensoria Bibliography Site Detecting and Preventing Type flaws at Static Time
Chiara Bodei, Linda Brodo, Pierpaolo Degano, Han Gao
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 analysing the
extended LySa which 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,
either subject to type flaw attacks or not.
The results show that the analysis is able to capture type flaw attacks
on the former security protocols (only those subject to attacks).
The implementation complexity of the analysis
is low polynomial.
