Logical formalisation and analysis of the Mifare Classic card in PVS

DOI10.1007/978-3-642-22863-6_3zbMATH Open1342.68288OpenAlexW1507859865MaRDI QIDQ3087992FDOQ3087992

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

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

Mathematics Subject Classification ID

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

Cites Work

• Formal certification of code-based cryptographic proofs
• Isabelle/HOL. A proof assistant for higher-order logic
• Models and Proofs of Protocol Security: A Progress Report
• A survey of symbolic methods in computational analysis of cryptographic systems
• Title not available (Why is that?)
• Fundamentals of cryptology. A professional reference and interactive tutorial. Incl. 1 CD-ROM

Cited In (1)

• Formal analysis of PIN block attacks

Uses Software

• Isabelle
• Isabelle/HOL
• PVS

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)