Formal Verification of the CRC Algorithm Properties

SMRČKA, Aleš, Petr HLÁVKA, David ŠAFRÁNEK, Vojtěch ŘEHÁK, Pavel ŠIMEČEK and Tomáš VOJNAR. Formal Verification of the CRC Algorithm Properties. In Proceedings of 2nd Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS 2006). Brno: FIT BUT, 2006, p. 55-62. ISBN 80-214-3287-X.

Basic information

Original name

Formal Verification of the CRC Algorithm Properties

Name in Czech

Formální verifikace vlastností CRC algoritmů

Authors

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

Edition

Brno, Proceedings of 2nd Doctoral Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS 2006), p. 55-62, 2006

Publisher

FIT BUT

---

Other information

Language

English

Type of outcome

Stať ve sborníku

Field of Study

10201 Computer sciences, information science, bioinformatics

Country of publisher

Czech Republic

Confidentiality degree

není předmětem státního či obchodního tajemství

RIV identification code

RIV/00216224:14330/06:00015972

Organization unit

Faculty of Informatics

ISBN

80-214-3287-X

Keywords in English

formal verification; CRC algorithms; generating polynomial

Tags

CRC algorithms, formal verification, generating polynomial

Tags

International impact, Reviewed

---

Abstract

V originále

This paper presents verification of the CRC algorithm properties. We examine a way of verifying the CRC algorithm using exhaustive state space exploration by model checking method. The CRC algorithm is used for the calculation of the hash value of a message and we focused to verify the property of finding minimum Hamming distance between two messages having the same hash value. We deal with some of 16, 32 and 64 bits CRC generator polynomials, especially with one used in the Liberouter project, for comparison with others used in the ethernet networking.

In Czech

Článek se zabývá experimentální metodou ověření vlastností algoritmů CRC používaných v projektu Liberouter při vývoji síťového hardware. Zejména je navržena a v případové studii demonstrována metoda hledání minimální Hammingovy vzdálenosti dvou zpráv naléžejícím témuž hashovacímu klíči (kolizní dvojice). Při navrhovaném přístupu je použito metody ověřování modelů.

---

Links

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
1M0545, research and development project	Name: Institut Teoretické Informatiky Investor: Ministry of Education, Youth and Sports of the CR, Institute for Theoretical Computer Science