A calculus for control flow analysis of security protocols

摘要

The design of a process calculus for analysing security protocols is governed by three factors: expressing the security protocol in a precise and faithful manner, accommodating the variety of attack scenarios, and utilising the strengths (and limit the weaknesses) of the underlying analysis methodology. We pursue an analysis methodology based on control flow analysis in flow logic style, whose ability to analyse a variety of security protocols we have shown previously [7]. This paper develops a calculus, LySa~(ns), which allows for much greater control and clarity in the description of attack scenarios, gives a more flexible format for expressing protocols, and at the same time allows one to circumvent some of the 'false positives' arising in [7].