Disclaimer: This page refers to an external person. It only lists all the interactions between this person and the Crypto Group. Validity or accuracy of the following information is thus not guaranteed in any way.
Seminars given
February 25, 2008 - Protocol elaboration via the authentication tests
by Joshua Guttman
| Abstract: | In practice, cryptographic protocol designers try to use a stepwise
method. They build protocols from simpler versions that achieve some
of the desired goals. Familiar heuristics help keep existing goals
independent of new message structure. In this paper we introduce a
theory to explain when these heuristics are correct.
A permissible refinement step introduces message structure, requiring
additional work in protocol analysis. However, to be permissible, it
must leave unchanged the protocol analysis for the existing message
structure. We represent protocol analysis by a search for minimal,
essentially different executions, driven by unsatisfied
authentication tests.
The protocol analysis search forms a labeled transition system. We
stipulate that the analysis of the more refined protocol Rho must be
weakly bisimilar to the analysis of the less refined protocol Pi.
The silent transitions that make this bisimulation a weak one---all
belonging to the more refined Rho---are the analysis steps required
for Rho's new message structure.
Our main theorem is that weak bisimularity implies that Rho preserves
the security goals achieved by Pi. |
