Beta 1


Title Secure Protocol Implementation with LySa
Author Vind, Søren
Vildhøj, Hjalte Wedel
Supervisor Pilegaard, Henrik (Language-Based Technology, Department of Informatics and Mathematical Modeling, Technical University of Denmark, DTU, DK-2800 Kgs. Lyngby, Denmark)
Institution Technical University of Denmark, DTU, DK-2800 Kgs. Lyngby, Denmark
Thesis level Bachelor thesis
Year 2009
Abstract Using LySatool it is possible to verify security properties such as confidentiality and authentication for protocols modelled in the LySa process calculus[1][2]. However, before a protocol can be used in practice it must be implemented in a suitable programming language. If this implementation is not done properly, it risks breaking the security properties guaranteed by LySatool. In this thesis we introduce YALT, Yet Another LySa Translator, that automatically derives protocol implementations in Java from LySa specifications. To facilitate the derivation, we create an extension of the LySa calculus called metaLySa. YALT also features a sophisticated LySa runtime environment used to execute generated protocol implementations. We account for the challenges in designing this tool and present the application FilePilot that uses the runtime environment to transfer les securely with user-selected protocol implementations. YALT requires the Java Cryptography Extension Unlimited Strength Jurisdiction Policy Files, for which installation guidelines is enclosed in section 4.3.1.2.
Series IMM-B.Sc.-2009-21
Fulltext
Original PDF bac09_21.pdf (2.71 MB)
Admin Creation date: 2009-07-20    Update date: 2010-08-25    Source: dtu    ID: 247185    Original MXD