Dr. Vinh-Thong TA, PhD.
(Tien si cong nghe thong tin)
Address: 56 Boulevard Niels Bohr, 69100 Villeurbanne, France
Office: 8, 3rd floor
E-mails: thong (*) crysys.hu (primary, permanent email)
vinh-thong.ta (*) inria.fr
Vinh-Thong TA was born in 1983 in Hanoi, the capital city of Vietnam. He came to Hungary when he was 9 ages old in 1992. He received the MSc degree in 2008 in computer science from the Budapest University of Technology and Economics (BUTE). He earned the PhD degree in 2014 in IT security from the Budapest University of Technology and Economics (BUTE), at the Laboratory of Cryptography and System Security (CrySyS Lab), under the supervision of Dr. Levente Buttyán. Since Feb. 2014 he works as postdoctoral researcher at Institut national de recherche en informatique et en automatique (INRIA) in Lyon, in the group of Dr. Daniel Le Métayer. At INRIA he investigates possible solutions for privacy by design and accountability problems.
- June 2002: Fazekas Mihály Fővárosi Gyakorló Gimnázium, Budapest, Hungary.
- Specialized mathematics class.
- Jan 2008: MSc Degree at Budapest University of Technology and Economics (BUTE), Budapest, Hungary.
- In computer science and IT security.
- Sept 2008 - Jan 2014: PhD student at Laboratory of Cryptography and System Security (CrySyS), BUTE.
- His research area: Automated and formal security verification of protocols, firewalls, APIs, and systems .
- His supervisor was: Dr. Levente, BUTTYÁN, PhD. associate professor
- 01/2014: PhD degree in Computer Science/ IT security (with Summa Cum Laude)
- Budapest University of Technology and Economics (BME)
- Title: Automated security verification of networking protocols and query auditing algorithms for wireless sensor networks
- defended: January 2014
International courses :
- 2008: SWING, PhD School on Security of Wireless Networking. Bertinoro, Italy. Lecturers :
- Postdoctoral researcher at INRIA (Institut national de recherche en informatique et en automatique) Rhone-Alpes, Lyon.
- Automated verification of security API .
Hardware Security Modules (HSM) are indispensable in many applications, such as ATM networks, public key infrastructures, electronic ticketing in public transportation, electronic payment systems, and electronic commerce, in general. A HSM is a hardware device (including the firmware and software components) which has some tamper resistance properties, and it is used to store cryptographic keys and to perform various security-critical cryptographic operations. Besides physical tampering and side channel attacks, HSMs can also be attacked through their APIs by exploiting some design weaknesses in the API's logic. Being fully software based, this kind of attacks is much less expensive than physical and side-channel attacks, and depending on the weaknesses that are exploited, it may have devastating effects. One promising approach of API analysis is to apply some formal verification method such as those used in software engineering. We follow this approach, and propose an API verification method based on the applied pi-calculus that seems to be extremely well-suited for the formal modeling of security APIs, the precise definition of the security requirements, and the rigorous analysis of the provided security properties. We demonstrate our approach through the analysis of the SeVeCom HSM API. (See the poster of this topic.)
- Automated security verification of firewalls.
Firewalls are routinely used today to protect internal networks from attacks originating from the Internet. However, firewalls are often misconfigured leaving security holes in the defense system. As firewalls can be stateful and firewall rule sets may contain a very large number of rules, such misconfigurations are hard to discover by informal analysis. We are investigating how formal verification techniques can be used to alleviate this problem.(See the poster of this topic.)
- Formal and Automatic security verification of secure routing protocols.
Ad-hoc networks are not based on pre-defined topology, thus, before each data exchange a route discovery is accomplished. The route discovery procedures are defined by routing protocols. Numerous attacks against routing protocols have been published, in which the attacker can achieve that the honest nodes attempt to exchange data through the route that does not exist. This type of attacks is critical because they can lead to futile energy consumption and degrade the efficiency of the network.(See the poster of this topic.)
- Query Auditing in Statistical Databases.
In remote patient monitoring applications, sensor readings are collected on personal mobile device, such as a mobile phone. Third parties can then access these database sending queries to the mobile device. In order to preserve the privacy of users, the mobile device should enforce some access control policy that prevents statistical disclosure of private information. A technique to achieve this is auditing the queries and denying to respond if the response can be used to compute private information, such as the health status of the patients. The goal of the research project is to design and implement such a query auditing algorihm on a mobile platform. (See the paper of this topic.)
- Formal and Automated Security Verification of Transport Protocols. We address the problem of formal and automated security verification of WSN transport protocols that may perform cryptographic operations. The verification of this class of protocols is difficult because they typically consist of complex behavioral characteristics, such as real-time, probabilistic, and cryptographic operations. To solve this problem, we propose a probabilistic timed calculus for cryptographic protocols along with an automatic verification method, and demonstrate how to use them for proving security or vulnerability of protocols. (See the poster of this topic.)
- Formal Aspects on Privacy By Design (work at INRIA) Our goal is to propose a formal method to prove that a low level systems/protocols conform to high-level (privacy guaranteed) architectures. A ("privacy-aware") architecture abstracts away from the specific detailed protocols used by PETs, while a protocol is more detailed (with message orders, timing, etc.). The problem is how to check that the integrated protocols really implement (conform) the architecture. (Our paper published at FPS'2014)
- Formal Aspects on Accountability (work at INRIA) Our goal is to design a formal language for defining accountability properties and policies, for data protection. We apply the language for the Video and Biometric Surveillance case study ( with in the scope of the PARIS EU FP7 project).
Conferences and Journals
 L. Buttyán, Ta Vinh Thong, Biztonsági API analízis a spi-kalkulussal, Hiradástechnika, Volume LXIII. , number 8, 2007, 16–21. (PDF)
 L. Buttyán, Ta Vinh Thong, Security API analysis with the spi-calculus, Hiradástechnika, Volume LXII. , number 1, 2008, 43–49. (PDF)
 L. Buttyán, G. Pék, Ta Vinh Thong, Consistency verification of stateful firewalls is not harder than the stateless case, Infocommunications Journal, Volume LXIV., number 2009/2-3., 2–3, 2009 (PDF)
 L. Buttyán, Ta Vinh Thong, Formal verification of secure ad-hoc network routing protocols using deductive model-checking, IFIP Wireless and Mobile Networking Conference (WMNC’2010). (PDF)
 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, Volume 46, number 11, 2008 november (PDF) L. Buttyán, Ta Vinh Thong, Formal verification of secure ad-hoc network routing protocols., Periodica Polytechnica Electrical Engineering Journal, 2011 (To appear)
 Ta Vinh Thong, L. Buttyán. On automating the verification of secure ad-hoc network routing protocols, Telecommunication Systems Journal, Springer, 2011 (LINK)  Ta Vinh Thong, Levente Buttyán, Query Auditing for Protecting Max/Min Values of Sensitive Attributes in Statistical Databases. 9th International Conference on Trust, Privacy & Security in Digital Business (TrustBus) 2012. (LINK)  Amit Dvir, Levente Buttyán, Ta Vinh Thong SDTP+: Securing a Distributed Transport Protocol for WSNs using Merkle Trees and Hash Chains. IEEE ICC 2013 - Communication and Information Systems Security Symposium.
 Ta Vinh Thong, Amit Dvir, Levente Buttyán On automatic security verification of WSN transport protocols. ISRN Sensor Networks Journal, Hindawi., id:891467, 2014, (In Press)
 Ta Vinh Thong, Amit Dvir, Levente Buttyán Formal Security Verification of Transport Protocols for Wireless Sensor Networks. In proceedings of the 2nd International Conference on Computer Science, Applied Mathematics and Applications (ICCSAMA) 2014. pp 389-403.
 Ta Vinh Thong, Thibaud Antignac. Privacy By Design: On the Conformance Between Protocols and Architectures. The 7th International Symposium on Foundations & Practice of Security FPS'2014, Montreal, Canada, November 3-5, 2014.
[T1] Ta Vinh Thong, Biztonsági API-k formális analizise a spi-kalkulussal. 2007, TDK, BME VIK.
[T2] Ta Vinh Thong, Security API analysis with the spi-calculus and the ProVerif tool. 2008, CrySyS Lab., BME. (PDF)
[T3] Ta Vinh Thong, Levente Buttyán, Formal Verification of the SeVeCom HSM API with the applied pi-calculus and the ProVerif tool. 2009, CrySyS Lab., BME. (PDF)
[T4] Ta Vinh Thong, Formal verification of secure ad-hoc network routing protocols using deductive model-checking. 2012, CrySyS Lab., BME. (PDF, at IACR Cryptology ePrint Archive )
[T5] Ta Vinh Thong, Levente Buttyán, Query Auditing for Protecting Max/Min Values of Sensitive Attributes in Statistical Databases. 2012, CrySyS Lab., BME. (PDF)
[T6] Amit Dvir, Levente Buttyán, Ta Vinh Thong, A Secure Distributed Transport Protocol for Wireless Sensor Networks. 2012, CrySyS Lab., BME.
[T7] Ta Vinh Thong, Amit Dvir . On automatic security verification of WSN transport protocols 2013, CrySyS Lab., BME. (PDF, at IACR Cryptology ePrint Archive)
- SeVeCom: Secure Vehicular Communications EU(027795).
Vehicular communications (VC) and inter-vehicular communications (IVC) bring the promise of improved road safety and optimized road traffic through co-operative systems applications. To this end, a number of initiatives have been launched, such as the Car-2-Car Communication Consortium (C2C-CC) in Europe, or DSRC in North America. A prerequisite for the successful deployment of vehicular communications is to make them secure. For example, it is essential to make sure that life-critical information cannot be modified by an attacker; it should also protect as far as possible the privacy of the drivers and passengers. The specific operational environment (moving vehicles, sporadic connectivity, ...) makes the problem very novel and challenging. SeVeCom addresses security of future vehicle communication networks, including both the security and privacy of inter-vehicular and vehicle-infrastructure communication. Its objective is to define the security architecture of such networks, as well as to propose a roadmap for progressive deployment of security functions in these networks. (Website.)
- WSAN4CIP: Wireless Sensor and Actuator Networks for Critical Infrastructure Protection (EU FP7 STREP).
The goal of WSAN4CIP is to advance the technology of Wireless Sensor and Actuator Networks (WSANs) beyond the current state of the art, in order to improve the protection of Critical Infrastructures (CIs). By advancing WSAN technology, the project will contribute to networked information and process control systems which are more secure and resilient. The distributed nature of WSANs enables them to survive malicious attacks as well as accidents and operational failures. It makes them dependable in critical situations, when information is needed to prevent further damage to CIs. (Website.)
- CHIRON: CYCLIC AND PERSON-CENTRIC HEALTH MANAGEMENT (EU ARTEMIS IP).
The CHIRON Project intends to combine state-of-the art technologies and innovative solutions into an integrated framework designed for an effective and person-centric health management along the complete care cycle. In this vision, CHIRON will address and harmonize the needs and interests of all the three main beneficiaries of the healthcare process, i.e. the citizens using the services, the medical professionals and the whole community. CHIRON will also position the citizens at the core of the whole healthcare cycle by considering them as “persons” with specificities and identities and will empower them to manage their own health. Then, CHIRON will enlarge the boundaries of healthcare by fostering a seamless integration of clinical setting, at home setting and mobile setting in a concept of a continuum of care. this will speed up the move from treatment of acute episodes to prevention. The project will provide the physicians with extensive support for treatment monitoring and management, timely decisions and appropriate actions in both the clinical and home environments.(Website.)
- PARIS: PrivAcy pReserving Infrastructure for Surveillance, (EU FP7).
The goal of the project PARIS (PrivAcy pReserving Infrastructure for Surveillance) is to define and demonstrate a methodological approach for the development of a surveillance infrastructure which enforces the right of citizens for privacy, justice and freedom. At the same time, it takes into account the evolving nature of such rights, since aspects that are acceptable today might not be acceptable in the future. It also includes the social and ethical nature of such rights, since the perception of such rights varies over time and in different countries.(Website.)
- Security of Telecommunication Systems I. (BMEVIHIM220)
- Security of Telecommunication Systems II. (BMEVIHIM305)
- Laboratory Exercises I (Faculty of Computer Science).
- Laboratory Exercises II (Faculty of Computer Science).
- Formal and Automated Security Verification of Protocols (Lecture, part of Security Protocols (BMEVIHIM132))
Supervised student projects:
- BSc diploma project, 2009 (co-supervised with Levente Buttyán).
- The title of the BSc. thesis: "Security verification of stateful firewalls".
- MSc diploma project, 2009 (co-supervised with Levente Buttyán).
- The title of her MSc. thesis: "Formal verification of firewalls".
- MSc diploma project, 2011 (supervised).
- MSc. thesis: "Automated security verification of routing protocols" (In Hungarian).
Conference organizations (took part in):
- The 3rd International Conference on Decision and Game Theory for Security, GameSec 2012, Budapest, Hungary.
- The 6th ACM Conference on Security and Privacy in Wireless and Mobile Networks, WiSec 2013, Budapest, Hungary.
- The 8th International Conference on Computers, Privacy & Data Protection (CPDP) 2015, Brussels, Belgium.
- International Conference on Computer Science, Applied Mathematics and Applications, ICCSAMA 2015.
- The IEEE International Conference on Communications, ICC 2015.
- International Conference on Computer Science, Applied Mathematics and Applications, ICCSAMA 2014.
- The 23rd IEEE WETICE Conference, WETICE 2014.
- The 6th ACM Conference on Security and Privacy in Wireless and Mobile Networks, WiSec 2013.
- The IEEE International Conference on Communications, ICC 2013.
- Computers & Security Journal, Elsevier, COSE 2013.
- The IEEE International Conference on Communications, ICC 2012.
- The 10th International Conference on Applied Cryptography and Network Security, ACNS 2012.
- The 18th Annual Network & Distributed System Security Conference, NDSS 2011.
- Computer Communications Journal, Elsevier, COM-COM 2011.
- The IEEE Conference on Computer Communications, INFOCOM 2010.
- Journal of Communications (JCM), Academic Publisher, 2009.
- The IEEE Conference on Computer Communications, INFOCOM 2009.
- The 4th ACM International Workshop on Vehicular Ad Hoc Networks, VANET 2007.
- In addition, he was reviewer of several Master reports.
- IEEE ComSoc Membership.
- Student scientific competition (TDK) 2007, won 1st prize as student.
- Student scientific competition (TDK) 2008, won 1st prize as supervisor.
- Student scientific competition (OTDK) 2009, won 3rd prize as supervisor.
- Pollák-Virág prize, 2010.
- BME research grant award for outstanding achievements, 2011.
- HSN Lab-Ericsson scholarship , 2008-2011.
- Hungarian TÁMOP scholarship, 2012-2013.
- Vietnamese: native.
- Hungarian: fluently.
- English: read, written and spoken fluently.
- French: elementary.
- Playing and watching football.
- Spending time with friends and family.
- Go to cinema, theatre.