A framework for proving the correctness of cryptographic protocol properties by linear temporal logic

Alabdulatif, A, Ma, X ORCID: https://orcid.org/0000-0003-0074-4192 and Nolle, L, 2013. A framework for proving the correctness of cryptographic protocol properties by linear temporal logic. International Journal of Digital Society (IJDS), 4 (2), pp. 789-797. ISSN 2040-2570

Preview

Text 219534_PubSub1929.Ma.pdf Download (2MB) | Preview

Abstract

In this paper, a framework for cryptographic protocol analysis using linear temporal logic is proposed. The framework can be used to specify and analyse security protocols. It aims to investigate and analyse the security protocols properties that are secure or have any flaws. The framework extends the linear temporal logic by including the knowledge of participants in each status that may change over the time. It includes two main parts, the Language of Temporal Logic (LTL) and the domain knowledge. The ability of the framework is demonstrated by analysing the Needham-Schroeder public key protocol and the Andrew Secure RPC protocol as examples.

Item Type:	Journal article
Publication Title:	International Journal of Digital Society (IJDS)
Creators:	Alabdulatif, A., Ma, X. and Nolle, L.
Publisher:	Infonomics Society
Date:	2013
Volume:	4
Number:	2
ISSN:	2040-2570
Identifiers:	Number Type 10.20533/ijds.2040.2570.2013.0096 DOI 539813 Other
Divisions:	Schools > School of Science and Technology
Record created by:	EPrints Services
Date Added:	09 Oct 2015 10:56
Last Modified:	27 Mar 2024 15:20
URI:	https://irep.ntu.ac.uk/id/eprint/20360

Actions (login required)

Edit View

Statistics

Views

Downloads