5. TA4SP

Before describing further the method used in TA4SP, it should be noted that if we do not limit the number of sessions of a protocol that can run in parallel, it is undecidable whether this protocol is sensitive to man-in-the-middle attacks, i.e. it is not possible to create a program that takes as input the description of a security protocol and gives an analysis of this protocol each time. To get back to a decidable case, i.e. one that can be implemented by a machine every time, it is necessary to make certain restrictions or assumptions. The most common is to limit the number of protocol sessions that can run in parallel, usually to two or three. This is justified a posteriori by the fact that almost all known protocol flaws use only two sessions (or very rarely three). Even with these assumptions, the problem is more complex than it seems and requires the development of dedicated algorithms....