5. Results and limitations

5.1 Automatic analysis tools

In this formal framework, however, the preservation of secrecy by a protocol is an undecidable problem, i.e. it can be shown [5] that it is impossible to construct an algorithm which, given a protocol, answers whether it preserves the requested secrecy. The undecidability of this problem stems from the fact that many parameters are unbounded:

• the number of agents is arbitrary;

• the number of sessions is arbitrary;

• at each stage, the number of possible actions is arbitrary, as the opponent can send any deducible message of his choice;

• new arbitrary...