Compositional logic for proof of correctness of proposed UDT security mechanisms

Bernardo, DV; Hoang, DB

Compositional logic for proof of correctness of proposed UDT security mechanisms

Bernardo, DV

Hoang, DB

Permalink

Publication Type:: Conference Proceeding
Citation:: Proceedings - International Conference on Advanced Information Networking and Applications, AINA, 2012, pp. 686 - 694
Issue Date:: 2012-05-14

Closed Access

	Filename	Description	Size
	2012004351OK.pdf		344.39 kB	Adobe PDF	View/Open

Copyright Clearance Process

Recently Added
In Progress
Closed Access

This item is closed access and not available.

Full metadata record

Field	Value	Language
dc.contributor.author	Bernardo, DV https://orcid.org/0000-0002-0533-6377	en_US
dc.contributor.author	Hoang, DB https://orcid.org/0000-0003-1798-4926	en_US
dc.date.issued	2012-05-14	en_US
dc.identifier.citation	Proceedings - International Conference on Advanced Information Networking and Applications, AINA, 2012, pp. 686 - 694	en_US
dc.identifier.isbn	9780769546513	en_US
dc.identifier.issn	1550-445X	en_US
dc.identifier.uri	http://hdl.handle.net/10453/22957
dc.description.abstract	We present an approach to analyze the applicability and secrecy properties of the selected security mechanisms when implemented with UDT. This approach extends applicability refinement methodology with symbolic model in UDT implementations. In our approach, we carry out a formal proof of correctness, therefore, determining applicability, using formal composition logic. This approach is modular, comprising a separate proof of each protocol section and providing insight into the network environment in which each section can be reliably employed. Moreover, the proof holds for a variety of failure recovery strategies and other implementation and configuration options. We derive our technique from the protocol composite logic on TLS and Kerberos in the literature. We, maintain, however, the novelty of our work for UDT specifically our newly developed mechanisms such as UDT-AO, UDT-DTLS, UDT-Kerberos(GSS-API) specifically for UDT. © 2012 IEEE.	en_US
dc.relation.ispartof	Proceedings - International Conference on Advanced Information Networking and Applications, AINA	en_US
dc.relation.isbasedon	10.1109/AINA.2012.45	en_US
dc.title	Compositional logic for proof of correctness of proposed UDT security mechanisms	en_US
dc.type	Conference Proceeding
utslib.for	0805 Distributed Computing	en_US
dc.location.activity	Fukuoka	en_US
dc.location.activity	Fukuoka Inst Technol (FIT), Fukuoka, JAPAN
pubs.embargo.period	Not known	en_US
pubs.organisational-group	/University of Technology Sydney
pubs.organisational-group	/University of Technology Sydney/Faculty of Engineering and Information Technology
pubs.organisational-group	/University of Technology Sydney/Faculty of Engineering and Information Technology/School of Electrical and Data Engineering
utslib.copyright.status	closed_access
pubs.publication-status	Published	en_US

Abstract:

We present an approach to analyze the applicability and secrecy properties of the selected security mechanisms when implemented with UDT. This approach extends applicability refinement methodology with symbolic model in UDT implementations. In our approach, we carry out a formal proof of correctness, therefore, determining applicability, using formal composition logic. This approach is modular, comprising a separate proof of each protocol section and providing insight into the network environment in which each section can be reliably employed. Moreover, the proof holds for a variety of failure recovery strategies and other implementation and configuration options. We derive our technique from the protocol composite logic on TLS and Kerberos in the literature. We, maintain, however, the novelty of our work for UDT specifically our newly developed mechanisms such as UDT-AO, UDT-DTLS, UDT-Kerberos(GSS-API) specifically for UDT. © 2012 IEEE.

Please use this identifier to cite or link to this item:

http://hdl.handle.net/10453/22957