Typing correspondence assertions for communication protocols

DOI10.1016/S0304-3975(02)00333-XzbMath1023.68006OpenAlexW1995469872MaRDI QIDQ1399972

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)

Related Items (10)

A generic type system for the pi-calculus ⋮ Type checking a multithreaded functional language with session types ⋮ Combining behavioural types with security analysis ⋮ Verification of Correspondence Assertions in a Calculus for Mobile Ad Hoc Networks ⋮ Proof-relevant π-calculus: a constructive account of concurrency and causality ⋮ Formal Analysis of Dynamic, Distributed File-System Access Controls ⋮ Objects and session types ⋮ Subtyping for session types in the pi calculus ⋮ A Chart Semantics for the Pi-Calculus ⋮ Specifying Properties of Concurrent Computations in CLF

Uses Software

• Automath
• PIPER

Cites Work

• Region-based memory management
• The chemical abstract machine
• A calculus for cryptographic protocols: The spi calculus
• Region analysis and a π-calculus with groups
• A generic type system for the Pi-calculus
• Types as models
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

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