Technical reports

Message reception in the inductive approach

Giampaolo Bella

March 1999, 16 pages

DOI: 10.48456/tr-460

Abstract

Cryptographic protocols can be formally analysed in great detail by means of Paulson’s Inductive Approach, which is mechanised by the theorem prover Isabelle. The approach only relied on message sending (and noting) in order to keep the models simple. We introduce a new event, message reception, and show that the price paid in terms of runtime is negligible because old proofs can be reused. On the other hand, the new event enhances the global expressiveness, and makes it possible to define an accurate notion of agents’ knowledge, which extends and replaces Paulson’s notion of spy’s knowledge. We have designed new guarantees to assure each agent that the peer does not know the crucial message items of the session. This work thus extends the scope of the Inductive approach. Finally, we provide general guidance on updating the protocols analysed so far, and give examples for some cases.

Full text

PDF (0.9 MB)

BibTeX record

@TechReport{UCAM-CL-TR-460,
  author =	 {Bella, Giampaolo},
  title = 	 {{Message reception in the inductive approach}},
  year = 	 1999,
  month = 	 mar,
  url = 	 {https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-460.pdf},
  institution =  {University of Cambridge, Computer Laboratory},
  doi = 	 {10.48456/tr-460},
  number = 	 {UCAM-CL-TR-460}
}