Formally based semi-automatic implementation of an open security protocol