Strand spaces: why is a security protocol correct?

摘要: A strand is a sequence of events; it represents either the execution an action by legitimate party in security protocol or else actions penetrator. space collection strands, equipped with graph structure generated causal interaction. In this framework, correctness claims may be expressed terms connections between strands different kinds. paper, we develop notion space. We then prove generally useful lemma, as sample result giving general bound on abilities penetrator any protocol. apply formalism to Needham-Schroeder-Lowe (G. Lowe, 1995, 1996). Our approach gives detailed view conditions under which achieves authentication and protects secrecy values exchanged. also use our proof methods explain why original Needham-Schroeder (1978) fails. believe that distinguished from other work verification simplicity model ease producing intelligible reliable proofs even without automated support.