{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,8]],"date-time":"2025-07-08T01:18:47Z","timestamp":1751937527782,"version":"3.37.3"},"reference-count":19,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2019,12,9]],"date-time":"2019-12-09T00:00:00Z","timestamp":1575849600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2019,12,9]],"date-time":"2019-12-09T00:00:00Z","timestamp":1575849600000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Mobile Netw Appl"],"published-print":{"date-parts":[[2020,6]]},"DOI":"10.1007\/s11036-019-01433-1","type":"journal-article","created":{"date-parts":[[2019,12,9]],"date-time":"2019-12-09T17:03:06Z","timestamp":1575910986000},"page":"1125-1139","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":5,"title":["Formalization and Analysis of Haystack Architecture from Process Algebra Perspective"],"prefix":"10.1007","volume":"25","author":[{"given":"Jiaqi","family":"Yin","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Huibiao","family":"Zhu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0797-0152","authenticated-orcid":false,"given":"Phan Cong","family":"Vinh","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2019,12,9]]},"reference":[{"key":"1433_CR1","doi-asserted-by":"crossref","unstructured":"Albesher A, Alhussain T (2013) Privacy and security issues in social networks: an evaluation of facebook. In: ISDOC 2013 international conference on information systems and design of communication, ISDOC\u201913, Lisboa, Portugal, July 11-12, 2013, pp 7\u201310","DOI":"10.1145\/2503859.2503861"},{"key":"1433_CR2","doi-asserted-by":"crossref","unstructured":"Batista GC, Miers CC, Koslovski GP, Pillon MA, Gonzalez NM, Jr MAS (2018) Using externals idps on openstack: a security analysis of openid connect, facebook connect, and openstack authentication. In: 32nd IEEE international conference on advanced information networking and applications, AINA 2018, Krakow, Poland, May 16-18, 2018, pp 920\u2013927","DOI":"10.1109\/AINA.2018.00135"},{"key":"1433_CR3","unstructured":"Beaver D, Kumar S, Li HC, Sobel J, Vajgel P (2010) Finding a needle in Haystack: facebook\u2019s photo storage. In: 9th USENIX symposium on operating systems design and implementation, OSDI 2010, October 4-6, 2010, Vancouver, BC, Canada, Proceedings, pp 47\u201360"},{"issue":"3","key":"1433_CR4","doi-asserted-by":"publisher","first-page":"560","DOI":"10.1145\/828.833","volume":"31","author":"SD Brookes","year":"1984","unstructured":"Brookes SD, Hoare CAR, Roscoe AW (1984) A theory of communicating sequential processes. J ACM 31(3):560\u2013599","journal-title":"J ACM"},{"key":"1433_CR5","doi-asserted-by":"crossref","unstructured":"Fei Y, Zhu H, Wu X, Fang H, Qin S (2018) Comparative modelling and verification of Pthreads and Dthreads. J Softw Evolution Process 30(3)","DOI":"10.1002\/smr.1919"},{"key":"1433_CR6","doi-asserted-by":"crossref","unstructured":"Gummadi PK, Dunn RJ, Saroiu S, Gribble SD, Levy HM, Zahorjan J (2003) Measurement, modeling, and analysis of a peer-to-peer file-sharing workload. In: Proceedings of the 19th ACM symposium on operating systems principles 2003, SOSP 2003, Bolton Landing, NY, USA, October 19-22, 2003, pp 314\u2013329","DOI":"10.1145\/945445.945475"},{"key":"1433_CR7","volume-title":"Communicating sequential processes","author":"CAR Hoare","year":"1985","unstructured":"Hoare CAR (1985) Communicating sequential processes. Prentice-Hall, Englewood Cliffs"},{"key":"1433_CR8","doi-asserted-by":"crossref","unstructured":"Huang Q, Birman K, van Renesse R, Lloyd W, Kumar S, Li HC (2013) An analysis of facebook photo caching. In: ACM SIGOPS 24th symposium on operating systems principles, SOSP\u201913, Farmington, PA, USA, November 3-6, 2013, pp 167\u2013181","DOI":"10.1145\/2517349.2522722"},{"key":"1433_CR9","doi-asserted-by":"crossref","unstructured":"Jung J, Krishnamurthy B, Rabinovich M (2002) Flash crowds and denial of service attacks: characterization and implications for cdns and web sites. In: Proceedings of the eleventh international world wide web conference, WWW 2002, May 7-11, 2002, Honolulu, Hawaii, USA, pp 293\u2013304","DOI":"10.1145\/511446.511485"},{"key":"1433_CR10","doi-asserted-by":"crossref","unstructured":"Liu A, Popovic M, Zhu H (2017) Formalization and verification of the PSTM architecture. In: 24th Asia-Pacific software engineering conference, APSEC 2017, Nanjing, China, December 4-8, 2017, pp 427\u2013435","DOI":"10.1109\/APSEC.2017.49"},{"issue":"10","key":"1433_CR11","doi-asserted-by":"publisher","first-page":"659","DOI":"10.1109\/32.637148","volume":"23","author":"G Lowe","year":"1997","unstructured":"Lowe G, Roscoe AW (1997) Using CSP to detect errors in the TMN protocol. IEEE Trans Software Eng 23(10):659\u2013669","journal-title":"IEEE Trans Software Eng"},{"key":"1433_CR12","volume-title":"The theory and practice of concurrency","author":"AW Roscoe","year":"1997","unstructured":"Roscoe AW (1997) The theory and practice of concurrency. Prentice Hall, Englewood Cliffs"},{"key":"1433_CR13","doi-asserted-by":"crossref","unstructured":"Roscoe AW (2010) Understanding concurrent systems. Texts in Computer Science, Springer","DOI":"10.1007\/978-1-84882-258-0"},{"key":"1433_CR14","doi-asserted-by":"crossref","unstructured":"Saroiu S, Gummadi PK, Dunn RJ, Gribble SD, Levy HM (2002) An analysis of internet content delivery systems. In: 5th symposium on operating system design and implementation (OSDI 2002), Boston, Massachusetts, USA, December 9-11, 2002","DOI":"10.1145\/1060289.1060319"},{"key":"1433_CR15","doi-asserted-by":"crossref","unstructured":"Sciarretta G, Armando A, Carbone R, Ranise S (2016) Security of mobile single sign-on: a rational reconstruction of facebook login solution. In: Proceedings of the 13th international joint conference on e-business and telecommunications (ICETE 2016) - vol 4, SECRYPT, Lisbon, Portugal, July 26-28, 2016, pp 147\u2013158","DOI":"10.5220\/0005969001470158"},{"key":"1433_CR16","doi-asserted-by":"crossref","unstructured":"Sharma R, Jain A, Rastogi R (2013) A new face to photo security of facebook. In: Sixth international conference on contemporary computing, IC3 2013, Noida, India, August 8-10, 2013, pp 415\u2013420","DOI":"10.1109\/IC3.2013.6612231"},{"key":"1433_CR17","doi-asserted-by":"publisher","first-page":"153","DOI":"10.1016\/j.future.2015.09.007","volume":"56","author":"X Wu","year":"2016","unstructured":"Wu X, Zhu H (2016) Formalization and analysis of the REST architecture from the process algebra perspective. Future Generation Comp Syst 56:153\u2013168","journal-title":"Future Generation Comp Syst"},{"issue":"2","key":"1433_CR18","first-page":"318","volume":"22","author":"W Xie","year":"2017","unstructured":"Xie W, Zhu H, Wu X, Xiang S, Guo J, Vinh PC (2017) Modeling and verifying HDFS using process algebra. MONET 22(2):318\u2013331","journal-title":"MONET"},{"key":"1433_CR19","doi-asserted-by":"crossref","unstructured":"Xu C, Zhu H, Xie W (2017) Modeling and verifying identity authentication security of HDFS using CSP. In: 24th Asia-Pacific software engineering conference, APSEC 2017, Nanjing, China, December 4-8, 2017, pp 259\u2013268","DOI":"10.1109\/APSEC.2017.32"}],"container-title":["Mobile Networks and Applications"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11036-019-01433-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s11036-019-01433-1\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11036-019-01433-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,12,8]],"date-time":"2020-12-08T00:50:47Z","timestamp":1607388647000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s11036-019-01433-1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,12,9]]},"references-count":19,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2020,6]]}},"alternative-id":["1433"],"URL":"https:\/\/doi.org\/10.1007\/s11036-019-01433-1","relation":{},"ISSN":["1383-469X","1572-8153"],"issn-type":[{"type":"print","value":"1383-469X"},{"type":"electronic","value":"1572-8153"}],"subject":[],"published":{"date-parts":[[2019,12,9]]},"assertion":[{"value":"9 December 2019","order":1,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}