非表示:
キーワード:
-
要旨:
We study an automatic technique for the verification of cryptographic
protocols based on a Horn clause model of the protocol. This technique
yields proofs valid for an unbounded number of sessions of the
protocol. However, up to now, it gave no definite information
when the proof failed.
In this paper, we present an algorithm for reconstructing
an attack against the protocol when the desired security property
does not hold.
We have proved soundness, termination, as well as a partial completeness
result for our algorithm. We have also implemented it in the automatic
protocol verifier ProVerif.
As an extreme example, we could reconstruct an attack involving 200
parallel sessions against the f$^{200}$g$^{200}$ protocol.
