ACTS OKAPI project @ RUN
ULg ACTS OKAPI project RUN
Open Kernel for Access to Protected Interoperable interactive services


Home

People

Research Topics

Projects

Publications

IFIP WG 6.1

Events and Conferences

CSS

How to Reach Us

Main objectives of the project

The European ACTS OKAPI project (AC051) has developed a trusted kernel, which appears like a distributed Operating System. This OKAPI Kernel ensures interoperability, openness, equity, user privacy and evolutivity for opening the European multimedia market to every potential service provider and user. A major target was to achieve through the kernel a maximum degree of commonality for the future European Multimedia Services Distribution System.

For further information on the project, but also on the trials set up in the frame of OKAPI, such as the Kernel Simulator and also information about the research programme and other projects, please refer to the general OKAPI home page.

The Research Unit in Networking (RUN) was involved in three main tasks described below.

  1. Protocol specification and verification

    We use the formal language LOTOS to specify the Equicrypt protocol and verify its robustness to attacks by an intruder. We have used the model-based CADP verification tools from the Eucalyptus toolbox to discover some successful attacks against this protocol.

  2. TCP over ATM

    The ATM Forum proposes four service classes CBR, VBR, ABR and UBR. Recently, the GFR service category (also called UBR+) has been added to provide bandwidth guarantees and with a simpler implementation than ABR in ATM networks. We studied the performance of TCP in a LAN and WAN ATM networks supporting the GFR service category with the proposed FIFO-based and WFQ-based switch implementations. Our simulations show that with the FIFO-based implementation for the GFR service category, TCP is unable to benefit from the bandwidth guarantees. With the proposed WFQ-based implementation, the performance of TCP is good when no losses occur, but it becomes quickly degraded if tagging is used inside the network. These simulations results have been widely discussed within the standardisation bodies during the last few months.

  3. ATM Trial

    ULg also participated in the ATM trial, which consists of interconnecting two sites: CSELT (running the VoD Service Provider) and ULg (running the User). ULg was connected to the JAMES network via Belgacom. Once the connectivity via JAMES was established and operational, the trial was run with success between the two sites. In particular, the video streams have been decrypted in real-time, and the functionality of the certification authority was emulated.

Publications

* Verification of Security Protocols using LOTOS - Method and Application
G. Leduc and F. Germeau
Keywords : LOTOS, model-checking, protocol verification, security protocol
Read the abstract
Download the PDF document
Computer Communications, special issue on Formal Description Techniques in Practice, vol. 23, nb. 12, Jul. 2000, pp. 1089-1103
(ISI IF 2000 = 0.341)
* Model-Based Verification of a Security Protocol for the Conditional Access to Services
G. Leduc, O. Bonaventure, E. Koerner, L. Léonard and C. Pecheur
Keywords : Equicrypt, LOTOS, model checking, security protocols
Read the abstract
Download the PostScript document
Formal Methods in System Design, vol. 14, nb. 2, March 1999, pp. 171-191
* A simulation study of TCP with the GFR service category
O. Bonaventure
Read the abstract
Proc. of Third International Workshop on Architecture and Protocols for High-Performance Networks, 15-20 Jun. 1997, Schloss Dagstuhl, Germany, A. Danthine, O. Spaniol, W. Effelsberg, D. Ferrari (eds.), High-Performance Networks for Multimedia Applications, pp. 19-53, Kluwer Academic Publishers
* A Computer Aided Design of a Secure Registration Protocol
F. Germeau and G. Leduc
Keywords : authentication, formal verification, Guillou-Quisquater, LOTOS sprecification, registration protocol, security, trusted third party
Read the abstract
Download the PostScript document or the compressed PostScript (gzip) document
Proc. of Formal Description Techniques X / Protocol Specification, Testing and Verification XVII (FORTE/PSTV'97), Nov. 1997, Osaka, Japan, Chapman and Hall
* A simulation study of TCP with the proposed GFR service category
O. Bonaventure
Keywords : Asynchronous Tranfer Mode (ATM), simulations, TCP Guaranteed Frame Rate (GFR)
Read the abstract
Download the PostScript document or the compressed PostScript (gzip) document
Dagstuhl Seminar 9725 on High Performance Networks for Multimedia Applications, 15-20 Jun. 1997, Schloss Dagstuhl, Germany
* Model-based Design and Verification of Security Protocols using LOTOS
F. Germeau and G. Leduc
Keywords : authentication, formal verification, LOTOS specification, registration protocol, security, trusted third party
Read the abstract
Download the PostScript document or the compressed PostScript (gzip) document
Proc. of the DIMACS Workshop on Design and Formal Verification of Security Protocols, 3-5 Sep. 1997, Rutgers University, New Jersey
* Specification and verification of a TTP protocol for the conditional access to services
G. Leduc, O. Bonaventure, E. Koerner, L. Léonard, C. Pecheur and D. Zanetti
Keywords : formal verification, LOTOS, model-checking, security protocol
Read the abstract
Download the PostScript document or the compressed PostScript (gzip) document
Proc. of the 12th J. Cartier Workshop on Formal Methods and their Applications: Telecommunications, VLSI and Real-Time Computerized Control Systems, Oct. 1996, Montreal, Canada

[ Home | People | Research Topics | Projects | Publications | IFIP WG 6.1 | Events and Conferences | CSS | How to Reach Us ]

Editor: - G. Leduc -
Webmaster: - C. Soldani -
Still running IPv4 at: 54.161.3.96... RUN | Montefiore | ULg
© 2000-2015.