Formal Specification of Sectrace:
A Protocol to Set up Security Associations and Policies in IPSec Networks

Keywords: IPSec, Security Associations, Security Policies, Formal Specification

To provide encryption and authentication services IPSec assumes the existence of suitable security associations and policies. Setting up such associations and policies is not a trivial task, especially in the presence of nested channels and concatenated channels involving several security gateways. Since IPSec does not address this problem, the sectrace protocol has be designed in the draft below. In the context of the CONTESSA project we have developped an executable formal specification of the protocol and performed some preliminary analysis. Our analysis indicated that the solutions found by the protocol are not always optimal, because certain possibilities to set up correct security associations are missed. It also shows that that concurrent runs of the protocol can cause undesirable interference effects. As a result ouf this analysis we are currently investigating formal prototypes of alternative protocol designs.

Relevant References:

1. SECURE TRACEROUTE (SECTRACE), Draft 0, December 2002, Carl A. Gunter, Alwyn Goodloe, and Michael McDougall
2. SECURE TRACEROUTE (SECTRACE), Draft 1, March 2003, Carl A. Gunter, Alwyn Goodloe, and Michael McDougall

Presentations:

1. Formal Specification of Sectrace (joint work with A. Sridharanarayanan), Workshop on Context Sensitive Systems Assurance (Contessa'03), April 1, 2003, Philadelphia. Slides available here: ps pdf.

The Formal Specification in Maude 2.0 (available here) can be found here.
This package contains the following files:

• README: instructions on how to run the examples
• sectrace.maude: specification of the programming language syntax
• Examples:
  • basic-test-1.maude: simple example with concatenation of security associations
    basic-test-1.sol: result of analysis
  • basic-test-2.maude: simple example with nested tunnels
    basic-test-2.sol: result of analysis
  • ext-test-seq-c1-c2.maude: example with two clients from the sectrace draft (sequential execution c1 ; c2)
    ext-test-seq-c1-c2.sol: result of analysis
  • ext-test-seq-c2-c1.maude: example with two clients from the sectrace draft (sequential execution: c2 ; c1)
    ext-test-seq-c2-c1.sol: result of analysis
  • ext-test-inter.maude: example with two clients from the sectrace draft (concurrent execution: c1 || c2)
    ext-test-inter.sol: result of analysis
    ext-test-inter.trace1: trace for equivalence class 1 of solutions
    ext-test-inter.trace2: trace for equivalence class 2 of solutions
    ext-test-inter.trace3: trace for equivalence class 3 of solutions
    ext-test-inter.trace4: trace for equivalence class 4 of solutions
    (a graphical representation of these traces can be found in the CONTESSA workshop presentation)