The principle of guarantee availability for security protocol analysis.

Conformity to prudent design principles is an established approach to protocol correctness although it is not free of limitations. We term goal availability a design principle that is often implicitly followed, prescribing protocols to aim at principal-centric goals. Adherence to a design principle is normally established through protocol analysis that is an evaluation of whether a protocol achieves its goals. However, the literature shows that there exists no clear guidance on how to conduct and interpret such an analysis, a process that is only left to the analyzer’s skill and experience. Goal availability has the desirable feature that its supporting protocol analysis can be precisely guided by what becomes a principle of realistic analysis, which we call guarantee availability. It prescribes that the outcome of the analysis, which is the set of guarantees confirming the protocol goals, be practically applicable by the protocol participants. In consequence, the guarantees must be based on assumptions that the principals have the capacity to verify. Our focus then turns entirely to protocol analysis, because an analysis conforming to guarantee availability signifies that the analyzed protocol conforms to goal availability. Existing analysis of (both classical and deployed) protocols has been reconsidered with the aim of studying their conformity to guarantee availability. Some experiments clarify the relationships between goal availability and the existing design principles, with particular reference to explicitness. Other experiments demonstrate that boosting an analysis with guarantee availability generally makes it deeper, unveiling additional protocol niceties that depending on the analyzer’s skills may remain overseen otherwise. In particular, an established claim about a protocol (made using a well-known formal method) can be subverted. [ABSTRACT FROM AUTHOR]