Publication result 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

English Title

Formal Verification of the CRC Algorithm Properties

Type

Paper in proceedings (conference paper)

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.

English 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

Key words in English

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.

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