Formal Modelling of Cryptographic Protocols in Situation Calculus

José Hernández-Orallo, Javier Pinto

Abstract

We present here a generic model in Situation Calculus (S.C.) to formalise several cryptographic protocols. It distinguishes from other logics of cryptographic modelling using the concepts of believing or secret because it is based on the concepts of knowledge and it will not be required any special construct out of S.C. As a working example, we take the ISO/IEC 9798-2 5.1.2 protocol, which we specify formally. Subsequently we prove some correction properties of it. Expecting the range of applications and a possible semi-automatisation of proofs, maybe the most promising result till now is that the protocol specification remains in an extremely plain and explicit manner, justifying per se the formalisation. In the end, we comment a set of requirements that are necessary to the general goal of fully formalising cryptographic protocols.
Key words: Cryptography, Situation Calculus, Security Protocols, Knowledge Modelling, ISO/IEC 9798-2 5.1.2. protocol

Go back to my home page .