add bruteforce tactic and fill in some admits in HMAC concat