Protocol elaboration via the authentication tests
 
Joshua Guttman, The MITRE Corporation


 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.