University of Surrey

Test tubes in the lab Research in the ATI Dance Research

Verifying Security Properties in Unbounded Multiagent Systems

Boureanu, IC, Kouvaros, P and Lomuscio, A (2016) Verifying Security Properties in Unbounded Multiagent Systems In: 2016 International Conference on Autonomous Agents & Multiagent Systems (AAMAS '16), 2016-05-09 - 2016-05-13, Singapore.

Full text not available from this repository.


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.

Item Type: Conference or Workshop Item (Conference Paper)
Subjects : Computing
Divisions : Surrey research (other units)
Authors :
Kouvaros, P
Lomuscio, A
Date : 9 May 2016
Funders : Engineering and Physical Sciences Research Council (EPSRC)
Copyright Disclaimer : © 2016 International Foundation for Autonomous Agents and Multiagent Systems ( All rights reserved.
Contributors :
publisherInternational Foundation for Autonomous Agents and Multiagent Sy,
Depositing User : Symplectic Elements
Date Deposited : 17 May 2017 13:58
Last Modified : 23 Jan 2020 19:00

Actions (login required)

View Item View Item


Downloads per month over past year

Information about this web site

© The University of Surrey, Guildford, Surrey, GU2 7XH, United Kingdom.
+44 (0)1483 300800