Merging the Cryptographic Security Analysis and the Algebraic-Logic Security Proof of {PACE}

Lassaad Cheikhrouhou, Werner Stephan, Oezguer Dagdelen, Marc Fischlin, Markus Ullmann

In: Neeraj Suri, Michael Waidner (editor). Sicherheit 2012 - 6. Jahrestagung des Fachbereichs "Sicherheit - Schutz und Zuverlässigkeit" der GI. GI-Fachtagungen March 7-9 Darmstadt Germany Pages 83-94 LNI 195 ISBN 978-3-88579-289-5 GI 2012.


In this paper we report on recent results about the merge of the cryptographic security proof for the Password Authenticated Connection Establishment (PACE), used within the German identity cards, with the algebraic-logic symbolic proof for the same protocol. Both proofs have initially been carried out individually, but have now been combined to get “the best of both worlds”: an automated, error- resistant analysis with strong cryptographic security guarantees.

German Research Center for Artificial Intelligence
Deutsches Forschungszentrum für Künstliche Intelligenz