equal
deleted
inserted
replaced
1 (****************************************************************************** |
1 (* Title: HOL/Auth/Guard/P2.thy |
2 from G. Karjoth, N. Asokan and C. Gulcu |
2 Author: Frederic Blanqui, University of Cambridge Computer Laboratory |
|
3 Copyright 2002 University of Cambridge |
|
4 |
|
5 From G. Karjoth, N. Asokan and C. Gulcu |
3 "Protecting the computation results of free-roaming agents" |
6 "Protecting the computation results of free-roaming agents" |
4 Mobiles Agents 1998, LNCS 1477 |
7 Mobiles Agents 1998, LNCS 1477. |
5 |
8 *) |
6 date: march 2002 |
|
7 author: Frederic Blanqui |
|
8 email: blanqui@lri.fr |
|
9 webpage: http://www.lri.fr/~blanqui/ |
|
10 |
|
11 University of Cambridge, Computer Laboratory |
|
12 William Gates Building, JJ Thomson Avenue |
|
13 Cambridge CB3 0FD, United Kingdom |
|
14 ******************************************************************************) |
|
15 |
9 |
16 header{*Protocol P2*} |
10 header{*Protocol P2*} |
17 |
11 |
18 theory P2 imports Guard_Public List_Msg begin |
12 theory P2 imports Guard_Public List_Msg begin |
19 |
13 |