In this paper we focus on the analysis and design stages of the protocol engineering development cycle. We start by sketching an application framework dedicated to a web-based learning environment called Baghera whose aim is to teach geometry problems. We then apply our protocol engineering process to protocols for checking mathematical proofs a student happens to build. The following section discusses the analysis stage of such a protocol. We then briefly introduce our component-based formal specification language in order to then describe the protocol?s design stage. Finally we present a tool built upon the FIPA norm (making use of the PDN or UAML notation) which supports the analysis and design of interaction protocols.