Logics for reasoning about cryptographic constructions

摘要

We present two logical systems for reasoning about cryptographic constructions which are sound with respect to standard cryptographic definitions of security. Soundness of the first system is proved using techniques from non-standard models of arithmetic. Soundness of the second system is proved by an interpretation into the first system. We also present examples of how these systems may be used to formally prove the correctness of some elementary cryptographic constructions.