Ceremonies Formal Analysis in PKI’s Context
Jean Everson Martina
University of Cambridge
Computer Laboratory
15 JJ Thomson Avenue
Cambridge – United Kingdom
Email: Jean.Martina@cl.cam.ac.uk
Tu´lio Cı´cero Salvaro de Souza, Ricardo Felipe Custo´dio
Laborato´rio de Seguranc¸a em Computac¸a˜o
Universidade Federal de Santa Catarina
Caixa Postal 476 – 88040-900
Floriano´polis – SC – Brasil
Email: fsalvaro,custodiog@inf.ufsc.br
Abstract—Ceremonies are a useful tool to establish trust in
scenarios where protocols operate. They describe a greater
range of issues not taken into account by protocol designers.
We take an already-designed protocol and ceremony for a key
management protocol operating in a Public-Key Infrastructure
environment and test it using a formal method. The ceremonies
were analysed to test human peers’ cognition pitfalls using
formal methods. The analysis came up with a potential cogni-
tive slip in one early design. This directly affects trust in the
protocol.
Keywords-Key Management Protocols, Ceremony Design,
Ceremony Analysis
I. INTRODUCTION
Despite being important to safe protocol operation, cere-
monies are not often seen in research. Recently, ceremony
design and analysis were introduced by Ellison [1], [2].
He states: “ceremonies extends the concept of protocols
by including human beings as nodes in the network”, this
can be extended even further to the environment and the
relations between subjects and security targets, dealing di-
rectly with their capacity for trust establishment. This kind
of description gives a broader coverage of out of bounds
operations which arise from day-by-day protocol usage. We
also note that human peers are often mentioned in protocol
designs, since a protocol is commonly defined as a system
of rules used during a ceremony, but normally their expected
behaviour is not tested against the protocols’ goals. We adopt
the idea of ceremonies as extensions of protocols, taking into
account environmental variables and by extension human
peers.
Ellison establishes the basis on ceremony description. He
describes the important out of bounds operations that we
should consider in ceremony analysis. Although he states
the possibility of using formal methods available for security
protocol analysis, no major work is found today. This lead to
empirical analysis, which proved to be hard and error-prone.
Our idea is to use Ellison’s approach and to survey in the,
until now untouched, area of formal ceremony verification.
Jean Everson Martina is supported by the CAPES Foundation/Brazil on
grant #4226-05-4
Taking Ellison’s ideas on security ceremonies requires a
vast amount of things to be covered to declare a ceremony
secure and trusted. One reasonable approach is breaking the
problem into small parts and try to verify them separately.
By dividing the approach we can find two different classes of
problems to deal with when analysing ceremonies: The first
regards humans peers interaction/expectation and the second
regards environmental conditions which the ceremony is
subject to. The problem regarding human peers - choice of
the current work - can be understood as how adapted the
protocol is to cope with limitations of humans behind the
computer screens. Especially how this affects the security
and trust in a systematic manner. The second class is broader,
and can include almost anything that is not included in the
ceremony as a protocol or a human peer. Furthermore, the
representation and verification of environmental conditions
in ceremonies, and, by extension, protocols, can be a key
to understand better problems on protocols’ composability,
making them trustworthy.
The work of Ruksˇe˙nas et al. [3], [4] can answer part
of the first class of problems. They developed a human
error cognitive model, which was applied to interaction with
interfaces. This model can be directly applied to a human-
protocol interface. Furthermore, taking recent Ruksˇe˙nas et
al. [3] extensions, cognitive slips can be easily verified in
protocols in the presence of attackers. Their model supports
a description of any human peer in protocols, taking its point
of view, describing its interpretation, the effects it can cause
in security and it’s impressions on the protocol run (trust).
Another important feature of Ruksˇe˙nas et al. is the support
of environmental descriptions. Although not yet developed,
it shows potential to model the second class of interactions.
Ruksˇe˙nas et al. does not formalise the environment due to
its complexity, but leaves an input to add it later.
An approach to embrace Ruksˇe˙nas et al. method and
use it in ceremonies is by applying it using Bella’s [5]
goal availability ideas. By this principle, we must take
into account each peers point of view and work towards
guarantees available to each human peer. The approach
requires that the guarantees must be checkable only by what
is visible to the peer during its participation. This correlates