Modular verification of security protocol code by typing

No abstract is available for this paper.

• Publication year

  2010

• Venue

  ACM-SIGACT Symposium on Principles of Programming Languages

• Publication date

  2010-01-17

• Fields of study

  Computer Science

• Identifiers
  DOI 10.1145/1706299.1706350
• External record

  Open on Semantic Scholar

• Source metadata

  Semantic Scholar

• No claims are published for this paper.

• No concepts are published for this paper.

• Union and Intersection Types for Secure Protocol Implementations

  2011cited by this paper
• Sound automatic implementation generation and monitoring of security protocol implementations from verified formal specifications

  2010cited by this paper
• Enforcing Stateful Authorization and Information Flow Policies in Fine

  2010cited by this paper
• Pre- and Post-conditions for Security Typechecking

  2010cited by this paper
• Dependent types from counterexamples

  2010cited by this paper
• Principles and Applications of Refinement Types

  2010cited by this paper
• Dependent type inference with interpolants

  2009cited by this paper
• Cryptographic Protocol Synthesis and Verification for Multiparty Sessions

  2009cited by this paper
• Type-checking Implementations of Protocols Based on Zero-knowledge Proofs – Work in Progress –

  2009cited by this paper
• Towards a Verified Reference Implementation of a Trusted Platform Module

  2009cited by this paper
• ASPIER: An Automated Framework for Verifying Security Protocol Implementations

  2009influential reference
• Refinement Types for Secure Implementations

  2008influential reference
• Z3: An Efficient SMT Solver

  2008cited by this paper
• Liquid types

  2008cited by this paper
• Verified implementations of the information card federated identity-management protocol

  2008cited by this paper
• Cryptographically verified implementations for TLS

  2008influential reference
• AURA: a programming language for authorization and audit

  2008cited by this paper
• UTP semantics for web services

  2007cited by this paper
• Cryptol: specification, implementation and verification of high-grade cryptographic applications

  2007cited by this paper
• Dependent ML An approach to practical programming with dependent types

  2007cited by this paper
• Type-Based Verification of Correspondence Assertions for Communication Protocols

  2007cited by this paper
• Type Reconstruction for General Refinement Types

  2007cited by this paper
• Verifying an implementation of SSH

  2007cited by this paper
• Breaking and fixing public-key Kerberos

  2006cited by this paper
• A computationally sound mechanized prover for security protocols

  2006cited by this paper
• A verifying core for a cryptographic language compiler

  2006cited by this paper
• Hybrid type checking

  2006cited by this paper
• Verified Reference Implementations of WS-Security Protocols

  2006influential reference
• Verified interoperable implementations of security protocols

  2006influential reference
• Rule-based static analysis of network protocol implementations

  2006cited by this paper
• On the Relationship Between Web Services Security and Traditional Protocols

  2006cited by this paper
• Cryptographic Protocol Analysis on Real C Code

  2005cited by this paper
• A bisimulation for dynamic sealing

  2004cited by this paper
• Spi2Java: automatic cryptographic protocol Java code generation from spi calculus

  2004cited by this paper
• A semantics for web services authentication

  2004cited by this paper
• Automated Attack Analysis and Code Generation in a Multi-Dimensional Security Protocol Engineering Framework

  2003cited by this paper
• Authentication by correspondence

  2003cited by this paper
• Types and effects for asymmetric cryptographic protocols

  2002cited by this paper
• AGVI - Automatic Generation, Verification, and Implementation of Security Protocols

  2001cited by this paper
• An efficient cryptographic protocol verifier based on prolog rules

  2001influential reference
• Cryptographic protocol generation from capsl

  2001cited by this paper
• Authenticated Encryption: Relations among Notions and Analysis of the Generic Composition Paradigm

  2000cited by this paper
• TAPS: a first-order verifier for cryptographic protocols

  2000cited by this paper
• Secrecy by typing in security protocols

  1999cited by this paper
• Logic and Proof

  1999cited by this paper
• The inductive approach to verifying cryptographic protocols

  1998cited by this paper
• Breaking and Fixing the Needham-Schroeder Public-Key Protocol Using FDR

  1996cited by this paper
• Semantics of programming languages: structures and techniques

  1993cited by this paper
• Reasoning about programs in continuation-passing style

  1992cited by this paper
• Semantics of programming languages

  1991cited by this paper
• Semantics of programming languages

  1991cited by this paper
• Introduction to lattices and order

  1990cited by this paper
• Efficient and timely mutual authentication

  1987cited by this paper
• On the security of public key protocols

  1981cited by this paper
• Using encryption for authentication in large networks of computers

  1978cited by this paper
• Protection in programming languages

  1973cited by this paper
• Logic and Proof

  1970cited by this paper
• 2008 IEEE Symposium on Security and Privacy FABLE: A Language for Enforcing User-defined Security Policies

  year unknowncited by this paper

• SoK: Robust properties, robust abstractions and back-translations

  2026cites this paper
• Automated Side-Channel Analysis of Cryptographic Protocol Implementations

  2025cites this paper
• SpecMon: Modular Black-Box Runtime Monitoring of Security Protocols

  2024cites this paper
• CryptoBap: A Binary Analysis Platform for Cryptographic Protocols

  2023cites this paper
• Dartmouth Digital Commons Dartmouth Digital Commons

  2023cites this paper
• Layered Symbolic Security Analysis in DY$^\star$

  2023cites this paper
• Confirmed Malaria Cases in Children under Five Years: The Influence of Suspected Cases, Tested Cases, and Climatic Conditions

  2023cites this paper
• A Generic Methodology for the Modular Verification of Security Protocol Implementations

  2022cites this paper
• Noise*: A Library of Verified High-Performance Secure Channel Protocol Implementations

  2022cites this paper
• Sound Verification of Security Protocols: From Design to Interoperable Implementations

  2022cites this paper
• Cache Refinement Type for Side-Channel Detection of Cryptographic Software

  2022cites this paper
• $\text{DY}^{\star}$: A Modular Symbolic Verification Framework for Executable Cryptographic Protocol Code

  2021influential citation
• Learning Assumptions for Verifying Cryptographic Protocols Compositionally

  2021cites this paper
• An In-Depth Symbolic Security Analysis of the ACME Standard

  2021cites this paper
• A Tutorial-Style Introduction to DY*

  2021cites this paper
• System-Level Non-interference of Constant-Time Cryptography. Part II: Verified Static Analysis and Stealth Memory

  2020cites this paper
• Automated Symbolic Verification of Telegram's MTProto 2.0

  2020cites this paper
• A Dynamic Data Slice Approach to the Vulnerability Analysis of E-Commerce Systems

  2020cites this paper
• Statically verified refinements for multiparty protocols

  2020cites this paper
• On Higher-Order Cryptography

  2020cites this paper
• Analyzing Security Protocol Web Implementations Based on Model Extraction With Applied PI Calculus

  2020influential citation
• On Higher-Order Cryptography (Long Version)

  2020cites this paper
• Formal Models and Verified Protocols for Group Messaging: Attacks and Proofs for IETF MLS

  2019cites this paper
• Blocks' Network: Redesign Architecture Based on Blockchain Technology

  2019cites this paper
• Uncovering Information Flow Policy Violations in C Programs

  2019cites this paper
• Secure, fast and verified cryptographic applications: a scalable approach. (Implémentations cryptographiques sures, performantes et verifiées: une approche passant a l'échelle)

  2018cites this paper
• Symbolic Execution of Security Protocol Implementations: Handling Cryptographic Primitives

  2018cites this paper
• Implementation-level analysis of cryptographic protocols and their applications to e-voting systems

  2018cites this paper
• Analyzing E-Commerce Business Process Nets via Incidence Matrix and Reduction

  2018cites this paper
• A Dictionary Sequence Model to Analyze the Security of Protocol Implementations at the Source Code Level

  2017cites this paper
• Recalling a witness: foundations and applications of monotonic state

  2017cites this paper
• A New Method to Analyze the Security of Protocol Implementations Based on Ideal Trace

  2017cites this paper
• Verified Models and Reference Implementations for the TLS 1.3 Standard Candidate

  2017cites this paper
• Recalling a Witness

  2017cites this paper
• Paragon – Practical programming with information flow control

  2017cites this paper
• Modeling and Verification of Online Shopping Business Processes by Considering Malicious Behavior Patterns

  2016cites this paper
• Dependent types and multi-monadic effects in F*

  2016influential citation
• Verifying cryptographic protocols. Applying the symbolic model to cryptographic APIs for C

  2016influential citation
• Modeling and Verifying Security Protocols with the Applied Pi Calculus and ProVerif

  2016cites this paper
• miTLS: Verifying Protocol Implementations against Real-World Attacks

  2016cites this paper
• A Reduction Method of Analyzing Data-Liveness and Data-Boundedness for a Class of E-commerce Business Process Nets

  2016cites this paper
• Design and implementation of secure protocols for practical authentication and fair anonymity systems

  2015cites this paper
• Automated type-based analysis of injective agreement in the presence of compromised principals

  2015influential citation
• A Logic of Programs with Interface-Confined Code

  2015cites this paper
• Verifying Protocol Implementations by Augmenting Existing Cryptographic Libraries with Specifications

  2015cites this paper
• Semantic Purity and Effects Reunited in F (cid:63)

  2015cites this paper
• Affine Refinement Types for Secure Distributed Programming

  2015influential citation
• Vérification automatique de protocoles d'examen, de monnaie, de réputation, et de routage. (Automated Verification of Exam, Cash, aa Reputation, and Routing Protocols)

  2015cites this paper
• Verifying cryptographic security implementations in C using automated model extraction

  2015cites this paper
• Probabilistic relational verification for cryptographic implementations

  2014cites this paper
• Local temporal reasoning

  2014influential citation
• Verified Implementations for Secure and Verifiable Computation

  2014cites this paper
• Mechanized Network Origin and Path Authenticity Proofs

  2014cites this paper
• Typing secure implementation of authentication protocols in environments with compromised principals

  2014cites this paper
• Extending and Applying a Framework for the Cryptographic Verification of Java Programs

  2014cites this paper
• System M: A Program Logic for Code Sandboxing and Identification

  2014cites this paper
• Union, intersection and refinement types and reasoning about type disjointness for secure protocol implementations

  2014influential citation
• System-level Non-interference for Constant-time Cryptography

  2014cites this paper
• Cryptographically Verified Design and Implementation of a Distributed Key Manager

  2014cites this paper
• Modeling and Validating E-Commerce Business Process Based on Petri Nets

  2014cites this paper
• Efficient construction of machine-checked symbolic protocol security proofs

  2013cites this paper
• Static verification and enforcement of authorization policies

  2013influential citation
• Differential Privacy by Typing in Security Protocols

  2013cites this paper
• Logical Foundations of Secure Resource Management in Protocol Implementations

  2013influential citation
• ZQL: A Compiler for Privacy-Preserving Data Processing

  2013cites this paper
• Implementing TLS with

  2013cites this paper
• Security Applications of Formal Language Theory

  2013cites this paper
• A Hybrid Approach for Proving Noninterference and Applications to the Cryptographic Verification of

  2013cites this paper
• Proving cryptographic C programs secure with general-purpose verification tools

  2013cites this paper
• Formal Verification of Voting and Auction Protocols : From Privacy to Fairness and Verifiability

  2013cites this paper
• Advancing automated security protocol verification

  2013cites this paper
• Implementing TLS with Verified Cryptographic Security

  2013cites this paper
• Verifying Implementations of Security Protocols by Refinement

  2012cites this paper
• From Computationally-proved Protocol Specifications to Implementations

  2012cites this paper
• Security Protocol Verification: Symbolic and Computational Models

  2012cites this paper
• Vérification semi-automatique de primitives cryptographiques

  2012cites this paper
• A Framework for the Cryptographic Verification of Java-Like Programs

  2012cites this paper
• A Multiparty Multi-session Logic

  2012cites this paper
• Linearly Refined Session Types

  2012cites this paper
• Computational verification of C protocol implementations by symbolic execution

  2012cites this paper
• A formal methodology for integral security design and verification of network protocols

  2012cites this paper
• A unified formal model for service oriented architecture to enforce security contracts

  2012cites this paper
• Self-certification: bootstrapping certified typecheckers in F* with Coq

  2012cites this paper
• Union, intersection, and refinement types and reasoning about type disjointness for security protocol analysis

  2012cites this paper
• Paragon for Practical Flow-Oriented Programming

  2012cites this paper
• Affine Refinement Types for Authentication and Authorization

  2012cites this paper
• Historical Background and Further Reading

  2012cites this paper
• Formally based semi-automatic implementation of an open security protocol

  2012cites this paper
• Cryptographic Verification by Typing for a Sample Protocol Implementation

  2011cites this paper
• Modular code-based cryptographic verification

  2011cites this paper
• Secure distributed programming with value-dependent types

  2011cites this paper
• Type-Based Automated Verification of Authenticity in Asymmetric Cryptographic Protocols

  2011cites this paper
• Automated Synthesis of Privacy-Preserving Distributed Applications

  2011cites this paper
• Automated Formal Methods for Security Protocol Engineering

  2011cites this paper
• Rigorous specifications of the SSH Transport Layer

  2011cites this paper
• Practical, Flexible programming with Information Flow Control

  2011cites this paper
• Formal Analysis of the EMV Protocol Suite

  2011cites this paper
• Verifying Cryptographic Code in C: Some Experience and the Csec Challenge

  2011cites this paper
• Union and Intersection Types for Secure Protocol Implementations

  2011influential citation
• How to Shop for Free Online -- Security Analysis of Cashier-as-a-Service Based Web Stores

  2011cites this paper