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.
- 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.
- 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.
- 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
|
