Title :
Using a formal technique for protocol idealization: a cautionary note
Author_Institution :
Comput. & Inf. Sci. Dept., Univ. of Massachusetts Dartmouth, North Dartmouth, MA, USA
Abstract :
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.
Keywords :
cryptography; formal logic; protocols; BAN-type logics; cryptographic protocols; formal reasoning technique; idealization errors; logical abstraction; protocol idealization; Authentication; Body sensor networks; Computer errors; Concrete; Cryptographic protocols; Error correction; Guidelines; Information analysis; Information science; Logic design;
Conference_Titel :
Database and Expert Systems Applications, 2002. Proceedings. 13th International Workshop on
Print_ISBN :
0-7695-1668-8
DOI :
10.1109/DEXA.2002.1045942
