Verification of the Woo-Lam Protocol Based on APTC

This paper presents a formal modeling and verification of the Woo-Lam authentication protocol using Algebra of True Concurrent Processes (APTC). APTC accurately describes concurrent behaviors and causal relationships within security protocols through true concurrency semantics and bisimulation equivalence. The paper constructs an APTC model of the protocol, defining state transitions and communication functions for participants Alice, Bob, and Trent. Using encapsulation (∂H) and abstraction (\({\tau }_I\)) operators, it focuses on external behavior analysis. The protocol is proven secure under root branch bisimulation, effectively resisting information leakage, replay attacks, and man-in-the-middle attacks while demonstrating expected behavior in non-attack scenarios.