Typing correspondence assertions for communication protocols

DOI10.1016/S0304-3975(02)00333-XMaRDI QIDQ1399972zbMATH OpenOpenAlexFDO

Authors Andrew D. Gordon, Alan Jeffrey

Publication date 30 July 2003

Published in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/s0304-3975(02)00333-x

zbMATH Keywords

security protocols

Mathematics Subject Classification ID

Data encryption (aspects in computer science) (68P25) Network protocols (68M12)

Recommendations

• Typing Correspondence Assertions for Communication Protocols
• Type-Based Verification of Correspondence Assertions for Communication Protocols
• Unmediated communication with partially verifiable types
• scientific article; zbMATH DE number 3878340
• MULTISTAGE COMMUNICATION WITH AND WITHOUT VERIFIABLE TYPES
• Communication equilibria with partially verifiable types
• Correspondence assertions for process synchronization in concurrent communications
• scientific article; zbMATH DE number 1962753
• Algebraic specification and verification of communication protocols

Cites work

• scientific article; zbMATH DE number 954809 (Why is no real title available?)
• scientific article; zbMATH DE number 3695144 (Why is no real title available?)
• scientific article; zbMATH DE number 50149 (Why is no real title available?)
• scientific article; zbMATH DE number 1231689 (Why is no real title available?)
• scientific article; zbMATH DE number 1296290 (Why is no real title available?)
• scientific article; zbMATH DE number 1538026 (Why is no real title available?)
• A calculus for cryptographic protocols: The spi calculus
• A generic type system for the \(\pi\)-calculus
• Region analysis and a π-calculus with groups
• Region-based memory management
• The chemical abstract machine
• Types as models: model checking message-passing programs

Cited in

(14)

• Formal Analysis of Dynamic, Distributed File-System Access Controls
• Verification of correspondence assertions in a calculus for mobile ad hoc networks
• Specifying properties of concurrent computations in CLF
• Typing copyless message passing
• Objects and session types
• Proof-relevant \(\pi\)-calculus: a constructive account of concurrency and causality
• Type checking a multithreaded functional language with session types
• A generic type system for the pi-calculus
• Type-Based Verification of Correspondence Assertions for Communication Protocols
• Combining behavioural types with security analysis
• Typing Correspondence Assertions for Communication Protocols
• scientific article; zbMATH DE number 1962753 (Why is no real title available?)
• A chart semantics for the pi-calculus
• Subtyping for session types in the pi calculus

Describes a project that uses

Uses Software

• PIPER
• Automath

This page was built for publication: Typing correspondence assertions for communication protocols

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1399972)