Publication Details

CRC64 Algorithm Analysis and Verification

HLÁVKA Petr, KRATOCHVÍLA Tomáš, ŘEHÁK Vojtěch, ŠAFRÁNEK David, ŠIMEČEK Pavel and VOJNAR Tomáš. CRC64 Algorithm Analysis and Verification. Brno: CESNET National Research and Education Network, 2005.
Czech title
Analýza a verifikace CRC64 algoritmu
Type
technical report
Language
english
Authors
Hlávka Petr, Ing. (FBM BUT)
Kratochvíla Tomáš (FI MUNI)
Řehák Vojtěch, doc. RNDr. (FI MUNI)
Šafránek David, doc. Mgr., Ph.D. (FI MUNI)
Šimeček Pavel (FI MUNI)
Vojnar Tomáš, prof. Ing., Ph.D. (DITS FIT BUT)
URL
Keywords

formal verification, model checking, CRC64

Abstract

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.

Published
2005
Pages
7
Publisher
CESNET National Research and Education Network
Place
Brno, CZ
BibTeX 
@TECHREPORT{FITPUB7996,
   author = "Petr Hl\'{a}vka and Tom\'{a}\v{s} Kratochv\'{i}la and Vojt\v{e}ch \v{R}eh\'{a}k and David \v{S}afr\'{a}nek and Pavel \v{S}ime\v{c}ek and Tom\'{a}\v{s} Vojnar",
   title = "CRC64 Algorithm Analysis and Verification",
   pages = 7,
   year = 2005,
   location = "Brno, CZ",
   publisher = "CESNET National Research and Education Network",
   language = "english",
   url = "https://www.fit.vut.cz/research/publication/7996"
}
Back to top