Conference paper

HLÁVKA Petr, ŘEHÁK Vojtěch, SMRČKA Aleš, ŠAFRÁNEK David, ŠIMEČEK Pavel and VOJNAR Tomáš. Formal Verification of the CRC Algorithm Properties. In: MEMICS 2006 Second Doctoral Workshop on Mathematical and Engineering Methods in Computer Science. Mikulov, 2006, pp. 55-62. ISBN 80-214-3287-X.
Publication language:english
Original title:Formal Verification of the CRC Algorithm Properties
Title (cs):Formální verifikace vlastností algoritmu CRC
Pages:55-62
Proceedings:MEMICS 2006 Second Doctoral Workshop on Mathematical and Engineering Methods in Computer Science
Conference:2nd Doctoral Workshop on Mathematical and Engineering Methods in Computer Science -- MEMICS'06
Place:Mikulov, CZ
Year:2006
ISBN:80-214-3287-X
URL:http://www.fit.vutbr.cz/~smrcka/pub/fmcrc-MEMICS06.pdf [PDF]
Keywords
CRC formal verification, minimal Hamming distance, colliding messages
Annotation
This paper presents the verification of CRC algorithm properties. We examine
a way of verifying of a CRC algorithm using exhaustive state space exploration
by model checking method. The CRC algorithm is used for calculation of a
message hash value and we focus on verification of the property of finding
minimal Hamming distance between two messages having the same hash value. We
deal with 16, 32 and 64 bits CRC generator polynomials, especially
with one used in the Liberouter project.
BibTeX:
@INPROCEEDINGS{
   author = {Petr Hl{\'{a}}vka and Vojt{\v{e}}ch {\v{R}}eh{\'{a}}k and
	Ale{\v{s}} Smr{\v{c}}ka and David {\v{S}}afr{\'{a}}nek and
	Pavel {\v{S}}ime{\v{c}}ek and Tom{\'{a}}{\v{s}} Vojnar},
   title = {Formal Verification of the CRC Algorithm Properties},
   pages = {55--62},
   booktitle = {MEMICS 2006 Second Doctoral Workshop on Mathematical and
	Engineering Methods in Computer Science},
   year = {2006},
   location = {Mikulov, CZ},
   ISBN = {80-214-3287-X},
   language = {english},
   url = {http://www.fit.vutbr.cz/research/view_pub.php?id=8206}
}

Your IPv4 address: 54.234.255.29
Switch to IPv6 connection

DNSSEC [dnssec]