Security protocols make use of cryptographic techniques to achieve goals such as confidentiality, authentication and integrity. However, the fact that strong cryptographic algorithms exist does not guarantee the security of a communications system. In fact, it is recognised that the engineering of security protocols is a challenging task, since protocols that appear secure can contain subtle flaws that attackers can exploit. A number of techniques exist for the analysis of security protocol specifications. Individually they are not capable of detecting every possible flaw or attack against a protocol. However, when combined, these techniques all complement each other, allowing a protocol engineer to obtain a more accurate overview of the security of a protocol that is being designed. This is the rationale for multi-dimensional security protocol engineering, a concept introduced by previous projects of ours over several years. We propose an attack construction approach to security protocol analysis within a multi-dimensional context. This analysis method complements the existing inference construction analysis tools developed earlier in the group. We give a brief overview of the concepts associated with the project, including a summary of existing security protocol analysis techniques, and a description of the strand space model, which is the intended formalism for the analysis.
展开▼
