Composable Formal Models
for High-Assurance Fault Tolerant Networks
Case Study:
Formal Modeling and Analysis of a Secure Service Proxy Toolkit
Abstract
In a distributed system, a remote service framework must provide mechanisms
for service publication and discovery, and for interacting with remote
services. In addition there should be support for a variety of security
properties: protecting information communicated between client and server,
assuring client and server of each others identity, and enforcing access
policies. The latter should be largely transparent to the client and service
applications. To address these requirements, the Secure Service Proxy
Toolkit (SSPTK), was developed by John Mitchell, Ninghui Li, and Derrick
Tong at Stanford, based on Java RMI and Jini technologies. The objective of
the work reported herein was to formally model and analyze the SSPTK using
Maude (http://maude.cs.uiuc.edu). The formal models developed provided
clear documentation of the design, and refined it to provide security
protection tuned to against different types of attack. In the process of
modeling and analysis a security hole was found in the design (and
implementation) that was subsequently fixed. To analyze these models,
models of attackers with different capabilities were developed. Properties
of interest, for example success of different attacks, were modeled as as
patterns such that a system state satisfies the property if it matches the
pattern. Analysis resulted in tables documenting which attacks succeed or
fail for toolkits providing given security levels.