Publication detail

Formal Verification of the CRC Algorithm Properties

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

Original Title

Formal Verification of the CRC Algorithm Properties

Type

conference paper

Language

English

Original 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

Authors

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

RIV year

2006

Released

16. 11. 2006

Location

Mikulov

ISBN

80-214-3287-X

Book

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

Pages from

55

Pages to

62

Pages count

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