Protocol with Counters. We present here a simple protocol that uses state in order to avoid replay attacks. This is a simplified version of a security protocol in automotive, where signals are sent between control units in a car: A → B : sign(Signal || Counter, KAB) When A sends a signal to B, it increases a counter and signs the signal with the current value, using the shared key KAB. Upon receiving the message, B compares the counter with its own local copy; if the received counter is greater than B’s local counter, then the message is accepted, otherwise it is ignored. Here follows the code for the main protocol, with omitted type signatures: let k = keygen sig prop let sender s = let c = next cnt () in assume (Signal s c); let t = Format.signal s c in let m = mac k t in send (append t m); None let receiver () = let msg = recv () in ( if length msg <> signal size + macsize then Some "Wrong.length" else | → let (t, m) = split msg signal size in match Format.signal split t with Some (s, c) if not (fresh cnt c) then Some "Counter.already.used" else if not (verify k t m) then Some "MAC.failed" else (∗ Signal accepted ∗) ( assert (Signal s c); xxx xxxxx s c !log p; log recv s c; update cnt c; None ) | None → Some "Bad.tag" ) Both principals sender and receiver share a session key k, which is generated once and for all in the protocol with an attached property sig prop, which specifies the security property, as we will see later. The sender encodes the signal into a tagged bytestring using the function Format.signal, produces its signature, and finally sends the assembled message. The receiver disassembles it, checking all the conditions that violate the property. Such conditions are signaled by the use of the option return type. The function next cnt increments and returns a counter kept by the sender, the function fresh cnt returns true if the counter has not been observed by the receiver, and update cnt updates the counter for the receiver to the newer version. Communication between the two parties is done using the send and recv functions, while the cryptographic component is handled by the MAC module.
