DocumentCode
2430830
Title
Using a formal technique for protocol idealization: a cautionary note
Author
Mathuria, Anish
Author_Institution
Comput. & Inf. Sci. Dept., Univ. of Massachusetts Dartmouth, North Dartmouth, MA, USA
fYear
2002
fDate
2-6 Sept. 2002
Firstpage
468
Lastpage
472
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;
fLanguage
English
Publisher
ieee
Conference_Titel
Database and Expert Systems Applications, 2002. Proceedings. 13th International Workshop on
ISSN
1529-4188
Print_ISBN
0-7695-1668-8
Type
conf
DOI
10.1109/DEXA.2002.1045942
Filename
1045942
Link To Document