Dr Anca Jurcut
Research Interests: Network Security, Security Protocols Design & Analysis, Automated Techniques for Formal Verification, Cryptography, Security for Internet of Things , Blockchain Technologies, Mathematical Modelling
My research focus on network and information security, security for internet of things (IoT), applications of blockchain technologies, security protocols, formal verification techniques and mathematical modelling.
Some of the key contributions of my research include: (i) development of a novel logic-based technique for the formal verification of protocols; (ii) design and implementation of an automated tool (CDVT/AD: Crytpographic-Procotol Development and Verification Tool with Attack Detection) for the formal analysis and design validation of security protocols; (iii) discovery of several hitherto unknown protocol design flaws and the publication of new verifiably correct protocols; (iv) development and publication of a new set of design guidelines to guarantee protocol robustness against attacks.
Crytpographic-Procotol Development and Verification Tool with Attack Detection (CDVT/AD) is an automated system implementing a modal logic of knowledge and an attack detection theory. Hence, CDVT/AD tool can analyse both:
(a) the evolution of knowledge and belief during a protocol execution and therefore it is useful in addressing issues of both security and trust and
(b) the design vulnerabilities of a protocol and therefore it is useful for the detection of freshness, interleaving session and man-in-the-middle attacks.
Additionally, another benefit of using CDVT/AD tool is that this verification technique is very efficient in terms of memory requirements and execution times (i.e. milliseconds) required for protocol verification . Furthermore, this tool successfully verified a large and various set of security protocols , , , ,  .
How to use CDVT/AD Tool:
Prior to the automated verification the protocol must be formalized, i.e. translated into the language of the tool (i.e.Protocol Specification Language (PSL) - paper that details the language of CDVT/AD tool and demonstrates its application by demonstrating the use of CDVT/AD tool, finding weaknesses in the protocol, and correcting the design of the verified protocol)
A formalized protocol consists of three components:
1. Initial assumptions (conditions that hold before the protocol starts);
2. Protocol steps (the messages exchanged between the principals);
3. Protocol goals (conditions that are expected to hold if the protocol terminates successfully).
Sample Specification File: Contains the formalisation into the language of the CDVT_AD tool of Andrew Secure RPC protocol.
The CDVT/AD tool applies the axioms and rules of the implemented logic of knowledge in an attempt to derive the protocol goals as a logical consequence of the initial assumptions and the protocol steps. If such a derivation exists, the verification is successful and the verified protocol can be considered secure within the scope of the logic.
- Braeken, A., Liyanage, M., Jurcut, A. D., “Anonymous Lightweight Proxy Based Key Agreement for IoT (ALPKA)”, Wireless Personal Communications: 1-20, 2019.
- Jurcut, A.D., Coffey, T., Dojen, R., "A Novel Security Protocol Attack Detection Logic with Unique Fault Discovery Capability for Freshness Attacks and Interleaving Session Attacks", In: IEEE Transactions on Dependable and Secure Computing, IEEE Xplore, Print ISSN: 1545-5971, Online ISSN: 1545-5971, 10.1109/TDSC.2017.2725831, available under the "Early Access" on IEEEXplore, 11 July 2017.
- Liyanage, L., Braeken, An., Jurcut, A.D., Ylianttila, M.,Gurtov. A., “Secure Communication Channel Architecture for Software Defined Mobile Networks”, Journal of Computer Networks114:32-50 , Elsevier, February 2017 DOI: 10.1016/j.comnet.2017.01.007
- Jurcut, A.D., Coffey, T. , Dojen, R., “Design Guidelines for Security Protocols to Prevent Replay & Parallel Session Attacks”, Journal of Computers & Security, Elsevier, Volume 45, pp. 255–273, September 2014, DOI: 10.1016/j.cose.2014.05.010
- Jurcut, A.D., Coffey, T., Dojen, R., “Establishing and Fixing Security Protocols Weaknesses using a Logic-based Verification Tool”, Journal of Communication, Vol. 8, No. 11, ISSN 1796-2021, pp. 795-806 , November 2013, DOI: 10.12720/jcm.8.11.795-805
- Jurcut, A.D., Liyanage, M., Chen J., Gyorodi C., He, J., “On the Security Verification of a Short Message Service Protocol”, 16th IEEE Wireless Communications and Networking Conference, Barcelona, Spain , April 2018.
- Ranaweera, P., Jurcut, A.D., Liyanage, M., “Realizing Multi-Access Edge Computing Feasibility:Security Perspective”, accepted at IEEE Conference on Standards for Communications and Networking (CSCN 2019), Granada, Spain, October 2019.
- Jurcut, A.D., Coffey, T., Dojen, R., "On the Prevention and Detection of Replay Attacks using a Logic-based Verification Tool", In: Computer Networks, Series: Communications in Computer and Information Science, Springer International Publishing Switzerland, Volume 431, ISBN: 978-3-319-07940-0, pp. 128-137, June , 2014.
- Jurcut, A.D., Coffey, T., Dojen, R., "Design requirements to counter parallel session attacks in security protocols", Twelfth Annual Conference on Privacy, Security and Trust (PST 2014), IEEE, ISBN: 978-1-4799-3502-4, pp. 298 - 305, Toronto, Canada , July 2014, DOI: 10.1109/PST.2014.6890952.
- Dojen, R., Jurcut, A., Coffey, T. and Gyorodi, C., “On establishing and fixing a parallel session attack in a security protocol”, In: Intelligent Distributed Computing, Systems and Applications, Series: Studies in Computational Intelligence, Springer Berlin / Heidelberg, Volume 162/2008, ISBN 978-3-540-85256-8, pp.239-244, September 2008, DOI: 10.1007/978-3-540-85257-5_24