Merging the Cryptographic Security Analysis and the Algebraic-Logic Security Proof of PACE.
Lassaad Cheikhrouhou, Stephan Werner, Özgür Dagdelen, Marc Fischlin, Markus Ullmann · 2012
Abstract: In this paper we report on recent results about the merge of the cryp-tographic 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. 1