Analysis of LYSA-calculus with explicit confidentiality annotations. - Han Gao 002; Hanne Riis Nielson (AINA (2), 2006)

A Formal Analysis for Capturing Replay Attacks in Cryptographic Protocols. - Han Gao 002; Chiara Bodei; Pierpaolo Degano; Hanne Riis Nielson (ASIAN, 2007)

Detecting and Preventing Type flaws: a Control Flow Analysis with Tags. - Chiara Bodei; Pierpaolo Degano; Han Gao 002; Linda Brodo (SecCO@CONCUR, 2007)

A Formal Analysis of Complex Type Flaw Attacks on Security Protocols. - Han Gao 002; Chiara Bodei; Pierpaolo Degano (AMAST, 2008)

Analysis of Security Protocols by Annotations. - Han Gao 002 (2008)

The CaPiTo Approach to Protocol Validation - (Invited Talk). - Flemming Nielson; Han Gao 002; Hanne Riis Nielson (ARSPA-WITS, 2010)

Detecting and preventing type flaws at static time. - Chiara Bodei; Linda Brodo; Pierpaolo Degano; Han Gao 002 (J. Comput. Secur., 2010)

Analysing Protocol Stacks for Services. - Han Gao 002; Flemming Nielson; Hanne Riis Nielson (Results of the SENSORIA Project, 2011)

CaPiTo: protocol stacks for services. - Han Gao 002; Flemming Nielson; Hanne Riis Nielson (Formal Aspects Comput., 2011)