Imperial College London

ProfessorAlessioLomuscio

Faculty of EngineeringDepartment of Computing

Professor of Logic for Multiagent Systems
 
 
 
//

Contact

 

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

 
 
//

Location

 

504Huxley BuildingSouth Kensington Campus

//

Summary

 

Publications

Citation

BibTex format

@inproceedings{Boureanu:2016,
author = {Boureanu, I and Kouvaros, P and Lomuscio, A},
pages = {1209--1217},
publisher = {ACM},
title = {Verifying Security Properties in Unbounded Multiagent Systems},
url = {http://hdl.handle.net/10044/1/34130},
year = {2016}
}

RIS format (EndNote, RefMan)

TY  - CPAPER
AB - 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
PB - ACM
PY - 2016///
SP - 1209
TI - Verifying Security Properties in Unbounded Multiagent Systems
UR - http://hdl.handle.net/10044/1/34130
ER -