Imperial College London


Faculty of EngineeringDepartment of Computing

Professor of Logic for Multiagent Systems



+44 (0)20 7594 8414a.lomuscio Website




504Huxley BuildingSouth Kensington Campus






BibTex format

author = {Boureanu, I and Kouvaros, P and Lomuscio, A},
pages = {1209--1217},
title = {Verifying security properties in unbounded multiagent systems},
url = {},
year = {2016}

RIS format (EndNote, RefMan)

AB - Copyright © 2016, International Foundation for Autonomous Agents and Multiagent Systems ( All rights reserved. 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.
AU - Boureanu,I
AU - Kouvaros,P
AU - Lomuscio,A
EP - 1217
PY - 2016///
SN - 1548-8403
SP - 1209
TI - Verifying security properties in unbounded multiagent systems
UR -
ER -