Doctoral School of Information Science and Technology

Department of Telecommunications, Faculty of Electrical Engineering and Informatics

Supervisor: Dr. BUTTYÁN Levente

Formal Analysis of Security Protocols

Introducing the research area

The security of infocommunication networks and computer systems are very important issues nowadays. Conventional data security objectives, such as secrecy, integrity and authenticity, can be achieved by the application of security protocols.  Unfortunately, designing security protocols is a very difficult issue, which is confirmed by the fact that critical security holes are found in many widely used security protocols.           

Informal analysis of security protocols and systems is error-prone, thus, it is not considered to be a reliable approach. Instead, formal analysis and systematic methods are required, which are more precise. One further advantage of using formal methods is that they enable automated verification.  

 

The goal of my research is to propose effective formal and automated verification methods with allow either proving the security of protocols and systems or detect security holes. My research covers three main topics: formal analysis of security APIs; automated verification of secure routing protocols; and automated misconfiguration detection in stateful firewalls. 

Brief introduction of the research place

Currently I am working at the Laboratory of Cryptography and System Security (CrySyS). The laboratory provides outstanding research and teaching in the field of cryptography and system security. The heads of the laboratory are Dr. István Vajda and my supervisor, Dr. Levente Buttyán. Our main research areas include the security of wireless systems and embedded systems. More details about our laboratory can be found here.

History and context of the research

Hardware Security Modules (HSM) are indispensable in many applications, such as ATM networks and electronic commerce. HSMs are hardware devices which has some tamper resistance properties, and are used to store secrets such as cryptographic keys. The primary goal of attacking an HSM is to extract the secret data stored in it. Classic attacks against HSMs are physical attacks, which usually make use of expensive equipment. However, HSMs can also be attacked through their Application Programming Interfaces (API) by exploiting some design weaknesses in the API’s logic. Being fully software based, this kind of attacks is much cheaper than physical attacks. Many API attacks have been found against several widely-used, commercially available HSMs, which otherwise provide very strong physical protection [3,5]. (More)

Ad-hoc networks are not based on pre-defined topology, thus, in order to allow one party to communicate with an another party, route discovery is accomplished. Once a route between two parties has been found, they start to exchange data on this route such that each party in the route forward the packet it received to the target. The route discovery procedure is defined by routing protocols. Numerous attacks against routing protocols have been published, in which attacker(s) can achieve that the honest parties attempt to exchange data through the route that does not exist in reality, without being aware of it [9]. This type of attacks is critical because they can lead to futile energy consumption and degrade the efficiency of the network. (More)

Firewalls play an important role in the enforcement of access control policies in contemporary networks. However, firewalls are effective only if they are configured correctly such that their access rules are consistent and the firewall indeed implements and enforces the intended access control policy. Unfortunately, due to the potentially large number of access rules and their complex relationships with each other, the task of firewall configuration is error-prone, and in practice, firewalls are often misconfigured leaving security holes in the protection system [6,7]. Methods for detecting misconfiguration in stateful firewalls need to be proposed. (More)

In all the three areas formal and automated security verification methods are required.

The research goal, open questions

There are many questions in each field that I have to answer:

Real life security APIs may contain thousands of functions, which generates a huge number of states during the verification. Furthermore, functions may execute specific operations and use special elements that are difficult to model. Methods published earlier are inefficient, because they lack formal syntax and semantics for reasoning about cryptographic operations. My goal is to propose a better approach. (More)        

During the automatic verification of routing protocols a large number of network topology and a strong attacker model need to be considered. This induces a huge number of states to be examined, which a computer cannot always handle. My goal is to propose the first method that can handle arbitrary network topology and strong attacker model, which previous methods cannot. (More)    

The ruleset of stateful firewalls periodically varies during the automated verification and may contain thousands of access rules. This generate a huge number of states to be checked. Besides, stateful access rules may contain special elements that are very hard to model. Former methods focus entirely on verifying stateless firewalls, which does not meet the state explosion problem. My goal is to provide a method  for stateful case. (More)

Methodology

In the topic of analyzing security APIs, I applied the well-known spi-calculus [2] and the ProVerif [1] automated verification tool for this purpose. Both the spi-calculus and the ProVerif tool are originally proposed for analyzing security protocols and not for security APIs. However, in my publications I showed that by some modifications they can be applied in a new context, namely, to analyze security APIs. The main advantage of my method compared to other, non-algebra based methods, is that it can provide more expressive and precise modelling language and more effective verification at the same time. (More)

In the topic of analyzing security verifying secure routing protocols, my goal was to propose a new formal language and new automated verification tool that are optimized for secure routing protocols. So far, no formal and automated verification methods have been proposed specifically for secure routing protocols. Previous methods use general purpose model-checking tools, which are not designed for reasoning about ad-hoc networks. Hence, they lack syntax and semantics to model ad-hoc networks. Additionally, their verification algorithms are not optimized to secure routing protocols. My method, on the one hand, is a combination and extension of three well-known calculi, namely, CMAN, the applied pi-calculus and the omega-calculus [10,11,12]. On the other hand, my automated verification tool is the extension of the well-known ProVerif tool. (More)

In the topic of detecting misconfigurations in stateful firewalls, I applied the terminology of static analysis. In particular, my method is based on FIREMAN [8], an automatic tool proposed for detecting misconfigurations in stateless firewalls. In contrast to the stateless firewalls the ruleset of stateful firewalls are periodically changed. Therefore, the verification in stateful case seems to be more difficult than the stateless case. In my publication I showed that this is not the case, in particular, I proved that the problem of verification of stateful firewalls can be simplified to the problem of stateless case. (More)

Results

I proposed an algebra based method for automated verification of security APIs of Hardware Security Modules [18,19,22,25]. To the best of my knowledge this is the first application of algebra for analyzing security APIs. I applied my method in the SeVeCom - Secure Vehicular Communication European project, which investigated the secure communication between future vehicles in order to prevent accidents on the roads. To achieve secure communications cryptographic protocols are used, which require the usage of cryptographic keys. To store these keys, hardware security modules are setup in vehicles. I used my method to verify the security API proposed for the this hardware module. (More)

 

To verify secure routing protocols I proposed a new algebra based formal language and new automated verification software tool [21,23,24, 26]. The main advantage of my method compared to the previous approaches is that it is designed specifically for secure routing protocols, hence, it is more effective than methods based on general purpose  tools. To my best knowledge, this is the first method that was optimized for secure routing protocols. I applied my method to analyze well-known routing protocols such as SRP [13] and Ariadne [14]. Besides, my method was applied in the WSAN4CIP – Securing Tomorrow's Critical Infrastructures European project. (More)

I proposed an efficient automated method for detecting inconsistency in the rulesets of stateful firewalls based on the well-known FIREMAN tool [20]. For detecting inconsistency in the rulesets of stateful firewalls I proposed an efficient automated method and a verification software tool based on the theoretical approach. I applied my method to verify the firewall of our laboratory. To the best of my knowledge, I was the first who proposed an automated misconfiguration detection method in stateful firewalls.  (More) 

Expected impact and further research

In the future, I aim at improving the efficiency of my methods and applying them to verify security APIs used at banks and firewalls of companies. The topic of verifying security APIs is a promising topic because the problem of API attacks is not only present in ATM networks, but in many other contexts such as attacking the APIs designed for web, facebook, and android application developers. In the future, I will extend my method of verifying APIs in those contexts. Finally, I'm also working on a fourth topic that is concerned with the automated security verification of transport layer protocols.

Publications, references, links

References:

[1] M. Abadi and B. Blanchet. Analyzing Security Protocols with Secrecy Types and Logic Programs. Journal of the ACM (JACM). 52(1):102–146, Jan. 2005. (PDF)

[2] M. Abadi and A. Gordon. A calculus for cryptographic protocols: the Spi calculus. Technical Report SRC RR 149, Digital Equipment Corporation, Systems Research Center, January 1998. (PDF)

[3] R. Anderson, M. Bond, J. Clulow, and S. Skorobogatov. Cryptographic processors – a survey. Technical Report UCAM-CL-TR-641, University of Cambridge, Computer
Laboratory, August 2005.  (PDF)

[4] B. Blanchet. Automatic Proof of Strong Secrecy for Security Protocols. In IEEE Symposium on Security and Privacy, pages 86–100, Oakland, California, May 2004. (PDF)

[5] M. Bond. Understanding security APIs. PhD thesis, University of Cambridge, 2004. (PDF)

[6]  E. Al-Shaer and H. Hamed. Design and Implementation of Firewall Policy Advisor Tools. Technical Report CTI-techrep0801, School of Computer Science Telecommunications and Information Systems, DePaul University, August 2002. (PDF)

[7] Ehab Al-Shaer, Hazem Hamed, Raouf Boutaba and Masum Hasan. Conflict Classification and Analysis of Distributed Firewall Policies. IEEE Journal on selected areas in communications, vol. 23., No. 10, October 2005. (PDF)

[8] L. Yuan, J. Mai, Z. Su, H. Chen, C. Chuah, and P. Mohapatra. FIREMAN: A toolkit for firewall modeling and analysis. In IEEE Symposium on Security and Privacy, pages199–213, 2006.(PDF)

[9] Gergely Ács. Secure Routing in Multi-hop Wireless Networks. PhD Thesis. February 2009. University of Technology and economics. (PDF)

[10] C. Fournet and M. Abadi. Mobile values, new names, and secure communication. Proceedings of the 28th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p:104–115,  2001. (PDF)

[11] A. Singh, C. R. Ramakrishnan, and S. A. Smolka. A process calculus for mobile ad hoc networks. Sci. Comput. Program., 75(6):440–469, 2010. (PDF)

[12] J. C. Godskesen. A calculus for mobile ad hoc networks. In COORDINATION Journal, pages 132–150, 2007. (PDF)

[13] P. Papadimitratos and Z. Haas. Secure routing for mobile ad hoc networks. In Networks and Distributed Systems Modeling and Simulation, 2002. (PDF)

[14] Y.-C. Hu, A. Perrig, and D. B. Johnson. Ariadne: a secure on-demand routing protocol for ad hoc networks. Wirel. Netw., 11(1-2):21–38, 2005. (PDF)

My publications

Conference and Magazines

[18] L. Buttyán, T. V. Thong. Security API analysis with the spi-calculus. Hiradástechnika, vol. LXII, 8, 2007, pp. 43–49. (PDF) 

[19] L. Buttyán, T. V. Thong. Security API analysis with the spi-calculus. Hiradástechnika, vol. LXIII, 1, 2008, pp. 16–21.(PDF)

[20] L. Buttyán, G. Pék, T. V. Thong. Consistency verification of stateful firewalls is not harder than the stateless case. Infocommunications Journal, vol. LXIV, no. 2009/2-3, 2–3, 2009. (PDF)

[21] L. Buttyán, T. V. Thong. Formal verification of secure ad-hoc network routing protocols using deductive model-checking. IFIP Wireless and Mobile Networking Conference (WMNC’2010). (PDF)

Journals

[22] F. Kargl, P. Papadimitratos, L. Buttyan, M. Mueter, E. Schoch, B. Wiedersheim, Ta Vinh Thong, G. Calandriello, A. Held, A. Kung, J.-P. Hubaux. Secure Vehicular Communication Systems: Implementation, Performance, and Research Challenges. IEEE Communications Magazine, Vol. 46, No. 11, November 2008. (PDF)

[23] L. Buttyán, T. V. Thong. Formal verification of secure ad-hoc network routing protocols using deductive model-checking. Periodica Polytechnica Journal, 2011. (PDF)

[24] T. V. Thong, L. Buttyán. On automating the verification of secure ad-hoc network routing protocols. Telecommunication Systems Journal 2011. (PDF)

Others

[25 ] T. V. Thong. Security API analysis with the spi-calculus, 2008, BME. (PDF)

[26] L. Buttyán, T. V. Thong. Formal verification of secure ad-hoc network routing protocols, 2010, BME. (PDF)