CRC64 Algorithm Analysis and Verification

ŠAFRÁNEK, David; Vojtěch ŘEHÁK; Tomáš KRATOCHVÍLA; Pavel ŠIMEČEK; Petr HLÁVKA and Tomáš VOJNAR. CRC64 Algorithm Analysis and Verification. Brno: CESNET, z. s. p. o., 2005. Technical Report 27/2005.

Basic information

Original name

CRC64 Algorithm Analysis and Verification

Name in Czech

CRC64 Algorithm Analysis and Verification

Authors

ŠAFRÁNEK, David (203 Czech Republic, guarantor); Vojtěch ŘEHÁK (203 Czech Republic); Tomáš KRATOCHVÍLA (203 Czech Republic); Pavel ŠIMEČEK (203 Czech Republic); Petr HLÁVKA (203 Czech Republic) and Tomáš VOJNAR (203 Czech Republic)

Edition

Brno, Technical Report 27/2005, 2005

Publisher

CESNET, z. s. p. o.

---

Other information

Language

English

Type of outcome

Audiovisual works

Field of Study

10201 Computer sciences, information science, bioinformatics

Country of publisher

Czech Republic

Confidentiality degree

is not subject to a state or trade secret

References:

URL

RIV identification code

RIV/00216224:14330/05:00012922

Organization unit

Faculty of Informatics

Keywords in English

CRC64; formal verification; correctness of CRC algorithm

Tags

correctness of CRC algorithm, CRC64, formal verification

---

Abstract

V originále

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.

In Czech

Zpráva obsahuje analýzu a verifikaci algoritmu implementovaného v hardware pro kontrolní součet CRC64. Základy algoritmu CRC jsou popsány v první části právce, po té jsou stanoveny klíčové vlastnosti zaručující korektnost - pravděpodobnost kolize, Hammingova vzálenost a kvalita distribuce hašujících funkcí.

---

Links

GA201/03/0509, research and development project	Name: Automatizovaná verifikace paralelních a distribuovaných systémů Investor: Czech Science Foundation, Automated Verification of Parallel and Distributed Systems
GD102/05/H050, research and development project	Name: Integrovaný přístup k výchově studentů DSP v oblasti paralelních a distribuovaných systémů Investor: Czech Science Foundation, Integrated approach to education of PhD students in the area of parallel and distributed systems
MSM0021622419, plan (intention)	Name: Vysoce paralelní a distribuované výpočetní systémy Investor: Ministry of Education, Youth and Sports of the CR, Highly Parallel and Distributed Computing Systems
1ET408050503, research and development project	Name: Techniky automatické verifikace a validace softwarových a hardwarových systémů Investor: Academy of Sciences of the Czech Republic, Techniques for automatic verification and validation of software nad hardware systems