Detail publikace

CRC64 Algorithm Analysis and Verification

HLÁVKA, P. KRATOCHVÍLA, T. ŘEHÁK, V. ŠAFRÁNEK, D. ŠIMEČEK, P. VOJNAR, T.

Originální název

CRC64 Algorithm Analysis and Verification

Typ

zpráva odborná

Jazyk

angličtina

Originální abstrakt

This work analyzes the use of a CRC64 algorithm as a hashing function in the Netflow project. We describe the basis of Cyclic Redundancy Check (CRC) algorithms and consider properties like collision probability, Hamming distance, and quality of distribution, which are crucial for hashing functions. Lower or upper bounds of these properties are described mathematically. However, to give more precise numbers to hardware designers, we also try to find them using model checking method.

Klíčová slova

formal verification, model checking, CRC64

Autoři

HLÁVKA, P.; KRATOCHVÍLA, T.; ŘEHÁK, V.; ŠAFRÁNEK, D.; ŠIMEČEK, P.; VOJNAR, T.

Rok RIV

2005

Vydáno

2. 12. 2005

Nakladatel

CESNET National Research and Education Network

Místo

Brno

Strany počet

7

URL

http://www.cesnet.cz/doc/techzpravy/2005/crc64/

BibTex

@techreport{BUT57653,
  author="Petr {Hlávka} and Tomáš {Kratochvíla} and Vojtěch {Řehák} and David {Šafránek} and Pavel {Šimeček} and Tomáš {Vojnar}",
  title="CRC64 Algorithm Analysis and Verification",
  year="2005",
  publisher="CESNET National Research and Education Network",
  address="Brno",
  pages="7",
  url="http://www.cesnet.cz/doc/techzpravy/2005/crc64/"
}