Copyright Notice:
The publication copies distributed in this site are
provided to ensure timely dissemination of scholarly and technical
work. Copyright and all rights therein are retained by authors or by
other copyright holders (as explicitly indicated). All persons copying
this information are expected to adhere
to the terms and constraints invoked by each copyright. In
most cases, these works may not be reposted without the explicit
permission of the copyright holder
Ivan Cibrario Bertolotti, Luca Durante, Riccardo Sisto, Adriano Valenzano,
Efficient representation of the attacker’s knowledge in cryptographic protocols analysis,
Formal Aspects of Computing, Vol. 20, No. 3 (March 2008), Springer, pp. 303-348.
©2008 Springer
doi: 10.1007/s00165-008-0078-3
Abstract
This paper addresses the problem of representing the intruder’s knowledge in the formal verification of cryptographic protocols,
whose main challenges are to represent the intruder’s knowledge efficiently and without artificial limitations on the structure
and size of messages. The new knowledge representation strategy proposed in this paper achieves both goals and leads to practical
implementation because it is incrementally computable and is easily amenable to work with various term representation languages.
In addition, it handles associative and commutative term composition operators, thus going beyond the free term algebra framework.
An extensive computational complexity analysis of the proposed representation strategy is included in the paper.
Back to Riccardo Sisto's publications