Cordial Security Protocol Programming The Obol Protocol Language

摘要

Obol is a protocol programming language. The language is domain specific, and has been designed to facilitate error-free implementation of security protocols. Selecting the primitives of the language is, basically, concerned with determining which issues needs to be visible to the protocol programmer, and which can be left to the runtime without further ado. The basic abstractions of Obol has been modelled after the ones offered by the BAN logic of authentication. By building on these abstractions Obol makes it less hard to bridge the gap between logical analysis and implementation. Obol has been designed with the implementation of security protocols in mind, but the language can be used to implement also other types of protocols. At the core of the design and implementation is pattern-matching machinery enabling the runtime to parse packets as they arrive in order to free the programmer from a wide range of low-level issues know to foster all sorts of implementation difficulties.