Result Details
Formal Verification of the CRC Algorithm Properties
SMRČKA, A.; HLÁVKA, P.; ŘEHÁK, V.; ŠAFRÁNEK, D.; ŠIMEČEK, P.; VOJNAR, T. Formal Verification of the CRC Algorithm Properties. In MEMICS 2006 Second Doctoral Workshop on Mathematical and Engineering Methods in Computer Science. Mikulov: 2006. p. 55-62. ISBN: 80-214-3287-X.
Type
conference paper
Language
English
Authors
Smrčka Aleš, Ing., Ph.D., DITS (FIT)
Hlávka Petr, Ing.
Řehák Vojtěch, doc. RNDr.
Šafránek David, doc. RNDr., Ph.D.
Šimeček Pavel
Vojnar Tomáš, prof. Ing., Ph.D., DITS (FIT)
Hlávka Petr, Ing.
Řehák Vojtěch, doc. RNDr.
Šafránek David, doc. RNDr., Ph.D.
Šimeček Pavel
Vojnar Tomáš, prof. Ing., Ph.D., DITS (FIT)
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.
Keywords
CRC formal verification, minimal Hamming distance, colliding messages
URL
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
ISBN
80-214-3287-X
Place
Mikulov
BibTeX
@inproceedings{BUT22282,
author="Aleš {Smrčka} and Petr {Hlávka} and Vojtěch {Řehák} and David {Šafránek} and Pavel {Šimeček} and Tomáš {Vojnar}",
title="Formal Verification of the CRC Algorithm Properties",
booktitle="MEMICS 2006 Second Doctoral Workshop on Mathematical and Engineering Methods in Computer Science",
year="2006",
pages="55--62",
address="Mikulov",
isbn="80-214-3287-X"
}
Projects
Integrated approach to education of PhD students in the area of parallel and distributed systems, GACR, Doktorské granty, GD102/05/H050, start: 2005-01-01, end: 2008-12-31, completed
Optická síť národního výzkumu a její nové aplikace, MŠMT, Výzkumná centra (2000-2004), MSM6383917201, start: 2004-01-01, end: 2010-12-31, completed
Optická síť národního výzkumu a její nové aplikace, MŠMT, Výzkumná centra (2000-2004), MSM6383917201, start: 2004-01-01, end: 2010-12-31, completed
Research groups
Departments