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 Statically detecting message confusions in a multi-protocol setting
Chiara Bodei, Linda Brodo, Pierpaolo Degano, Han Gao
abstract:
In a multi-protocol setting, different protocols are concurrently executed, and each principal can participate in more than one.
The possibilities of attacks therefore increase, often due to the presence of similar patterns in messages. Messages coming from one protocol can be confused with similar messages coming from another protocol.
As a consequence, data of one type may be interpreted as data of another, and it is also possible that the type is the expected one, but the message is addressed to another protocol.
In this paper, we shall present an extension of the LySa calculus that decorates encryption with tags including the protocol identifier, the protocol step identifier and the intended types of the encrypted terms.
The additional information allows us to find the
messages that can be confused and therefore to have hints to
reconstruct the attack. We extend accordingly the standard static
Control Flow Analysis for LySa, which over-approximates all the
possible behaviour of the studied protocols, included the possible
message confusions that may occur at run-time.
Our analysis has been implemented and successfully applied to
small sets of protocols. In particular, we discovered an
undocumented family of attacks, that may arise when
Bauer-Berson-Feiertag and the Woo-Lam authentication protocols are
running in parallel. The implementation complexity of the analysis
is low polynomial.
