Publication Details

Formal Verification of the CRC Algorithm Properties

HLÁVKA Petr, ŘEHÁK Vojtěch, SMRČKA Aleš, ŠAFRÁNEK David, ŠIMEČEK Pavel and VOJNAR Tomáš. Formal Verification of the CRC Algorithm Properties. In: MEMICS 2006 Second Doctoral Workshop on Mathematical and Engineering Methods in Computer Science. Mikulov, 2006, pp. 55-62. ISBN 80-214-3287-X.
Czech title
Formální verifikace vlastností algoritmu CRC
Type
conference paper
Language
english
Authors
Hlávka Petr, Ing. (FBM BUT)
Řehák Vojtěch, doc. RNDr. (FI MUNI)
Smrčka Aleš, Ing., Ph.D. (DITS FIT BUT)
Šafránek David, doc. Mgr., Ph.D. (FI MUNI)
Šimeček Pavel (FI MUNI)
Vojnar Tomáš, prof. Ing., Ph.D. (DITS FIT BUT)
URL
Keywords

CRC formal verification, minimal Hamming distance, colliding messages

Abstract

This paper presents the verification of CRC algorithm properties. We examine
a way of verifying of a CRC algorithm using exhaustive state space exploration
by model checking method. The CRC algorithm is used for calculation of a
message hash value and we focus on verification of the property of finding
minimal Hamming distance between two messages having the same hash value. We
deal with 16, 32 and 64 bits CRC generator polynomials, especially
with one used in the Liberouter project.

Published
2006
Pages
55-62
Proceedings
MEMICS 2006 Second Doctoral Workshop on Mathematical and Engineering Methods in Computer Science
Conference
2nd Doctoral Workshop on Mathematical and Engineering Methods in Computer Science -- MEMICS'06, Mikulov, CZ
ISBN
80-214-3287-X
Place
Mikulov, CZ
BibTeX 
@INPROCEEDINGS{FITPUB8206,
   author = "Petr Hl\'{a}vka and Vojt\v{e}ch \v{R}eh\'{a}k and Ale\v{s} Smr\v{c}ka and David \v{S}afr\'{a}nek and Pavel \v{S}ime\v{c}ek and Tom\'{a}\v{s} Vojnar",
   title = "Formal Verification of the CRC Algorithm Properties",
   pages = "55--62",
   booktitle = "MEMICS 2006 Second Doctoral Workshop on Mathematical and Engineering Methods in Computer Science",
   year = 2006,
   location = "Mikulov, CZ",
   ISBN = "80-214-3287-X",
   language = "english",
   url = "https://www.fit.vut.cz/research/publication/8206"
}
Back to top