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. 12-1231-2384.pdf (281.37 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). 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. 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). 14-1231-1482.pdf (425.98 KB)
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). 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. 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). 14-1231-3002.pdf (1.54 MB)
2014 Allwein G, Harrison WL.  2014.  Distributed Logics. NRL Memorandum Report. 14-1231-3181.pdf (583.12 KB)
2013 Jansen R, Johnson A, Syverson P.  2013.  LIRA: Lightweight Incentivized Routing for Anonymity. 20th Annual Network & Distributed System Security Symposium (NDSS '13). 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. 13-1231-2077.pdf (2.99 MB)
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. 13-1231-0835.pdf (436.64 KB)
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). 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) 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). Wolinsky etal2012b.pdf (280.01 KB)
2012 Jansen R, Bauer K, Hopper N, Dingledine R.  2012.  Methodically Modeling the Tor Network. Workshop on Cyber Security Experimentation and Test (CSET). 12-1231-2496.pdf (598.31 KB)
2012 Jansen R, Syverson P, Hopper N.  2012.  Throttling Tor Bandwidth Parasites. USENIX Security Symposium. 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). 11-1226-3413.pdf (1.13 MB)
2011 Johnson A, Syverson P, Dingledine R, Mathewson N.  2011.  Truth-based Anonymous Communication: Adversary Models and Routing Algorithms. Proceedings of the 18th ACM Conference on Computer and Communications Security (CCS 2011). 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). 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). 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. 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. 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 4776 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. 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. OverlierSyverson2006.pdf (656.17 KB)
2006 Overlier L, Syverson P.  2006.  Locating Hidden Servers. IEEE Symposium on Security and Privacy. 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 . AhmedMoskowitz2005.pdf (486.33 KB)
2005 Dingledine R, Mathewson N, Syverson P.  2005.  Challenges in deploying low-latency anonymity. NRL CHACS. 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). Juels etal2005.pdf (125.29 KB)
2005 Moskowitz IS, Newman R.  2005.  Multiple Access Covert Channels. IASTED CNIS 2005. 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) AhmedMoskowitz2004.pdf (424.74 KB)
2004 Ahmed F, Moskowitz IS.  2004.  The Binary Phase Only Filter as an Image Watermark. NRL CHACS Tech Memo. 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. 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). Dingledine etal2004b.pdf (303.49 KB)
2004 Miller AR, Moskowitz IS.  2004.  Difference of Sums Containing Products of Binomial Coefficients and their Logarithms. 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. 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. ShostackSyverson2004.pdf (65.66 KB)
2004 Zhan Z, Chang LW, Matwin S.  2004.  Privacy-Preserving Naive Bayesian Classification. IASTED conference on AIA. 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 Cervesato I, Meadows C.  2003.  A Fault Tree Representation of NPATRL Security Requirements. Workshop on Issues in Theory of Security 2003. CervesatoMeadows2003.pdf (221.4 KB)
2003 Chang LW.  2003.  Statistical Sensitive Data Protection And Inference Prevention with Decision Tree Methods. Joint Statistical Meeting 2003. Chang2003.pdf (119.01 KB)
2003 Meadows C.  2003.  Towards a Hierarchy of Cryptographic Protocol Models. FMSE 2003: Formal Methods in Security Engineering. 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. Meadows2003b.pdf (168.07 KB)
2003 Meadows C.  2003.  A Procedure for Verifying Security Against Type Confusion Attacks. 16th IEEE Computer Security Foundations Workshop. Meadows2003c.pdf (145.43 KB)
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. 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. Meadows etal2003.pdf (334.45 KB)
2003 Moskowitz IS, Newman R, Syverson P.  2003.  Quasi-Anonymous Channels. CNIS 2003. 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. 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. 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). 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. 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. Moskowitz etal2003b.pdf (356.86 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. 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. 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. ChangTracy2002.pdf (204 KB)
2002 Dingledine R, Syverson P.  2002.  Reliable MIX Cascade Networks through Reputation. Financial Cryptography 2002. DingledineSyverson2002.pdf (210 KB)
2002 Dingledine R, Mathewson N, Syverson P.  2002.  Reputation in Privacy Enhancing Technologies. Computer, Freedom, and Privacy. 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. Meadows2002.pdf (1.55 MB)
2002 Meadows C.  2002.  Identifying Potential Type Confusion in Authenticated Messages. Workshop on Foundations of Computer Security. Meadows2002b.pdf (125.64 KB)
2002 Moskowitz IS, Johnson NF, Jacobs M.  2002.  A Detection Study of an NRL Steganographic Method. NRL Memorandum Report. Moskowitz etal2002.pdf (14.22 MB)
2002 Moskowitz IS, Chang LW, Newman R.  2002.  Capacity is the Wrong Paradigm. New Security Paradigms Workshop (NSPW). 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. 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. 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. Canetti etal2002.pdf (186.26 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. 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. SyversonCervesato2001.pdf (492.12 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. 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. Meadows etal2001.pdf (148.49 KB)
2000 Meadows C.  2000.  A Cost-Based Framework for Analysis of Denial of Service in Networks. Journal of Computer Security. 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. Meadows2000b.pdf (21.31 KB)
2000 Meadows C.  2000.  Invariant Generation Techniques in Cryptographic Protocol Analysis. 13th Computer Security Foundations Workshop. Meadows2000c.pdf (100.12 KB)
2000 Meadows C.  2000.  Open Issues in Formal Methods for Cryptographic Protocol Analysis. DISCEX 2000. :237-250. Meadows2000d.pdf (168.94 KB)
2000 Moskowitz IS, Longdon GE, Chang LW.  2000.  A New Paradigm Hidden in Steganography. New Security Paradigms Workshop. 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. 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. 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. 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. Syverson etal2000c.pdf (154.68 KB)