Deductive Verification of Cryptographic Software

[摘要] We report on the application of an off-the-shelf verification platform to the RC4 stream cipher cryptographic software implementation (as available in the openSSL library), and introduce a deductive verification technique based on self-composition for proving the absence of error propagation.

[发布日期] 2009-04-01

[学科分类] 软件