Solution
Security protocols are a highly specialized problem domain. Consequently, general-purpose and relatively low-level tools such as Java aren't always the best match to such a problem domain and its high-level abstractions. For example, when you have to juggle knowledge properties ("A believes B said x" [5]) and authentication derivatives ("A ^ O|B speaks-for A for B" [6]), you really don't want to care about endianess, for-loop indexes, hash-tables, or string encoding. You only want to deal with the security problem at hand. For this reason, we have built the domain-specific Obol language to deal only with security protocols at a level of abstraction that is as close as possible to the theoretical tools used to analyze and describe security protocols. This lets you focus only on the relevant security issues, and allows experimentation without major redesign and reimplementation efforts. If a highly optimized integrated implementation is desirable, this can more easily be done when the resulting protocol and its interface is fully understood.
In any given protocol there are two or more participants. The protocol has a specific purpose and consists of a number of steps that must be taken by participants to fulfill this purpose. For a language dealing only with security protocols, the issues of interest are:
- How to update a participant's local state.
- What data to send to peers.
- What to cryptographically transform (encrypt/decrypt, sign/verify).
- How to receive data from peers and recognize that it is consistent with the protocol.
Obol provides eight operators and a syntactic notation to address these points:
- believe/generate update local state
- encrypt/decrypt, sign/verify deal with cryptographic transformations
- send/receive deal with data transmission
There are other operators, called "metacommands," for controlling the Obol runtime, and dealing with input/output to protocols.
An Obol program is called a "script," and describes a participant's role in the protocol (see the sidebar "How To Program in Obol"). Scripts are interpreted by the Obol runtime, sometimes called "Lobo." Applications connect to the runtime and request that a particular script be loaded and instantiated. A script-dependent handle is then returned to the application. All subsequent interaction with the protocol is done via this handle—starting/stopping, setting and retrieving parameters, state queries, and so on. Figure 1 is an overview of the Obol runtime.
Scripts can configure the runtime to receive messages in two different modes:
- In point-to-point mode, messages are expected to be received synchronously over a given channel.
- In pool-mode, messages can be received asynchronously, on any channel (as long as the runtime is told where to look), and are placed in a pool of received messages, which is then matched to the messages expected by the running scripts.
An early prototype of Obol was written in Common Lisp, and this is still evident in the syntax: parens enclosed prefix statements with a variable number of arguments. Metacommands use square-brackets instead of parens. Like Lisp, symbols are named places to store data values, symbols can have any number of associated key—value properties, of which some are predefined; for example, type (which would be the type of the symbol's value, not the symbol).
