Data is received that characterizes a computing architecture including at least one web-based server and an associated cryptographic web protocol to be implemented on such computing architecture according to a desired formal specification. Thereafter, a plurality of inattentive variants complying with the web protocol are generated without associated security checks. Messages to and from each inattentive variant are then monitored while executing the associated security checks. At least one security monitor is generated based on the monitored messages that is configured to address security vulnerabilities in the computing architecture relative to the formal specification. At least one generated security monitor can be later deployed in the computing architecture. Related apparatus, systems, techniques and articles are also described.