×

Probabilistic relational verification for cryptographic implementations. (English) Zbl 1284.68380

Proceedings of the 41st ACM SIGPLAN-SIGACT symposium on principles of programming languages, POPL ’14, San Diego, CA, USA, January 22–24, 2014. New York, NY: Association for Computing Machinery (ACM) (ISBN 978-1-4503-2544-8). 193-205 (2014).

MSC:

68Q60 Specification and verification (program logics, model checking, etc.)
03B70 Logic in computer science
68N18 Functional programming and lambda calculus
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
94A60 Cryptography

Software:

Coq; EasyCrypt; Ynot; z3
PDFBibTeX XMLCite
Full Text: DOI