Using a formal technique for protocol idealization: a cautionary note
Anish Mathuria · 2004
Analysis of cryptographic protocols by BAN-type logics requires an idealization step to transform a concrete protocol into a logical abstraction. Experience shows that the idealization task is notoriously error-prone. A protocol may be seriously flawed, yet an incorrect idealization can cause a proof of a protocol's correctness using the logical rules to go through. Mao (1995) has proposed a formal reasoning technique to guard against protocol idealization errors. A simple example demonstrates that his technique misses certain kinds of idealization errors that appear to be within its scope.