Verification of security protocols: a multi-agent systems approach
Lead Research Organisation:
Imperial College London
Department Name: Computing
Abstract
The project investigates automatic verification of computer security protocols by using formal tools and techniques drawn from the areas of multi-agent systems, automatic verification and formal logic. Upon succesful completion of the project, a range of security protocols will be verified automatically by computer tools.
People |
ORCID iD |
| Alessio Lomuscio (Principal Investigator) |
Publications
Boureanu I
(2012)
Automatic verification of temporal-epistemic properties of cryptographic protocols
in Journal of Applied Non-Classical Logics
Boureanu I
(2010)
Model checking detectability of attacks in multiagent systems
in 9th International Conference on Autonomous Agents and Multi-Agent systems (AAMAS10)
Boureanu I.
(2012)
Automatic verification of epistemic specifications under convergent equational theories
in 11th International Conference on Autonomous Agents and Multiagent Systems 2012, AAMAS 2012: Innovative Applications Track
Cohen M
(2009)
Abstraction in model checking multi-agent systems
in 8th International Conference on Autonomous Agents and Multi-Agent systems (AAMAS09)
Cohen M.
(2009)
A symmetry reduction technique for model checking temporal-epistemic logic
in IJCAI International Joint Conference on Artificial Intelligence
Lomuscio A
(2015)
MCMAS: an open-source model checker for the verification of multi-agent systems
in International Journal on Software Tools for Technology Transfer
| Description | In the project we developed novel methodologies for verifying security protocols. We have put forward languages to specify security protocols and developed new effective ways to verify their correctness. We have been able to verify protocols before deployment and put forward techniques to detect anomalies at run time. |
| Exploitation Route | The software we released is open source and can be suitably extended by others. The theory we developed is published in academic journals and conferences and can likewise be extended. In a security context the methodology can be expanded to assess privacy properties in communication protocols and the robustness of evoting protocols. |
| Sectors | Aerospace Defence and Marine Digital/Communication/Information Technologies (including Software) Security and Diplomacy |
| Description | The findings have been used in an academic context to verify the correctness of major security and evoting protocols. |
| Sector | Digital/Communication/Information Technologies (including Software),Security and Diplomacy |
| Impact Types | Cultural Economic |
| Description | Imperial College London |
| Amount | £1,080,000 (GBP) |
| Funding ID | EP/I00520X/1 |
| Organisation | Engineering and Physical Sciences Research Council (EPSRC) |
| Sector | Public |
| Country | United Kingdom |
| Start | 08/2010 |
| End | 09/2016 |
| Description | Imperial College London |
| Amount | £380,000 (GBP) |
| Funding ID | 257593 (EU FP7 STREP) |
| Organisation | Imperial College London |
| Sector | Academic/University |
| Country | United Kingdom |
| Start | 01/2007 |
| End | 01/2010 |
| Description | Polish Academy of Sciences |
| Organisation | Polish Academy of Sciences |
| Country | Poland |
| Sector | Public |
| PI Contribution | In this collaboration we jointly developed methodologies for the verification of autonomous systems. Specifically we provided BDD-based expertise and developed novel forms of symbolic model checking. |
| Collaborator Contribution | The Polish partners at PAS contributed bounded-model checking methodologies and parameter synthesis techniques that we adapted for the verification of multi-agent systems. |
| Impact | Andrew V. Jones, Michal Knapik, Wojciech Penczek, Alessio Lomuscio: Group synthesis for parametric temporal-epistemic logic. AAMAS 2012:1107-1114 Alessio Lomuscio, Wojciech Penczek: Symbolic Model Checking for Temporal-Epistemic Logic. Logic Programs, Norms and Action 2012:172-195 Alessio Lomuscio, Wojciech Penczek, Monika Solanki, Maciej Szreter: Runtime Monitoring of Contract Regulated Web Services. Fundam. Inform. (FUIN) 111(3):339-355 (2011) Alessio Lomuscio, Wojciech Penczek, Hongyang Qu: Partial order reductions for model checking temporal epistemic logics over interleaved multi-agent systems. AAMAS 2010:659-666 Alessio Lomuscio, Monika Solanki, Wojciech Penczek, Maciej Szreter: Runtime monitoring of contract regulated web services. AAMAS 2010:1449-1450 Alessio Lomuscio, Wojciech Penczek, Hongyang Qu: Partial Order Reductions for Model Checking Temporal-epistemic Logics over Interleaved Multi-agent Systems. Fundam. Inform. (FUIN) 101(1-2):71-90 (2010) Alessio Lomuscio, Wojciech Penczek: LDYIS: a Framework for Model Checking Security Protocols. Fundam. Inform. (FUIN) 85(1-4):359-375 (2008) Alessio Lomuscio, Wojciech Penczek, Hongyang Qu: Towards Partial Order Reduction for Model Checking Temporal Epistemic Logic. MoChArt 2008:106-121 Alessio Lomuscio, Wojciech Penczek, Bozena Wozna: Bounded model checking for knowledge and real time. Artif. Intell. (AI) 171(16-17):1011-1038 (2007) Alessio Lomuscio, Wojciech Penczek: Logic Column 19: Symbolic Model Checking for Temporal-Epistemic Logics CoRR abs/0709.0446 (2007) Alessio Lomuscio, Wojciech Penczek: Symbolic model checking for temporal-epistemic logics. SIGACT News (SIGACT) 38(3):77-99 (2007) Magdalena Kacprzak, Alessio Lomuscio, Artur Niewiadomski, Wojciech Penczek, Franco Raimondi, Maciej Szreter: Comparing BDD and SAT Based Techniques for Model Checking Chaum's Dining Cryptographers Protocol. Fundam. Inform. (FUIN) 72(1-3):215-234 (2006) Bozena Wozna, Alessio Lomuscio, Wojciech Penczek: Bounded model checking for knowledge and real time. AAMAS 2005:165-172 Bozena Wozna, Alessio Lomuscio, Wojciech Penczek: Bounded Model Checking for Deontic Interpreted Systems. Electr. Notes Theor. Comput. Sci. (ENTCS) 126:93-114 (2005) 2004 Magdalena Kacprzak, Alessio Lomuscio, Wojciech Penczek: Verification of Multiagent Systems via Unbounded Model Checking. AAMAS 2004:638-645 Magdalena Kacprzak, Alessio Lomuscio, T. Lasica, Wojciech Penczek, Maciej Szreter: Verifying Multi-agent Systems via Unbounded Model Checking. FAABS 2004:189-212 Magdalena Kacprzak, Alessio Lomuscio, Wojciech Penczek: From Bounded to Unbounded Model Checking for Temporal Epistemic Logic. Fundam. Inform. (FUIN) 63(2-3):221-240 (2004) 2003 Wojciech Penczek, Alessio Lomuscio: Verifying epistemic properties of multi-agent systems via bounded model checking. AAMAS 2003:209-216 Wojciech Penczek, Alessio Lomuscio: Verifying Epistemic Properties of Multi-agent Systems via Bounded Model Checking. Fundam. Inform. (FUIN) 55(2):167-185 (2003) Alessio Lomuscio, T. Lasica, Wojciech Penczek: Bounded Model Checking for Interpreted Systems: Preliminary Experimental Results. FAABS 2002:115-125 |
| Start Year | 2007 |