非表示:
キーワード:
-
要旨:
We investigate a resolution-based verification method for
secrecy and authentication properties of cryptographic protocols.
In experiments, we could enforce its termination by
\emph{tagging}, a syntactic transformation of messages that leaves
attack-free executions invariant. In this paper, we generalize the
experimental evidence: we prove that the verification method always
terminates for tagged protocols.
