Verifying Security Properties in Unbounded Multiagent Systems
File(s)
Accepted version
Author(s)
Boureanu, I
Kouvaros, P
Lomuscio, A
Type
Conference Paper
Abstract
We study the problem of analysing the security for an unbounded number of concurrent sessions of a cryptographic protocol. Our formal model accounts for an arbitrary number of agents involved in a protocol-exchange which is subverted by a Dolev-Yao attacker. We define the parameterised model checking problem with respect to security requirements expressed in temporal-epistemic logics. We formulate sufficient conditions for solving this problem, by analysing several finite models of the system. We primarily explore authentication and key-establishment as part of a larger class of protocols and security requirements amenable to our methodology. We introduce a tool implementing the technique, and we validate it by verifying the NSPK and ASRPC protocols.
Date Issued
2016-05-13
Date Acceptance
2016-05-09
Citation
Proceedings of the 2016 International Conference on Autonomous Agents & Multiagent Systems (AAMAS '16), 2016, pp.1209-1217
ISBN
978-1-4503-4239-1
Publisher
ACM
Start Page
1209
End Page
1217
Journal / Book Title
Proceedings of the 2016 International Conference on Autonomous Agents & Multiagent Systems (AAMAS '16)
Copyright Statement
© 2016 International Foundation for Autonomous Agents and Multiagent Systems. This is the author's version of the work. It is posted here for your personal use. Not for redistribution. The definitive Version of Record was published in Proceedings of the 2016 International Conference on Autonomous Agents & Multiagent Systems.
Sponsor
Engineering & Physical Science Research Council (EPSRC)
Commission of the European Communities
Engineering & Physical Science Research Council (EPSRC)
Grant Number
EP/I00520X/1
661362
COLAR_P60375
Source
2016 International Conference on Autonomous Agents & Multiagent Systems (AAMAS '16)
Start Date
2016-05-09
Finish Date
2016-05-09
Coverage Spatial
Singapore