[Prev][Next][Index][Thread]
Cryptographic Protocol Logic (CPL)
The extended abstract for the LICS2003 short presentation
"A Language and a Notion of Truth for Cryptographic Properties"
is available at:
http://lampwww.epfl.ch/~kramer/publ/kramer-LICS03.pdf
MINI ABSTRACT:
We provide a logical language and outline a notion of truth for the
specification and verification of cryptographic protocols. The language
integrates modalities for temporal, epistemic, and normative statements.
It allows one to express and compare arbitrary cryptographic properties
intuitively, succinctly, and in an endogenous fashion. The notion of
truth
is external and defined through satisfaction in terms of models of
generic
guarded cryptographic processes. It allows for mechanical verification
by means of model-checking.
The formalism will be called CPL (for Cryptographic Protocol Logic).
Latest changes to the formalism (not mentioned in the extended
abstract):
(1) the replacement of the predicate for syntactic equality of messages
by
a predicate for sub-term-related messages
(2) the addition of two atomic predicates for typing messages and
sub-typing message types