Anlauff, M., Pavlovic, D., Waldinger, R., and Westfold, S. Proving Authentication Properties in the Protocol Derivation Assistant, in FLoC-06 Joint Workshop on Foundations of Computer Security and Automated Reasoning for Security Protocol Analysis, Springer Lecture Notes in Computer Science, August 2006.
Abstract
We present a formal framework for incremental reasoning about authentication protocols, supported by the Protocol Derivation Assistant (Pda). A salient feature of our derivational approach is that proofs of properties of complex protocols are factored into simpler proofs of properties of their components, combined with proofs that the relevant refinement and composition operations preserve the proven properties or transform them in the desired way. In the present paper, we introduce an axiomatic theory of authentication suitable for the automatic proof of authentication properties. We describe a proof of the authentication property of a simple protocol, as derived in Pda, for which the the proof obligations have been automatically generated and discharged. Producing the proof forced us to spell out previously unrecognized assumptions, on which the correctness of the protocol depends.
Pda is a public-domain tool, with support for collaboration and for tool integration.
Keywords: Artificial Intelligence, security, authentication, theorem proving, derivation, protocols, Pda, Specware, SNARK