查看文章

ENGLISH SUMMARY: Security is hard to maintain in distributed systems especially for communicating agents restricted to lightweight computations, as in the Internet of Things, which struggle to implement strong cryptographic security. A methodology is developed for specifying and reasoning algebraically about security in such systems which combines epistemic logic and a state-based formalism. The knowledge modality K is used to define a uthentication a nd s ecrecy int erms ofw hat e ach agent knows. Operations are defined ass tate t ransitions. Having g ained c onfidence in our methodology by applying it to the benchmark case studies Needham-Schroeder and Diffie-Hellman protocols, we then apply it to the contemporary examples Signal and Long-Range Wide-Area Network protocols. A mitigation is proposed and verified for a Long-Range Wide-Area Network.