Verification of security protocols: a multi-agent systems approach

Lead Research Organisation: Imperial College London
Department Name: Dept of 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.

Publications

10 25 50
publication icon
Boureanu I (2010) Model checking detectability of attacks in multiagent systems in 9th International Conference on Autonomous Agents and Multi-Agent systems (AAMAS10)

publication icon
Boureanu I (2012) Automatic verification of temporal-epistemic properties of cryptographic protocols in Journal of Applied Non-Classical Logics

publication icon
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

publication icon
Cohen M (2009) Abstraction in model checking multi-agent systems in 8th International Conference on Autonomous Agents and Multi-Agent systems (AAMAS09)

publication icon
Cohen M. (2009) A symmetry reduction technique for model checking temporal-epistemic logic in IJCAI International Joint Conference on Artificial Intelligence

publication icon
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 £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 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 09/2010 
End 09/2016
 
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