25 October 2007, Logic Tea, Simon Kramer

We propose a denotational definition for the (actual) meaning of a cryptographic message and, based on it, an equational definition for the context-sensitivity of that meaning, both via hypothetical knowledge and provability. As a result, we obtain a formalisation of the first of Abadi and Needham's principles for prudent engineering practice for - and a tentative denotational semantics of - cryptographic protocols. Building on this (published) work, we present ongoing work on the distinction between the intended and the actual meaning of a cryptographic message and protocol. Our notions are viable for general multi-agent systems.

The Logic Tea homepage can be found at http://www.illc.uva.nl/logic_tea/ For more information, please contact Joel Uckelmann (juckelma at science.uva.nl) or Edgar Andrade (E.J.AndradeLotero at uva.nl