Sciweavers

CONCUR
2005
Springer

Selecting Theories and Recursive Protocols

13 years 9 months ago
Selecting Theories and Recursive Protocols
Many decidability results are known for non-recursive cryptographic protocols, where the protocol steps can be expressed by simple rewriting rules. Recently, a tree transducer-based model was proposed for recursive protocols, where the protocol steps involve some kind of recursive computations. This model has, however, some limitations: (1) rules are assumed to have linear left-hand sides (so no equality tests can be performed), (2) only finite amount of information can be conveyed from one receive-send action to the next ones. It has been proven that, in this model, relaxing these assumptions leads to undecidability. In this paper, we propose a formalism, called selecting theories, which extends the standard non-recursive term rewriting model and allows participants to compare and store arbitrary messages. This formalism can model recursive protocols, where participants, in each protocol step, are able to send a number of messages unbounded w.r.t. the size of the protocol. We prove t...
Tomasz Truderung
Added 26 Jun 2010
Updated 26 Jun 2010
Type Conference
Year 2005
Where CONCUR
Authors Tomasz Truderung
Comments (0)