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

Ma, X ORCID: 0000-0003-0074-4192, 2013. A framework for proving the correctness of cryptographic protocol properties by linear temporal logic. International Journal of Digital Society (IJDS), 41 (12), pp. 749-757. ISSN 2040-2570

[img]
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: Ma, X.
Publisher: Infonomics Society
Date: 2013
Volume: 41
Number: 12
ISSN: 2040-2570
Divisions: Schools > School of Science and Technology
Depositing User: EPrints Services
Date Added: 09 Oct 2015 10:56
Last Modified: 09 Jun 2017 13:45
URI: http://irep.ntu.ac.uk/id/eprint/20360

Actions (login required)

Edit View Edit View

Views

Views per month over past year

Downloads

Downloads per month over past year