Logics for reasoning about cryptographic constructions

2 March 2004

conference paper
Published by Institute of Electrical and Electronics Engineers (IEEE)

p. 372-383
https://doi.org/10.1109/sfcs.2003.1238211

Abstract

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 nonstandard 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.

Keywords

This publication has 9 references indexed in Scilit:

Universally composable security: a new paradigm for cryptographic protocols
Published by Institute of Electrical and Electronics Engineers (IEEE) ,2001
A Calculus for Cryptographic Protocols: The Spi Calculus
Information and Computation, 1999
A probabilistic poly-time framework for protocol analysis
Published by Association for Computing Machinery (ACM) ,1998
Bit commitment using pseudorandomness
Journal of Cryptology, 1991
A logic of authentication
Published by Association for Computing Machinery (ACM) ,1989
On the security of public key protocols
IEEE Transactions on Information Theory, 1983
Coin flipping by telephone a protocol for solving impossible problems
ACM SIGACT News, 1983
Theory and application of trapdoor functions
Published by Institute of Electrical and Electronics Engineers (IEEE) ,1982
Existence and feasibility in arithmetic
The Journal of Symbolic Logic, 1971