Logical formalisation and analysis of the Mifare Classic card in PVS

DOI10.1007/978-3-642-22863-6_3MaRDI QIDQ3087992zbMATH OpenOpenAlexFDO

Authors Bart Jacobs, Ronny Wichers Schreur

Publication date 17 August 2011

Published in Interactive Theorem Proving (Search for Journal in Brave)

Full work available at URL http://hdl.handle.net/2066/83531

Mathematics Subject Classification ID

Cryptography (94A60) Authentication, digital signatures and secret sharing (94A62)

Recommendations

• Cryptanalytic attacks on MIFARE classic protocol
• The fall of a tiny star
• A practical attack on patched MIFARE Classic
• Formal analysis of PIN block attacks
• scientific article; zbMATH DE number 1696610

Cites work

• scientific article; zbMATH DE number 4033137 (Why is no real title available?)
• A survey of symbolic methods in computational analysis of cryptographic systems
• Formal certification of code-based cryptographic proofs
• Fundamentals of cryptology. A professional reference and interactive tutorial. Incl. 1 CD-ROM
• Isabelle/HOL. A proof assistant for higher-order logic
• Models and Proofs of Protocol Security: A Progress Report

Cited in

(4)

• Formal analysis of PIN block attacks
• Cryptanalytic attacks on MIFARE classic protocol
• The fall of a tiny star
• A practical attack on patched MIFARE Classic

Describes a project that uses

Uses Software

• PVS
• Isabelle/HOL
• Isabelle

This page was built for publication: Logical formalisation and analysis of the Mifare Classic card in PVS

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3087992)