Technical report

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.
Publication language:english
Original title:CRC64 Algorithm Analysis and Verification
Title (cs):Analýza a verifikace CRC64 algoritmu
Place:Brno, CZ
Publisher:CESNET National Research and Education Network
formal verification, model checking, CRC64
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.
   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 = {}

Your IPv4 address:
Switch to https