Analysis of a Receipt-Free Auction Protocol in the Applied Pi Calculus