Code 5543 is the Formal Methods Section in the Center for High Assurance Computer Systems Branch of the Information Technology Division.

The mission of the Formal Methods Section is to perform research on extensible and adaptable foundational theories that can be applied to present and emerging security problems. Our current areas of interest are listed below.

Cryptographic Protocol and Analysis
Theory and Design
  • Applications of rewriting logic and unification to cryptographic protocol analysis
  • Logical and mathematical techniques for verifying security of authentication in pervasive computing
Products and Applications
  • The Maude-NRL Protocol Analyzer (Maude-NPA) Learn more here
  • Secure Network Localization protocol (SNLP), a protocol for securely determining and distributing location information in a wireless network
  • Security analyses of proximity verification protocols

Selected Publications

In Press Harrison WL, Andrews D, Allwein G.  In Press.  Simulation Logic. Logic and Logical Philosophy. PDF icon 12-1231-2384.pdf (281.37 KB)
2020 Jansen R.  2020.  Reducing Kernel Queuing Delays with TCP Window Space Events. The 14th Technical Conference on Linux Networking (NetDev 0x14). PDF icon Reducing Kernel Queuing Delays with TCP Window Space Events.pdf (215.23 KB)
2019 Traudt M, Syverson P.  2019.  Does Pushing Security on Clients Make Them Safer? 12th Workshop on Hot Topics in Privacy Enhancing Technologies (HotPETs2019). PDF icon Does Pushing Security on Clients Make Them Safer_.pdf (113.15 KB)
2017 Kirby, Jr J, McDermott J, Campbell G..  2017.  Commonality and Variability Analysis for Xenon Family of Separation Virtual Machine Monitors (CVAX). PDF icon 17-1231-2039.pdf (524.15 KB)
2017 Jaggard A, Syverson P.  2017.  Onions in the Crosshairs: When the Man Really is Out to Get You. 17th Privacy Enhancing Technologies Symposium (PETS 2017). PDF icon wpes06-jaggardAT3.pdf (850.78 KB)
2017 Jaggard A, Syverson P.  2017.  Oft Target: Tor Adversary Models That Don’t Miss the Mark. 10th Workshop on Hot Topics in Privacy Enhancing Technologies (HotPETs 2017). PDF icon targets-hotpets-1707.pdf (95.83 KB)
2015 Syverson P, Boyce G.  2015.  Genuine Onion: Simple, Fast, Flexible, and Cheap Website Authentication. IEEE Workshop on Web 2.0 Security & Privacy. PDF icon 15-1231-0478.pdf (77.83 KB)
2015 Jaggard AD, Johnson A, Cortes S, Syverson P, Feigenbaum J.  2015.  20,000 In League Under the Sea: Anonymous Communication, Trust, MLATs, and Undersea Cables Proceedings on Privacy Enhancing Technologies. Proceedings on Privacy Enhancing Technologies. 1(1):4-24.PDF icon 15-1231-0586.pdf (1.36 MB)
2015 Juen J, Johnson A, Das A, Borisov N, Caesar M.  2015.  Defending Tor from Network Adversaries: A Case Study of Network Path Prediction. Proceedings on Privacy Enhancing Technologies. 1PDF icon 15-1231-1429.pdf (2.06 MB)
2015 Goulet D, Johnson A, Kadianakis G, Loesing K.  2015.  Hidden-service statistics reported by relays. NRL Technical Reports. PDF icon 15-1231-1605.pdf (131.38 KB)
2015 Miller A, Jansen R.  2015.  Shadow-Bitcoin: Scalable Simulation via Direct Execution of Multi-threaded Applications. 8th Workshop on Cyber Security Experimentation and Test (CSET). PDF icon 15-1231-1593.pdf (3.24 MB)
2014 Ghosh M, Richardson M, Ford B, Jansen R.  2014.  A TorPath to TorCoin: Proof-of-Bandwidth Altcoins for Compensating Relays. 7th Workshop on Hot Topics in Privacy Enhancing Technologies (HotPETs). PDF icon 14-1231-1559.pdf (837.86 KB)
2014 Jansen R, Geddes J, Wacek C, Sherr M, Syverson P.  2014.  Never Been KIST: Tor’s Congestion Management Blossoms with Kernel-Informed Socket Transport. 23rd Usenix Security Symposium. PDF icon 14-1231-2094.pdf (1.26 MB)
2014 Geddes J, Jansen R, Hopper N.  2014.  IMUX: Managing Tor Connections from Two to Infinity, and Beyond. Workshop on Privacy in Electronic Society (WPES). PDF icon 14-1231-3002.pdf (1.54 MB)
2014 Allwein G, Harrison WL.  2014.  Distributed Logics. NRL Memorandum Report. PDF icon 14-1231-3181.pdf (583.12 KB)
2014 Jansen R, Tschorsch F, Johnson A, Scheuermann B.  2014.  The Sniper Attack: Anonymously Deanonymizing and Disabling the Tor Network. 21st Annual Network & Distributed System Security Symposium (NDSS '14). PDF icon 13-1231-3743.pdf (552.48 KB)
2014 Jaggard AD, Johnson A, Syverson P, Feigenbaum J.  2014.  Representing Network Trust and Using it to Improve Anonymous Communication. Privacy Enhancing Technologies Symposium. PDF icon 14-1231-1483.pdf (1.15 MB)
2014 Jansen R, Miller A, Syverson P, Ford B.  2014.  From Onions to Shallots: Rewarding Tor Relays with TEARS. 7th Workshop on Hot Topics in Privacy Enhancing Technologies (HotPETs). PDF icon 14-1231-1482.pdf (425.98 KB)
2013 Syta E, Johnson A, Corrigan-Gibbs H, Weng S-C, Wolinsky D, Ford B.  2013.  Security Analysis of Accountable Anonymous Group Communication in Dissent. Yale University Technical Report. PDF icon 13-1231-0835.pdf (436.64 KB)
2013 Jansen R, Johnson A, Syverson P.  2013.  LIRA: Lightweight Incentivized Routing for Anonymity. 20th Annual Network & Distributed System Security Symposium (NDSS '13). PDF icon Jansen etal2013.pdf (1.14 MB)
2013 Johnson A, Wacek C, Jansen R, Sherr M, Syverson P.  2013.  Users Get Routed: Traffic Correlation on Tor by Realistic Adversaries. 20th ACM Conference on Computer and Communications Security. PDF icon 13-1231-2077.pdf (2.99 MB)
2012 Jansen R, Bauer K, Hopper N, Dingledine R.  2012.  Methodically Modeling the Tor Network. Workshop on Cyber Security Experimentation and Test (CSET). PDF icon 12-1231-2496.pdf (598.31 KB)
2012 Jansen R, Syverson P, Hopper N.  2012.  Throttling Tor Bandwidth Parasites. USENIX Security Symposium. PDF icon 12-1231-2049.pdf (1.13 MB)
2012 Jansen R, Hopper N.  2012.  Shadow: Running Tor in a Box for Accurate and Efficient Experimentation. Symposium on Network and Distributed System Security (NDSS). PDF icon 11-1226-3413.pdf (1.13 MB)
2012 Wolinsky DIsaac, Corrigan-Gibbs H, Ford B, Johnson A.  2012.  Strong, Scalable Anonymity in Dissent. Tenth USENIX Symposium on Operating Systems Design and Implementation (OSDI '12). PDF icon Wolinsky etal2012.pdf (898.57 KB)
2012 Feigenbaum J, Johnson A, Syverson P.  2012.  Probabilistic Analysis of Onion Routing in a Black-box Model. ACM Transactions on Information and System Security (TISSEC). 15(3)PDF icon Feigenbaum etal2012.pdf (363.26 KB)
2012 Wolinsky DIsaac, Corrigan-Gibbs H, Ford B, Johnson A.  2012.  Scalable Anonymous Group Communication in the Anytrust Model. Fifth European Workshop on System Security (EuroSec 2012). PDF icon Wolinsky etal2012b.pdf (280.01 KB)
2011 Johnson A, Syverson P, Dingledine R, Mathewson N.  2011.  Trust-based Anonymous Communication: Adversary Models and Routing Algorithms. Proceedings of the 18th ACM Conference on Computer and Communications Security (CCS 2011). PDF icon Johnson etal2011.pdf (320.76 KB)
2010 Feigenbaum J, Johnson A, Syverson P.  2010.  Preventing Active Timing Attacks in Low-Latency Anonymous Communication (Extended Abstract). 10th Privacy Enhancing Technologies Symposium (PETS 2010). PDF icon Feigenbaum etal 2010.pdf (232.21 KB)
2009 Johnson A, Syverson P.  2009.  More Anonymous Onion Routing Through Trust. 22nd IEEE Computer Security Foundations Symposium (CSF 2009). PDF icon Johnson etal2009.pdf (197.77 KB)
2008 Merrell R, Cooper RA.  2008.  Analysis and Reduction of Embedding Error for a Semi-Reversible Image Authentication Watermark. IASTED Telehealth/AT 2008.
2007 Feigenbaum J, Johnson A, Syverson P.  2007.  Probabilistic Analysis of Onion Routing in a Black-box Model [Extended Abstract]. WPES'07: Proceedings of the 2007 ACM Workshop on Privacy in Electronic Society. :1-10.PDF icon Feigenbaum etal2007.pdf (228.68 KB)
2007 Dingledine R, Mathewson N, Syverson P.  2007.  Deploying Low-Latency Anonymity: Design Challenges and Social Factors. IEEE Security & Privacy. 5(5):83-87.PDF icon Dingledine etal2007.pdf (71.26 KB)
2007 Overlier L, Syverson P.  2007.  Improving Efficiency and Simplicity of Tor circuit establishment and hidden services. 2007 Privacy Enhancing Technologies Symposium. LNCS 4776PDF icon OverlierSyverson2007.pdf (619.35 KB)
2007 Feigenbaum J, Johnson A, Syverson P.  2007.  A Model of Onion Routing with Provable Anonymity. Financial Cryptography and Data Security, 11th International Conference, FC 2007. PDF icon Feigenbaum etal2007b.pdf (224.34 KB)
2006 Overlier L, Syverson P.  2006.  Valet Services: Improving Hidden Servers with a Personal Touch. Privacy Enhancing Technologies Workshop. PDF icon OverlierSyverson2006.pdf (656.17 KB)
2006 Overlier L, Syverson P.  2006.  Locating Hidden Servers. IEEE Symposium on Security and Privacy. PDF icon OverlierSyverson2006b.pdf (852.47 KB)
2006 [Anonymous].  2006.  A semi-reversible watermark for medical image authentication. 1st Transdisciplinary Conference on Distributed Diagnosis and Home Healthcare, D2H2 2006. :59-62.
2005 Ahmed F, Moskowitz IS.  2005.  Composite Signature Based Watermarking for Fingerprint Authentication. ACM Multimedia and Security Workshop, ACM2005 . PDF icon AhmedMoskowitz2005.pdf (486.33 KB)
2005 Dingledine R, Mathewson N, Syverson P.  2005.  Challenges in deploying low-latency anonymity. NRL CHACS. PDF icon Dingledine etal2005.pdf (202.95 KB)
2005 Juels A, Syverson P, Bailey D.  2005.  High-Power Proxies for Enhancing RFID Privacy and Utility. Privacy Enhancing Technologies Workshop (PET 2005). PDF icon Juels etal2005.pdf (125.29 KB)
2005 Moskowitz IS, Newman R.  2005.  Multiple Access Covert Channels. IASTED CNIS 2005. PDF icon MoskowitzNewman2005.pdf (2.33 MB)
2005 [Anonymous].  2005.  Phase-signature based watermarking for multimedia authentication: Analysis and design. Multimedia Systems and Applications VIII.
2004 Ahmed F, Moskowitz IS.  2004.  Correlation-Based Watermarking Method for Image Authentication Applications. Optical Engineering. 43(8)PDF icon AhmedMoskowitz2004.pdf (424.74 KB)
2004 Ahmed F, Moskowitz IS.  2004.  The Binary Phase Only Filter as an Image Watermark. NRL CHACS Tech Memo. PDF icon AhmedMoskowitz2004b.pdf (192.31 KB)
2004 [Anonymous].  2004.  A New Framework for Shannon Information Theory. NRL Memorandum Report.
2004 Dingledine R, Mathewson N, Syverson P.  2004.  Tor: The Second-Generation Onion Router. 13th USENIX Security Symposium. PDF icon Dingledine etal2004.pdf (214.58 KB)
2004 Dingledine R, Shmatikov V, Syverson P.  2004.  Synchronous Batching: From Cascades to Free Routes. Privacy Enhancing Technologies workshop (PET 2004). PDF icon Dingledine etal2004b.pdf (303.49 KB)
2004 Miller AR, Moskowitz IS.  2004.  Difference of Sums Containing Products of Binomial Coefficients and their Logarithms. PDF icon MillerMoskowitz2004.pdf (671.78 KB)
2004 [Anonymous].  2004.  Covert Channels and Simple Timed Mix-firewalls. NRL Memorandum Report.
2004 Newman R, Nalla VR, Moskowitz IS.  2004.  Anonymity and Covert Channels in Simple Timed Mix-firewalls. PET2004. PDF icon Newman etal2004.pdf (312.75 KB)
2004 Shostack A, Syverson P.  2004.  What Price Privacy? (and why identity theft is about neither identity nor theft) Economics of Information Security. :129-142.PDF icon ShostackSyverson2004.pdf (65.66 KB)
2004 Zhan Z, Chang LW, Matwin S.  2004.  Privacy-Preserving Naive Bayesian Classification. IASTED conference on AIA. PDF icon Zhan etal2004.pdf (132.97 KB)
2004 [Anonymous].  2004.  Phase signature-based umage authentication watermark robust to compression and coding. Mathematics of Data/Image Coding, Compression and Encrption VII, with Applications. :133-144.
2003 Meadows C.  2003.  Formal Methods for Cryptographic Protocol Analysis: Emerging Issues and Trends. IEEE Journal on Selected Areas in Communication. 21(1):44-54.PDF icon Meadows2003d.pdf (106.87 KB)
2003 Meadows C, Syverson P, Cervesato I.  2003.  Formal Specification and Analysis of the Group Domain of Interpretation Protocol Using NPATRL and the NRL Protocol Analyzer. Journal of Computer Security. PDF icon Meadows etal2003.pdf (334.45 KB)
2003 Moskowitz IS, Newman R, Syverson P.  2003.  Quasi-Anonymous Channels. CNIS 2003. PDF icon Moskowitz etal2003.pdf (60.86 KB)
2003 [Anonymous].  2003.  A Detailed Mathematical Analysis of a Class of Covert Channels Arising in Certain Anonymizing Networks. NRL Memorandum Report.
2003 Newman R, Moskowitz IS, Syverson P, Serjantov A.  2003.  Metrics for Traffic Analysis Prevention. PET 2003 Workshop on Privacy Enhancing Technologies. PDF icon Newman etal2003.pdf (218.12 KB)
2003 Shyu M-L, Chen S-C, Sarinnapakorn K, Chang LW.  2003.  A Novel Anomaly Detection Scheme Based on Principal Component Classifier. ICDM Foundation and New Direction of Data Mining workshop. :172-179.PDF icon Shyu etal2003.pdf (359.15 KB)
2003 Syverson P.  2003.  The Paradoxical Value of Privacy. 2nd Annual Workshop on Economics and Information Security (WEIS 2003). PDF icon Syverson2003.pdf (89.15 KB)
2003 Tracy J, Chang LW, Moskowitz IS.  2003.  An Agent-based Approach to Inference Prevention in Distributed Database Systems. International Journal on Artificial Intelligence Tools. 12(3):297-314.PDF icon Tracy etal2003.pdf (220.93 KB)
2003 [Anonymous].  2003.  Privacy-preserving Collaborative Data Mining. ICDM Foundation and New Directions of Data Mining workshop. :228-235.
2003 Moskowitz IS, Newman R, Miller AR, Crepeau DP.  2003.  Covert Channels and Anonymizing Networks. WPES'03. PDF icon Moskowitz etal2003b.pdf (356.86 KB)
2003 Cervesato I, Meadows C.  2003.  A Fault Tree Representation of NPATRL Security Requirements. Workshop on Issues in Theory of Security 2003. PDF icon CervesatoMeadows2003.pdf (221.4 KB)
2003 Chang LW.  2003.  Statistical Sensitive Data Protection And Inference Prevention with Decision Tree Methods. Joint Statistical Meeting 2003. PDF icon Chang2003.pdf (119.01 KB)
2003 Meadows C.  2003.  Towards a Hierarchy of Cryptographic Protocol Models. FMSE 2003: Formal Methods in Security Engineering. PDF icon Meadows2003.pdf (49.02 KB)
2003 Meadows C.  2003.  What Makes a Cryptographic Protocol Secure? The Evolution of Requirements Specification in Formal Cryptographic Protocol Analysis ESOP 03. PDF icon Meadows2003b.pdf (168.07 KB)
2003 Meadows C.  2003.  A Procedure for Verifying Security Against Type Confusion Attacks. 16th IEEE Computer Security Foundations Workshop. PDF icon Meadows2003c.pdf (145.43 KB)
2002 Dingledine R, Mathewson N, Syverson P.  2002.  Reputation in Privacy Enhancing Technologies. Computer, Freedom, and Privacy. PDF icon Dingledine etal2002.pdf (25.17 KB)
2002 [Anonymous].  2002.  A Unification Algorithm for the Group Diffie-Hellman Protocol. WITS '02.
2002 Meadows C.  2002.  Using a Declarative Language to Build an Experimental Analysis Tool. PADL '02. Springer Verlag LNCS 2257:1-2.PDF icon Meadows2002.pdf (1.55 MB)
2002 Meadows C.  2002.  Identifying Potential Type Confusion in Authenticated Messages. Workshop on Foundations of Computer Security. PDF icon Meadows2002b.pdf (125.64 KB)
2002 Moskowitz IS, Johnson NF, Jacobs M.  2002.  A Detection Study of an NRL Steganographic Method. NRL Memorandum Report. PDF icon Moskowitz etal2002.pdf (14.22 MB)
2002 Moskowitz IS, Chang LW, Newman R.  2002.  Capacity is the Wrong Paradigm. New Security Paradigms Workshop (NSPW). PDF icon Moskowitz etal2002b.pdf (247.04 KB)
2002 Newman R, Moskowitz IS, Chang LW, Brahmadesam MM.  2002.  A Steganographic Embedding Undetectable by JPEG Compatibility Steganalysis. Information Hiding. PDF icon Newman etal2002.pdf (251.68 KB)
2002 Serjantov A, Dingledine R, Syverson P.  2002.  From a Trickle to a Flood: Active Attacks on Several Mix Types. Information Hiding. Springer-Verlag LNCS 2578:36-52.PDF icon Serjantov etal2002.pdf (222.02 KB)
2002 Canetti R, Meadows C, Syverson P.  2002.  Environmental Requirements for Authentication Protocols. International Symposium on Software Security. Springer-Verlag LNCS 2609:339-355.PDF icon Canetti etal2002.pdf (186.26 KB)
2002 Tracy J, Chang LW, Moskowitz IS.  2002.  An Agent-based Approach to Inference Prevention in Distributed Database Systems. 14th IEEE International Conference on Tools with Artificial Intelligence. :413-422.PDF icon Tracy etal2002.pdf (220.93 KB)
2002 Chang LW, Moskowitz IS.  2002.  A Study of Inference Problems in Distributed Databases. IFIP 11.3 WG in Data Security and Applications. PDF icon ChangMoskowitz2002.pdf (256.28 KB)
2002 [Anonymous].  2002.  Issues in Information Hiding Transform Techniques. NRL Memorandum Report.
2002 Chang LW, Tracy J.  2002.  Multi-Dimensional Inference and Confidential Data Protection with Decision Tree Methods. ICDM02 Workshop: The Foundation of Data Mining and Knowledge Discovery. :195-200.PDF icon ChangTracy2002.pdf (204 KB)
2002 Dingledine R, Syverson P.  2002.  Reliable MIX Cascade Networks through Reputation. Financial Cryptography 2002. PDF icon DingledineSyverson2002.pdf (210 KB)
2001 [Anonymous].  2001.  An Integrated Framework for Database Privacy Protection. Data And Applications Security: Developments and Directions. :161-172.
2001 Chang LW, Moskowitz IS.  2001.  A Bayesian Network Schema for Lessoning Database Inference. International Conference on Computational Intelligence for Modeling, Control and Automation. PDF icon ChangMoskowitz2001.pdf (151.37 KB)
2001 Meadows C, Syverson P, Cervesato I.  2001.  Formalizing GDOI Group Key Management Requirements in NPATRL. 8th ACM Computer and Communications Security Conference - CCS'01. :235-244.PDF icon Meadows etal2001.pdf (148.49 KB)
2001 Moskowitz IS, Kang M, Chang LW, Longdon GE.  2001.  Randomly Roving Agents for Intrusion Detection. 15th IFIP WG 11.3 Working Conference on Database and Application Security. PDF icon Moskowitz etal2001.pdf (257.73 KB)
2001 Syverson P, Cervesato I.  2001.  The Logic of Authentication Protocols. Foundations of Security Analysis and Design --- FOSAD'00. Springer-Verlag LNCS 2171:63-136.PDF icon SyversonCervesato2001.pdf (492.12 KB)
2000 Meadows C.  2000.  Open Issues in Formal Methods for Cryptographic Protocol Analysis. DISCEX 2000. :237-250.PDF icon Meadows2000d.pdf (168.94 KB)
2000 Moskowitz IS, Longdon GE, Chang LW.  2000.  A New Paradigm Hidden in Steganography. New Security Paradigms Workshop. PDF icon Moskowitz etal2000.pdf (247.73 KB)
2000 [Anonymous].  2000.  A Decision Based System for Information Downgrading. JCIS.
2000 Stubblebine S, Syverson P.  2000.  Authentic Attributes with Fine-Grained Anonymity Protection. Financial Cryptography. PDF icon StubblebineSyverson2000.pdf (286.58 KB)
2000 Syverson P, Meadows C, Cervesato I.  2000.  Dolev-Yao is no better than Machiavelli. First Workshop on Issues in the Theory of Security - WITS'00. :87-92.PDF icon Syverson etal2000.pdf (169.38 KB)
2000 Syverson P, Tsudik G, Reed M, Landwehr C.  2000.  Towards an Analysis of Onion Routing Security. Workshop on Design Issues in Anonymity and Unobservability. PDF icon Syverson etal2000b.pdf (252.37 KB)
2000 Syverson P, Reed M, Goldschlag D.  2000.  Onion Routing Access Configurations. DISCEX 2000: Proceedings of the DARPA Information Survivability Conference and Exposition. 1:34-40.PDF icon Syverson etal2000c.pdf (154.68 KB)
2000 Meadows C.  2000.  A Cost-Based Framework for Analysis of Denial of Service in Networks. Journal of Computer Security. PDF icon Meadows2000.pdf (245.87 KB)
2000 Meadows C.  2000.  Extending Formal Cryptographic Protocol Analysis Techniques for Group Protocols and Low-Level Cryptographic Primitives. First Workshop on Issues in the Theory of Security - WITS'00. :87-92.PDF icon Meadows2000b.pdf (21.31 KB)
2000 Meadows C.  2000.  Invariant Generation Techniques in Cryptographic Protocol Analysis. 13th Computer Security Foundations Workshop. PDF icon Meadows2000c.pdf (100.12 KB)