Formal Verification of the CRC Algorithm Properties

SMRČKA, Aleš, Petr HLÁVKA, David ŠAFRÁNEK, Vojtěch ŘEHÁK, Pavel ŠIMEČEK a 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, s. 55-62. ISBN 80-214-3287-X.

Základní údaje

Originální název

Formal Verification of the CRC Algorithm Properties

Název česky

Formální verifikace vlastností CRC algoritmů

Autoři

SMRČKA, Aleš (203 Česká republika), Petr HLÁVKA (203 Česká republika), David ŠAFRÁNEK (203 Česká republika, garant), Vojtěch ŘEHÁK (203 Česká republika), Pavel ŠIMEČEK (203 Česká republika) a Tomáš VOJNAR (203 Česká republika)

Vydání

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

Nakladatel

FIT BUT

---

Další údaje

Jazyk

angličtina

Typ výsledku

Stať ve sborníku

Obor

10201 Computer sciences, information science, bioinformatics

Stát vydavatele

Česká republika

Utajení

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

Kód RIV

RIV/00216224:14330/06:00015972

Organizační jednotka

Fakulta informatiky

ISBN

80-214-3287-X

Klíčová slova anglicky

formal verification; CRC algorithms; generating polynomial

Štítky

CRC algorithms, formal verification, generating polynomial

Příznaky

Mezinárodní význam, Recenzováno

---

Anotace

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.

Česky

Č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ů.

---

Návaznosti

GD102/05/H050, projekt VaV	Název: Integrovaný přístup k výchově studentů DSP v oblasti paralelních a distribuovaných systémů Investor: Grantová agentura ČR, Integrovaný přístup k výchově studentů DSP v oblasti paralelních a distribuovaných systémů
MSM0021622419, záměr	Název: Vysoce paralelní a distribuované výpočetní systémy Investor: Ministerstvo školství, mládeže a tělovýchovy ČR, Vysoce paralelní a distribuované výpočetní systémy
1M0545, projekt VaV	Název: Institut Teoretické Informatiky Investor: Ministerstvo školství, mládeže a tělovýchovy ČR, Institut Teoretické Informatiky