Towards an Independent Semantics and Verification Technology for the HLPSL Specification Language

We present an algorithm for the translation of security protocol specifications in the HLPSL language developed in the framework of the AVISPA project to a dialect of the applied pi calculus. This algorithm provides us with two interesting scientific contributions: at first, it provides an independent semantics of the HLPSL specification language and, second, makes it possible to verify protocols specified in HLPSL with the applied pi calculus-based ProVerif tool. Our technique has been implemented and tested on various security protocols. The translation can handle a large part of the protocols modelled in HLPSL.     

Use of a formal description technique in the specification of authentication protocols

Formal specification techniques have been employed over the past decade or so by various workers in data communication and computer network systems in order to provide both definitional specifications of protocols and models of protocols for analytic purposes. This paper considers the use of the specification language LOTOS (Language of Temporal Ordering Specification) for specifying some authentication protocols developed in the security field. The language LOTOS recently became an International ISO Standard and the protocols specified form part of the ISO and CCITT Standards. In fact, the CCITT protocol which is considered in this paper, has been used in the LOCATOR (X.400 Secure Mail) project within HPLabs. We first give a brief introduction to LOTOS and then specify two security protocols from ISO/DP 9798 and CCITT X.509 Standards. We feel that a formal specification of protocols is a useful and a necessary step towards understandability, analysis and implementation of the protocols. Further, we feel that LOTOS possesses the necessary features required for specifying such protocols.     

Specifications,models, and implementations of data abstractions

We consider the specification and verification of modules in hierarchically structured programs, as proposed by Parnas and Hoare. We argue that a specification for such a module is a set of sentences in some logical language in which the names to be exported by the module appear as nonlogical symbols. We further argue that an implementation of one module in terms of another module is a translation of the nonlogical symbols of the first specification into the language of the second. Equality must also be interpreted. We proposed necessary conditions which any such notion of ‘correct implementation’ ought to satisfy. These criteria provide a basis for judging the logical adequacy of any proposed specification language and definition of implementation. We then study DLP, a specification language obtained by adding uninterpreted procedure symbols to Pratt's first order dynamic logic. We present a definition of ‘implementation’ for DLP, and we show it satisfies these conditions. The main theorem, called the implementation Theorem, extends the Interpretation Theorem from first-order logic to DLP. The proof of this theorem is complicated by the necessity of dealing with modalities, parameters to procedures, interpretations of equality, and interpretations of sorts as tuples.     

Hlpsl2Cpp——一个安全协议编译器

安全协议的人工实现是一个低效且易错的过程.安全协议编译器Hlpsl2Cpp可以自动从用HLPSL语言描述的安全协议生成C 的协议实现代码.Hlpsl2Cpp节省了人工实现协议的大量重复劳动,避免了人工实现安全协议带来的各种讹误和实现相关漏洞.     

安全协议的规范化设计

提出运用组合方法进行安全协议设计。给出了协议中基件与组件的定义,根据组件的安全属性设计实现相应安全目标的单步协议;定义组合规则,确保不同的单步协议能够组合成为一个复合协议,同时各个单步协议还能实现各自的安全目标。根据具体的应用背景选择合适的单步协议,按照组合规则组合后可得到满足需求的安全协议。该组合方法可将一个复合协议分解为若干基于组件的简单单步协议,使得协议的设计与分析易于实现。     

On constructing communication protocols from component-based service specifications

Constructing communication protocols from component service specifications, each of which specifies a subfunction of the target protocol, enables efficient development of a large and complex communication protocol. Concerning this construction, related techniques have been already proposed: integration of component protocol specifications into a single protocol specification and transformation of service specifications to protocol specifications. However, the integration needs special knowledge of communication protocols, and the transformation requires that a large and complex service specification should be developed as input to produce the target protocol. In order to cope with these problems, this paper proposes a new method which at first integrates component service specifications into a single service specification, and then transforms the service specification into the target protocol by a protocol synthesis technique. The most important point of view is that component integration is performed at the service specification level rather than the protocol specification level. Additionally, we define a class of ‘well-formed’ service specification which ensures correctness of the target protocol. As a result, the integration and transformation can be efficiently executed in small state space without special knowledge of communication protocols. Finally, we have shown the effectiveness of the proposed method by constructing a part of the real-life OSI protocol FTAM.     

Development and Structure of an X.25 Implementation

This paper describes experience with an implementation of the X25 communication protocols for accessing public data networks. Ihe implementation effort is characterized by: 1) the development of a formalized protocol specification on which all further implementation work is based, and 2) the use of Concurrent Pascal as the implementation language. The main features of the formalized protocol specification are given, and a method for deriving a protocol implementation based on parallel processes, monitors, and classes is explained. The overall structure of the system and the step-wise refinements leading to the complete implementation are discussed. Some comments on the possible implementation on multiple microprocessors are also given.     

Requirements for a Practical Network Event Recognition Language

We propose a run-time monitoring and checking architecture for network protocols called Network Event Recognition. Our framework is based on passively monitoring the packet trace produced by a protocol implementation and checking it for properties written in a formal specification language, NERL. In this paper, we describe the design requirements for NERL. We show how the unique requirements of network protocol monitoring impact design and implementation options. Finally we outline our prototype implementation of NERL and discuss two case studies: checking the correctness of network protocol simulations and privacy issues in packet-mode surveillance.     

An algebraic specification of method combination for the Common Lisp Object System

The Common Lisp Object System (CLOS) is an extension of Common Lisp for object-oriented programming being designed as part of the ANSI X3J13 Common Lisp standardization process. This report describes an algebraic specification of the method combination and application component of CLOS. The specification is based on a draft of the standard presented to the ANSI committee in spring of 1987, and was done using an executable, typed functional programming language called Axis. The result suggests a logical mapping from the abstract data types and operations in the specification to the classes and methods which could become that part of the CLOS kernel (called the metaobject protocol) involved in method combination. In addition, the existence of a formal algebraic specification for CLOS allows the effects of changes in the language to be tested during the design phase, rather than during implementation. This is illustrated by showing how the language semantics change when thecall-next-method function is allowed to take arguments, an extension proposed in the draft standard. Standardization documents like the CLOS standard are usually written in a semi-natural language, but if they are accompanied by an additional formal specifiction during their generation, the probability of undetected or lately discovered errors in the design decreases, and the specification also provides an unambiguous source of reference for implementors.     

一个基于属性文法的通信协议形式描述语言及协议开发环境

通信协议是网络技术的核心。由于异质构环境中网络协议固有的复杂性,因此需要研制一磁建立在严格数学模型基础这之上的协议开发方法和集成工具环境,以降低协议开发难度,提高协议开发效率。本文旨在探索一种用于协议形式描述和工程开发的扩展属性文法,重点研究了设计属性文法描述语言的原理及结构特点等,并通过一个完整例子说明如何使用我们所设计的属性文法描述语言Ｌ＿ＰＳＡＧ定义一个协议,然后给出一个基于属性文法的协议设     

The synthesis of communication protocols

We define a notation (specification language) for describing desired patterns of communication among components of a distributed system through multiport, unreliable channels. Our language specifies the network topology, and the kinds of information transmission desired. We give a polynomial-time algorithm for determining whether a specification is satisfiable; our algorithm can actually construct a protocol that achieves the specified exchange of information, optimized with respect to two possible criteria. Examples suggest that our method can automatically synthesize reasonably complex protocols.     

Formal Analysis of Multiparty Contract Signing

We analyze the multiparty contract-signing protocols of Garay and MacKenzie (GM) and of Baum and Waidner (BW). We use a finite-state tool, Mocha, which allows specification of protocol properties in a branching-time temporal logic with game semantics. While our analysis does not reveal any errors in the BW protocol, in the GM protocol we discover serious problems with fairness for four signers and an oversight regarding abuse-freeness for three signers. We propose a complete revision of the GM subprotocols in order to restore fairness.     

Modelling and querying geographical data warehouses

A number of proposals for integrating geographical (Geographical Information Systems—GIS) and multidimensional (data warehouse—DW and online analytical processing—OLAP) processing are found in the database literature. However, most of the current approaches do not take into account the use of a GDW (geographical data warehouse) metamodel or query language to make available the simultaneous specification of multidimensional and spatial operators. To address this, this paper discusses the UML class diagram of a GDW metamodel and proposes its formal specifications. We then present a formal metamodel for a geographical data cube and propose the Geographical Multidimensional Query Language (GeoMDQL) as well. GeoMDQL is based on well-known standards such as the MultiDimensional eXpressions (MDX) language and OGC simple features specification for SQL and has been specifically defined for spatial OLAP environments based on a GDW. We also present the GeoMDQL syntax and a discussion regarding the taxonomy of GeoMDQL query types. Additionally, aspects related to the GeoMDQL architecture implementation are described, along with a case study involving the Brazilian public healthcare system in order to illustrate the proposed query language.     

HB协议的形式规约与验证

形式化方法是确保安全协议设计正确性的重要工具,利用形式化方法已经发现了许多安全协议的设计错误.首次利用形式规约语言Z对RFID安全协议HB进行形式规约, 并对HB协议应该满足的安全性质进行形式化描述,使用Z模式推理从协议及其运行环境两个方面验证了协议的关键安全属性,发现了HB协议在设计方面的缺陷,提出了HB协议的一种改进方法.