Detail publikace

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.
Název česky
Formální verifikace vlastností algoritmu CRC
Typ
článek ve sborníku konference
Jazyk
anglicky
Autoři
Smrčka Aleš, Ing., Ph.D. (UITS)
Hlávka Petr, Ing.
Řehák Vojtěch, doc. RNDr.
Šafránek David
Šimeček Pavel
Vojnar Tomáš, prof. Ing., Ph.D. (UITS)
URL
Klíčová slova

CRC formal verification, minimal Hamming distance, colliding messages

Abstrakt

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.

Rok
2006
Strany
55–62
Sborník
MEMICS 2006 Second Doctoral Workshop on Mathematical and Engineering Methods in Computer Science
ISBN
80-214-3287-X
Místo
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"
}
Nahoru