Formal modeling and verification is a powerful and widely adopted tool in the field of cybersecurity. It consists of devising and analyzing abstract models of real-life systems or situations to be evaluated. Creating accurate formal models that faithfully represent reality is crucial for performing meaningful analysis. Due to the diversity of aspects – technical, physical, human, and environmental – that may impact ceremony execution, formal modeling of ceremonies is a challenging task. The objective of our work is to scrutinize an existing formal framework for ceremony modeling and assess its ability to capture unexpected situations caused by faults, errors, negligence, or misbehavior. We analyze the framework’s building components and formulate pragmatic guidelines to assist modelers in designing meaningful, rich ceremony models. We validate our findings on a two-factor authentication case study.