Formal analysis of trusted computing: One case study

Hong Wei Zhou; Jin Hui Yuan

doi:10.1109/CMC.2011.108

Formal analysis of trusted computing: One case study

Hong Wei Zhou^*
, Jin Hui Yuan

^*Corresponding author for this work

Ministry of Education of the People's Republic of China
School of Information
University of China

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

1 Scopus citations

Abstract

LS2 is the logic to reason about the property of trusted computing. However, it lacks the capability of modeling the isolation provided by virtualization which is often involved in previous trusted computing system. With the support of changed LS2, we model three types of isolation. Moreover, we formally analyze the integrity measurement property of Trust Visor proposed recently which provides the isolated execution environment for security-sensitive code.

Original language	English
Title of host publication	Proceedings - 2011 3rd International Conference on Communications and Mobile Computing, CMC 2011
Pages	55-58
Number of pages	4
DOIs	https://doi.org/10.1109/CMC.2011.108
State	Published - 2011
Externally published	Yes
Event	2011 3rd International Conference on Communications and Mobile Computing, CMC 2011 - Qingdao, China Duration: 18 Apr 2011 → 20 Apr 2011

Publication series

Name	Proceedings - 2011 3rd International Conference on Communications and Mobile Computing, CMC 2011

Conference

Conference	2011 3rd International Conference on Communications and Mobile Computing, CMC 2011
Country/Territory	China
City	Qingdao
Period	18/04/11 → 20/04/11

Keywords

TPM
isolation
trusted computing
virtualization

Access to Document

10.1109/CMC.2011.108

Cite this

@inproceedings{520e5f87e76d4decbddec0761099a70e,

title = "Formal analysis of trusted computing: One case study",

abstract = "LS2 is the logic to reason about the property of trusted computing. However, it lacks the capability of modeling the isolation provided by virtualization which is often involved in previous trusted computing system. With the support of changed LS2, we model three types of isolation. Moreover, we formally analyze the integrity measurement property of Trust Visor proposed recently which provides the isolated execution environment for security-sensitive code.",

keywords = "TPM, isolation, trusted computing, virtualization",

author = "Zhou, \{Hong Wei\} and Yuan, \{Jin Hui\}",

year = "2011",

doi = "10.1109/CMC.2011.108",

language = "英语",

isbn = "9780769543574",

series = "Proceedings - 2011 3rd International Conference on Communications and Mobile Computing, CMC 2011",

pages = "55--58",

booktitle = "Proceedings - 2011 3rd International Conference on Communications and Mobile Computing, CMC 2011",

note = "2011 3rd International Conference on Communications and Mobile Computing, CMC 2011 ; Conference date: 18-04-2011 Through 20-04-2011",

}

Zhou, HW & Yuan, JH 2011, Formal analysis of trusted computing: One case study. in Proceedings - 2011 3rd International Conference on Communications and Mobile Computing, CMC 2011., 5931124, Proceedings - 2011 3rd International Conference on Communications and Mobile Computing, CMC 2011, pp. 55-58, 2011 3rd International Conference on Communications and Mobile Computing, CMC 2011, Qingdao, China, 18/04/11. https://doi.org/10.1109/CMC.2011.108

Formal analysis of trusted computing: One case study. / Zhou, Hong Wei; Yuan, Jin Hui.
Proceedings - 2011 3rd International Conference on Communications and Mobile Computing, CMC 2011. 2011. p. 55-58 5931124 (Proceedings - 2011 3rd International Conference on Communications and Mobile Computing, CMC 2011).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

TY - GEN

T1 - Formal analysis of trusted computing

T2 - 2011 3rd International Conference on Communications and Mobile Computing, CMC 2011

AU - Zhou, Hong Wei

AU - Yuan, Jin Hui

PY - 2011

Y1 - 2011

N2 - LS2 is the logic to reason about the property of trusted computing. However, it lacks the capability of modeling the isolation provided by virtualization which is often involved in previous trusted computing system. With the support of changed LS2, we model three types of isolation. Moreover, we formally analyze the integrity measurement property of Trust Visor proposed recently which provides the isolated execution environment for security-sensitive code.

AB - LS2 is the logic to reason about the property of trusted computing. However, it lacks the capability of modeling the isolation provided by virtualization which is often involved in previous trusted computing system. With the support of changed LS2, we model three types of isolation. Moreover, we formally analyze the integrity measurement property of Trust Visor proposed recently which provides the isolated execution environment for security-sensitive code.

KW - TPM

KW - isolation

KW - trusted computing

KW - virtualization

UR - https://www.scopus.com/pages/publications/79960778260

U2 - 10.1109/CMC.2011.108

DO - 10.1109/CMC.2011.108

M3 - 会议稿件

AN - SCOPUS:79960778260

SN - 9780769543574

T3 - Proceedings - 2011 3rd International Conference on Communications and Mobile Computing, CMC 2011

SP - 55

EP - 58

BT - Proceedings - 2011 3rd International Conference on Communications and Mobile Computing, CMC 2011

Y2 - 18 April 2011 through 20 April 2011

ER -

Formal analysis of trusted computing: One case study

Abstract

Publication series

Conference

Keywords

Access to Document

Other files and links

Fingerprint

Cite this