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 A formal analysis of complex type flaw attacks on security protocols
Han Gao, Chiara Bodei, Pierpaolo Degano
abstract:
A simple type confusion attack occurs in a security protocol, when
a principal interprets data of one type as data of another. These
attacks can be successfully prevented by "tagging'' types of each
field of a message. Complex type confusions occur instead when
tags can be confused with data and when fields or sub-segments of
fields may be confused with concatenations of fields of other
types. Capturing these kinds of confusions is not easy in a
process calculus setting, where it is generally assumed that
messages are correctly interpreted. In this paper, we model in the
process calculus LySa only the misinterpretation due to the
confusion of a concatenation of fields with a single field, by
extending the notation of one-to-one variable binding to
many-to-one binding. We further present a formal way of detecting
these possible misinterpretations, based on a Control Flow
Analysis for this version of the calculus. The analysis
over-approximates all the possible behaviour of a protocol,
including those effected by these type confusions. As an example,
we considered the amended Needham-Schroeder symmetric protocol,
where we succeed in detecting the type confusion that lead to a
complex type flaw attacks it is subject to.
Therefore, the analysis can capture potential type confusions of this kind on
security protocols, besides other security properties such as
confidentiality, freshness and message authentication.
