This is very interesting. Has anyone seen any models of HTTP in pi-calculus? A quick search didn't turn anything up, but then http is a tainted keyword.