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.

Originální název

Formal Verification of the CRC Algorithm Properties

Typ

článek ve sborníku ve WoS nebo Scopus

Jazyk

angličtina

Originální 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.

Klíčová slova

CRC formal verification, minimal Hamming distance, colliding messages

Autoři

SMRČKA, A.; HLÁVKA, P.; ŘEHÁK, V.; ŠAFRÁNEK, D.; ŠIMEČEK, P.; VOJNAR, T.

Rok RIV

2006

Vydáno

16. 11. 2006

Místo

Mikulov

ISBN

80-214-3287-X

Kniha

MEMICS 2006 Second Doctoral Workshop on Mathematical and Engineering Methods in Computer Science

Strany od

55

Strany do

62

Strany počet

8

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"
}