Penn Security Lab

Penn Security Lab was a facility for research and education at the Univerrsity of Pennsylvania in Philadelphia. It was directed by Carl A. Gunter, a professor at Penn, and Dave Millar, the Penn Information Security Officer. The lab was initiated in January of 2000 and closed at the end of 2004. It was initially funded by NSF and the Penn School of Engineering and Applied Science (SEAS). This page summarizes some of the contributions and people from the lab.

Projects and Contributions

  • A core aim of the lab was to improve security education at Penn. Gunter, with help from the lab interns and Dave Millar, developed and taught the first regular security courses at the graduate and undergraduate levels at Penn.
  • Another key element of the educational mission of the lab was training of interns. The first of these was Mike Clark, who set up the lab itself and originated the idea of a Virtual Honeynet, which was the first attempt to use virtualization to enhance the function of honeynets.
  • The lab had a number of further technical contributions through a series of projects funded by diverse sources that made contributions to further lab activities. The Verinet project, funded by DARPA and Cisco, was one of the first of these. The project made seminal contributions to the formal analysis of routing protocols, including the first use of formal methods to analyze ad hoc networks and the first use of formal methods in the analysis of network simulations (the Verisim system) and network event recognition (the Network Event Recongnizer Language – NERL).
  • Another project of the lab, with support from ARO and NSF, was the OpEm project, which focused on how to develop open APIs for embedded systems. This project introduced a Programmable Microwave Oven that could read a recipe in a two-dimensional barcode and a Programmable Payment Card (PPC), in which a Java smart card running the GlobalPlatform enabled custom policies on the card itself to enforce purchace policies.
  • The lab also supported research on network security through the Contessa MURI Project, where Penn researchers introduced the concepts of the shared channel model and selective verification, which provide foundations for the rigorous analysis of DoS and new countermeasures.
  • A grant from Microsoft initiated research in the lab on WSEmail, the idea of founding messaging systems on web services in which legacy protocols like SMTP and S/MIME are replaced by modern distributed computing standards like SOAP and XMLDSIG. Research in the lab considered applications, theory, and performance based on a substantial implementation using .NET.

Students and Interns

  • Watee Arsjamat (Intern) – OpEm
  • Karthikeyan Bhargavan (PhD) – Verinet
  • Nayan Bhattad (Intern) – Contessa
  • Mike Clark (Intern) – Virtual Honeynets
  • Gabriel Eichler (Undergrad) – P2P
  • Alwyn Goodloe (PhD) – OpEm and Contessa
  • Ron Lin (Undergrad) – P2P
  • Kevin Lux (Intern) – WSEmail
  • Michael J. May (PhD) – WSEmail
  • Michael McDougall (PhD) – OpEm
  • Davor Obradovic (PhD) – Verinet
  • Kaijun Tan (Staff) – Contessa
  • Yosef Weiner (Intern) – OpEm



WSEmail: An architecture and system for secure Internet messaging based on web services.
Michael J. May, Kevin D. Lux, and Carl A. Gunter.
Service Oriented Computing and Applications (2020) 14:5–17.

WSEmail: A Retrospective on a System for Secure Internet Messaging Based on Web Services..
Michael J. May, Kevin D. Lux, and Carl A. Gunter.
arXiv:1908.02108 [cs.NI], December, 2019.

Completeness of Discovery Protocols
Alwyn Goodloe and Carl A. Gunter
Assurable and Usable Security Configuration (SafeConfig ’09), Chicago, IL, November 2009.

Strong and Weak Policy Relations
Michael J. May, Insup Lee, Carl A. Gunter and Steve Zdancewic
IEEE International Symposium on Policies for Distributed Systems and Networks (POLICY ’09), London, UK, July 2009.

Adaptive Selective Verification
Sanjeev Khanna, Santosh S. Venkatesh, Omid Fatemieh, Fariba Khan and Carl A. Gunter
IEEE Conference on Computer Communications (INFOCOM ’08), Phoenix, AZ, April 2008. [PPT][BIB]

Emergency Alerts as RSS Feeds with Interdomain Authorization
Filippo Gioachin, Ravinder Shankesi, Michael J. May, Carl A. Gunter and Wook Shin
IARIA International Conference on Internet Monitoring and Protection (ICIMP ’07), Santa Clara, CA, July 2007. [PPT][BIB]

Securing the Drop-Box Architecture for Assisted Living
Michael J. May, Wook Shin, Carl A. Gunter and Insup Lee
ACM Formal Methods in Security Engineering (FMSE ’06), Alexandria, VA, November 2006. [BIB]

Privacy APIs: Access Control Techniques to Analyze and Verify Legal Privacy Policies
Michael J. May, Carl A. Gunter and Insup Lee
IEEE Computer Security Foundations Workshop (CSFW  ’06), Venice, Italy, July 2006. [PPT][BIB][CITES]

L3A: A Protocol for Layer Three Accounting
Alwyn Goodloe, Carl A. Gunter, Matthew Jacobs and Gaurav Shah
IEEE Workshop on Secure Network Protocols (NPsec ’05), Boston, MA, November 2005. [PPT][BIB]

Mitigating DoS Attack Through Selective Bin Verification
Micah Sherr, Michael Greenwald, Carl A. Gunter, Sanjeev Khanna and Santosh Venkatesh
IEEE Workshop on Secure Network Protocols (NPsec ’05), Boston, MA, November 2005. [PPT][BIB]

WSEmail: Secure Internet Messaging Based on Web Services
Kevin D. Lux, Michael J. May, Nayan L. Bhattad and Carl A. Gunter
IEEE International Conference on Web Services (ICWS ’05), Orlando, FL, July 2005. [PPT][BIB]

Formal Prototyping in Early Stages of Protocol Design
Alwyn Goodloe, Carl A. Gunter and Mark-Oliver Stehr
IFIP/ACM Workshop on Issues in the Theory of Security (WITS ’05), Long Beach, CA, January 2005. [PPT][BIB]

Network Event Recognition
Karthikeyan Bhargavan and Carl A. Gunter
Formal Methods in System Design, volume 27, number 3, pages 213-251, 2005.

Modeling and Analyzing Integrated Policies
Michael McDougall
Doctoral Thesis, University of Pennsylvania, 2005.

Fair Coalitions for Power-Aware Routing in Wireless Networks
Ratul K. Guha, Carl A. Gunter and Saswati Sarkar
IEEE Conference on Decision and Control (CDC ’04), Paradise Island, Bahamas, December 2004.

A Model-Based Approach to Integrating Security Policies for Embedded Devices
Michael McDougall, Rajeev Alur and Carl A. Gunter
ACM International Conference on Embedded Software (EMSOFT ’04), Pisa, Italy, September 2004.

Design and Analysis of Sectrace: A Protocol to Set up Security Associations and Policies in IPSec Networks,
Alwyn Goodloe, Michael McDougall, Carl A. Gunter, and Mark-Oliver Stehr.
Technical Report, September, 2004.

The Consistency of Task-Based Authorization Constraints in Workflow Systems
Kaijun Tan, Jason Crampton and Carl A. Gunter
IEEE Computer Security Foundations Workshop (CSFW ’04), Monterey, CA, July 2004.

DoS Protection for Reliably Authenticated Broadcast
Carl A. Gunter, Sanjeev Khanna, Kaijun Tan and Santosh Venkatesh
ICSOC Network and Distributed Systems Security Symposium (NDSS ’04), San Diego, CA, February 2004.

Open APIs for Embedded Security
Carl A. Gunter
European Conference on Object-Oriented Programming (ECOOP ’03), volume 2743, Lecture Notes in Computer Science, pages 225-247, Darmstadt, Germany, July 2003. Invited paper. [BIB]

Network Event Recognition
Karthikeyan Bhargavan
Doctoral Thesis, University of Pennsylvania, 2003.

Predictable Programs in Barcodes
Alwyn Goodloe, Michael McDougall, Rajeev Alur and Carl A. Gunter
International Conference on Compilers, Architecture, and Synthesis for Embedded Systems (CASES ’02), pages 298-303, Grenoble, France, October 2002. [BIB]

Formal Verification of Standards for Distance Vector Routing Protocols
Karthikeyan Bhargavan, Davor Obradovic and Carl A. Gunter
Journal of the ACM, volume 49, number 4, pages 538-576, July 2002.

Verisim: Formal Analysis of Network Simulations
Karthikeyan Bhargavan, Carl A. Gunter, Moonjoo Kim, Insup Lee, Davor Obradovic, Oleg Sokolsky and Mahesh Viswanathan
IEEE Transactions on Software Engineering, volume 28, number 2, pages 129-145, February 2002.

Requirements for a Practical Network Event Recognition Language
Karthikeyan Bhargavan and Carl A. Gunter
Electronic Notes in Theoretical Computer Science, volume 70, number 4, 2002.

Formal Analysis of Routing Protocols
Davor Obradovic
Doctoral Thesis, University of Pennsylvania, 2002.

Virtual Honeynets
Michael Clark, November 2001.

What Packets May Come: Automata for Network Monitoring
Karthikeyan Bhargavan, Satish Chandra, Peter J. McCann and Carl A. Gunter
ACM Symposium on Principles of Programming Languages (POPL ’01), Maui, HI, January 2001.

Last updated on Monday, July 25, 2011, 4:32 pm